On Mon, May 7, 2012 at 3:27 PM, Phil Scott <[email protected]> wrote:
> 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?
>
Demand for migration or for additional niceties in particular?
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.
>
> 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
>
------------------------------------------------------------------------------
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
