Hi Bill, > By grepping, I see occurrences of Format.print_string and > Format.print_newline commands in e.g. make.ml, but isn't the Format > prefix here unnecessary, because they're pervasive? Isn't that > explained in section 20.2 Module Pervasives : The initially opened > module of the ocaml reference manual, and p 318 for print_string and > print_newline?
Yes, the use of the "Format" prefix in HOL Light's make.ml is unnecessary because it's already included as a result of printer.ml in hol.ml. But it does no harm being there. Regarding what the OCaml reference manual says: OCaml's Pervasives module is initially opened, but not its Format module. > Your failwith idea sounds great, but I didn't understand it. I think just look at my last two emails again - it should be pretty clear. And look at the HOL Zero source code in the places I suggested. I can't really think how to explain it better. > For instance, should all error messages be pretty-printed? If not, do I > really want to override the standard printer? All exceptions are pretty printed in OCaml, and I thought the whole point of your post was that you weren't happy with this pretty printing for Failure exceptions, and so I explained how to override it just for Failure exceptions and keep the pretty printer for all other exceptions exactly the same. > I grepped through your Tactician sources and I see a lot, so I bet you > understand this quite well... Not really. My starting point was Zumkeller's code in HOL Light's update_database.ml, and then I searched a bit on the web for info about Obj, etc. My Tactican code examines the memory representation of ML bindings to have a guess at the ML type of these bindings. There may be a better way of doing this. I don't really have time to examine Freek's code, but it looks like he's done a similar thing to me in terms of using update_database.ml as a starting point. Yes, the Toploop and Lexing stuff is taking a string and running it as OCaml. I don't really know much about the OCaml Lexing module, I'm afraid. My use of it in Tactician's mlconcrete.ml is just a cut-and-pasting. HOL Light and HOL Zero don't use OCaml's lexing facilities, but implement their own from scratch. > BTW I looked at your HOL Zero page > http://www.proof-technologies.com/holzero/index.html, and remind me of > something I should know: Does your HOL Zero do type quantification? No it doesn't. You need HOL-Omega for that. This and many other aspects of HOL are covered in my glossary. Mark. ------------------------------------------------------------------------------ Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
