Last year I wrote some functions for calling Hol(y)Hammer remotely: https://github.com/JUrban/hol-advisor/blob/master/hol-advice.el
It was done on top of this HOL Light mode (used by Flyspeck I think): https://github.com/JUrban/hol-advisor/blob/master/hol-light.el . I think I changed that mode a bit to work with emacs24 and (try to) work with DMTCP images. There is an addition to that mode in the Flyspeck repo by Sean McLaughlin: https://code.google.com/p/flyspeck/source/browse/trunk/emacs/hol-light-mode.el . Josef On Wed, Nov 4, 2015 at 6:32 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > You forgot to mention the comprehensive Vim mode for HOL4. > (See tools/vim in the HOL4 repository.) > > On 4 November 2015 at 16:22, Joe Leslie-Hurd <j...@gilith.com> wrote: >> For those of you who use HOL Light in an Emacs shell, I wrote some >> simple Emacs Lisp macros to support interactive proof: >> >> https://github.com/gilith/hol-light-emacs >> >> It's just basic stuff, but I have found that they speed up proof >> development (and the jump-to-proof-point is a boon to proof >> maintenance). >> >> These macros fill a gap between more comprehensive efforts: Michael >> Norrish's hol-mode for interacting with HOL4 in Emacs, and Freek >> Wiedijk's vi mode for HOL Light. >> >> Cheers, >> >> Joe >> >> ------------------------------------------------------------------------------ >> _______________________________________________ >> 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 ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
