Job 1861

CakeML:80dbdc408d661d56e349acf8aed8ea42fe20e2e2
  Add CF specs for Array.appi [Apr 12 09:06:24]
#878 (array-appi-fix)
Merging into:746be7b61665e6297b7ce29f70b74eec6efc7a79
  Merge pull request #873 from CakeML/issue871 [Apr 08 11:13:44]
HOL:3b1931c130fcab243da332adb2c1413c42c59cf9
  Escape # in TeX output [Apr 12 23:45:24]
Machine:oven3

Apr 16 01:34:10 Claimed job
Apr 16 01:34:18 Building HOL
Apr 16 01:54:32 Starting developers
Apr 16 01:54:41 Finished developers                                               9s 165MB
Apr 16 01:54:42 Starting developers/bin
Apr 16 01:55:02 Finished developers/bin                                          20s   1GB
Apr 16 01:55:03 Starting semantics/ffi
Apr 16 01:55:27 Finished semantics/ffi                                           24s 258MB
Apr 16 01:55:28 Starting semantics
Apr 16 01:59:53 Finished semantics                                             4m24s   1GB
Apr 16 01:59:53 Starting semantics/proofs
Apr 16 02:08:46 Finished semantics/proofs                                      8m53s   2GB
Apr 16 02:08:47 Starting semantics/alt_semantics
Apr 16 02:09:40 Finished semantics/alt_semantics                                 52s 472MB
Apr 16 02:09:40 Starting semantics/alt_semantics/proofs
Apr 16 02:16:17 Finished semantics/alt_semantics/proofs                        6m37s   1GB
Apr 16 02:16:17 Starting basis/pure
Apr 16 02:22:53 Finished basis/pure                                            6m35s   1GB
Apr 16 02:22:53 Starting translator
Apr 16 02:29:10 Finished translator                                            6m16s   1GB
Apr 16 02:29:10 Starting compiler/parsing
Apr 16 02:31:59 Finished compiler/parsing                                      2m48s   2GB
Apr 16 02:31:59 Starting characteristic
Apr 16 02:45:30 Finished characteristic                                       13m30s   2GB
Apr 16 02:45:30 Starting translator/monadic
Apr 16 02:49:29 Finished translator/monadic                                    3m58s   1GB
Apr 16 02:49:29 Starting basis
Apr 16 04:32:22 Finished basis                                              1h42m50s  13GB
Apr 16 04:32:22 Starting compiler/inference
Apr 16 04:35:30 Finished compiler/inference                                    3m07s   1GB
Apr 16 04:35:30 Starting compiler/backend/reg_alloc
Apr 16 04:38:41 Finished compiler/backend/reg_alloc                            3m10s   1GB
Apr 16 04:38:41 Starting compiler/backend/gc
Apr 16 04:47:07 Finished compiler/backend/gc                                   8m25s   2GB
Apr 16 04:47:07 Starting compiler/backend
Apr 16 04:57:53 Finished compiler/backend                                     10m45s   1GB
Apr 16 04:57:53 Starting compiler/encoders/asm
Apr 16 04:58:57 Finished compiler/encoders/asm                                 1m03s 677MB
Apr 16 04:58:57 Starting compiler/encoders/x64
Apr 16 05:01:28 Finished compiler/encoders/x64                                 2m30s   1GB
Apr 16 05:01:28 Starting compiler/encoders/arm7
Apr 16 05:06:15 Finished compiler/encoders/arm7                                4m47s   1GB
Apr 16 05:06:16 Starting compiler/encoders/arm8
Apr 16 05:07:54 Finished compiler/encoders/arm8                                1m38s 896MB
Apr 16 05:07:54 Starting compiler/encoders/arm8_asl
Apr 16 09:16:45 Finished compiler/encoders/arm8_asl                         4h08m50s  42GB
Apr 16 09:16:46 Starting compiler/encoders/mips
Apr 16 09:20:12 Finished compiler/encoders/mips                                3m26s   1GB
Apr 16 09:20:13 Starting compiler/encoders/riscv
Apr 16 09:24:05 Finished compiler/encoders/riscv                               3m51s   1GB
Apr 16 09:24:05 Starting compiler/encoders/ag32
Apr 16 09:24:53 Finished compiler/encoders/ag32                                  47s 630MB
Apr 16 09:24:53 Starting compiler/backend/x64
Apr 16 09:25:41 Finished compiler/backend/x64                                    47s   1GB
Apr 16 09:25:41 Starting compiler/backend/arm7
Apr 16 09:26:31 Finished compiler/backend/arm7                                   49s   1GB
Apr 16 09:26:31 Starting compiler/backend/arm8
Apr 16 09:27:16 Finished compiler/backend/arm8                                   44s   1GB
Apr 16 09:27:16 Starting compiler/backend/mips
Apr 16 09:28:05 Finished compiler/backend/mips                                   48s   1GB
Apr 16 09:28:05 Starting compiler/backend/riscv
Apr 16 09:28:54 Finished compiler/backend/riscv                                  48s   1GB
Apr 16 09:28:54 Starting compiler/backend/ag32
Apr 16 09:32:00 Finished compiler/backend/ag32                                 3m05s   1GB
Apr 16 09:32:00 Starting compiler/parsing/proofs
Apr 16 09:40:22 Finished compiler/parsing/proofs                               8m21s   1GB
Apr 16 09:40:22 Starting compiler/inference/proofs
Apr 16 09:46:05 Finished compiler/inference/proofs                             5m42s   1GB
Apr 16 09:46:05 Starting compiler/backend/semantics
Apr 16 10:48:11 Finished compiler/backend/semantics                         1h02m05s   2GB
Apr 16 10:48:11 Starting compiler/backend/reg_alloc/proofs
Apr 16 10:56:06 Finished compiler/backend/reg_alloc/proofs                     7m54s   1GB
Apr 16 10:56:06 Starting compiler/backend/proofs
Apr 16 12:37:40 Finished compiler/backend/proofs                            1h41m33s  18GB
Apr 16 12:37:40 Starting compiler/backend/serialiser
Apr 16 12:40:57 Finished compiler/backend/serialiser                           3m16s   2GB
Apr 16 12:40:57 Starting compiler/encoders/x64/proofs
Apr 16 13:02:25 Finished compiler/encoders/x64/proofs                         21m26s   4GB
Apr 16 13:02:25 Starting compiler/encoders/arm7/proofs
Apr 16 13:31:57 Finished compiler/encoders/arm7/proofs                        29m32s   3GB
Apr 16 13:31:57 Starting compiler/encoders/arm8/proofs
Apr 16 13:47:19 Finished compiler/encoders/arm8/proofs                        15m21s   1GB
Apr 16 13:47:20 Starting compiler/encoders/arm8_asl/proofs
Apr 16 15:39:10 Finished compiler/encoders/arm8_asl/proofs                  1h51m48s   5GB
Apr 16 15:39:10 Starting compiler/encoders/mips/proofs
Apr 16 16:01:24 Finished compiler/encoders/mips/proofs                        22m13s   2GB
Apr 16 16:01:24 Starting compiler/encoders/riscv/proofs
Apr 16 16:21:35 Finished compiler/encoders/riscv/proofs                       20m10s   1GB
Apr 16 16:21:35 Starting compiler/encoders/ag32/proofs
Apr 16 16:27:23 Finished compiler/encoders/ag32/proofs                         5m48s 847MB
Apr 16 16:27:23 Starting compiler/backend/x64/proofs
Apr 16 16:28:25 Finished compiler/backend/x64/proofs                           1m01s   1GB
Apr 16 16:28:25 Starting compiler/backend/arm7/proofs
Apr 16 16:29:29 Finished compiler/backend/arm7/proofs                          1m04s   1GB
Apr 16 16:29:30 Starting compiler/backend/arm8/proofs
Apr 16 16:30:30 Finished compiler/backend/arm8/proofs                          1m00s   1GB
Apr 16 16:30:31 Starting compiler/backend/arm8_asl
Apr 16 16:31:22 Finished compiler/backend/arm8_asl                               51s   1GB
Apr 16 16:31:22 Starting compiler/backend/mips/proofs
Apr 16 16:32:26 Finished compiler/backend/mips/proofs                          1m03s   1GB
Apr 16 16:32:26 Starting compiler/backend/riscv/proofs
Apr 16 16:33:27 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Apr 16 16:33:28 Starting compiler/backend/ag32/proofs
Apr 16 17:01:32 Finished compiler/backend/ag32/proofs                         28m04s   2GB
Apr 16 17:01:33 Starting compiler/proofs
Apr 16 17:06:29 Finished compiler/proofs                                       4m56s   3GB
Apr 16 17:06:30 Starting candle/set-theory
Apr 16 17:07:39 Finished candle/set-theory                                     1m09s 994MB
Apr 16 17:07:40 Starting candle/syntax-lib
Apr 16 17:08:09 Finished candle/syntax-lib                                       28s 666MB
Apr 16 17:08:09 Starting candle/standard/syntax
Apr 16 17:12:30 Finished candle/standard/syntax                                4m20s   1GB
Apr 16 17:12:30 Starting candle/standard/semantics
Apr 16 17:16:31 Finished candle/standard/semantics                             4m01s   1GB
Apr 16 17:16:32 Starting candle/standard/monadic
Apr 16 17:20:35 Finished candle/standard/monadic                               4m03s   1GB
Apr 16 17:20:35 Starting candle/standard/ml_kernel
Apr 16 17:33:40 Finished candle/standard/ml_kernel                            13m04s   3GB
Apr 16 17:33:40 Starting candle/overloading/syntax
Apr 16 17:40:45 Finished candle/overloading/syntax                             7m04s   1GB
Apr 16 17:40:45 Starting candle/overloading/semantics
Apr 16 18:07:10 Finished candle/overloading/semantics                         26m24s   2GB
Apr 16 18:07:10 Starting candle/overloading/monadic
Apr 16 18:12:34 Finished candle/overloading/monadic                            5m23s   1GB
Apr 16 18:12:34 Starting candle/overloading/ml_kernel
Apr 16 18:27:20 Finished candle/overloading/ml_kernel                         14m44s   3GB
Apr 16 18:27:20 Starting candle/overloading/ml_checker
Apr 16 18:32:40 Finished candle/overloading/ml_checker                         5m19s   3GB
Apr 16 18:32:40 Starting candle/prover
Apr 16 18:51:40 Finished candle/prover                                        18m59s   3GB
Apr 16 18:51:40 Starting pancake
Apr 16 18:59:21 Finished pancake                                               7m40s   3GB
Apr 16 18:59:21 Starting pancake/ffi
Apr 16 18:59:22 Finished pancake/ffi                                              0s  31MB
Apr 16 18:59:23 Starting pancake/semantics
Apr 16 18:59:56 FAILED: pancake/semantics
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)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[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$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/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/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanned 79 directories
Starting work on README.md
Starting work on compactDSLSemTheory
Starting work on panSemTheory
Starting work on pan_commonPropsTheory
README.md                                                                                                                                                                                             (0s)     OK
Starting work on loopSemTheory
pan_commonPropsTheory                                                                                                                                                                                (24s)FAIL<1>
 first subgoal not solved by second tactic (THEN1 on line 66)
 error in quse /root/regression/cakeml-1861/pancake/semantics/pan_commonPropsScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 66)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /root/regression/cakeml-1861/pancake/semantics/pan_commonPropsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 66)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 l f m e n. OPT_MMAP f l = SOME m  MEM e l  f e = SOME n  MEM n m
 
 failed.
 Failed to prove theorem opt_mmap_mem_defined.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 66)", origin_function = "THEN1", origin_structure = "Tactical"}
compactDSLSemTheory                                                                                                                                                                                  (25s)MKILLED
panSemTheory                                                                                                                                                                                         (25s)MKILLED
loopSemTheory                                                                                                                                                                                        (24s)MKILLED