On Thu, Mar 11, 2021, at 08:38, Heiko Becker wrote: > I assume that you want to run an interactive session of HOL-light, > right? What worked quite nice for me is using the hol-light.el bindings > for emacs (https://github.com/gilith/hol-light-emacs). There seems to > also be a vi mode (https://www.cs.ru.nl/~freek/step/step.tar.gz), but I > have never used it before. I just found it here: > https://sourceforge.net/p/hol/mailman/hol-info/thread/CAMej%3D27hGGcVYxfMBf-F4b3sZsH-dYu1djYs3vddcc8GzsMv%3DA%40mail.gmail.com/#msg34592229 > > With those proof modes you can edit your proof script on one side of > the screen and send the things you are typing to an interactive session > that is run for you. I hope that is what you were looking for.
I can add to this list a vim plugin I wrote and have been happily using to edit HOL Light proofs [1]. Combined with an ad-hoc snapshotting library [2], it makes HOL Light very convenient to use interactively. [1] https://github.com/mpu/vim-hol [2] https://c9x.me/git/selfie.git _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
