CakeML Regression Test

Job 2152

CakeML:135219d1574381e477d599e8aec119e9d6e1e638
  Fix for proof broken by changes in HOL master [Jun 15 11:45:28]
HOL:106c414d7a58f852a56165b10cd1665f04dddfbf
  Get emacs-mode to handle Proof-attributes when goals are started [Jun 15 12:32:21]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jun 17 08:17:21 Claimed job
Jun 17 08:17:26 Building HOL
Jun 17 08:29:50 Starting developers
Jun 17 08:29:55 Finished developers                                               5s 150MB
Jun 17 08:29:55 Starting developers/bin
Jun 17 08:30:02 Finished developers/bin                                           6s   1GB
Jun 17 08:30:02 Starting compiler/proofs
Jun 17 10:23:18 Finished compiler/proofs                                    1h53m12s  17GB
Jun 17 10:23:19 Starting compiler/bootstrap/translation
Jun 17 18:26:04 Finished compiler/bootstrap/translation                     8h02m43s  39GB
Jun 17 18:26:04 Starting semantics/ffi
Jun 17 18:26:10 Finished semantics/ffi                                            5s 218MB
Jun 17 18:26:10 Starting semantics
Jun 17 18:26:12 Finished semantics                                                1s  18MB
Jun 17 18:26:12 Starting semantics/proofs
Jun 17 18:26:46 Finished semantics/proofs                                        34s   1GB
Jun 17 18:26:46 Starting semantics/alt_semantics
Jun 17 18:27:17 Finished semantics/alt_semantics                                 31s 707MB
Jun 17 18:27:18 Starting semantics/alt_semantics/proofs
Jun 17 18:39:03 Finished semantics/alt_semantics/proofs                       11m45s   1GB
Jun 17 18:39:04 Starting basis/pure
Jun 17 18:39:05 Finished basis/pure                                               1s  22MB
Jun 17 18:39:05 Starting translator
Jun 17 18:40:54 Finished translator                                            1m49s   1GB
Jun 17 18:40:55 Starting compiler/parsing
Jun 17 18:40:56 Finished compiler/parsing                                         1s  22MB
Jun 17 18:40:56 Starting characteristic
Jun 17 18:40:58 Finished characteristic                                           1s  19MB
Jun 17 18:40:58 Starting translator/monadic
Jun 17 18:41:00 Finished translator/monadic                                       1s  27MB
Jun 17 18:41:00 Starting basis
Jun 17 18:45:02 Finished basis                                                 4m01s   2GB
Jun 17 18:45:02 Starting compiler/inference
Jun 17 18:45:04 Finished compiler/inference                                       1s  20MB
Jun 17 18:45:04 Starting compiler/backend/reg_alloc
Jun 17 18:45:05 Finished compiler/backend/reg_alloc                               1s  20MB
Jun 17 18:45:05 Starting compiler/backend/gc
Jun 17 18:45:08 Finished compiler/backend/gc                                      2s  27MB
Jun 17 18:45:08 Starting compiler/backend
Jun 17 18:45:20 Finished compiler/backend                                        11s 630MB
Jun 17 18:45:20 Starting compiler/encoders/asm
Jun 17 18:45:22 Finished compiler/encoders/asm                                    1s  22MB
Jun 17 18:45:22 Starting compiler/encoders/x64
Jun 17 18:45:24 Finished compiler/encoders/x64                                    1s  20MB
Jun 17 18:45:24 Starting compiler/encoders/arm7
Jun 17 18:45:26 Finished compiler/encoders/arm7                                   1s  27MB
Jun 17 18:45:26 Starting compiler/encoders/arm8
Jun 17 18:45:27 Finished compiler/encoders/arm8                                   1s  24MB
Jun 17 18:45:28 Starting compiler/encoders/arm8_asl
Jun 17 21:08:50 Finished compiler/encoders/arm8_asl                         2h23m21s  34GB
Jun 17 21:08:50 Starting compiler/encoders/mips
Jun 17 21:08:52 Finished compiler/encoders/mips                                   1s  21MB
Jun 17 21:08:52 Starting compiler/encoders/riscv
Jun 17 21:08:54 Finished compiler/encoders/riscv                                  1s  23MB
Jun 17 21:08:54 Starting compiler/encoders/ag32
Jun 17 21:08:55 Finished compiler/encoders/ag32                                   1s  23MB
Jun 17 21:08:56 Starting compiler/backend/x64
Jun 17 21:08:58 Finished compiler/backend/x64                                     2s  28MB
Jun 17 21:08:58 Starting compiler/backend/arm7
Jun 17 21:09:00 Finished compiler/backend/arm7                                    2s  22MB
Jun 17 21:09:00 Starting compiler/backend/arm8
Jun 17 21:09:02 Finished compiler/backend/arm8                                    2s  24MB
Jun 17 21:09:03 Starting compiler/backend/mips
Jun 17 21:09:05 Finished compiler/backend/mips                                    2s  26MB
Jun 17 21:09:05 Starting compiler/backend/riscv
Jun 17 21:09:07 Finished compiler/backend/riscv                                   2s  25MB
Jun 17 21:09:07 Starting compiler/backend/ag32
Jun 17 21:10:35 Finished compiler/backend/ag32                                 1m27s   1GB
Jun 17 21:10:35 Starting compiler/parsing/proofs
Jun 17 21:10:36 Finished compiler/parsing/proofs                                  1s  26MB
Jun 17 21:10:37 Starting compiler/inference/proofs
Jun 17 21:10:38 Finished compiler/inference/proofs                                1s  20MB
Jun 17 21:10:39 Starting compiler/backend/semantics
Jun 17 21:11:50 Finished compiler/backend/semantics                            1m11s   1GB
Jun 17 21:11:50 Starting compiler/backend/reg_alloc/proofs
Jun 17 21:11:52 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Jun 17 21:11:53 Starting compiler/backend/proofs
Jun 17 21:12:53 Finished compiler/backend/proofs                                 59s   3GB
Jun 17 21:12:53 Starting compiler/backend/serialiser
Jun 17 21:12:56 Finished compiler/backend/serialiser                              2s  29MB
Jun 17 21:12:56 Starting compiler/encoders/x64/proofs
Jun 17 21:22:46 Finished compiler/encoders/x64/proofs                          9m50s   4GB
Jun 17 21:22:47 Starting compiler/encoders/arm7/proofs
Jun 17 21:36:31 Finished compiler/encoders/arm7/proofs                        13m44s   3GB
Jun 17 21:36:31 Starting compiler/encoders/arm8/proofs
Jun 17 21:43:27 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Jun 17 21:43:28 Starting compiler/encoders/arm8_asl/proofs
Jun 17 21:46:27 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/home/cug/hk324/cml-regression/cakeml-2152/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/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/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  (4s)FAIL<1>
 No var with name "x" free in goal, or in outer universal quantifiers
 error in quse /home/cug/hk324/cml-regression/HOL-106c414d7a58f852a56165b10cd1665f04dddfbf/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_miscScript.sml : HOL_ERR {message = "at BasicProvers.find_subterm:\nNo var with name \"x\" free in goal, or in outer universal quantifiers", origin_function = "Cases_on", origin_structure = "BasicProvers"}
 error in load /home/cug/hk324/cml-regression/HOL-106c414d7a58f852a56165b10cd1665f04dddfbf/examples/l3-machine-code/arm8/asl-equiv/l3_equivalence_miscScript : HOL_ERR {message = "at BasicProvers.find_subterm:\nNo var with name \"x\" free in goal, or in outer universal quantifiers", origin_function = "Cases_on", origin_structure = "BasicProvers"}
 Proof of 
 
 i w. i < dimindex (:)  (i >< i) w = v2w [word_bit i w]
 
 failed.
 Failed to prove theorem extract_bit.
 Uncaught exception: HOL_ERR {message = "at BasicProvers.find_subterm:\nNo var with name \"x\" free in goal, or in outer universal quantifiers", origin_function = "Cases_on", origin_structure = "BasicProvers"}
l3_equivalenceTheory                                                                                                                   examples/l3-machine-code/arm8/asl-equiv  (4s)MKILLED