Ref maintenance notes: PHP-based version of AEtnaNova/Referee on the server



Server side: etnanova_main.php

This PHP script checks that the user owns the right password and has identified himself by one of the 3-letter user names (e.g., "Gue" for "guest") known to AEtnaNova.

If so, it converts the user name into a corresponding file prefix (e.g. "g_", standing for "g_folder", in the case of a guest), identifying the file system folder into which the user-defined pieces of the scenario must be uploaded; subsequently, AEtnaNova outputs will be stored in this folder, too.

Then uploading of the various pieces of the scenario takes place. The scenario might include the common shared scenario already available on the server (this is the case when the user has chosen the "Share" option): it is hence perfectly legal that no file upload at all takes place; but generally 1 to 3 pieces of scenario are uploaded from user-specified files; moreover, an extra piece of scenario can be drawn directly from one of the fields of the user form and then saved.

Upload is the only activity to be done when the user has identified himself as a user who only wants to submit bug reports; but normally...

...A command line is constructed in order to then launch Ref's SETL-execution, which will process the scenario consisting of the various parts mentioned above. The ranges of theorems whose proofs must be checked (or just pretty-printed), drawn from the user's form, also contribute to this command line.

The output of Ref's execution is then translated into a nice-looking multi-sheet HTML table (where multi=3 or multi=6).


$users: This table, occurring inside the etnanova_main.php file, establishes the one-one correspondende between user names and file prefixes (the latter referring, as mentioned above, to the folders which contains all files uploaded or generated by the single users).

To set up a new user account, enter the user name into the table above, choosing a user code and corresponding file prefix.
This will launch a SETL program of the form k_invoke_verifier, in general (prefix)_invoke_verifier, which must have been precompiled into the library being used. These mini_programs all have the common form

		program k_invoke_verifier;			-- small program to invoke logic verifier
			use verifier_top_level;			-- use the logic verifier
			verifier_invoker("k_folder/");		-- master invocation routine
		end k_invoke_verifier;
and are found in Setl2/EtnaNova_main_stl, which must be recompiled to install a new user.


Server side: get_server_prefix.php

The final element needed by a user is checked by the get_server_prefix function in the file get_server_prefix.php
This checks for the password in the call to this file, which is found in the Logic_repository/EtnaNova_prelim_worksheet.html file that should be used for invocation of this file (see below).



User side: EtnaNova_prelim_worksheet.html

This html-file specifies the AetnaNova user's form (named "Preliminary Worksheet") comprising all fields needed for assembling a scenario and for choosing the ranges of theorems whose proofs must be checked or pretty-printed. The form contains the "Go" button needed to launch Ref's processing.