Ref maintenance notes: Installing AEtnaNova/Referee on a new machine
AEtnaNova folder set up
The content of the folder containing the main PHP file consists of the following items:
- AEtnaNova activation stub:
- EtnaNova_prelim_worksheet.html: user worksheet, a copy of which must be supplied to every AEtnaNova user
- AEtnaNova PHP files:
- etnanova_main.php: main PHP file
- get_server_prefix.php: password test
- AEtnanova logo:
- etna_logo.gif: portraits of the logicians Cantor, von Neumann, Gödel, and Peano (these will appear on the user worksheet page)
- logicians.jpg: additional portraits of logicians (these will appear on the AEtnaNova output page produced by etnanova_main.php
- Ref[eree] SETL sources (removable, in principle, once they have been compiled):
- EtnaNova_main.stl: verifier invokers (one program for each user) and Ref's front-end procedures
- EtnaNova_ELEM_collection.stl: Ref's back-end procedures, part 1
- EtnaNova_ELEM_supplement.stl: Ref's back-end procedures, part 2
- SETL code (generic library extended with Ref-specific procedures):
- setl2.lib: compiled SETL code (for virtual SETL machine)
- User folders:
- [a-z]_folder: subfolders (one for each user), containing
- uploaded proof-scenario fragments, which corresponding user has submitted for automatic verification
- verification output files
- e[1-9]folder: bug and doubt reports uploaded by the users
- Proof scenarios:
- common_scenario.txt: common scenario, which users can share during verification; acccessible through the Ref's user_manual (see below)
- orderedGroups_otMA.txt (and possibly others): files produced by external theorem provers (e.g. Otter), subsidiary to the common scenario
- User manual:
- Ref_user_manual.html: main page of the Ref's user manual, linked inside the AEtnaNova worksheet
- common_scenario.txt: common scenario, linked inside Ref_user_manual.html and shareable during verification
- user_manual_xref: folder consisting of html files, each one showing the list of all theorems which in common_scenario.txt refer to a specific symbol
- *.gif: screen shots appearing inside the Ref's user manual
- Additional documentation for the user:
- search_folder: currently this only contains a pretty-printed version of common_scenario, linked inside the AEtnaNova worksheet.
- intro.html, Logic_textbooks.html: draft book on computational logic and set theory (by D. Cantone, E.G. Omodeo, and J.T. Schwartz).
- Records for user maintenance:
- users.txt: this contains all information about the enabled users and the three-letter names by which they are known to AEtnaNova
- Tools for scenario maintenance:
- tools_folder: this contains the tools discussed within [Click]
- Maintenance notes for AEtnaNova/Referee:
- maintenance_folder: this contains the group of html files, including ths one, into which the [Ref's maintainer notes]
ramify
Important proviso: The information within the AEtnaNova activation stub must be manually set up so that it properly match
- the password appearing within get_server_prefix.php;
- the URL reaching the AEtnaNova server and, within that machine, the AEtnaNova folder described above.
We omit explaining here, taking them as obvious, the access rights to be associated with each file.
Compilation
The three SETL files constituting the Referee system, which are
- EtnaNova_ELEM_collection.stl,
- EtnaNova_ELEM_supplement.stl, and
- EtnaNova_main.stl,
must be compiled in this order. For reasons explained in [Click],
the name of the folder which, inside the file system, hosts the two pieces of the scenario needed for a standalone
run, may need being redefined manually within the code of the SETL procedure "verifier_invoker", inside the package "verifier_top_level",
before compilation.
Their compilation presupposes the presence of the following packages inside the compiled SETL library setl2.lib:
- string_utility_pak,
- get_lines_pak,
- parser,
- sort_pak
Besides these, the following files must also be available within the folder /usr/local/bin/, in order that SETL compilation on the one hand, and execution of the SETL virtual machine on the other, can be carried out:
Run-time support
The SETL library setl2.lib must be complemented with the following files within the folder /usr/local/lib/:
- libsetl2.so libsetl2.la libsetl2.a
- STRINGM.so STRINGM.la STRINGM.a
- PARSER.so PARSER.la PARSER.a
- STRING_UTILITY_PAK.so STRING_UTILITY_PAK.la STRING_UTILITY_PAK.a
- RX.so RX.la RX.a
- ZIP_PAK.so ZIP_PAK.la ZIP_PAK.a