Job 3137

CakeML:318dcc10fd9d50e786bed691427ee44195b5ac27
  fix pbc_normalise [Jan 14 04:00:09]
#1304 (mcandidate-fix)
Merging into:680922ba96c3158bcdb7f7becd76a1976dbcbe16
  Use mlstring in ast and related theories (#1298) [Jan 13 07:21:12]
HOL:ec2580f47550bf224fbbcb8063c4ece8e08de73c
  Sketch implementation of facility to handle script chunks [Jan 12 05:55:57]
Machine:lammmington

Jan 14 08:32:21 Claimed job
Jan 14 08:32:26 Reusing HOL
Jan 14 08:32:33 Starting developers
Jan 14 08:32:39 Finished developers                                               4s 146MB
Jan 14 08:32:39 Starting developers/bin
Jan 14 08:32:44 Finished developers/bin                                           3s  91MB
Jan 14 08:32:45 Starting misc
Jan 14 08:33:28 Finished misc                                                    42s   1GB
Jan 14 08:33:29 Starting compiler/proofs
Jan 14 09:37:10 Finished compiler/proofs                                    1h03m39s  13GB
Jan 14 09:37:11 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 14 15:46:42 Finished compiler/bootstrap/compilation/x64/64/proofs       6h09m30s 103GB
Jan 14 15:46:43 Starting semantics/ffi
Jan 14 15:46:54 Finished semantics/ffi                                           10s 531MB
Jan 14 15:46:55 Starting semantics
Jan 14 15:46:57 Finished semantics                                                1s  95MB
Jan 14 15:46:57 Starting semantics/proofs
Jan 14 15:47:21 Finished semantics/proofs                                        22s   1GB
Jan 14 15:47:22 Starting semantics/alt_semantics
Jan 14 15:47:42 Finished semantics/alt_semantics                                 19s 624MB
Jan 14 15:47:43 Starting semantics/alt_semantics/proofs
Jan 14 15:51:48 Finished semantics/alt_semantics/proofs                        4m03s   2GB
Jan 14 15:51:49 Starting basis/pure
Jan 14 15:51:51 Finished basis/pure                                               0s  91MB
Jan 14 15:51:51 Starting translator
Jan 14 15:52:55 Finished translator                                            1m03s   3GB
Jan 14 15:52:56 Starting compiler/parsing
Jan 14 15:52:58 Finished compiler/parsing                                         1s 100MB
Jan 14 15:52:59 Starting characteristic
Jan 14 15:53:01 Finished characteristic                                           1s 118MB
Jan 14 15:53:02 Starting translator/monadic
Jan 14 15:53:04 Finished translator/monadic                                       1s 124MB
Jan 14 15:53:05 Starting translator/monadic/monad_base
Jan 14 15:53:07 Finished translator/monadic/monad_base                            0s  92MB
Jan 14 15:53:08 Starting profiler
Jan 14 15:53:38 Finished profiler                                                29s   1GB
Jan 14 15:53:39 Starting basis
Jan 14 15:55:16 Finished basis                                                 1m35s   4GB
Jan 14 15:55:17 Starting compiler
Jan 14 15:55:20 Finished compiler                                                 2s 223MB
Jan 14 15:55:21 Starting compiler/inference
Jan 14 15:55:23 Finished compiler/inference                                       1s 110MB
Jan 14 15:55:24 Starting compiler/backend/reg_alloc
Jan 14 15:55:26 Finished compiler/backend/reg_alloc                               1s  92MB
Jan 14 15:55:27 Starting compiler/backend/gc
Jan 14 15:55:29 Finished compiler/backend/gc                                      1s 140MB
Jan 14 15:55:30 Starting compiler/backend
Jan 14 15:55:36 Finished compiler/backend                                         5s 287MB
Jan 14 15:55:37 Starting compiler/encoders/asm
Jan 14 15:55:39 Finished compiler/encoders/asm                                    1s 107MB
Jan 14 15:55:40 Starting compiler/encoders/x64
Jan 14 15:55:42 Finished compiler/encoders/x64                                    1s 108MB
Jan 14 15:55:43 Starting compiler/encoders/arm7
Jan 14 15:55:45 Finished compiler/encoders/arm7                                   1s 106MB
Jan 14 15:55:45 Starting compiler/encoders/arm8
Jan 14 15:55:47 Finished compiler/encoders/arm8                                   1s 107MB
Jan 14 15:55:48 Starting compiler/encoders/arm8_asl
Jan 14 17:56:00 Finished compiler/encoders/arm8_asl                         2h00m10s  43GB
Jan 14 17:56:01 Starting compiler/encoders/mips
Jan 14 17:56:03 Finished compiler/encoders/mips                                   1s 108MB
Jan 14 17:56:04 Starting compiler/encoders/riscv
Jan 14 17:56:06 Finished compiler/encoders/riscv                                  1s 107MB
Jan 14 17:56:07 Starting compiler/encoders/ag32
Jan 14 17:56:09 Finished compiler/encoders/ag32                                   1s 106MB
Jan 14 17:56:09 Starting compiler/encoders/tests
Jan 14 17:56:12 Finished compiler/encoders/tests                                  1s 126MB
Jan 14 17:56:12 Starting compiler/encoders/monadic_enc
Jan 14 17:56:34 Finished compiler/encoders/monadic_enc                           20s   1GB
Jan 14 17:56:34 Starting compiler/backend/x64
Jan 14 17:56:37 Finished compiler/backend/x64                                     1s 145MB
Jan 14 17:56:38 Starting compiler/backend/arm7
Jan 14 17:56:40 Finished compiler/backend/arm7                                    1s 141MB
Jan 14 17:56:41 Starting compiler/backend/arm8
Jan 14 17:56:43 Finished compiler/backend/arm8                                    1s 143MB
Jan 14 17:56:44 Starting compiler/backend/mips
Jan 14 17:56:46 Finished compiler/backend/mips                                    1s 143MB
Jan 14 17:56:47 Starting compiler/backend/riscv
Jan 14 17:56:50 Finished compiler/backend/riscv                                   1s 145MB
Jan 14 17:56:51 Starting compiler/backend/ag32
Jan 14 17:57:51 Finished compiler/backend/ag32                                   59s   2GB
Jan 14 17:57:52 Starting compiler/backend/pattern_matching
Jan 14 17:57:53 Finished compiler/backend/pattern_matching                        1s  88MB
Jan 14 17:57:54 Starting compiler/parsing/ocaml
Jan 14 17:59:42 Finished compiler/parsing/ocaml                                1m46s   1GB
Jan 14 17:59:43 Starting compiler/printing
Jan 14 17:59:45 Finished compiler/printing                                        1s 122MB
Jan 14 17:59:46 Starting compiler/parsing/proofs
Jan 14 17:59:48 Finished compiler/parsing/proofs                                  1s  98MB
Jan 14 17:59:49 Starting compiler/inference/proofs
Jan 14 17:59:51 Finished compiler/inference/proofs                                1s 120MB
Jan 14 17:59:52 Starting compiler/backend/semantics
Jan 14 18:02:02 Finished compiler/backend/semantics                            2m09s   2GB
Jan 14 18:02:03 Starting compiler/backend/reg_alloc/proofs
Jan 14 18:02:05 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Jan 14 18:02:06 Starting compiler/backend/proofs
Jan 14 18:02:47 Finished compiler/backend/proofs                                 40s   2GB
Jan 14 18:02:48 Starting compiler/backend/serialiser
Jan 14 18:02:50 Finished compiler/backend/serialiser                              1s 155MB
Jan 14 18:02:51 Starting compiler/encoders/x64/proofs
Jan 14 18:02:53 Finished compiler/encoders/x64/proofs                             1s 107MB
Jan 14 18:02:54 Starting compiler/encoders/arm7/proofs
Jan 14 18:13:53 Finished compiler/encoders/arm7/proofs                        10m58s  12GB
Jan 14 18:13:54 Starting compiler/encoders/arm8/proofs
Jan 14 18:20:31 Finished compiler/encoders/arm8/proofs                         6m35s   6GB
Jan 14 18:20:31 Starting compiler/encoders/arm8_asl/proofs
Jan 14 18:21:29 FAILED: compiler/encoders/arm8_asl/proofs
  HOLORIG=/scratch/cakeml/regression3/cakeml-3137/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)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
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/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(CAKEMLDIR)/basis/pure
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 48 directories
Starting work on l3_equivalenceTheory
Starting work on l3_equivalence_miscTheory
l3_equivalence_miscTheory  examples/l3-machine-code/arm8/asl-equiv (12s)FAIL<1>
 Saved theorem _______ "add_F"
 Saved theorem _______ "n2v_ADD"
 Saved theorem _______ "v2n_add"
 Saved theorem _______ "LENGTH_add_MAX"
 Saved theorem _______ "bool_list_eq"
 Proved triviality ___ "LOG_2_ADD1_lemma"
 Saved theorem _______ "LOG_2_ADD1"
 Saved theorem _______ "v2n_EVERY_T"
 Saved theorem _______ "LOG_LT"
 Saved theorem _______ "v2n_REPLICATE_F"
 Saved theorem _______ "extract_all_bits"
 Saved theorem _______ "HD_MAP"
 Saved theorem _______ "v2w_word1_eq"
 Saved theorem _______ "extract_bit"
 Saved theorem _______ "extract_bit_64"
 Saved theorem _______ "w2v_not_NIL"
 Saved theorem _______ "word_ror_alt"
 Saved theorem _______ "FLAT_REPLICATE_singleton"
 Saved theorem _______ "w2i_alt_def"
 Saved theorem _______ "word_quot_alt_def"
 Saved theorem _______ "INT_DIV_NEGL"
 Saved theorem _______ "INT_CEILING_NEG_DIV"
 Saved theorem _______ "v2w_fixwidth_dimindex"
 Saved theorem _______ "TAKE_REPLICATE"
 Saved theorem _______ "MAX_ALT_DEF"
 Saved theorem _______ "MIN_ALT_DEF"
 Saved theorem _______ "w2n_word_abs_lt"
 Saved theorem _______ "word_arith_lemma2"
 Proved triviality ___ "v2n_add_less_limit"
 Saved theorem _______ "v2n_add_v2n_not"
 Saved theorem _______ "forall_fixwidth"
 Saved theorem _______ "neg_v2n_lemma"
 Saved theorem _______ "LENGTH_add"
 Proved triviality ___ "LENGTH_ADD"
 Saved theorem _______ "LENGTH_eq_64"
 Saved theorem _______ "LENGTH_eq_128"
 Saved theorem _______ "v2w_TAKE_64_fixwidth_128"
 Saved theorem _______ "v2w_REPLICATE_F"
 Saved theorem _______ "v2w_PAD_LEFT"
 Saved theorem _______ "sw2sw_word1"
 Saved theorem _______ "v2n_w2v"
 Proof of 
 
 v2n (DROP n (w2v w)) = w2n w MOD 2 ** (dimindex (:)  n)
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactic.CONJ_TAC: Failed to prove theorem "v2n_DROP_w2v":
 
 Full log: /scratch/cakeml/regression3/HOL-ec2580f47550bf224fbbcb8063c4ece8e08de73c/examples/l3-machine-code/arm8/asl-equiv/.hol/logs/l3_equivalence_miscTheory
l3_equivalenceTheory       examples/l3-machine-code/arm8/asl-equiv (12s)MKILLED