Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Rob, >>[...] and Freek Wiedijk's vi mode for HOL Light. >Where do I find the above-mentioned vi mode? The current version has been on the web for a while at but there is no link yet. Everyone should feel free to do with it whatever they like.

Re: [Hol-info] Emacs Macros for HOL Light Proof

Freek sent me the vi mode via private mail: I don't know if it is publicly available anywhere. Cheers, Joe On Sun, Nov 8, 2015 at 9:32 AM, Rob Arthan wrote: > >> On 4 Nov 2015, at 05:22, Joe Leslie-Hurd wrote: >> >> and Freek >> Wiedijk's vi mode for HOL Light. > > Where do I find the above-m

Re: [Hol-info] Emacs Macros for HOL Light Proof

> On 4 Nov 2015, at 05:22, Joe Leslie-Hurd wrote: > > and Freek > Wiedijk's vi mode for HOL Light. Where do I find the above-mentioned vi mode? Regards, Rob. -- ___ hol-in

Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Petros/Joe, I must admit that I'm not particularly familiar with any of these Emacs/etc modes for HOL Light and HOL4, although I have seen Proof General, and ProofTree that interacts with it. How do these other facilities compare? > Tactician is more general and gives you a full breakdown of

Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Joe, On 04/11/2015 18:07, Joe Leslie-Hurd wrote: > I was thinking of a lightweight HOL Light mode that highlighted quoted > terms/tacticals/etc and knew about indentation of tactic proofs, > rather than extending an OCaml mode that has a lot of features that > don't really apply to HOL Ligh

Re: [Hol-info] Emacs Macros for HOL Light Proof

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 b

Re: [Hol-info] Emacs Macros for HOL Light Proof

Hi Petros, > It should be possible to make it compatible with the commonly used > tuareg mode. > (There are some conflicting keyboard shortcuts and the tuareg mode > window is named *caml-toplevel* instead of *shell*.) I was thinking of a lightweight HOL Light mode that highlighted quoted terms/t

Re: [Hol-info] Emacs Macros for HOL Light Proof

This is interesting and quite useful! Thank you for sharing. It should be possible to make it compatible with the commonly used tuareg mode. (There are some conflicting keyboard shortcuts and the tuareg mode window is named *caml-toplevel* instead of *shell*.) Jump-to-proof-point is quite nice!

Re: [Hol-info] Emacs Macros for HOL Light Proof

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 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.c