Job 1894

CakeML:78cfcc3394380b58e965139b8b51f3f0e091b082
  extend concrete_v_def [May 09 08:02:58]
#865 (Iced_cake)
Merging into:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma [May 09 03:44:38]
HOL:66b3a9840d7383e92b62bfdb206f6012f4161e6f
  Add new [simp] theorem to indexedLists: MAPi ( [May 06 03:53:57]
Machine:oven3

May 09 08:04:46 Claimed job
May 09 08:04:54 Building HOL
May 09 08:25:27 Starting developers
May 09 08:25:36 Finished developers                                               9s 146MB
May 09 08:25:37 Starting developers/bin
May 09 08:25:49 Finished developers/bin                                          12s   1GB
May 09 08:25:50 Starting semantics/ffi
May 09 08:26:13 Finished semantics/ffi                                           23s 294MB
May 09 08:26:14 Starting semantics
May 09 08:31:38 Finished semantics                                             5m23s   1GB
May 09 08:31:38 Starting semantics/proofs
May 09 08:47:28 Finished semantics/proofs                                     15m49s   1GB
May 09 08:47:28 Starting semantics/alt_semantics
May 09 08:48:28 Finished semantics/alt_semantics                                 59s 530MB
May 09 08:48:28 Starting semantics/alt_semantics/proofs
May 09 09:13:53 Finished semantics/alt_semantics/proofs                       25m24s   1GB
May 09 09:13:53 Starting basis/pure
May 09 09:21:24 Finished basis/pure                                            7m30s 971MB
May 09 09:21:24 Starting translator
May 09 09:29:12 Finished translator                                            7m47s   1GB
May 09 09:29:12 Starting compiler/parsing
May 09 09:32:14 Finished compiler/parsing                                      3m01s   4GB
May 09 09:32:14 Starting characteristic
May 09 09:46:51 Finished characteristic                                       14m36s   2GB
May 09 09:46:51 Starting translator/monadic
May 09 09:51:08 Finished translator/monadic                                    4m16s   1GB
May 09 09:51:08 Starting basis
May 09 11:44:42 Finished basis                                              1h53m33s  25GB
May 09 11:44:42 Starting compiler/inference
May 09 11:48:05 Finished compiler/inference                                    3m23s   1GB
May 09 11:48:06 Starting compiler/backend/reg_alloc
May 09 11:51:20 Finished compiler/backend/reg_alloc                            3m13s   2GB
May 09 11:51:20 Starting compiler/backend/gc
May 09 11:59:43 Finished compiler/backend/gc                                   8m23s   2GB
May 09 11:59:44 Starting compiler/backend
May 09 12:11:09 Finished compiler/backend                                     11m25s   3GB
May 09 12:11:10 Starting compiler/encoders/asm
May 09 12:12:15 Finished compiler/encoders/asm                                 1m04s 670MB
May 09 12:12:15 Starting compiler/encoders/x64
May 09 12:14:46 Finished compiler/encoders/x64                                 2m30s   1GB
May 09 12:14:47 Starting compiler/encoders/arm7
May 09 12:19:27 Finished compiler/encoders/arm7                                4m40s   1GB
May 09 12:19:27 Starting compiler/encoders/arm8
May 09 12:21:03 Finished compiler/encoders/arm8                                1m35s   1GB
May 09 12:21:03 Starting compiler/encoders/arm8_asl
May 09 16:38:46 Finished compiler/encoders/arm8_asl                         4h17m43s  33GB
May 09 16:38:47 Starting compiler/encoders/mips
May 09 16:42:10 Finished compiler/encoders/mips                                3m22s   1GB
May 09 16:42:10 Starting compiler/encoders/riscv
May 09 16:46:07 Finished compiler/encoders/riscv                               3m57s 869MB
May 09 16:46:07 Starting compiler/encoders/ag32
May 09 16:46:55 Finished compiler/encoders/ag32                                  47s 920MB
May 09 16:46:55 Starting compiler/backend/x64
May 09 16:47:44 Finished compiler/backend/x64                                    48s   1GB
May 09 16:47:44 Starting compiler/backend/arm7
May 09 16:48:40 Finished compiler/backend/arm7                                   55s   1GB
May 09 16:48:40 Starting compiler/backend/arm8
May 09 16:49:28 Finished compiler/backend/arm8                                   47s   1GB
May 09 16:49:29 Starting compiler/backend/mips
May 09 16:50:20 Finished compiler/backend/mips                                   50s   1GB
May 09 16:50:20 Starting compiler/backend/riscv
May 09 16:51:06 Finished compiler/backend/riscv                                  46s   1GB
May 09 16:51:07 Starting compiler/backend/ag32
May 09 16:54:03 Finished compiler/backend/ag32                                 2m55s   1GB
May 09 16:54:03 Starting compiler/parsing/proofs
May 09 17:02:36 Finished compiler/parsing/proofs                               8m32s   1GB
May 09 17:02:36 Starting compiler/inference/proofs
May 09 17:08:34 Finished compiler/inference/proofs                             5m57s   1GB
May 09 17:08:34 Starting compiler/backend/semantics
May 09 18:18:54 Finished compiler/backend/semantics                         1h10m18s   2GB
May 09 18:18:54 Starting compiler/backend/reg_alloc/proofs
May 09 18:26:43 Finished compiler/backend/reg_alloc/proofs                     7m49s   1GB
May 09 18:26:44 Starting compiler/backend/proofs
May 09 20:15:42 Finished compiler/backend/proofs                            1h48m58s  18GB
May 09 20:15:42 Starting compiler/backend/serialiser
May 09 20:19:05 Finished compiler/backend/serialiser                           3m22s   2GB
May 09 20:19:05 Starting compiler/encoders/x64/proofs
May 09 20:40:29 Finished compiler/encoders/x64/proofs                         21m23s   5GB
May 09 20:40:29 Starting compiler/encoders/arm7/proofs
May 09 21:10:06 Finished compiler/encoders/arm7/proofs                        29m36s   5GB
May 09 21:10:06 Starting compiler/encoders/arm8/proofs
May 09 21:25:43 Finished compiler/encoders/arm8/proofs                        15m35s   1GB
May 09 21:25:43 Starting compiler/encoders/arm8_asl/proofs
May 09 21:32:48 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/root/regression/cakeml-1894/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_equivalence_miscTheory                                                                                                                                    examples/l3-machine-code/arm8/asl-equiv (14s)FAIL<1>
 No matching sub-term found
 error in quse /root/regression/HOL-66b3a9840d7383e92b62bfdb206f6012f4161e6f/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_miscScript.sml : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 error in load /root/regression/HOL-66b3a9840d7383e92b62bfdb206f6012f4161e6f/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_miscScript : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 Proof of 
 
 w. w2n (word_abs w)  2 ** (dimindex (:)  1)
 
 failed.
 Failed to prove theorem w2n_word_abs_lt.
 Uncaught exception: HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
l3_equivalenceTheory                                                                                                                                         examples/l3-machine-code/arm8/asl-equiv (14s)MKILLED