Hi Bill, | there is probably a gap in the market for a tutorial and/or | reference for miz3 from the user perspective. | | Great! This is my main task now. But I don't know enough to write | this miz3 tutorial and user reference manual (more below).
I hope you manage to produce something. Curiously enough, Freek wrote a lot of documentation to explicate Trybulec's Mizar, so maybe you will end up doing the same for Freek's miz3. http://cs.ru.nl/~freek/mizar/index.html | I am really grateful to you, John, and I couldn't have done without | you, but, uh, I was hoping you'd do even more The reference manual | says not to use new_axiom. Yes, for now you can replace the "new_axiom" stuff with the explicit model construction I sent out earlier. I will experiment a bit to find the nicest way of doing things with the axioms as hypotheses. I like Freek's idea of having the hypothesis in the assumption list of the theorem rather than as the antecedent of an implication, but I need to dig into miz3 a bit more deeply or get help from Freek to make it work. | Better error messages would be great. I'll defer to Freek on miz3-specific things, but I will try to improve cases where the native HOL Light error reporting is part of the problem. | Or another dumb question: How do you run miz3 code? I'm just | selecting in an Emacs window and then pasting into a terminal running | hol_light> ocaml | #use "hol.ml";; | Why can't I paste in a use command like | #use "John5-8ModelTarski.ml";; | I know Freek describes a vi-based system but I haven't learned it yet. I do pretty much that, either for miz3 or native HOL Light proofs, just copying and pasting from an editor window into an OCaml session. This video might give an impression: http://www.math.kobe-u.ac.jp/icms2006/icms2006-video/video/v103.html I think you may be hitting something I also noticed, which is that the special parsing of miz3 proofs within `;...` only gets set up after the miz3 file is loaded, and OCaml parses an entire source file before anything gets executed. This means that having this in one file: loadt "miz3/miz3.ml";; ... `; ... a miz3 proof`;; doesn't work, since when this file is loaded `;....` isn't interpreted correctly. But you can simply have a root file called "make.ml" or whatever containing (it shouldn't matter if you use loadt or #use): loadt "miz3/miz3.ml";; loadt "file_with_miz3_proofs.ml";; John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
