Job 1684

CakeML:3a6994628d6d8aa2fe79d9cf4e6261345b8b3202
  Fix a strange bit of proof rot [Dec 11 21:30:20]
HOL:c51de550191d516cb9dfe47c6a1e866b232f2c96
  Remove another use of .. that causes grammar precedence problems [Dec 09 23:13:20]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 11 21:35:49 Claimed job
Dec 11 21:35:54 Reusing HOL
Dec 11 21:36:32 Starting developers
Dec 11 21:36:37 Finished developers                                               4s 100MB
Dec 11 21:36:37 Starting developers/bin
Dec 11 21:36:44 Finished developers/bin                                           6s   1GB
Dec 11 21:36:45 Starting semantics/ffi
Dec 11 21:36:53 Finished semantics/ffi                                            8s 223MB
Dec 11 21:36:53 Starting semantics
Dec 11 21:38:19 Finished semantics                                             1m25s   1GB
Dec 11 21:38:19 Starting semantics/proofs
Dec 11 21:42:07 Finished semantics/proofs                                      3m47s   1GB
Dec 11 21:42:08 Starting semantics/alt_semantics
Dec 11 21:42:19 Finished semantics/alt_semantics                                 11s 372MB
Dec 11 21:42:19 Starting semantics/alt_semantics/proofs
Dec 11 21:44:56 Finished semantics/alt_semantics/proofs                        2m35s   1GB
Dec 11 21:44:56 Starting basis/pure
Dec 11 21:45:47 Finished basis/pure                                              51s 831MB
Dec 11 21:45:47 Starting translator
Dec 11 21:48:45 Finished translator                                            2m57s   2GB
Dec 11 21:48:45 Starting compiler/parsing
Dec 11 21:50:04 Finished compiler/parsing                                      1m18s   2GB
Dec 11 21:50:04 Starting characteristic
Dec 11 21:56:01 Finished characteristic                                        5m56s   1GB
Dec 11 21:56:01 Starting translator/monadic
Dec 11 21:57:45 Finished translator/monadic                                    1m43s   1GB
Dec 11 21:57:45 Starting basis
Dec 11 22:46:18 Finished basis                                                48m32s  10GB
Dec 11 22:46:18 Starting compiler/inference
Dec 11 22:47:27 Finished compiler/inference                                    1m08s   1GB
Dec 11 22:47:27 Starting compiler/backend/reg_alloc
Dec 11 22:48:35 Finished compiler/backend/reg_alloc                            1m08s   1GB
Dec 11 22:48:36 Starting compiler/backend/gc
Dec 11 22:52:11 Finished compiler/backend/gc                                   3m34s   1GB
Dec 11 22:52:11 Starting compiler/backend
Dec 11 22:56:58 Finished compiler/backend                                      4m46s   2GB
Dec 11 22:56:58 Starting compiler/encoders/asm
Dec 11 22:57:22 Finished compiler/encoders/asm                                   23s 730MB
Dec 11 22:57:22 Starting compiler/encoders/x64
Dec 11 22:57:48 Finished compiler/encoders/x64                                   26s 985MB
Dec 11 22:57:48 Starting compiler/encoders/arm7
Dec 11 22:58:43 Finished compiler/encoders/arm7                                  53s 661MB
Dec 11 22:58:43 Starting compiler/encoders/arm8
Dec 11 22:58:57 Finished compiler/encoders/arm8                                  13s 774MB
Dec 11 22:58:57 Starting compiler/encoders/mips
Dec 11 22:59:15 Finished compiler/encoders/mips                                  17s   1GB
Dec 11 22:59:15 Starting compiler/encoders/riscv
Dec 11 22:59:32 Finished compiler/encoders/riscv                                 16s 744MB
Dec 11 22:59:32 Starting compiler/encoders/ag32
Dec 11 22:59:51 Finished compiler/encoders/ag32                                  18s 854MB
Dec 11 22:59:51 Starting compiler/backend/x64
Dec 11 23:00:10 Finished compiler/backend/x64                                    18s 930MB
Dec 11 23:00:10 Starting compiler/backend/arm7
Dec 11 23:00:33 Finished compiler/backend/arm7                                   22s   1GB
Dec 11 23:00:33 Starting compiler/backend/arm8
Dec 11 23:00:54 Finished compiler/backend/arm8                                   20s   1GB
Dec 11 23:00:54 Starting compiler/backend/mips
Dec 11 23:01:14 Finished compiler/backend/mips                                   20s   1GB
Dec 11 23:01:14 Starting compiler/backend/riscv
Dec 11 23:01:35 Finished compiler/backend/riscv                                  20s   1GB
Dec 11 23:01:35 Starting compiler/backend/ag32
Dec 11 23:02:47 Finished compiler/backend/ag32                                 1m11s   1GB
Dec 11 23:02:47 Starting compiler/parsing/proofs
Dec 11 23:06:51 Finished compiler/parsing/proofs                               4m03s   1GB
Dec 11 23:06:51 Starting compiler/inference/proofs
Dec 11 23:09:22 Finished compiler/inference/proofs                             2m31s 948MB
Dec 11 23:09:22 Starting compiler/backend/semantics
Dec 11 23:41:25 Finished compiler/backend/semantics                           32m02s   2GB
Dec 11 23:41:25 Starting compiler/backend/reg_alloc/proofs
Dec 11 23:45:11 Finished compiler/backend/reg_alloc/proofs                     3m45s   1GB
Dec 11 23:45:12 Starting compiler/backend/proofs
Dec 12 00:43:06 Finished compiler/backend/proofs                              57m52s  16GB
Dec 12 00:43:06 Starting compiler/backend/serialiser
Dec 12 00:44:20 Finished compiler/backend/serialiser                           1m13s   1GB
Dec 12 00:44:20 Starting compiler/encoders/x64/proofs
Dec 12 00:54:38 Finished compiler/encoders/x64/proofs                         10m18s   5GB
Dec 12 00:54:39 Starting compiler/encoders/arm7/proofs
Dec 12 01:08:52 Finished compiler/encoders/arm7/proofs                        14m13s   3GB
Dec 12 01:08:53 Starting compiler/encoders/arm8/proofs
Dec 12 01:16:09 Finished compiler/encoders/arm8/proofs                         7m16s   1GB
Dec 12 01:16:09 Starting compiler/encoders/mips/proofs
Dec 12 01:26:49 Finished compiler/encoders/mips/proofs                        10m39s   2GB
Dec 12 01:26:49 Starting compiler/encoders/riscv/proofs
Dec 12 01:36:17 Finished compiler/encoders/riscv/proofs                        9m27s   1GB
Dec 12 01:36:17 Starting compiler/encoders/ag32/proofs
Dec 12 01:39:03 Finished compiler/encoders/ag32/proofs                         2m45s 687MB
Dec 12 01:39:03 Starting compiler/backend/x64/proofs
Dec 12 01:39:26 Finished compiler/backend/x64/proofs                             22s   1GB
Dec 12 01:39:26 Starting compiler/backend/arm7/proofs
Dec 12 01:39:50 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 12 01:39:51 Starting compiler/backend/arm8/proofs
Dec 12 01:40:15 Finished compiler/backend/arm8/proofs                            23s   1GB
Dec 12 01:40:15 Starting compiler/backend/mips/proofs
Dec 12 01:40:40 Finished compiler/backend/mips/proofs                            25s   1GB
Dec 12 01:40:40 Starting compiler/backend/riscv/proofs
Dec 12 01:41:04 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 12 01:41:05 Starting compiler/backend/ag32/proofs
Dec 12 01:54:31 Finished compiler/backend/ag32/proofs                         13m26s   2GB
Dec 12 01:54:31 Starting compiler/proofs
Dec 12 01:56:34 Finished compiler/proofs                                       2m01s   3GB
Dec 12 01:56:34 Starting candle/set-theory
Dec 12 01:57:03 Finished candle/set-theory                                       28s 682MB
Dec 12 01:57:03 Starting candle/syntax-lib
Dec 12 01:57:14 Finished candle/syntax-lib                                       10s 637MB
Dec 12 01:57:14 Starting candle/standard/syntax
Dec 12 01:59:06 Finished candle/standard/syntax                                1m51s 881MB
Dec 12 01:59:06 Starting candle/standard/semantics
Dec 12 02:00:52 Finished candle/standard/semantics                             1m46s   1GB
Dec 12 02:00:53 Starting candle/standard/monadic
Dec 12 02:02:40 Finished candle/standard/monadic                               1m47s   1GB
Dec 12 02:02:40 Starting candle/standard/ml_kernel
Dec 12 02:08:33 Finished candle/standard/ml_kernel                             5m52s   2GB
Dec 12 02:08:33 Starting candle/overloading/syntax
Dec 12 02:11:47 Finished candle/overloading/syntax                             3m13s   1GB
Dec 12 02:11:47 Starting candle/overloading/semantics
Dec 12 02:24:03 Finished candle/overloading/semantics                         12m15s   2GB
Dec 12 02:24:03 Starting pancake
Dec 12 02:26:01 Finished pancake                                               1m57s   2GB
Dec 12 02:26:02 Starting pancake/ffi
Dec 12 02:26:02 Finished pancake/ffi                                              0s   5MB
Dec 12 02:26:03 Starting pancake/semantics
Dec 12 02:28:31 Finished pancake/semantics                                     2m28s   1GB
Dec 12 02:28:32 Starting pancake/proofs
Dec 12 02:31:06 FAILED: pancake/proofs
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)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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/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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/pancake/semantics
Starting work on README.md
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
Starting work on pan_simpProofTheory
README.md                                                           (0s)     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                               (22s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                (35s)     OK
Starting work on time_to_panProofTheory
loop_liveProofTheory                                               (23s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                             (87s)     OK
Starting work on loop_to_wordProofTheory
pan_to_crepProofTheory                                            (115s)     OK
time_to_panProofTheory                                            (113s)FAIL<1>
      (SOME (Exception panic (ValWord 0w)),empty_locals t)) 
     n. e = SOME n  lbl = LPanic (PanicInput n)  n + 1 < dimword (:) 
         FLOOKUP t.locals event = SOME (ValWord (n2w (n + 1))) 
         FLOOKUP t.eshapes panic = SOME One 
         evaluate (compTerms clks clks event tms,t) =
         (SOME (Exception panic (ValWord 0w)),empty_locals t)
 
 failed.
 Failed to prove theorem pick_term_thm.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 2926) (THEN1 on line 2936) (THEN1 on line 2938) (THEN1 on line 2946) (THEN1 on line 2956) (THEN1 on line 2914) (THEN1 on line 2961) (THEN1 on line 2996) (THEN1 on line 3127) (THEN1 on line 3349) (THEN1 on line 3442)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
crep_to_loopProofTheory                                           (102s)MKILLED
loop_to_wordProofTheory                                            (62s)MKILLED