Job 1783

CakeML:02b076ec472f896299ebdc34ccfeadf1f4037618
  Make translator use new lookup_indn from DefnBase [Feb 21 15:28:56]
HOL:b46e29d269344e1d2981f1c850969b4f6ff7a0ac
  Delete unused code; improve error messages in RealArith.sml [Feb 18 04:44:09]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 21 15:42:11 Claimed job
Feb 21 15:42:12 Reusing HOL
Feb 21 15:42:24 Starting developers
Feb 21 15:42:29 Finished developers                                               4s 114MB
Feb 21 15:42:29 Starting developers/bin
Feb 21 15:42:33 Finished developers/bin                                           4s 675MB
Feb 21 15:42:33 Starting semantics/ffi
Feb 21 15:42:43 Finished semantics/ffi                                            9s 247MB
Feb 21 15:42:43 Starting semantics
Feb 21 15:44:46 Finished semantics                                             2m02s   1GB
Feb 21 15:44:46 Starting semantics/proofs
Feb 21 15:48:27 Finished semantics/proofs                                      3m41s   1GB
Feb 21 15:48:28 Starting semantics/alt_semantics
Feb 21 15:48:44 Finished semantics/alt_semantics                                 16s 536MB
Feb 21 15:48:44 Starting semantics/alt_semantics/proofs
Feb 21 15:51:11 Finished semantics/alt_semantics/proofs                        2m26s   1GB
Feb 21 15:51:11 Starting basis/pure
Feb 21 15:52:15 Finished basis/pure                                            1m04s 843MB
Feb 21 15:52:15 Starting translator
Feb 21 15:55:17 Finished translator                                            3m02s   1GB
Feb 21 15:55:17 Starting compiler/parsing
Feb 21 15:56:34 Finished compiler/parsing                                      1m16s   2GB
Feb 21 15:56:34 Starting characteristic
Feb 21 16:03:01 Finished characteristic                                        6m26s   1GB
Feb 21 16:03:01 Starting translator/monadic
Feb 21 16:05:01 Finished translator/monadic                                    2m00s   1GB
Feb 21 16:05:01 Starting basis
Feb 21 16:51:18 Finished basis                                                46m13s  15GB
Feb 21 16:51:18 Starting compiler/inference
Feb 21 16:52:48 Finished compiler/inference                                    1m29s   1GB
Feb 21 16:52:48 Starting compiler/backend/reg_alloc
Feb 21 16:54:32 Finished compiler/backend/reg_alloc                            1m44s   1GB
Feb 21 16:54:32 Starting compiler/backend/gc
Feb 21 16:58:53 Finished compiler/backend/gc                                   4m20s   1GB
Feb 21 16:58:53 Starting compiler/backend
Feb 21 17:04:23 Finished compiler/backend                                      5m29s   2GB
Feb 21 17:04:23 Starting compiler/encoders/asm
Feb 21 17:04:53 Finished compiler/encoders/asm                                   29s 713MB
Feb 21 17:04:53 Starting compiler/encoders/x64
Feb 21 17:06:01 Finished compiler/encoders/x64                                 1m07s 777MB
Feb 21 17:06:01 Starting compiler/encoders/arm7
Feb 21 17:08:05 Finished compiler/encoders/arm7                                2m03s   1GB
Feb 21 17:08:05 Starting compiler/encoders/arm8
Feb 21 17:08:47 Finished compiler/encoders/arm8                                  41s 619MB
Feb 21 17:08:47 Starting compiler/encoders/arm8_asl
Feb 21 19:21:35 Finished compiler/encoders/arm8_asl                         2h12m46s  33GB
Feb 21 19:21:35 Starting compiler/encoders/mips
Feb 21 19:23:07 Finished compiler/encoders/mips                                1m32s   1GB
Feb 21 19:23:08 Starting compiler/encoders/riscv
Feb 21 19:24:58 Finished compiler/encoders/riscv                               1m50s   1GB
Feb 21 19:24:58 Starting compiler/encoders/ag32
Feb 21 19:25:20 Finished compiler/encoders/ag32                                  21s 662MB
Feb 21 19:25:20 Starting compiler/backend/x64
Feb 21 19:25:42 Finished compiler/backend/x64                                    21s   1GB
Feb 21 19:25:42 Starting compiler/backend/arm7
Feb 21 19:26:05 Finished compiler/backend/arm7                                   23s   1GB
Feb 21 19:26:06 Starting compiler/backend/arm8
Feb 21 19:26:27 Finished compiler/backend/arm8                                   21s   1GB
Feb 21 19:26:27 Starting compiler/backend/mips
Feb 21 19:26:49 Finished compiler/backend/mips                                   22s   1GB
Feb 21 19:26:49 Starting compiler/backend/riscv
Feb 21 19:27:12 Finished compiler/backend/riscv                                  22s   1GB
Feb 21 19:27:12 Starting compiler/backend/ag32
Feb 21 19:28:38 Finished compiler/backend/ag32                                 1m25s   1GB
Feb 21 19:28:38 Starting compiler/parsing/proofs
Feb 21 19:32:22 Finished compiler/parsing/proofs                               3m44s   1GB
Feb 21 19:32:22 Starting compiler/inference/proofs
Feb 21 19:34:51 Finished compiler/inference/proofs                             2m29s   1GB
Feb 21 19:34:51 Starting compiler/backend/semantics
Feb 21 20:03:40 Finished compiler/backend/semantics                           28m48s   2GB
Feb 21 20:03:40 Starting compiler/backend/reg_alloc/proofs
Feb 21 20:07:13 Finished compiler/backend/reg_alloc/proofs                     3m32s   1GB
Feb 21 20:07:13 Starting compiler/backend/proofs
Feb 21 20:58:55 Finished compiler/backend/proofs                              51m41s  15GB
Feb 21 20:58:56 Starting compiler/backend/serialiser
Feb 21 21:00:34 Finished compiler/backend/serialiser                           1m38s   2GB
Feb 21 21:00:34 Starting compiler/encoders/x64/proofs
Feb 21 21:10:05 Finished compiler/encoders/x64/proofs                          9m30s   5GB
Feb 21 21:10:05 Starting compiler/encoders/arm7/proofs
Feb 21 21:23:25 Finished compiler/encoders/arm7/proofs                        13m20s   3GB
Feb 21 21:23:25 Starting compiler/encoders/arm8/proofs
Feb 21 21:30:14 Finished compiler/encoders/arm8/proofs                         6m48s   1GB
Feb 21 21:30:14 Starting compiler/encoders/arm8_asl/proofs
Feb 21 21:50:59 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/home/cug/hk324/cml-regression/cakeml-1783/compiler/encoders/arm8_asl/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A[0m
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/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/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/arm8/step[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/prog[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8_asl[0m
Scanned 40 directories
Starting work on l3_equivalenceTheory
Starting work on l3_equivalence_miscTheory
l3_equivalenceTheory                                                                                                                     examples/l3-machine-code/arm8/asl-equiv (21s)     OK
l3_equivalence_miscTheory                                                                                                                examples/l3-machine-code/arm8/asl-equiv (22s)     OK
Starting work on l3_equivalence_lemmasTheory
l3_equivalence_lemmasTheory                                                                                                              examples/l3-machine-code/arm8/asl-equiv(790s)     OK
Starting work on l3_equivalenceProofTheory
l3_equivalenceProofTheory                                                                                                                examples/l3-machine-code/arm8/asl-equiv(283s)FAIL<1>
 <<HOL warning: arm8_stepLib.arm8_decode: fallback decode>>
 Saved theorem _______ "l3_models_asl_LogicalShiftedRegister_F"
 Saved theorem _______ "l3_models_asl_LogicalShiftedRegister"
 Saved theorem _______ "l3_models_asl_BitfieldMove"
 Saved theorem _______ "l3_models_asl_Division"
 /home/cug/hk324/cml-regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript.sml:1616: error: Value or constructor (just_list_primitive_def) has not been declared in structure sail2_valuesTheory
 Found near [sail2_valuesTheory.just_list_primitive_def]
 error in quse /home/cug/hk324/cml-regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/HOL-b46e29d269344e1d2981f1c850969b4f6ff7a0ac/examples/l3-machine-code/arm8/asl-equiv/l3_equivalenceProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"