Ramana: >For HOL Light, I have seen a Vim-integration by Freek Wiedijk which is >perhaps even better for interactive proof-viewing, since it also keeps >track of where you are up to in the editor buffer, and shows all subgoals >of the proof in the viewing terminal.
FWIW, this thing I developed for my own use, and I have hardly used it myself yet either. It also is a big hack. OTOH, I kind of like it, and anyone who wants to try it can have it, just mail me. What it is, it is a thing for HOL Light that clones the user experience of the Proof General/CoqIDE/etc way of working with proofs. You can step through HOL Light proofs as long as you use John's prove(`...`, ... THEN ... THENL ...) style (and I guess you can hack it to work for different styles too). So the proof will have been processed up to a certain point, and the goal at that point is shown in a different window. As it is low-tech vi, there's no highlighting, instead the current location in the proof is marked with a "|#" sign. But one doesn't need to copy-paste from one window to another, one just edits in the final file, and it gets processed. The thing can step through multiple goals in parallel (in Coq words "it can stop at semicolons too"), when a tactic produces multiple goals but one doesn't do a THENL then. This is something I first saw in Matita, and that I liked, so I imitated that. It means it behaves different from the normal interactive way of using HOL Light, as in that case you always only work on one goal at the time. The interface also can show the goals you're not working on right now (although you can turn that off too, if you don't want to be bothered). Freek ------------------------------------------------------------------------------ Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
