Job 1855

CakeML:ce7d2a18407525c943e5d48a2e9f60ee752d6f8e
  Fix translation for printing changes [Apr 08 09:54:26]
#872 (printing-type-check-each-dec)
Merging into: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 08 13:47:26 Claimed job
Apr 08 13:47:36 Building HOL
Apr 08 14:00:38 Starting developers
Apr 08 14:00:44 Finished developers                                               6s  60MB
Apr 08 14:00:45 Starting developers/bin
Apr 08 14:00:54 Finished developers/bin                                           9s   1GB
Apr 08 14:00:55 Starting semantics/ffi
Apr 08 14:01:08 Finished semantics/ffi                                           12s 207MB
Apr 08 14:01:08 Starting semantics
Apr 08 14:04:10 Finished semantics                                             3m01s 344MB
Apr 08 14:04:10 Starting semantics/proofs
Apr 08 14:11:08 Finished semantics/proofs                                      6m57s   1GB
Apr 08 14:11:08 Starting semantics/alt_semantics
Apr 08 14:11:45 Finished semantics/alt_semantics                                 36s 229MB
Apr 08 14:11:45 Starting semantics/alt_semantics/proofs
Apr 08 14:16:31 Finished semantics/alt_semantics/proofs                        4m45s 420MB
Apr 08 14:16:31 Starting basis/pure
Apr 08 14:20:38 Finished basis/pure                                            4m06s 394MB
Apr 08 14:20:38 Starting translator
Apr 08 14:24:59 Finished translator                                            4m20s 736MB
Apr 08 14:24:59 Starting compiler/parsing
Apr 08 14:26:49 Finished compiler/parsing                                      1m49s 708MB
Apr 08 14:26:49 Starting characteristic
Apr 08 14:36:05 Finished characteristic                                        9m16s 736MB
Apr 08 14:36:06 Starting translator/monadic
Apr 08 14:39:06 Finished translator/monadic                                    3m00s 576MB
Apr 08 14:39:06 Starting basis
Apr 08 15:47:33 Finished basis                                              1h08m24s   1GB
Apr 08 15:47:33 Starting compiler/inference
Apr 08 15:49:27 Finished compiler/inference                                    1m53s 442MB
Apr 08 15:49:27 Starting compiler/backend/reg_alloc
Apr 08 15:51:56 Finished compiler/backend/reg_alloc                            2m28s 314MB
Apr 08 15:51:57 Starting compiler/backend/gc
Apr 08 15:58:24 Finished compiler/backend/gc                                   6m27s 661MB
Apr 08 15:58:25 Starting compiler/backend
Apr 08 16:07:59 Finished compiler/backend                                      9m33s 907MB
Apr 08 16:07:59 Starting compiler/encoders/asm
Apr 08 16:08:43 Finished compiler/encoders/asm                                   43s 308MB
Apr 08 16:08:43 Starting compiler/encoders/x64
Apr 08 16:10:44 Finished compiler/encoders/x64                                 2m00s 320MB
Apr 08 16:10:44 Starting compiler/encoders/arm7
Apr 08 16:13:38 Finished compiler/encoders/arm7                                2m53s 930MB
Apr 08 16:13:38 Starting compiler/encoders/arm8
Apr 08 16:14:54 Finished compiler/encoders/arm8                                1m14s 311MB
Apr 08 16:14:54 Starting compiler/encoders/arm8_asl
Apr 08 19:27:36 Finished compiler/encoders/arm8_asl                         3h12m41s   5GB
Apr 08 19:27:36 Starting compiler/encoders/mips
Apr 08 19:29:57 Finished compiler/encoders/mips                                2m20s 521MB
Apr 08 19:29:57 Starting compiler/encoders/riscv
Apr 08 19:32:26 Finished compiler/encoders/riscv                               2m27s 588MB
Apr 08 19:32:26 Starting compiler/encoders/ag32
Apr 08 19:32:57 Finished compiler/encoders/ag32                                  29s 870MB
Apr 08 19:32:57 Starting compiler/backend/x64
Apr 08 19:33:31 Finished compiler/backend/x64                                    33s 623MB
Apr 08 19:33:31 Starting compiler/backend/arm7
Apr 08 19:34:12 Finished compiler/backend/arm7                                   39s 666MB
Apr 08 19:34:12 Starting compiler/backend/arm8
Apr 08 19:34:51 Finished compiler/backend/arm8                                   39s 676MB
Apr 08 19:34:52 Starting compiler/backend/mips
Apr 08 19:35:39 Finished compiler/backend/mips                                   47s 686MB
Apr 08 19:35:39 Starting compiler/backend/riscv
Apr 08 19:36:10 Finished compiler/backend/riscv                                  30s 685MB
Apr 08 19:36:10 Starting compiler/backend/ag32
Apr 08 19:38:05 Finished compiler/backend/ag32                                 1m53s 541MB
Apr 08 19:38:05 Starting compiler/parsing/proofs
Apr 08 19:43:23 Finished compiler/parsing/proofs                               5m17s 627MB
Apr 08 19:43:23 Starting compiler/inference/proofs
Apr 08 19:47:16 Finished compiler/inference/proofs                             3m52s 474MB
Apr 08 19:47:16 Starting compiler/backend/semantics
Apr 08 20:30:14 Finished compiler/backend/semantics                           42m56s 865MB
Apr 08 20:30:14 Starting compiler/backend/reg_alloc/proofs
Apr 08 20:35:02 Finished compiler/backend/reg_alloc/proofs                     4m47s 340MB
Apr 08 20:35:02 Starting compiler/backend/proofs
Apr 08 21:53:30 Finished compiler/backend/proofs                            1h18m26s   5GB
Apr 08 21:53:30 Starting compiler/backend/serialiser
Apr 08 21:56:14 Finished compiler/backend/serialiser                           2m42s 608MB
Apr 08 21:56:15 Starting compiler/encoders/x64/proofs
Apr 08 22:09:51 Finished compiler/encoders/x64/proofs                         13m35s   1GB
Apr 08 22:09:51 Starting compiler/encoders/arm7/proofs
Apr 08 22:28:40 Finished compiler/encoders/arm7/proofs                        18m48s   1GB
Apr 08 22:28:40 Starting compiler/encoders/arm8/proofs
Apr 08 22:37:27 Finished compiler/encoders/arm8/proofs                         8m46s 817MB
Apr 08 22:37:27 Starting compiler/encoders/arm8_asl/proofs
Apr 08 23:48:31 Finished compiler/encoders/arm8_asl/proofs                  1h11m03s   2GB
Apr 08 23:48:31 Starting compiler/encoders/mips/proofs
Apr 09 00:02:23 Finished compiler/encoders/mips/proofs                        13m51s   1GB
Apr 09 00:02:23 Starting compiler/encoders/riscv/proofs
Apr 09 00:14:27 Finished compiler/encoders/riscv/proofs                       12m03s 449MB
Apr 09 00:14:28 Starting compiler/encoders/ag32/proofs
Apr 09 00:17:54 Finished compiler/encoders/ag32/proofs                         3m25s 473MB
Apr 09 00:17:54 Starting compiler/backend/x64/proofs
Apr 09 00:18:52 Finished compiler/backend/x64/proofs                             58s 822MB
Apr 09 00:18:52 Starting compiler/backend/arm7/proofs
Apr 09 00:19:53 Finished compiler/backend/arm7/proofs                          1m00s 532MB
Apr 09 00:19:53 Starting compiler/backend/arm8/proofs
Apr 09 00:20:45 Finished compiler/backend/arm8/proofs                            51s 847MB
Apr 09 00:20:45 Starting compiler/backend/arm8_asl
Apr 09 00:21:40 Finished compiler/backend/arm8_asl                               54s 764MB
Apr 09 00:21:40 Starting compiler/backend/mips/proofs
Apr 09 00:22:44 Finished compiler/backend/mips/proofs                          1m02s 589MB
Apr 09 00:22:44 Starting compiler/backend/riscv/proofs
Apr 09 00:23:45 Finished compiler/backend/riscv/proofs                         1m01s 947MB
Apr 09 00:23:45 Starting compiler/backend/ag32/proofs
Apr 09 00:41:09 Finished compiler/backend/ag32/proofs                         17m23s   1GB
Apr 09 00:41:09 Starting compiler/proofs
Apr 09 00:45:21 Finished compiler/proofs                                       4m10s   1GB
Apr 09 00:45:21 Starting candle/set-theory
Apr 09 00:46:04 Finished candle/set-theory                                       42s 661MB
Apr 09 00:46:04 Starting candle/syntax-lib
Apr 09 00:46:28 Finished candle/syntax-lib                                       23s 244MB
Apr 09 00:46:28 Starting candle/standard/syntax
Apr 09 00:48:55 Finished candle/standard/syntax                                2m25s 806MB
Apr 09 00:48:55 Starting candle/standard/semantics
Apr 09 00:51:13 Finished candle/standard/semantics                             2m17s 816MB
Apr 09 00:51:13 Starting candle/standard/monadic
Apr 09 00:53:35 Finished candle/standard/monadic                               2m22s 870MB
Apr 09 00:53:36 Starting candle/standard/ml_kernel
Apr 09 01:02:28 Finished candle/standard/ml_kernel                             8m52s   1GB
Apr 09 01:02:29 Starting candle/overloading/syntax
Apr 09 01:06:26 Finished candle/overloading/syntax                             3m57s 541MB
Apr 09 01:06:26 Starting candle/overloading/semantics
Apr 09 01:21:58 Finished candle/overloading/semantics                         15m31s   1GB
Apr 09 01:21:58 Starting candle/overloading/monadic
Apr 09 01:25:33 Finished candle/overloading/monadic                            3m35s 419MB
Apr 09 01:25:34 Starting candle/overloading/ml_kernel
Apr 09 01:36:12 Finished candle/overloading/ml_kernel                         10m38s   1GB
Apr 09 01:36:12 Starting candle/overloading/ml_checker
Apr 09 01:39:23 Finished candle/overloading/ml_checker                         3m10s   1GB
Apr 09 01:39:23 Starting candle/prover
Apr 09 01:52:08 Finished candle/prover                                        12m44s   1GB
Apr 09 01:52:09 Starting pancake
Apr 09 01:58:37 Finished pancake                                               6m27s   1GB
Apr 09 01:58:37 Starting pancake/ffi
Apr 09 01:58:38 Finished pancake/ffi                                              0s  11MB
Apr 09 01:58:38 Starting pancake/semantics
Apr 09 01:59:07 FAILED: pancake/semantics
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
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/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 $(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/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)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
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
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                                              (19s)FAIL<1>
 first subgoal not solved by second tactic (THEN1 on line 66)
 error in quse /home/cake/oven/regression/cakeml-1855/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/cake/oven/regression/cakeml-1855/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                                                (20s)MKILLED
panSemTheory                                                       (22s)MKILLED
loopSemTheory                                                      (21s)MKILLED