Overview

Job 1564

CakeML: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\"}"