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 <http://www.cs.ru.nl/~freek/step/step.tar.gz> but there is no link yet. Everyone should feel free to do with it whatever they like. I haven't checked whether it's still compatible with the latest version of HOL Light (or vim, for that matter). There is a README with some explanations that I wrote for John (but as he's not a vi user, I'm not sure he has tried it.) This is very much not a polished thing. I never used it to write a significant HOL Light formalization. I'm sure that if I would, the commands for the thing (and maybe its behavior) would change significantly. This is an attempt to make something that behaves like interfaces like Proof General and CoqIDE and so on for HOL Light. I.e., one edits a file, and in a separate window a proof state is updated simulaneously that corresponds to a location in the file, without having to even think about commands being processed in a HOL Light session. So there is no concept of "copying from the file to a session". The file itself contains the proofs and proof steps, and that's just it. This only works for HOL Light proofs in "John Harrison style" (but of course can be adapted for different styles.) It also works on the lemma level, so it doesn't know about the file as a whole, it only knows about a single lemma at the time (a lemma being defined as a part of the file between two successive empty lines.) It imitates the Matita interface where one can step throught a ... THEN ... THEN ... chain that works on multiple subgoals simultaneously (in Coq terms: "also steps semicolons".) It's very "hacky", with communication through the file system (in /tmp), and with vi sessions talking to each other, and so on. I'm sure it can be organised better (named pipes? I kind of dislike that kind of thing), but am not really interested in trying to work on such a reorganised version myself. It also probably is easy to adapt this for emacs. Myself, I really like this interface. I'm sure that _if_ you want to use HOL Light in John's style, and _if_ you want to use vi (vim) as your editor, and _if_ this gets a bit more work, it really would be a helpful interface. And I would _love_ to see a HOL4 version of this :-) Freek ------------------------------------------------------------------------------ Presto, an open source distributed SQL query engine for big data, initially developed by Facebook, enables you to easily query your data on Hadoop in a more interactive manner. Teradata is also now providing full enterprise support for Presto. Download a free open source copy now. http://pubads.g.doubleclick.net/gampad/clk?id=250295911&iu=/4140 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
