No that again looks like malformed products of an incomplete build. Try
cleaning the relevant directory. (Or clean everything if you don't mind
starting again.)
On 3 April 2017 at 17:40, Lars Hupel <[email protected]> wrote:
> > As for avoiding the error above, you might like to try the fixes-5.6
> branch
> > of Poly/ML rather than the released version, since I think there were
> some
> > bug fixes made that are relevant to parallel Holmake (I'm not sure).
> > Alternatively, try passing the -j1 option to bin/build (or Holmake),
> which
> > turns off the parallelism.
>
> Okay, that seems to have solved that particular error. Now I'm getting
> this one:
>
>
> Theory "gcd" took 0.83000s to build
> Holmake failed with exception: LEX_ERROR "numpairScript.sml 39.9
> '.'-whitespace unexpected"
> Build failed in directory
> /home/lars/work/reify/HOL/src/num/extra_theories (exited with code 1)
>
>
> Could that also be related to a wrong Poly/ML version?
>
> Cheers
> Lars
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
