search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
616 stars 137 forks source link

Technology to record interactive sessions for documentation purposes #327

Closed mn200 closed 8 years ago

mn200 commented 8 years ago

Using the PolyML.compiler function, some custom filter analogous to the TeX munger should be possible here.

konrad-slind commented 8 years ago

I wonder if it could be used to record inputs for building "goal trees" in src/proofman/goalTree. Not being able to record the concrete syntax of tactics was one of the impediments to further development of this proof manager.

Konrad.

On Fri, Jan 8, 2016 at 3:48 AM, Michael Norrish notifications@github.com wrote:

Using the PolyML.compiler function, some custom filter analogous to the TeX munger should be possible here.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/327.

mn200 commented 8 years ago

It's not necessarily feature complete, but this has basically been done, as of ec15f9deab.