Ref's files

## Ref maintenance notes: Scenarios, proof archives, tables and files generated as output, and generated auxiliary files

# Scenarios

These are text files internally containing definitions, theorems, and proofs which Ref will process to check their syntactic validity first, and then their logical correctness. Although they can widely vary in names and number (each user may have his own scenario repository), only a few of then will be examined by Ref in a single run: two (called "common_scenario.txt" and "supp_scenario.txt", see below ) in the case of a stand-alone run --- a number not exceeding five (one of them being, typically, either the shared or a personal variant of the "common_scenario.txt" file, see below) in the case of a server-based run.

- ## common_scenario.txt

  This is the main shared scenario. Its content, when it gets modified, should be kept synchronized with the contents of the "Ref_user_manual" (see [Click]).

  From time to time, when changes in its content have accumulated, the numerical identifiers of the theorems appearing in it must be renumbered by means of the program "renumber_scenario.stl"; (see [Click]), which will obtain from it the files

  - common_scenario.ren.txt
  - common_scenario.error

- ## supp_scenario.txt

  This is the only extension to the main shared scenario permitted when the stand-alone version of Ref is used.

- ## uid + "F1", uid + "F2", uid + "F3"

  Scenarios uploaded from files during server-based execution of Ref.

- ## uid + "F4"

  Scenario uploaded through the AEtnaNova preliminary worksheet.

# Auxiliary input files

- ## uid + "F0" (command_file)

  Opened, read and analyzed, and then closed, by the procedure verifier_invoker of the SETL package verifier_top_level; internally associated with the command_handle.
  Only used in server running modality: it serves as a surrogate for the activation command line, as an intermediate file between the PHP script and the SETL user-associated program.

# Proof archives

These do not exist yet.

# Tables and files generated as output

- ## Outfile_nnn

  These are (for a suffix > 1) opened/closed and generated by the procedures set_output_phase and printy of the SETL package prynter, and internally associated with the ohandle.

  - Outfile_2: its content will be a preamble to the HTML reporting tables.

- ## theorem_summary

  Generated by the SETL procedure ???, and internally associated with the dump_theorems_handle

- ## definition_summary

  Generated by the SETL procedure ???, and internally associated with the dump_defs_handle

- ## theory_summary

  Generated by the SETL procedure ???, and internally associated with the dump_theories_handle

- ## theorem_summary2

  Generated by the SETL procedure ???, and internally associated with the dump_theorems_handle2
  Only used in standalone running modality, for dump in unpretty form.

- ## definition_summary2

  Generated by the SETL procedure ???, and internally associated with the dump_defs_handle2
  Only used in standalone running modality, for dump in unpretty form.

- ## theory_summary2

  Generated by the SETL procedure ???, and internally associated with the dump_theories_handle2
  Only used in standalone running modality, for dump in unpretty form.

- ## citations_file

  Generated by the SETL procedure citation_analysis(uid), and internally associated with the citations_handle

- ## Err

  Opened/closed and generated by the procedures set_output_phase and verifier_invoker of the SETL packages prynter and verifier_top_level, and internally associated with the ohandle. Its content will consist of "Good" HTML-table entries.
  Only used in standalone running modality.

- ## Ferr

  Entirely handled by the SETL procedures set_output_phase and printer within SETL the package prynter, and internally associated with the ferr_ohandle. Its content will consist of "Bad" HTML-table entries.
  Only used in standalone running modality.

# Generated auxiliary files

- ## digested_proof_file

  Generated by the SETL procedure parse_file(lines_tup), and internally associated with the digested_proof_handle

  digested_proof_file is a large list of tuples of tuples, each one of the upper-level tuples representing a proof and each one of the lower-level tuples representing one of the successive lines of a proof as a pair [step_descriptor,formula], for example ["ELEM", "{z} * s_inf /= 0 & {z} * s_inf = {z}"]. The labels of internally labeled statements are left in the "formula" part of this pair, for example ["a --> Stat1", "Stat2: (a in {cdr([x,f(x)]): x in s} & a notin {f(x) : x in s}) or (a notin {cdr([x,f(x)]): x in s} & a in {f(x) : x in s})"]

  ******* Note however ******* that each proof-representing tuple is prefixed by an integer, which is the "section number" of the corresponding proof. This number is one more than the section number of the corresponding theorem statement, which is used in the theorem_sno_map_file

- ## suppose_not_file

  Generated by the SETL procedure suppose_not_file(lines_tup), and internally associated with the suppose_not_handle

  suppose_not_file is a list of triples

      [subst_list,statement_in_suppose_not,statement_in_theorem]

  used to check the correctness of the Suppose_not statements used to open proofs by contradiction.

- ## theorem_map_file

  Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theorem_map_handle

  theorem_map_file contains a set of pairs giving a map of abbreviated theorem names (often of the form Tnnn) into the corresponding theorem statement.

- ## theorem_sno_map_file

  Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theorem_sno_map_handle

  theorem_sno_map_file contains a set of pairs giving a map of abbreviated theorem names (often of the form Tnnn) into the corresponding theorem section numbers. It also contains pairs which map symbol definition names into their associated section numbers, and which map theory names into their section numbers.

- ## definition_tup_file

  Generated by the SETL procedure parse_file(lines_tup), and internally associated with the definitions_handle

  definition_tup_file contains a set of triples, each giving the name of a definition, the body of the definition, and the theory to which it belongs

- ## theory_data_file

  Generated by the SETL procedure parse_file(lines_tup), and internally associated with the theory_data_handle

  theory_data_file is comprised of three subparts. The first is a map of theories into their parent theories. The second maps the name of each theory into the list of names of all the theorems and definitions belonging to the theory. The third maps the name of each theory into a pair giving the assumed function and the assumptions of the theory.