jorge-agra/hipcam

Tools for recording Hiproofs in hol-light and visualising them in a web browser

HipCam

Tools for recording Hiproofs in hol-light and visualising them in a web browser.

More extensive documentation on how to use these tools is coming soon. There is also a forthcoming paper about it. For some high-level information available now, see the slides in the file hiproofs_talk.pdf.

If you are eager to use it NOW, do the following:

• Install HOL Light (see hol.ml to see if the versions match).
• Copy the hiproofs directory and fusion.ml and hol.ml into the HOL Light directory

Make sure that the variable JGRAPH_BROWSER_COMMAND in hiproofs/main.ml is set properly for your environment. The default value is

open "/Applications/Google Chrome.app" $

which uses Chrome on Mac OS X as a browser. The dollar sign $ is where the location of the HTML file to display will be inserted.

You can now export a theorem T via

Hitools.export size T name

For adding your own hierarchical boxes to proofs, you can use the hilabel function or any of its derivatives:

hilabel : Hiproofs.label -> (thm list -> thm) -> thm list -> thm
hilabel_thm : Hiproofs.label -> thm -> thm
hilabel_tac : Hiproofs.label -> tactic -> tactic
hilabel_tac_goals : Hiproofs.label list -> tactic -> tactic
hilabel_tac_frame : Hiproofs.label -> tactic -> tactic

string_label : string -> Hiproofs.label

Have fun visualising!