Job 2526

CakeML:203c506371250ec02ecfafcc5d52f705f81a9b9a
  Add --explore output for new crep_arith pass [Aug 04 08:56:37]
#1031 (talsewell:pancake_mul_to_exp)
Merging into:6eebd384c0cb34314a58957d79a6489087db8721
  Add arm8 tar.gz to artefacts [Aug 03 14:16:31]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:lammmington

Aug 05 01:34:03 Claimed job
Aug 05 01:34:07 Reusing HOL
Aug 05 01:34:17 Starting developers
Aug 05 01:34:21 Finished developers                                               2s 212MB
Aug 05 01:34:22 Starting developers/bin
Aug 05 01:34:32 Finished developers/bin                                           9s   1GB
Aug 05 01:34:33 Starting compiler/proofs
Aug 05 03:27:06 Finished compiler/proofs                                    1h52m32s  33GB
Aug 05 03:27:07 Starting compiler/bootstrap/translation
Aug 05 11:38:23 Finished compiler/bootstrap/translation                     8h11m14s  91GB
Aug 05 11:38:24 Starting semantics/ffi
Aug 05 11:38:33 Finished semantics/ffi                                            7s 657MB
Aug 05 11:38:33 Starting semantics
Aug 05 11:38:35 Finished semantics                                                0s  63MB
Aug 05 11:38:36 Starting semantics/proofs
Aug 05 11:39:13 Finished semantics/proofs                                        36s   1GB
Aug 05 11:39:14 Starting semantics/alt_semantics
Aug 05 11:39:54 Finished semantics/alt_semantics                                 39s   1GB
Aug 05 11:39:55 Starting semantics/alt_semantics/proofs
Aug 05 11:51:05 Finished semantics/alt_semantics/proofs                       11m08s   3GB
Aug 05 11:51:06 Starting basis/pure
Aug 05 11:51:07 Finished basis/pure                                               0s  71MB
Aug 05 11:51:08 Starting translator
Aug 05 11:52:57 Finished translator                                            1m48s   3GB
Aug 05 11:52:58 Starting compiler/parsing
Aug 05 11:52:59 Finished compiler/parsing                                         0s  69MB
Aug 05 11:53:00 Starting characteristic
Aug 05 11:53:02 Finished characteristic                                           0s  94MB
Aug 05 11:53:03 Starting translator/monadic
Aug 05 11:53:04 Finished translator/monadic                                       0s 102MB
Aug 05 11:53:05 Starting basis
Aug 05 11:56:42 Finished basis                                                 3m36s   6GB
Aug 05 11:56:43 Starting compiler/inference
Aug 05 11:56:45 Finished compiler/inference                                       0s 103MB
Aug 05 11:56:46 Starting compiler/backend/reg_alloc
Aug 05 11:56:47 Finished compiler/backend/reg_alloc                               0s  68MB
Aug 05 11:56:48 Starting compiler/backend/gc
Aug 05 11:56:50 Finished compiler/backend/gc                                      0s 147MB
Aug 05 11:56:51 Starting compiler/backend
Aug 05 11:57:11 Finished compiler/backend                                        19s   1GB
Aug 05 11:57:12 Starting compiler/encoders/asm
Aug 05 11:57:14 Finished compiler/encoders/asm                                    0s  91MB
Aug 05 11:57:15 Starting compiler/encoders/x64
Aug 05 11:57:16 Finished compiler/encoders/x64                                    0s 104MB
Aug 05 11:57:17 Starting compiler/encoders/arm7
Aug 05 11:57:19 Finished compiler/encoders/arm7                                   0s  99MB
Aug 05 11:57:20 Starting compiler/encoders/arm8
Aug 05 11:57:21 Finished compiler/encoders/arm8                                   0s 100MB
Aug 05 11:57:22 Starting compiler/encoders/arm8_asl
Aug 05 11:59:37 Finished compiler/encoders/arm8_asl                            2m14s   1GB
Aug 05 11:59:38 Starting compiler/encoders/mips
Aug 05 11:59:40 Finished compiler/encoders/mips                                   0s 100MB
Aug 05 11:59:40 Starting compiler/encoders/riscv
Aug 05 11:59:42 Finished compiler/encoders/riscv                                  0s  99MB
Aug 05 11:59:43 Starting compiler/encoders/ag32
Aug 05 11:59:44 Finished compiler/encoders/ag32                                   0s  91MB
Aug 05 11:59:45 Starting compiler/backend/x64
Aug 05 11:59:47 Finished compiler/backend/x64                                     0s 137MB
Aug 05 11:59:48 Starting compiler/backend/arm7
Aug 05 11:59:50 Finished compiler/backend/arm7                                    0s 139MB
Aug 05 11:59:51 Starting compiler/backend/arm8
Aug 05 11:59:52 Finished compiler/backend/arm8                                    0s 139MB
Aug 05 11:59:53 Starting compiler/backend/mips
Aug 05 11:59:55 Finished compiler/backend/mips                                    0s 139MB
Aug 05 11:59:56 Starting compiler/backend/riscv
Aug 05 11:59:58 Finished compiler/backend/riscv                                   0s 139MB
Aug 05 11:59:59 Starting compiler/backend/ag32
Aug 05 12:01:20 Finished compiler/backend/ag32                                 1m20s   3GB
Aug 05 12:01:20 Starting compiler/parsing/proofs
Aug 05 12:01:22 Finished compiler/parsing/proofs                                  0s  76MB
Aug 05 12:01:23 Starting compiler/inference/proofs
Aug 05 12:01:24 Finished compiler/inference/proofs                                0s  94MB
Aug 05 12:01:25 Starting compiler/backend/semantics
Aug 05 12:05:14 Finished compiler/backend/semantics                            3m48s   3GB
Aug 05 12:05:15 Starting compiler/backend/reg_alloc/proofs
Aug 05 12:05:17 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Aug 05 12:05:18 Starting compiler/backend/proofs
Aug 05 12:06:22 Finished compiler/backend/proofs                               1m03s   2GB
Aug 05 12:06:23 Starting compiler/backend/serialiser
Aug 05 12:06:25 Finished compiler/backend/serialiser                              0s 150MB
Aug 05 12:06:25 Starting compiler/encoders/x64/proofs
Aug 05 12:15:50 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Aug 05 12:15:51 Starting compiler/encoders/arm7/proofs
Aug 05 12:28:37 Finished compiler/encoders/arm7/proofs                        12m44s   9GB
Aug 05 12:28:38 Starting compiler/encoders/arm8/proofs
Aug 05 12:34:59 Finished compiler/encoders/arm8/proofs                         6m20s   7GB
Aug 05 12:35:00 Starting compiler/encoders/arm8_asl/proofs
Aug 05 12:49:07 Finished compiler/encoders/arm8_asl/proofs                    14m05s   4GB
Aug 05 12:49:08 Starting compiler/encoders/mips/proofs
Aug 05 12:59:13 Finished compiler/encoders/mips/proofs                        10m03s   8GB
Aug 05 12:59:13 Starting compiler/encoders/riscv/proofs
Aug 05 13:07:37 Finished compiler/encoders/riscv/proofs                        8m22s   4GB
Aug 05 13:07:38 Starting compiler/encoders/ag32/proofs
Aug 05 13:10:02 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 05 13:10:03 Starting compiler/backend/x64/proofs
Aug 05 13:10:47 Finished compiler/backend/x64/proofs                             42s   3GB
Aug 05 13:10:48 Starting compiler/backend/arm7/proofs
Aug 05 13:11:32 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 05 13:11:33 Starting compiler/backend/arm8/proofs
Aug 05 13:12:15 Finished compiler/backend/arm8/proofs                            40s   3GB
Aug 05 13:12:16 Starting compiler/backend/arm8_asl
Aug 05 13:12:46 Finished compiler/backend/arm8_asl                               28s   2GB
Aug 05 13:12:46 Starting compiler/backend/mips/proofs
Aug 05 13:13:34 Finished compiler/backend/mips/proofs                            47s   3GB
Aug 05 13:13:35 Starting compiler/backend/riscv/proofs
Aug 05 13:14:27 Finished compiler/backend/riscv/proofs                           50s   4GB
Aug 05 13:14:28 Starting compiler/backend/ag32/proofs
Aug 05 13:28:32 Finished compiler/backend/ag32/proofs                         14m02s   6GB
Aug 05 13:28:33 Starting compiler/backend/cv_compute
Aug 05 13:30:16 Finished compiler/backend/cv_compute                           1m42s   3GB
Aug 05 13:30:17 Starting cv_translator
Aug 05 13:49:53 Finished cv_translator                                        19m34s  13GB
Aug 05 13:49:54 Starting candle/set-theory
Aug 05 13:50:44 Finished candle/set-theory                                       49s   1GB
Aug 05 13:50:45 Starting candle/syntax-lib
Aug 05 13:50:46 Finished candle/syntax-lib                                        0s  71MB
Aug 05 13:50:47 Starting candle/standard/syntax
Aug 05 13:51:05 Finished candle/standard/syntax                                  16s   1GB
Aug 05 13:51:06 Starting candle/standard/semantics
Aug 05 13:53:43 Finished candle/standard/semantics                             2m36s   4GB
Aug 05 13:53:44 Starting candle/standard/monadic
Aug 05 13:53:45 Finished candle/standard/monadic                                  0s 109MB
Aug 05 13:53:46 Starting candle/standard/ml_kernel
Aug 05 13:55:44 Finished candle/standard/ml_kernel                             1m56s   6GB
Aug 05 13:55:45 Starting candle/overloading/syntax
Aug 05 13:59:20 Finished candle/overloading/syntax                             3m34s   3GB
Aug 05 13:59:21 Starting candle/overloading/semantics
Aug 05 14:11:00 Finished candle/overloading/semantics                         11m38s   6GB
Aug 05 14:11:01 Starting candle/overloading/monadic
Aug 05 14:13:41 Finished candle/overloading/monadic                            2m39s   3GB
Aug 05 14:13:42 Starting candle/overloading/ml_kernel
Aug 05 14:21:26 Finished candle/overloading/ml_kernel                          7m43s   7GB
Aug 05 14:21:27 Starting candle/overloading/ml_checker
Aug 05 14:24:05 Finished candle/overloading/ml_checker                         2m36s   7GB
Aug 05 14:24:06 Starting candle/prover
Aug 05 14:34:07 Finished candle/prover                                        10m00s   6GB
Aug 05 14:34:08 Starting pancake
Aug 05 14:35:13 Finished pancake                                               1m04s   1GB
Aug 05 14:35:14 Starting pancake/ffi
Aug 05 14:35:15 Finished pancake/ffi                                              0s  23MB
Aug 05 14:35:16 Starting pancake/semantics
Aug 05 14:37:57 Finished pancake/semantics                                     2m39s   3GB
Aug 05 14:37:58 Starting pancake/parser
Aug 05 14:38:32 Finished pancake/parser                                          33s   2GB
Aug 05 14:38:33 Starting pancake/proofs
Aug 05 14:44:51 FAILED: pancake/proofs
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/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 55 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
README.md                                                           (0s)     OK
Starting work on pan_simpProofTheory
crep_arithProofTheory                                              (20s)     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                               (28s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                (55s)     OK
loop_liveProofTheory                                               (31s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                             (90s)     OK
Starting work on loop_to_wordProofTheory
crep_to_loopProofTheory                                            (95s)     OK
pan_to_crepProofTheory                                            (154s)     OK
loop_to_wordProofTheory                                           (253s)     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                             (20s)FAIL<1>
 semantics t (lc + first_name) = semantics s start
 
 failed.
 Failed to prove theorem state_rel_imp_semantics.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 705)
 error in quse /scratch/cakeml/regression2/cakeml-2526/pancake/proofs/pan_to_wordProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /scratch/cakeml/regression2/cakeml-2526/pancake/proofs/pan_to_wordProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 705)", origin_function = "THEN1", origin_structure = "Tactical"}