Hi William,
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
<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
<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
<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.
Cheers,
Heiko
On 11.03.21 06:25, William Mitchell Jr wrote:
Hi,
I downloaded the code and #use "init.ml <http://init.ml/>";; runs
without errors.
But how do I make OCaml's utop interactive with all of the .ml files?
Much Thanks,
William Mitchell
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
