Job 1785

CakeML:2894b0315f5585f5267c0f7b6bd3b54ddb2166e1
  Attempt a minimal fix to the translator [Feb 21 22:06:09]
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 22:15:56 Claimed job
Feb 21 22:15:57 Reusing HOL
Feb 21 22:16:09 Starting developers
Feb 21 22:16:14 Finished developers                                               4s 134MB
Feb 21 22:16:14 Starting developers/bin
Feb 21 22:16:18 Finished developers/bin                                           4s 675MB
Feb 21 22:16:18 Starting semantics/ffi
Feb 21 22:16:28 Finished semantics/ffi                                            9s 231MB
Feb 21 22:16:28 Starting semantics
Feb 21 22:18:30 Finished semantics                                             2m01s   1GB
Feb 21 22:18:30 Starting semantics/proofs
Feb 21 22:22:09 Finished semantics/proofs                                      3m39s   1GB
Feb 21 22:22:09 Starting semantics/alt_semantics
Feb 21 22:22:26 Finished semantics/alt_semantics                                 16s 522MB
Feb 21 22:22:26 Starting semantics/alt_semantics/proofs
Feb 21 22:24:53 Finished semantics/alt_semantics/proofs                        2m26s 891MB
Feb 21 22:24:53 Starting basis/pure
Feb 21 22:25:55 Finished basis/pure                                            1m01s 922MB
Feb 21 22:25:55 Starting translator
Feb 21 22:28:57 Finished translator                                            3m02s   1GB
Feb 21 22:28:57 Starting compiler/parsing
Feb 21 22:30:13 Finished compiler/parsing                                      1m15s   2GB
Feb 21 22:30:13 Starting characteristic
Feb 21 22:36:36 Finished characteristic                                        6m22s   2GB
Feb 21 22:36:36 Starting translator/monadic
Feb 21 22:38:33 Finished translator/monadic                                    1m56s   1GB
Feb 21 22:38:34 Starting basis
Feb 21 23:25:44 Finished basis                                                47m09s  14GB
Feb 21 23:25:44 Starting compiler/inference
Feb 21 23:27:06 Finished compiler/inference                                    1m21s   1GB
Feb 21 23:27:06 Starting compiler/backend/reg_alloc
Feb 21 23:28:49 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 21 23:28:50 Starting compiler/backend/gc
Feb 21 23:33:09 Finished compiler/backend/gc                                   4m19s   1GB
Feb 21 23:33:09 Starting compiler/backend
Feb 21 23:38:34 Finished compiler/backend                                      5m25s   2GB
Feb 21 23:38:34 Starting compiler/encoders/asm
Feb 21 23:39:04 Finished compiler/encoders/asm                                   29s 737MB
Feb 21 23:39:04 Starting compiler/encoders/x64
Feb 21 23:39:33 Finished compiler/encoders/x64                                   28s 665MB
Feb 21 23:39:33 Starting compiler/encoders/arm7
Feb 21 23:40:28 Finished compiler/encoders/arm7                                  54s   1GB
Feb 21 23:40:28 Starting compiler/encoders/arm8
Feb 21 23:40:44 Finished compiler/encoders/arm8                                  16s 702MB
Feb 21 23:40:44 Starting compiler/encoders/arm8_asl
Feb 21 23:43:17 Finished compiler/encoders/arm8_asl                            2m32s   1GB
Feb 21 23:43:17 Starting compiler/encoders/mips
Feb 21 23:43:38 Finished compiler/encoders/mips                                  21s   1GB
Feb 21 23:43:38 Starting compiler/encoders/riscv
Feb 21 23:43:58 Finished compiler/encoders/riscv                                 19s 905MB
Feb 21 23:43:58 Starting compiler/encoders/ag32
Feb 21 23:44:20 Finished compiler/encoders/ag32                                  21s 693MB
Feb 21 23:44:20 Starting compiler/backend/x64
Feb 21 23:44:43 Finished compiler/backend/x64                                    22s   1GB
Feb 21 23:44:43 Starting compiler/backend/arm7
Feb 21 23:45:06 Finished compiler/backend/arm7                                   22s   1GB
Feb 21 23:45:06 Starting compiler/backend/arm8
Feb 21 23:45:26 Finished compiler/backend/arm8                                   20s   1GB
Feb 21 23:45:27 Starting compiler/backend/mips
Feb 21 23:45:50 Finished compiler/backend/mips                                   23s   1GB
Feb 21 23:45:50 Starting compiler/backend/riscv
Feb 21 23:46:12 Finished compiler/backend/riscv                                  22s   1GB
Feb 21 23:46:12 Starting compiler/backend/ag32
Feb 21 23:47:39 Finished compiler/backend/ag32                                 1m26s   1GB
Feb 21 23:47:39 Starting compiler/parsing/proofs
Feb 21 23:51:23 Finished compiler/parsing/proofs                               3m43s   1GB
Feb 21 23:51:23 Starting compiler/inference/proofs
Feb 21 23:53:54 Finished compiler/inference/proofs                             2m31s   1GB
Feb 21 23:53:54 Starting compiler/backend/semantics
Feb 22 00:22:12 Finished compiler/backend/semantics                           28m17s   2GB
Feb 22 00:22:12 Starting compiler/backend/reg_alloc/proofs
Feb 22 00:25:45 Finished compiler/backend/reg_alloc/proofs                     3m32s   1GB
Feb 22 00:25:46 Starting compiler/backend/proofs
Feb 22 01:17:13 Finished compiler/backend/proofs                              51m27s  17GB
Feb 22 01:17:13 Starting compiler/backend/serialiser
Feb 22 01:18:51 Finished compiler/backend/serialiser                           1m38s   2GB
Feb 22 01:18:51 Starting compiler/encoders/x64/proofs
Feb 22 01:28:27 Finished compiler/encoders/x64/proofs                          9m34s   4GB
Feb 22 01:28:27 Starting compiler/encoders/arm7/proofs
Feb 22 01:41:21 Finished compiler/encoders/arm7/proofs                        12m54s   3GB
Feb 22 01:41:22 Starting compiler/encoders/arm8/proofs
Feb 22 01:48:06 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
Feb 22 01:48:06 Starting compiler/encoders/arm8_asl/proofs
Feb 22 01:52:56 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/home/cug/hk324/cml-regression/cakeml-1785/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_equivalenceProofTheory
l3_equivalenceProofTheory                                                                                                                examples/l3-machine-code/arm8/asl-equiv(282s)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"