On 3 April 2017 at 13:50, Lars Hupel <hu...@in.tum.de> wrote:
> Dear list,
>
> I've been trying to build a recent commit of HOL (4b08982).
>
> My environment is Arch Linux x64, Poly/ML 5.6.
>
> This is the output of "bin/build":
>
>
> Building directory src/holyhammer/hh [03 Apr, 14:01:12]
> hh_parse.ml / toolbox.. | Holmake: Fail exception: Unknown
> result status
>
> Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
> (exited with code 1)
>
>
Whatever the problem was here, it might have left some stale or incomplete
files in that directory, which might then be causing the subsequent
problems. You could clean the hh directory (either Holmake cleanAll or, for
really everything, git clean -xdf) before trying to build again.
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.
> If I re-run "bin/build" I get an error that seems to be related to OCaml:
>
> Building directory src/holyhammer/hh [03 Apr, 14:03:21]
> hh_parse.{cmi,cmx}
> FAILED!
> File "hh_parse.ml", line 1:
> Error: Could not find the .cmi file for interface hh_parse.mli.
> Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
> (exited with code 1)
>
>
> NB, the released Kananaskis 11 also fails to build, but with enough
> repeated invocations of "bin/build" it eventually succeeds.
>
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
