OverviewCakeML:76ed0b05089a77059dee72d197fc56c3dae661e8
Merge pull request #829 from CakeML/help
HOL:1dfda82edf04a50d842dac582fd1231a6d07239a
Remove .HOLMK directories before doing a build
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 121MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
FAILED: semantics/ffi
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Starting work on locationTheory
Starting work on lem_pervasivesTheory
Starting work on lem_pervasives_extraTheory
Starting work on README.md
README.md real: 0s user: 0s OK
locationTheory real: 1s user: 0s OK
lem_pervasives_extraTheory real: 3s user: 2s OK
lem_pervasivesTheory real: 3s user: 2s OK
Starting work on libTheory
libTheory real: 1s user: 1sFAIL<1>
WARNING: /home/cug/hk324/cakeml/.holpath overrides value for CAKEMLDIR from /home/cug/hk324/cml-regression/cakeml-1567/.holpath
error in quse /home/cug/hk324/cakeml/misc/lem_lib_stub/lem_pervasivesTheory.sml : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
error in load $(CAKEMLDIR)/misc/lem_lib_stub/lem_pervasivesTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
error in load /home/cug/hk324/cml-regression/cakeml-1567/misc/lem_lib_stub/libScript : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
<<HOL message: link_parents: the following parents of "lem_pervasives"
should already be in the theory graph (but aren't): ("Omega",1621956178,926023), ("int_arith",1621956179,13720), ("finite_map",1621956136,465368)>>
Uncaught exception: TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"