First version of HOL Light tactic recording.

See INSTRUCTIONS and LIMITATIONS files for more details.
Currently works for flattening "packaged-up" tactic proofs into g/e commands.
Won't work for most proofs because most tactics/thms haven't been promoted.
Support for exporting proof graph as a series of goal pairs.
Support for displaying extra information to be intercepter by PG for Prooftree.

1 files changed, 36 insertions, 0 deletions

diff --git a/hol-light/TacticRecording/INSTRUCTIONS b/hol-light/TacticRecording/INSTRUCTIONS
new file mode 100644
index 00000000..86380b93
--- /dev/null
+++ b/hol-light/TacticRecording/INSTRUCTIONS
@@ -0,0 +1,36 @@
+To use this:
+1. first compile HOL Light and any extra files up to the particular proof you want to record;
+     #use "hol.ml";;
+     #use ....
+
+2. Then process the 'main.ml' file
+     #use "TacticRecording/main.ml";;
+
+3. Then perform the tactic proof you want to record, using g/e's or prove:
+     g `...`;;
+     e (...);;
+     e (...);;
+  OR
+     prove (`...`, ... THEN ... THENL [...]);;
+
+4. Use the ML export commands to output the proof in the form you want:
+
+     print_executed_proof ();;
+         - Tries to reproduce the inputted proof verbatim, with steps
+          corresponding one-to-one to original.
+
+     print_flat_proof ();;
+         - Prints the proof as a flatten series single-tactic steps, with no
+          tacticals.
+
+     print_thenl_proof ();;
+         - Prints the proof as a single-step tactic, connected by THEN for
+          single goals and THENL for multiple goals.  This structure directly
+          reflects the tree structure of the proof as it was executed.
+
+     print_optimal_proof ();;
+         - Like 'print_thenl_proof', but prints a more concise proof, not
+          necessarily reflecting the original tree structure.  Currently this
+          only performs one improvement: seeing where THENL can be replaced
+          with THEN.
+