Hi Bill, > Let me try to explain. My only objection to my PrintErrorFail is minor: > it prints Exception: Failure "". at the end, but arguably this is a good > error message.
What you do is print out the message regardless of whether the exception bubbles up to the toplevel. The solution I'm suggesting only prints the message if the exception hits the toplevel. I don't know which functionality you want. > "fail" has an link in the HOL Light reference manual, and "failwith" is > only explain in the "fail" link: 'failwith' is part of OCaml itself, but 'fail' is a just a HOL Light thing. > I think that you understood a great deal more about pretty-printing error > messages, and I advise you to try to write up what you know.We need good > documentation.Perhaps you understand printer.ml well enough to recommend > some change by which all HOL Light error messages are pretty-printed. I > certainly don't see how to do this. Yes we do, and that's on of the things I'm aiming to do with HOL Zero. My hands are full with various projects of my own, and I don't really have time to document HOL Light. > I just looked at your Tactician sources, and I have some non-expert > responses: This from mlconcrete.ml > .... > > let exec x > (ignore o Toploop.execute_phrase false Format.std_formatter o > !Toploop.parse_toplevel_phrase o Lexing.from_string) x;; > > looks pretty similar to the code I borrowed from miz3.ml. Can you explain > it? Is this different from the Roland Zumkeller's Flyspeck code you > mention in autopromote.ml? Is this explained in Flyspeck somewhere? I know what it's doing but don't know the detailed functionality about each of the functions used. I got it as a cut-and-paste from update_database.ml! Roughly speaking it takes a string, turns it into lexical tokens, turns this into abstract syntax and then executes it. > I see that in termparser.ml you have > > let enable_flyspeck_parsing () > let env = Obj.magic !Toploop.toplevel_env > > I bet it would be a really good programming exercise for me to really > understand how Toploop/Obj.magic/Lexing code is used in the Ocaml sources, > or Flyspeck, or your Tactician. But I'd rather you explain it to me so I > can read Voevodsky's book. I think it's a better idea to get really familiar with the main parts of OCaml, which are explained in the reference manual. Dabbling with Toploop and Obj is a bit advanced and is very difficult to find good documentation about. I've only got a partial understanding, which is good enough for my purposes in Tactician. 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
