Re: [Hol-info] Similar trouble building HOL Light's pa_j.ml

[Rob A. <rd...@le...>]

Geoffrey,

I've attached the patch. I haven't looked at it since late 2013,
so I have no idea if it will work.

Regards,

Rob.

> On 6 Dec 2016, at 22:15, Geoffrey Irving <ir...@na...> wrote:
> 
> I'm getting the following trying to build HOL Light with ocaml 4.04, camlp5 6.17:
> 
> File "pa_j.ml", line 1918, characters 35-43:
> While expanding quotation "str_item":
> Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in
>   [str_item])
> 
> I found a similar issue on Github at https://github.com/jrh13/hol-light/issues/9, and a old thread by Rob Arthan on this list: https://sourceforge.net/p/hol/mailman/message/31518128.
> 
> Rob: The mailing list thread says you have a patch, but doesn't say what that patch is.  What was it, and was it upstreamed?  If not, does anyone know how to fix the issue?