Job 1862

CakeML: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:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 16 09:20:51 Claimed job
Apr 16 09:20:52 Reusing HOL
Apr 16 09:21:05 Starting developers
Apr 16 09:21:09 Finished developers                                               4s 120MB
Apr 16 09:21:09 Starting developers/bin
Apr 16 09:21:23 Finished developers/bin                                          13s   1GB
Apr 16 09:21:23 Starting semantics/ffi
Apr 16 09:21:33 Finished semantics/ffi                                            9s 237MB
Apr 16 09:21:33 Starting semantics
Apr 16 09:23:31 Finished semantics                                             1m57s   1GB
Apr 16 09:23:31 Starting semantics/proofs
Apr 16 09:27:35 Finished semantics/proofs                                      4m04s   3GB
Apr 16 09:27:35 Starting semantics/alt_semantics
Apr 16 09:28:00 Finished semantics/alt_semantics                                 24s 551MB
Apr 16 09:28:00 Starting semantics/alt_semantics/proofs
Apr 16 09:31:01 Finished semantics/alt_semantics/proofs                        3m00s   1GB
Apr 16 09:31:01 Starting basis/pure
Apr 16 09:32:08 Finished basis/pure                                            1m06s   1GB
Apr 16 09:32:08 Starting translator
Apr 16 09:35:08 Finished translator                                            2m59s   1GB
Apr 16 09:35:08 Starting compiler/parsing
Apr 16 09:36:22 Finished compiler/parsing                                      1m14s   3GB
Apr 16 09:36:22 Starting characteristic
Apr 16 09:42:52 Finished characteristic                                        6m26s   1GB
Apr 16 09:42:52 Starting translator/monadic
Apr 16 09:44:47 Finished translator/monadic                                    1m55s   1GB
Apr 16 09:44:48 Starting basis
Apr 16 10:31:28 Finished basis                                                46m40s  17GB
Apr 16 10:31:28 Starting compiler/inference
Apr 16 10:32:49 Finished compiler/inference                                    1m21s   1GB
Apr 16 10:32:49 Starting compiler/backend/reg_alloc
Apr 16 10:34:35 Finished compiler/backend/reg_alloc                            1m45s   1GB
Apr 16 10:34:35 Starting compiler/backend/gc
Apr 16 10:38:55 Finished compiler/backend/gc                                   4m20s   1GB
Apr 16 10:38:56 Starting compiler/backend
Apr 16 10:44:34 Finished compiler/backend                                      5m37s   2GB
Apr 16 10:44:34 Starting compiler/encoders/asm
Apr 16 10:45:04 Finished compiler/encoders/asm                                   29s 739MB
Apr 16 10:45:04 Starting compiler/encoders/x64
Apr 16 10:45:35 Finished compiler/encoders/x64                                   30s 870MB
Apr 16 10:45:35 Starting compiler/encoders/arm7
Apr 16 10:46:29 Finished compiler/encoders/arm7                                  54s 737MB
Apr 16 10:46:30 Starting compiler/encoders/arm8
Apr 16 10:46:46 Finished compiler/encoders/arm8                                  16s 764MB
Apr 16 10:46:47 Starting compiler/encoders/arm8_asl
Apr 16 10:49:16 Finished compiler/encoders/arm8_asl                            2m29s   1GB
Apr 16 10:49:16 Starting compiler/encoders/mips
Apr 16 10:49:38 Finished compiler/encoders/mips                                  21s   1GB
Apr 16 10:49:38 Starting compiler/encoders/riscv
Apr 16 10:49:58 Finished compiler/encoders/riscv                                 19s 968MB
Apr 16 10:49:58 Starting compiler/encoders/ag32
Apr 16 10:50:20 Finished compiler/encoders/ag32                                  22s 966MB
Apr 16 10:50:20 Starting compiler/backend/x64
Apr 16 10:50:43 Finished compiler/backend/x64                                    22s   1GB
Apr 16 10:50:43 Starting compiler/backend/arm7
Apr 16 10:51:06 Finished compiler/backend/arm7                                   23s   1GB
Apr 16 10:51:07 Starting compiler/backend/arm8
Apr 16 10:51:29 Finished compiler/backend/arm8                                   22s   1GB
Apr 16 10:51:29 Starting compiler/backend/mips
Apr 16 10:51:51 Finished compiler/backend/mips                                   21s   1GB
Apr 16 10:51:51 Starting compiler/backend/riscv
Apr 16 10:52:13 Finished compiler/backend/riscv                                  22s   1GB
Apr 16 10:52:14 Starting compiler/backend/ag32
Apr 16 10:53:41 Finished compiler/backend/ag32                                 1m26s   1GB
Apr 16 10:53:41 Starting compiler/parsing/proofs
Apr 16 10:57:25 Finished compiler/parsing/proofs                               3m44s   1GB
Apr 16 10:57:25 Starting compiler/inference/proofs
Apr 16 10:59:57 Finished compiler/inference/proofs                             2m31s   1GB
Apr 16 10:59:57 Starting compiler/backend/semantics
Apr 16 11:27:55 Finished compiler/backend/semantics                           27m58s   2GB
Apr 16 11:27:55 Starting compiler/backend/reg_alloc/proofs
Apr 16 11:31:28 Finished compiler/backend/reg_alloc/proofs                     3m32s 977MB
Apr 16 11:31:28 Starting compiler/backend/proofs
Apr 16 12:22:39 Finished compiler/backend/proofs                              51m09s  25GB
Apr 16 12:22:39 Starting compiler/backend/serialiser
Apr 16 12:24:18 Finished compiler/backend/serialiser                           1m38s   2GB
Apr 16 12:24:18 Starting compiler/encoders/x64/proofs
Apr 16 12:33:44 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Apr 16 12:33:44 Starting compiler/encoders/arm7/proofs
Apr 16 12:46:44 Finished compiler/encoders/arm7/proofs                        12m59s   3GB
Apr 16 12:46:44 Starting compiler/encoders/arm8/proofs
Apr 16 12:53:29 Finished compiler/encoders/arm8/proofs                         6m45s   1GB
Apr 16 12:53:29 Starting compiler/encoders/arm8_asl/proofs
Apr 16 13:08:50 Finished compiler/encoders/arm8_asl/proofs                    15m20s   2GB
Apr 16 13:08:50 Starting compiler/encoders/mips/proofs
Apr 16 13:18:57 Finished compiler/encoders/mips/proofs                        10m06s   1GB
Apr 16 13:18:57 Starting compiler/encoders/riscv/proofs
Apr 16 13:27:44 Finished compiler/encoders/riscv/proofs                        8m46s   1GB
Apr 16 13:27:44 Starting compiler/encoders/ag32/proofs
Apr 16 13:30:17 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Apr 16 13:30:17 Starting compiler/backend/x64/proofs
Apr 16 13:30:45 Finished compiler/backend/x64/proofs                             28s   1GB
Apr 16 13:30:46 Starting compiler/backend/arm7/proofs
Apr 16 13:31:14 Finished compiler/backend/arm7/proofs                            28s   1GB
Apr 16 13:31:14 Starting compiler/backend/arm8/proofs
Apr 16 13:31:43 Finished compiler/backend/arm8/proofs                            28s   1GB
Apr 16 13:31:43 Starting compiler/backend/arm8_asl
Apr 16 13:32:07 Finished compiler/backend/arm8_asl                               23s   1GB
Apr 16 13:32:07 Starting compiler/backend/mips/proofs
Apr 16 13:32:35 Finished compiler/backend/mips/proofs                            28s   1GB
Apr 16 13:32:35 Starting compiler/backend/riscv/proofs
Apr 16 13:33:04 Finished compiler/backend/riscv/proofs                           28s   1GB
Apr 16 13:33:04 Starting compiler/backend/ag32/proofs
Apr 16 13:45:45 Finished compiler/backend/ag32/proofs                         12m41s   2GB
Apr 16 13:45:45 Starting compiler/proofs
Apr 16 13:47:52 Finished compiler/proofs                                       2m05s   2GB
Apr 16 13:47:52 Starting candle/set-theory
Apr 16 13:48:27 Finished candle/set-theory                                       35s 836MB
Apr 16 13:48:27 Starting candle/syntax-lib
Apr 16 13:48:41 Finished candle/syntax-lib                                       13s 533MB
Apr 16 13:48:41 Starting candle/standard/syntax
Apr 16 13:50:43 Finished candle/standard/syntax                                2m02s   1GB
Apr 16 13:50:44 Starting candle/standard/semantics
Apr 16 13:52:35 Finished candle/standard/semantics                             1m51s 924MB
Apr 16 13:52:35 Starting candle/standard/monadic
Apr 16 13:54:29 Finished candle/standard/monadic                               1m53s   2GB
Apr 16 13:54:29 Starting candle/standard/ml_kernel
Apr 16 14:00:35 Finished candle/standard/ml_kernel                             6m06s   2GB
Apr 16 14:00:35 Starting candle/overloading/syntax
Apr 16 14:03:47 Finished candle/overloading/syntax                             3m11s   1GB
Apr 16 14:03:47 Starting candle/overloading/semantics
Apr 16 14:15:23 Finished candle/overloading/semantics                         11m36s   2GB
Apr 16 14:15:23 Starting candle/overloading/monadic
Apr 16 14:17:55 Finished candle/overloading/monadic                            2m31s   1GB
Apr 16 14:17:55 Starting candle/overloading/ml_kernel
Apr 16 14:25:02 Finished candle/overloading/ml_kernel                          7m07s   3GB
Apr 16 14:25:02 Starting candle/overloading/ml_checker
Apr 16 14:27:26 Finished candle/overloading/ml_checker                         2m23s   3GB
Apr 16 14:27:26 Starting candle/prover
Apr 16 14:35:37 Finished candle/prover                                         8m08s   3GB
Apr 16 14:35:37 Starting pancake
Apr 16 14:39:20 Finished pancake                                               3m42s   3GB
Apr 16 14:39:20 Starting pancake/ffi
Apr 16 14:39:20 Finished pancake/ffi                                              0s  35MB
Apr 16 14:39:20 Starting pancake/semantics
Apr 16 14:39:38 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                                              (13s)FAIL<1>
 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.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 66)
 error in quse /home/cug/hk324/cml-regression/cakeml-1862/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 /home/cug/hk324/cml-regression/cakeml-1862/pancake/semantics/pan_commonPropsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 66)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 66)", origin_function = "THEN1", origin_structure = "Tactical"}
compactDSLSemTheory                                                (14s)MKILLED
panSemTheory                                                       (14s)MKILLED
loopSemTheory                                                      (13s)MKILLED