Hi Felix, >* The miz3 version is not only readable, but also not too far away from >what I might write in an informal proof. This is great!
The miz3 language is just an almost exact copy of the Mizar proof language, so this praise should go to Poland :-) >- Working with definitions requires a trick: If you want to make a couple >of definitions, you need to make sure that there are no blank lines between >your definitions and the theorem you are working on Huh? No, that's not how I intended things. The "Ctrl-C RET" really does two completely different things, depending on what the "block" that you're in looks like. If it starts with "let LEMMANAME = thm `;" it will get the miz3 treatment, have errors messages put in if necessary, etc. But if it does _not_ look like that, it's just copy-pasted as ocaml to the HOL session. This second behavior was a late addition to the interface, just as a convenience. Apparently for you that has caused confusion. What you should do is to have blank lines around the defintion from the start. So process it with "Ctrl-C RET" (then it will be sent as ocaml and processed that way, because it doesn't look like a lemma) _or_ copy-paste it to the HOL session as you would have done without the miz3 thing. And then further leave it alone and go on with the lemmas after it. You can "run" miz3 proofs in the HOL session too, there is no need to use the "vim interface" at all, so if you (implicitly) copy-paste things like you seem to have done, _something_ will happen. But that's not how the system was meant to be used. >- Of course you cannot use backticks inside a block of miz3 syntax. So if >you want to do something like (SPEC `(\k. f k * recip f (x - k))` >SUM_CLAUSES_LEFT) within miz3 you need to write it as (SPEC (parse_term >"(\\k. f k * recip f (x - k))") SUM_CLAUSES_LEFT). I.e.: use the parse_term >function, use double-quotes and escape your backslashes. Exactly. I also regret this. Originally I wanted to use the syntax ``...`` for proofs and then allow "nested" quotes like ``... `...` ...``. However, to have accomplished that, I would have needed to tinker with the "pa_j.ml" file, which I consider "holy" and untouchable. Or, stated differently: I wanted to keep the whole thing contained to the single file "miz3.ml". So in the end I went for the `;...` syntax for proofs, as the second best option. And then there couldn't be nested quotes anymore. >- Some syntax errors are not reported in the vim buffer but only on the >REPL. These syntax errors are reported as "Error: File "/tmp/miz3_4802.ml", >line 17, characters 20-21: Parse error:..." which is not helpful, because >at the time the error is reported, the temporary file in question has >already been deleted. It would be great if the offending line could be >printed on the REPL as well. That sometimes happens, yes. It's related to the fact that internally I call the ocaml interpreter, and this kind of errors I then cannot catch. At least, I seem to remember that that was the case. It shows that miz3 really is a bit of a (large) hack. (As Makarius pointed out, ocaml is a "dirty" language, and I make a lot of use of that :-)) In other words: it's not _me_ that is giving that error. I don't remember/know whether I can even "see" that this situation occurs (so I can leave the tmp file in place), but I don't think it's easy. >I can drop REWRITE_TAC almost everywhere (and >list only the theorems I would pass to REWRITE_TAC) but for some reason >this does not work in these last two lines. The current miz3 system has two main weaknesses: - The "by" justifier is not what it should be. If you can prove something trivially by REWRITE_TAC, then "by" should be able to do that too. As you found out, currently it's not that way. This "wrong by" is of course orthogonal to the basic design of the system. But from a user's point of view it is very bad, yes. - There is not a good interface to "develop" the justification tactic in a "by" without already firing it into the proof. I have some ideas on an extension to the interface for this, but currently I'm not working on this either. The other shortcomings are _to me_ minor inconveniences. But these two are big ones, yes. Freek ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
