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

[Geoffrey I. <ir...@na...>]

The patch works without modification!  Thank you so much!

Should I submit a pull request to get this into HOL Light?  Some version
trickery would presumably be required to make it safe.  Also there have
been no pull requests to the Github repo to date, so I'm not sure if
they're the accepted mechanism.

On Tue, Dec 6, 2016 at 2:24 PM Rob Arthan <rd...@le...> wrote:

> 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?
>
>
>
>