Hi Bill & John, >| Better error messages would be great.
The way the error messages work is that first the proof is split into "steps" based on the semicolons and keywords. (I think certain keywords always start a new step and semicolons always end one, with "now" and "proof" being the exception because they count as a step but don't have a semicolon, and with bracketing taken into account, because you don't want to have REWRITE_TAC[FOO; BAR] split the step.) Anyway, then the errors always point at the end of such a step. And then errors 4 to 9 you should take to mean "something is seriously wrong", of the order of a syntax or type error, while for errors 1 to 3 you should think about the actual proof, i.e., they mean something like "the contents of the statements don't match up". Error 3, "skeleton error", means that the proof step doesn't match the "thesis", while errors 1 and 2 mean that the "by" didn't get it (or that the inference just doesn't hold in the first place). There actually are three parsers working together: my Mizar-style proof language parser (error 9), the HOL term and type parsers (error 8) and the ocaml parser for the items in a "by" list (which may be thms/tactics/conversions, so everything there is first given to the ocaml parser: that's error 5). >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. The main problem on that side is of course that the HOL term parser won't point out where the syntax error is if there is a syntax error. Still I don't know whether adding something for that would be too useful. If I get error 8, I generally put the offending statement between backquotes in the HOL session, and fiddle with it until it's right. And then copy/paste it back. 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
