CakeML Regression Test

Job 3354

CakeML:5ea273ee4c90961f8cff69afd3c3d2df6ee57520
  Merge branch 'master' into pancake-add-inst [May 22 16:07:48]
#1398 (pancake-add-inst)
Merging into:35898f2190ba17c7a38ab0f91fe57a4ce9dbbbc8
  pancake/loop: extend Break/Continue with nesting-depth num (#1395) [May 22 16:05:01]
HOL:9bc51265f47dd73330c063de58178125f58b6b6d
  docs -> html_docs [May 22 02:21:44]
Machine:lammmington

May 23 17:29:42 Claimed job
May 23 17:29:46 Reusing HOL
May 23 17:30:02 Starting developers
May 23 17:30:07 Finished developers                                               4s 189MB
May 23 17:30:08 Starting developers/bin
May 23 17:30:13 Finished developers/bin                                           3s  93MB
May 23 17:30:14 Starting misc
May 23 17:30:59 Finished misc                                                    44s   1GB
May 23 17:31:00 Starting compiler/proofs
May 23 17:31:11 FAILED: compiler/proofs
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanned 90 directories
Starting work on mllistTheory
Starting work on mlmapTheory
Starting work on mloptionTheory
Starting work on mlsetTheory
mllistTheory                                            basis/pure  (0s) CACHED
Starting work on mlstringTheory
mlmapTheory                                             basis/pure  (0s) CACHED
Starting work on mlvectorTheory
mloptionTheory                                          basis/pure  (0s) CACHED
mlsetTheory                                             basis/pure  (0s) CACHED
Starting work on namespaceTheory
Starting work on MarshallingTheory
namespaceTheory                                          semantics  (0s) CACHED
Starting work on pattern_commonTheory
MarshallingTheory                                            basis  (0s) CACHED
Starting work on parmoveTheory
pattern_commonTheory             compiler/backend/pattern_matching  (0s) CACHED
Starting work on backend_commonTheory
mlstringTheory                                          basis/pure  (0s)FAIL<1>
mlvectorTheory                                          basis/pure  (0s) killed
parmoveTheory                           compiler/backend/reg_alloc  (0s) killed
backend_commonTheory                              compiler/backend  (0s) killed
*** Holmake aborted - 1 target failed:
*** mlstringTheory in basis/pure (status 1)
 Checking cache for prebuilt theory...
 Cache miss; theory will be built locally.
 <<HOL message: link_parents: the following parents of "mllist"
   should already be in the theory graph (but aren't): ("misc",7b37a2f65cd539a5d47aee12e24fba2b097a6c6a)>>
 error in quse /scratch/cakeml/regression3/cakeml-3354/basis/pure/mllistTheory.sml : TheoryReader "Exception raised: HOL_ERR (HOL_ERROR {message = \"\", origins = [{origin_function = \"link_parents\", origin_structure = \"Theory\", source_location = Loc_Unknown}]})"
 error in load $(CAKEMLDIR)/basis/pure/mllistTheory : TheoryReader "Exception raised: HOL_ERR (HOL_ERROR {message = \"\", origins = [{origin_function = \"link_parents\", origin_structure = \"Theory\", source_location = Loc_Unknown}]})"
 error in load /scratch/cakeml/regression3/cakeml-3354/basis/pure/mlstringScript : TheoryReader "Exception raised: HOL_ERR (HOL_ERROR {message = \"\", origins = [{origin_function = \"link_parents\", origin_structure = \"Theory\", source_location = Loc_Unknown}]})"
 Uncaught exception at /scratch/cakeml/regression3/HOL-9bc51265f47dd73330c063de58178125f58b6b6d/src/postkernel/TheoryReader.sml:69: TheoryReader "Exception raised: HOL_ERR (HOL_ERROR {message = \"\", origins = [{origin_function = \"link_parents\", origin_structure = \"Theory\", source_location = Loc_Unknown}]})"
 Full log: /scratch/cakeml/regression3/cakeml-3354/basis/pure/.hol/logs/mlstringTheory