Hi Ramana, | I would be glad to see an update to HOL Light (mainly the Makefile and | some pa_j_xxx.ml) such that it builds smoothly with the latest OCaml | (3.12.1) and Camlp4.
This would certainly be very nice. It is probably not difficult in principle to switch to using camlp4. However, when the dramatic change to camlp4 happened in OCaml 3.10, the new camlp4 was completely undocumented, which is why I switched to camlp5. Perhaps things have improved since then. Adding basic syntax extensions like extra infixes, "it" and quotations is probably pretty easy (though quotations seem a bit more complicated in the new camlp4, requiring you to do work to get the content simply as a string). The complications may come with the lexical changes, the different case conventions and the use of `...` instead of <<...>> for quotations. Here camlp5 is not very satisfactory either: it seems that the only way to change the lexer is basically to copy the existing one and modify it, which is why the pa_j files are so hideous and camlp5-version-dependent. Anyway, I would be very happy if someone else feels like doing this. I doubt if I will get to it very soon myself, even though I understand the inconvenience it causes. On Phil's original problem that the HOL Light case conventions are incompatible with CamelCase identifiers as constructors or module names, such names are not used much in HOL Light (or in core OCaml libraries as far as I can see), so there would be no great problem with modifying the case conventions a bit. Also, as Phil may already know, you can temporarily knock out and restore the lexical changes by: unset_jrh_lexer;; .... stuff using conventional OCaml lexing .... set_jrh_lexer;; Using this sort of bracketing, one may be able to encapsulate the Batteries calls one needs. John. ------------------------------------------------------------------------------ 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
