Hi all. I've run up against numerous problems with the HOL Light syntax extension which I thought I'd share:
The current changes to the preprocessor mean that what would normally be regarded as uppercase identifiers such as BatMap are now seen as lower case and therefore not recognised as module identifiers. Since the entire of the batteries library uses CamelCase for its module names, this makes it difficult for HOL Light users to work with what is now the defacto standard library for Ocaml. There are various ways around this, and I've put in my own small changes to the pa_j.ml code to eliminate most of the issues I have. However, my latest stumbling block is in using the language extensions introduced in Ocaml 3.12. Most of these extensions are unavailable to HOL Light users, since pa_j.ml does not have entries for the latest Ocaml syntax. We could look to hacking the latest pa_o.ml preprocessor, but since Camlp5 is now deprecated in favour of Camlp4, I would rather migrate. I *think* this will allow users to bring in additional niceties such as list-comprehension syntax using topfind. Is there any demand for this from HOL Light users? Phil -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
