Job 2358

CakeML:77aba466f2652250e9b3dd44c55db74bdab6d392
  Add parameters to the scope-checker [Mar 27 13:07:18]
HOL:e546764f153c268543103c60ed61bd9941768e05
  Speedup examples/probability building process [Mar 21 22:39:36]
Machine:lammmington

Mar 27 13:11:44 Claimed job
Mar 27 13:11:48 Reusing HOL
Mar 27 13:11:58 Starting developers
Mar 27 13:12:01 Finished developers                                               2s 220MB
Mar 27 13:12:02 Starting developers/bin
Mar 27 13:12:13 Finished developers/bin                                           9s   1GB
Mar 27 13:12:14 Starting compiler/proofs
Mar 27 15:01:07 Finished compiler/proofs                                    1h48m52s  53GB
Mar 27 15:01:08 Starting compiler/bootstrap/translation
Mar 27 22:55:59 Finished compiler/bootstrap/translation                     7h54m49s  77GB
Mar 27 22:56:00 Starting semantics/ffi
Mar 27 22:56:08 Finished semantics/ffi                                            7s 721MB
Mar 27 22:56:09 Starting semantics
Mar 27 22:56:10 Finished semantics                                                0s  62MB
Mar 27 22:56:11 Starting semantics/proofs
Mar 27 22:56:48 Finished semantics/proofs                                        36s   1GB
Mar 27 22:56:49 Starting semantics/alt_semantics
Mar 27 22:57:28 Finished semantics/alt_semantics                                 37s   1GB
Mar 27 22:57:29 Starting semantics/alt_semantics/proofs
Mar 27 23:08:23 Finished semantics/alt_semantics/proofs                       10m53s   3GB
Mar 27 23:08:24 Starting basis/pure
Mar 27 23:08:25 Finished basis/pure                                               0s  68MB
Mar 27 23:08:26 Starting translator
Mar 27 23:10:13 Finished translator                                            1m45s   3GB
Mar 27 23:10:13 Starting compiler/parsing
Mar 27 23:10:15 Finished compiler/parsing                                         0s  72MB
Mar 27 23:10:16 Starting characteristic
Mar 27 23:10:17 Finished characteristic                                           0s  88MB
Mar 27 23:10:18 Starting translator/monadic
Mar 27 23:10:20 Finished translator/monadic                                       0s  90MB
Mar 27 23:10:21 Starting basis
Mar 27 23:13:58 Finished basis                                                 3m36s   9GB
Mar 27 23:13:59 Starting compiler/inference
Mar 27 23:14:01 Finished compiler/inference                                       0s  83MB
Mar 27 23:14:02 Starting compiler/backend/reg_alloc
Mar 27 23:14:03 Finished compiler/backend/reg_alloc                               0s  65MB
Mar 27 23:14:04 Starting compiler/backend/gc
Mar 27 23:14:06 Finished compiler/backend/gc                                      0s 133MB
Mar 27 23:14:06 Starting compiler/backend
Mar 27 23:14:24 Finished compiler/backend                                        16s   1GB
Mar 27 23:14:25 Starting compiler/encoders/asm
Mar 27 23:14:26 Finished compiler/encoders/asm                                    0s  92MB
Mar 27 23:14:27 Starting compiler/encoders/x64
Mar 27 23:14:29 Finished compiler/encoders/x64                                    0s  98MB
Mar 27 23:14:30 Starting compiler/encoders/arm7
Mar 27 23:14:31 Finished compiler/encoders/arm7                                   0s  93MB
Mar 27 23:14:32 Starting compiler/encoders/arm8
Mar 27 23:14:33 Finished compiler/encoders/arm8                                   0s  93MB
Mar 27 23:14:34 Starting compiler/encoders/arm8_asl
Mar 27 23:15:08 FAILED: compiler/encoders/arm8_asl
  HOLORIG=/scratch/cakeml/regression2/cakeml-2358/compiler/encoders/arm8_asl [ -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)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[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/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/rational[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/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
Scanned 36 directories
Starting work on sail2_operatorsTheory
Starting work on sail2_state_monadTheory
Starting work on sail2_valuesAuxiliaryTheory
sail2_valuesAuxiliaryTheory ...-asl-snapshot/A64_ISA_v86A/lib/sail (23s)FAIL<1>
 Saved theorem _______ "pad_list_rw"
 Saved theorem _______ "pad_list_ind_rw"
 Saved theorem _______ "reverse_endianness_list_rw"
 Saved theorem _______ "reverse_endianness_list_ind_rw"
 
 Exception raised at IntDP_Munge.COOPER_CONV:
 Tried to prove generalised goal (generalising to...) but it was false
 error in quse /scratch/cakeml/regression2/HOL-e546764f153c268543103c60ed61bd9941768e05/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail/sail2_valuesAuxiliaryScript.sml : HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
 error in load /scratch/cakeml/regression2/HOL-e546764f153c268543103c60ed61bd9941768e05/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail/sail2_valuesAuxiliaryScript : HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
 Uncaught exception: HOL_ERR {message = "at IntDP_Munge.COOPER_CONV:\nTried to prove generalised goal (generalising to...) but it was false", origin_function = "tprove", origin_structure = "Defn"}
sail2_operatorsTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/sail (24s)MKILLED
sail2_state_monadTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/sail (24s)MKILLED