John and Freek, the simplest way for me to understand my syntax and semantics would be to read and then rewrite miz3.ml. Right now I feel I couldn't possibly do that, because of what Freek writes on p 17--18:
if one leaves out enhancements like the caches and time-outs, the system becomes unusable for serious work. [...] In other words the full proof is processed every time a check is done. To make this ac- ceptably fast, there are two caches. The first cache holds inferences that have already been checked, to prevent the checker from having to run all tactics every time. The sec-ond cache holds the OCaml objects associated with the elements in the by justifications. These are calculated using the OCaml functions Toploop.parse_toplevel_phrase and Toploop.execute_phrase (which together are the OCaml equivalent of Lisp’s eval function). I'm not competent to deal with OCaml caches, and I bet it would impede my visibility of the `abstract description'. My only hope that we could rip out the OCaml code is Freek's preceding remark Specifically, when checking a proof from the vi interface by typing But I don't ever do that, and John doesn't either. -- Best, Bill ------------------------------------------------------------------------------ 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
