Job 1856

CakeML:746be7b61665e6297b7ce29f70b74eec6efc7a79
  Merge pull request #873 from CakeML/issue871 [Apr 08 11:13:44]
HOL:bf3e59ba99decc59cfe5a28a6d45dfea3e058afc
  Add a timeout on regression build attempts [Apr 07 04:13:36]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 08 16:56:18 Claimed job
Apr 08 16:56:20 Reusing HOL
Apr 08 16:56:32 Starting developers
Apr 08 16:56:37 Finished developers                                               4s 174MB
Apr 08 16:56:37 Starting developers/bin
Apr 08 16:56:44 Finished developers/bin                                           6s   1GB
Apr 08 16:56:44 Starting semantics/ffi
Apr 08 16:56:54 Finished semantics/ffi                                            9s 244MB
Apr 08 16:56:54 Starting semantics
Apr 08 16:58:52 Finished semantics                                             1m57s   1GB
Apr 08 16:58:52 Starting semantics/proofs
Apr 08 17:03:00 Finished semantics/proofs                                      4m08s   2GB
Apr 08 17:03:01 Starting semantics/alt_semantics
Apr 08 17:03:24 Finished semantics/alt_semantics                                 23s 489MB
Apr 08 17:03:24 Starting semantics/alt_semantics/proofs
Apr 08 17:06:24 Finished semantics/alt_semantics/proofs                        2m59s   1GB
Apr 08 17:06:24 Starting basis/pure
Apr 08 17:07:31 Finished basis/pure                                            1m06s 819MB
Apr 08 17:07:31 Starting translator
Apr 08 17:10:33 Finished translator                                            3m02s   1GB
Apr 08 17:10:33 Starting compiler/parsing
Apr 08 17:11:51 Finished compiler/parsing                                      1m18s   2GB
Apr 08 17:11:51 Starting characteristic
Apr 08 17:18:14 Finished characteristic                                        6m23s   2GB
Apr 08 17:18:14 Starting translator/monadic
Apr 08 17:20:22 Finished translator/monadic                                    2m07s   1GB
Apr 08 17:20:22 Starting basis
Apr 08 18:07:03 Finished basis                                                46m40s  12GB
Apr 08 18:07:03 Starting compiler/inference
Apr 08 18:08:25 Finished compiler/inference                                    1m21s   1GB
Apr 08 18:08:25 Starting compiler/backend/reg_alloc
Apr 08 18:10:09 Finished compiler/backend/reg_alloc                            1m43s   1GB
Apr 08 18:10:09 Starting compiler/backend/gc
Apr 08 18:14:31 Finished compiler/backend/gc                                   4m22s   1GB
Apr 08 18:14:31 Starting compiler/backend
Apr 08 18:20:12 Finished compiler/backend                                      5m40s   2GB
Apr 08 18:20:12 Starting compiler/encoders/asm
Apr 08 18:20:42 Finished compiler/encoders/asm                                   29s 734MB
Apr 08 18:20:42 Starting compiler/encoders/x64
Apr 08 18:21:12 Finished compiler/encoders/x64                                   29s   1GB
Apr 08 18:21:12 Starting compiler/encoders/arm7
Apr 08 18:22:06 Finished compiler/encoders/arm7                                  53s 872MB
Apr 08 18:22:06 Starting compiler/encoders/arm8
Apr 08 18:22:23 Finished compiler/encoders/arm8                                  16s 756MB
Apr 08 18:22:23 Starting compiler/encoders/arm8_asl
Apr 08 18:24:54 Finished compiler/encoders/arm8_asl                            2m31s   1GB
Apr 08 18:24:54 Starting compiler/encoders/mips
Apr 08 18:25:16 Finished compiler/encoders/mips                                  20s   1GB
Apr 08 18:25:16 Starting compiler/encoders/riscv
Apr 08 18:25:35 Finished compiler/encoders/riscv                                 19s 825MB
Apr 08 18:25:36 Starting compiler/encoders/ag32
Apr 08 18:25:57 Finished compiler/encoders/ag32                                  21s 716MB
Apr 08 18:25:58 Starting compiler/backend/x64
Apr 08 18:26:20 Finished compiler/backend/x64                                    21s   1GB
Apr 08 18:26:20 Starting compiler/backend/arm7
Apr 08 18:26:45 Finished compiler/backend/arm7                                   24s   1GB
Apr 08 18:26:45 Starting compiler/backend/arm8
Apr 08 18:27:07 Finished compiler/backend/arm8                                   21s   1GB
Apr 08 18:27:07 Starting compiler/backend/mips
Apr 08 18:27:29 Finished compiler/backend/mips                                   21s   1GB
Apr 08 18:27:29 Starting compiler/backend/riscv
Apr 08 18:27:51 Finished compiler/backend/riscv                                  22s   1GB
Apr 08 18:27:51 Starting compiler/backend/ag32
Apr 08 18:29:19 Finished compiler/backend/ag32                                 1m27s   1GB
Apr 08 18:29:19 Starting compiler/parsing/proofs
Apr 08 18:32:59 Finished compiler/parsing/proofs                               3m39s   1GB
Apr 08 18:32:59 Starting compiler/inference/proofs
Apr 08 18:35:29 Finished compiler/inference/proofs                             2m30s 946MB
Apr 08 18:35:30 Starting compiler/backend/semantics
Apr 08 19:04:17 Finished compiler/backend/semantics                           28m47s   2GB
Apr 08 19:04:17 Starting compiler/backend/reg_alloc/proofs
Apr 08 19:07:56 Finished compiler/backend/reg_alloc/proofs                     3m36s 817MB
Apr 08 19:07:58 Starting compiler/backend/proofs
Apr 08 19:58:32 Finished compiler/backend/proofs                              50m34s  16GB
Apr 08 19:58:32 Starting compiler/backend/serialiser
Apr 08 20:00:10 Finished compiler/backend/serialiser                           1m37s   2GB
Apr 08 20:00:10 Starting compiler/encoders/x64/proofs
Apr 08 20:09:44 Finished compiler/encoders/x64/proofs                          9m31s   7GB
Apr 08 20:09:45 Starting compiler/encoders/arm7/proofs
Apr 08 20:22:42 Finished compiler/encoders/arm7/proofs                        12m56s   5GB
Apr 08 20:22:42 Starting compiler/encoders/arm8/proofs
Apr 08 20:29:25 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Apr 08 20:29:25 Starting compiler/encoders/arm8_asl/proofs
Apr 08 20:44:06 Finished compiler/encoders/arm8_asl/proofs                    14m40s   2GB
Apr 08 20:44:06 Starting compiler/encoders/mips/proofs
Apr 08 20:54:05 Finished compiler/encoders/mips/proofs                         9m58s   2GB
Apr 08 20:54:05 Starting compiler/encoders/riscv/proofs
Apr 08 21:02:53 Finished compiler/encoders/riscv/proofs                        8m48s   1GB
Apr 08 21:02:53 Starting compiler/encoders/ag32/proofs
Apr 08 21:05:26 Finished compiler/encoders/ag32/proofs                         2m32s 666MB
Apr 08 21:05:26 Starting compiler/backend/x64/proofs
Apr 08 21:05:55 Finished compiler/backend/x64/proofs                             28s   1GB
Apr 08 21:05:55 Starting compiler/backend/arm7/proofs
Apr 08 21:06:25 Finished compiler/backend/arm7/proofs                            29s   1GB
Apr 08 21:06:25 Starting compiler/backend/arm8/proofs
Apr 08 21:06:54 Finished compiler/backend/arm8/proofs                            28s   1GB
Apr 08 21:06:54 Starting compiler/backend/arm8_asl
Apr 08 21:07:17 Finished compiler/backend/arm8_asl                               23s   1GB
Apr 08 21:07:17 Starting compiler/backend/mips/proofs
Apr 08 21:07:46 Finished compiler/backend/mips/proofs                            28s   1GB
Apr 08 21:07:46 Starting compiler/backend/riscv/proofs
Apr 08 21:08:14 Finished compiler/backend/riscv/proofs                           28s   1GB
Apr 08 21:08:14 Starting compiler/backend/ag32/proofs
Apr 08 21:21:23 Finished compiler/backend/ag32/proofs                         13m07s   2GB
Apr 08 21:21:23 Starting compiler/proofs
Apr 08 21:23:34 Finished compiler/proofs                                       2m10s   3GB
Apr 08 21:23:34 Starting candle/set-theory
Apr 08 21:24:09 Finished candle/set-theory                                       34s   1GB
Apr 08 21:24:09 Starting candle/syntax-lib
Apr 08 21:24:22 Finished candle/syntax-lib                                       12s 710MB
Apr 08 21:24:22 Starting candle/standard/syntax
Apr 08 21:26:24 Finished candle/standard/syntax                                2m02s   1GB
Apr 08 21:26:25 Starting candle/standard/semantics
Apr 08 21:28:15 Finished candle/standard/semantics                             1m50s   1GB
Apr 08 21:28:15 Starting candle/standard/monadic
Apr 08 21:30:10 Finished candle/standard/monadic                               1m54s   1GB
Apr 08 21:30:10 Starting candle/standard/ml_kernel
Apr 08 21:36:28 Finished candle/standard/ml_kernel                             6m18s   3GB
Apr 08 21:36:28 Starting candle/overloading/syntax
Apr 08 21:39:38 Finished candle/overloading/syntax                             3m09s   1GB
Apr 08 21:39:38 Starting candle/overloading/semantics
Apr 08 21:51:18 Finished candle/overloading/semantics                         11m39s   2GB
Apr 08 21:51:18 Starting candle/overloading/monadic
Apr 08 21:53:52 Finished candle/overloading/monadic                            2m33s   1GB
Apr 08 21:53:52 Starting candle/overloading/ml_kernel
Apr 08 22:00:58 Finished candle/overloading/ml_kernel                          7m06s   3GB
Apr 08 22:00:58 Starting candle/overloading/ml_checker
Apr 08 22:03:23 Finished candle/overloading/ml_checker                         2m24s   3GB
Apr 08 22:03:23 Starting candle/prover
Apr 08 22:11:59 Finished candle/prover                                         8m35s   2GB
Apr 08 22:11:59 Starting pancake
Apr 08 22:15:41 Finished pancake                                               3m41s   3GB
Apr 08 22:15:41 Starting pancake/ffi
Apr 08 22:15:41 Finished pancake/ffi                                              0s  35MB
Apr 08 22:15:41 Starting pancake/semantics
Apr 08 22:15:59 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-1856/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-1856/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                                                (13s)MKILLED
panSemTheory                                                       (13s)MKILLED
loopSemTheory                                                      (13s)MKILLED