OverviewCakeML:67fd272ad040a95fd349fe9a288ee581405236eb
Remove a typo
#831 (pancake)
Merging into:76ed0b05089a77059dee72d197fc56c3dae661e8
Merge pull request #829 from CakeML/help
HOL:8e564a6e4322326b526253a23abe0f85d1bb6f86
Make BIGINTER_2 globally available again, but from pred_setTheory
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 148MB
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: 0sFAIL<1>
WARNING: /home/cug/hk324/cakeml/.holpath overrides value for CAKEMLDIR from /home/cug/hk324/cml-regression/cakeml-1564/.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-1564/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\"}"