CakeML Regression Test

Job 2135

CakeML:e7813d9bdcb11d626cd27b973330da551f89a102
  check derived dominate associated constraints [Apr 03 10:14:22]
#955 (vipr)
Merging into:5e0612a6f93d34e570019c2a768cbd4736402abe
  Fix for change to finite_mapSyntax in HOL [May 25 02:29:21]
HOL:8a1c5607fb8c5be3be18fbe7a3653c704b0ea4da
  Manual: mention that LaTeX munging handles record types OK [May 23 05:56:07]
Machine:pavlova

May 25 10:54:36 Claimed job
May 25 10:54:40 Reusing HOL
May 25 10:54:49 Starting developers
May 25 10:54:53 Finished developers                                               2s 197MB
May 25 10:54:54 Starting developers/bin
May 25 10:55:03 Finished developers/bin                                           8s   1GB
May 25 10:55:04 Starting compiler/proofs
May 25 10:55:55 FAILED: compiler/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/proofs[0m
Scanned 83 directories
Starting work on osetTheory
Starting work on byteTheory
Starting work on libTheory
Finished $(HOLDIR)/examples/machine-code/multiword                     (0.000s) 
Starting work on ag32Theory
osetTheory                                   examples/balanced_bst  (5s)     OK
Finished $(HOLDIR)/examples/balanced_bst [#theories: 1]                (5.920s) 
Starting work on regexp_mapTheory
libTheory                                                     misc  (6s)     OK
Starting work on ffiTheory
byteTheory                                                    misc  (7s)     OK
Starting work on miscTheory
ag32Theory                                  compiler/encoders/ag32  (9s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm/model                  (0.000s) 
Finished $(HOLDIR)/examples/machine-code/decompiler                    (0.000s) 
Starting work on l3-heap
regexp_mapTheory                 examples/formal-languages/regular  (6s)     OK
Starting work on regexp_compilerTheory
ffiTheory                                            semantics/ffi  (6s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (6.540s) 
Starting work on arm8Theory
l3-heap                                   examples/l3-machine-code (23s)     OK
Finished $(HOLDIR)/examples/l3-machine-code                           (23.860s) 
Starting work on arm-heap
regexp_compilerTheory            examples/formal-languages/regular (18s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 2]   (25.150s) 
Starting work on mipsTheory
arm8Theory                     examples/l3-machine-code/arm8/model (20s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (20.000s) 
Starting work on arm8-heap
arm-heap                         examples/l3-machine-code/arm/step (52s)     OK
Starting work on arm_stepTheory
arm_stepTheory                   examples/l3-machine-code/arm/step  (0s)FAIL<1>
 Couldn't load HOL base-state /scratch/cakeml/regression/HOL-8a1c5607fb8c5be3be18fbe7a3653c704b0ea4da/examples/l3-machine-code/arm/step/arm-heap: Fail "The parent for this saved state does not match or has been changed"
miscTheory                                                    misc (33s)MKILLED
mipsTheory                     examples/l3-machine-code/mips/model  (9s)MKILLED
arm8-heap                       examples/l3-machine-code/arm8/step  (0s)MKILLED