Job 1893

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 09 04:03:53 Claimed job
May 09 04:03:57 Building HOL
May 09 04:14:37 Starting developers
May 09 04:14:42 Finished developers                                               4s 123MB
May 09 04:14:42 Starting developers/bin
May 09 04:14:49 Finished developers/bin                                           6s   1GB
May 09 04:14:49 Starting semantics/ffi
May 09 04:15:00 Finished semantics/ffi                                           10s 214MB
May 09 04:15:00 Starting semantics
May 09 04:17:18 Finished semantics                                             2m17s   1GB
May 09 04:17:18 Starting semantics/proofs
May 09 04:21:51 Finished semantics/proofs                                      4m32s   4GB
May 09 04:21:51 Starting semantics/alt_semantics
May 09 04:22:17 Finished semantics/alt_semantics                                 25s 479MB
May 09 04:22:17 Starting semantics/alt_semantics/proofs
May 09 04:25:31 Finished semantics/alt_semantics/proofs                        3m14s   1GB
May 09 04:25:32 Starting basis/pure
May 09 04:29:23 Finished basis/pure                                            3m51s 921MB
May 09 04:29:24 Starting translator
May 09 04:32:38 Finished translator                                            3m14s   1GB
May 09 04:32:39 Starting compiler/parsing
May 09 04:34:02 Finished compiler/parsing                                      1m23s   2GB
May 09 04:34:02 Starting characteristic
May 09 04:40:44 Finished characteristic                                        6m41s   1GB
May 09 04:40:45 Starting translator/monadic
May 09 04:42:46 Finished translator/monadic                                    2m01s   1GB
May 09 04:42:46 Starting basis
May 09 05:33:34 Finished basis                                                50m47s  16GB
May 09 05:33:35 Starting compiler/inference
May 09 05:35:08 Finished compiler/inference                                    1m33s   1GB
May 09 05:35:09 Starting compiler/backend/reg_alloc
May 09 05:36:58 Finished compiler/backend/reg_alloc                            1m48s   1GB
May 09 05:36:58 Starting compiler/backend/gc
May 09 05:41:44 Finished compiler/backend/gc                                   4m46s   1GB
May 09 05:41:45 Starting compiler/backend
May 09 05:47:46 Finished compiler/backend                                      6m01s   2GB
May 09 05:47:47 Starting compiler/encoders/asm
May 09 05:48:19 Finished compiler/encoders/asm                                   31s 707MB
May 09 05:48:19 Starting compiler/encoders/x64
May 09 05:49:32 Finished compiler/encoders/x64                                 1m13s   1GB
May 09 05:49:33 Starting compiler/encoders/arm7
May 09 05:51:53 Finished compiler/encoders/arm7                                2m20s   1GB
May 09 05:51:53 Starting compiler/encoders/arm8
May 09 05:52:38 Finished compiler/encoders/arm8                                  44s   1GB
May 09 05:52:38 Starting compiler/encoders/arm8_asl
May 09 08:22:20 Finished compiler/encoders/arm8_asl                         2h29m41s  38GB
May 09 08:22:20 Starting compiler/encoders/mips
May 09 08:24:05 Finished compiler/encoders/mips                                1m44s   1GB
May 09 08:24:05 Starting compiler/encoders/riscv
May 09 08:26:04 Finished compiler/encoders/riscv                               1m58s   1GB
May 09 08:26:05 Starting compiler/encoders/ag32
May 09 08:26:28 Finished compiler/encoders/ag32                                  23s 815MB
May 09 08:26:28 Starting compiler/backend/x64
May 09 08:26:51 Finished compiler/backend/x64                                    22s   1GB
May 09 08:26:52 Starting compiler/backend/arm7
May 09 08:27:16 Finished compiler/backend/arm7                                   23s   1GB
May 09 08:27:16 Starting compiler/backend/arm8
May 09 08:27:39 Finished compiler/backend/arm8                                   23s   1GB
May 09 08:27:40 Starting compiler/backend/mips
May 09 08:28:04 Finished compiler/backend/mips                                   24s   1GB
May 09 08:28:04 Starting compiler/backend/riscv
May 09 08:28:29 Finished compiler/backend/riscv                                  24s   1GB
May 09 08:28:29 Starting compiler/backend/ag32
May 09 08:30:00 Finished compiler/backend/ag32                                 1m31s   1GB
May 09 08:30:01 Starting compiler/parsing/proofs
May 09 08:34:04 Finished compiler/parsing/proofs                               4m03s   1GB
May 09 08:34:05 Starting compiler/inference/proofs
May 09 08:36:47 Finished compiler/inference/proofs                             2m42s   1GB
May 09 08:36:48 Starting compiler/backend/semantics
May 09 09:10:09 Finished compiler/backend/semantics                           33m20s   2GB
May 09 09:10:09 Starting compiler/backend/reg_alloc/proofs
May 09 09:14:06 Finished compiler/backend/reg_alloc/proofs                     3m56s   1GB
May 09 09:14:06 Starting compiler/backend/proofs
May 09 10:11:21 Finished compiler/backend/proofs                              57m13s  13GB
May 09 10:11:21 Starting compiler/backend/serialiser
May 09 10:13:05 Finished compiler/backend/serialiser                           1m43s   1GB
May 09 10:13:05 Starting compiler/encoders/x64/proofs
May 09 10:23:21 Finished compiler/encoders/x64/proofs                         10m15s   5GB
May 09 10:23:21 Starting compiler/encoders/arm7/proofs
May 09 10:37:25 Finished compiler/encoders/arm7/proofs                        14m03s   3GB
May 09 10:37:25 Starting compiler/encoders/arm8/proofs
May 09 10:44:43 Finished compiler/encoders/arm8/proofs                         7m18s   1GB
May 09 10:44:44 Starting compiler/encoders/arm8_asl/proofs
May 09 10:47:31 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/home/cake/oven/regression/cakeml-1893/compiler/encoders/arm8_asl/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanned 40 directories
Starting work on l3_equivalenceTheory
Starting work on l3_equivalence_miscTheory
l3_equivalence_miscTheory  examples/l3-machine-code/arm8/asl-equiv  (5s)FAIL<1>
 No matching sub-term found
 error in quse /home/cake/oven/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 /home/cake/oven/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  (5s)MKILLED