Job 1534

CakeML:1739080f58469d8870c0b095ab0f7aeb56b21fd1
  Adapt following change in HOL [May 20 20:33:54]
HOL:fe4634b86ea93f927bb796c73b7f77e15362962e
  Universally quantify statements [May 17 23:32:35]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 20 20:41:09 Claimed job
May 20 20:41:12 Building HOL
May 20 20:57:11 Starting developers
May 20 20:57:16 Finished developers                                               4s  91MB
May 20 20:57:16 Starting developers/bin
May 20 20:57:23 Finished developers/bin                                           6s   1GB
May 20 20:57:23 Starting semantics/ffi
May 20 20:57:35 Finished semantics/ffi                                           11s 232MB
May 20 20:57:35 Starting semantics
May 20 20:59:12 Finished semantics                                             1m36s   1GB
May 20 20:59:12 Starting semantics/proofs
May 20 21:03:06 Finished semantics/proofs                                      3m53s 970MB
May 20 21:03:06 Starting semantics/alt_semantics
May 20 21:03:16 Finished semantics/alt_semantics                                  9s 297MB
May 20 21:03:16 Starting semantics/alt_semantics/proofs
May 20 21:05:39 Finished semantics/alt_semantics/proofs                        2m22s 798MB
May 20 21:05:39 Starting basis/pure
May 20 21:08:43 Finished basis/pure                                            3m03s 929MB
May 20 21:08:43 Starting translator
May 20 21:12:20 Finished translator                                            3m36s   1GB
May 20 21:12:20 Starting compiler/parsing
May 20 21:13:36 Finished compiler/parsing                                      1m15s   3GB
May 20 21:13:36 Starting characteristic
May 20 21:19:31 Finished characteristic                                        5m55s   1GB
May 20 21:19:31 Starting translator/monadic
May 20 21:21:16 Finished translator/monadic                                    1m44s   1GB
May 20 21:21:17 Starting basis
May 20 22:08:24 Finished basis                                                47m07s  14GB
May 20 22:08:24 Starting compiler/inference
May 20 22:09:43 Finished compiler/inference                                    1m18s   1GB
May 20 22:09:43 Starting compiler/backend/reg_alloc
May 20 22:10:53 Finished compiler/backend/reg_alloc                            1m10s   1GB
May 20 22:10:54 Starting compiler/backend/gc
May 20 22:14:49 Finished compiler/backend/gc                                   3m54s   2GB
May 20 22:14:49 Starting compiler/backend
May 20 22:19:59 Finished compiler/backend                                      5m09s   3GB
May 20 22:19:59 Starting compiler/encoders/asm
May 20 22:20:22 Finished compiler/encoders/asm                                   22s 620MB
May 20 22:20:23 Starting compiler/encoders/x64
May 20 22:21:29 Finished compiler/encoders/x64                                 1m06s   1GB
May 20 22:21:29 Starting compiler/encoders/arm7
May 20 22:23:43 Finished compiler/encoders/arm7                                2m13s   1GB
May 20 22:23:43 Starting compiler/encoders/arm8
May 20 22:24:24 Finished compiler/encoders/arm8                                  40s 534MB
May 20 22:24:24 Starting compiler/encoders/mips
May 20 22:26:01 Finished compiler/encoders/mips                                1m37s   1GB
May 20 22:26:02 Starting compiler/encoders/riscv
May 20 22:27:56 Finished compiler/encoders/riscv                               1m54s   1GB
May 20 22:27:57 Starting compiler/encoders/ag32
May 20 22:28:16 Finished compiler/encoders/ag32                                  18s 891MB
May 20 22:28:16 Starting compiler/backend/x64
May 20 22:28:36 Finished compiler/backend/x64                                    19s   1GB
May 20 22:28:36 Starting compiler/backend/arm7
May 20 22:28:58 Finished compiler/backend/arm7                                   21s   1GB
May 20 22:28:58 Starting compiler/backend/arm8
May 20 22:29:18 Finished compiler/backend/arm8                                   19s   1GB
May 20 22:29:18 Starting compiler/backend/mips
May 20 22:29:37 Finished compiler/backend/mips                                   18s 989MB
May 20 22:29:37 Starting compiler/backend/riscv
May 20 22:29:58 Finished compiler/backend/riscv                                  20s   1GB
May 20 22:29:58 Starting compiler/backend/ag32
May 20 22:31:11 Finished compiler/backend/ag32                                 1m12s   1GB
May 20 22:31:11 Starting compiler/parsing/proofs
May 20 22:37:20 Finished compiler/parsing/proofs                               6m08s   1GB
May 20 22:37:20 Starting compiler/inference/proofs
May 20 22:40:00 Finished compiler/inference/proofs                             2m39s 910MB
May 20 22:40:00 Starting compiler/backend/semantics
May 20 23:13:11 Finished compiler/backend/semantics                           33m10s   2GB
May 20 23:13:11 Starting compiler/backend/reg_alloc/proofs
May 20 23:16:59 Finished compiler/backend/reg_alloc/proofs                     3m47s 854MB
May 20 23:16:59 Starting compiler/backend/proofs
May 21 00:15:29 Finished compiler/backend/proofs                              58m29s  15GB
May 21 00:15:29 Starting compiler/encoders/x64/proofs
May 21 00:25:51 Finished compiler/encoders/x64/proofs                         10m21s   4GB
May 21 00:25:51 Starting compiler/encoders/arm7/proofs
May 21 00:39:59 Finished compiler/encoders/arm7/proofs                        14m08s   4GB
May 21 00:40:00 Starting compiler/encoders/arm8/proofs
May 21 00:47:16 Finished compiler/encoders/arm8/proofs                         7m15s   1GB
May 21 00:47:16 Starting compiler/encoders/mips/proofs
May 21 00:58:08 Finished compiler/encoders/mips/proofs                        10m51s   2GB
May 21 00:58:08 Starting compiler/encoders/riscv/proofs
May 21 01:07:46 Finished compiler/encoders/riscv/proofs                        9m37s   1GB
May 21 01:07:46 Starting compiler/encoders/ag32/proofs
May 21 01:10:34 Finished compiler/encoders/ag32/proofs                         2m47s 699MB
May 21 01:10:34 Starting compiler/backend/x64/proofs
May 21 01:10:58 Finished compiler/backend/x64/proofs                             23s   1GB
May 21 01:10:58 Starting compiler/backend/arm7/proofs
May 21 01:11:23 Finished compiler/backend/arm7/proofs                            24s   2GB
May 21 01:11:23 Starting compiler/backend/arm8/proofs
May 21 01:11:46 Finished compiler/backend/arm8/proofs                            23s   1GB
May 21 01:11:47 Starting compiler/backend/mips/proofs
May 21 01:12:11 Finished compiler/backend/mips/proofs                            23s   1GB
May 21 01:12:11 Starting compiler/backend/riscv/proofs
May 21 01:12:35 Finished compiler/backend/riscv/proofs                           23s   1GB
May 21 01:12:35 Starting compiler/backend/ag32/proofs
May 21 01:26:02 Finished compiler/backend/ag32/proofs                         13m27s   3GB
May 21 01:26:02 Starting compiler/proofs
May 21 01:28:03 Finished compiler/proofs                                       2m00s   3GB
May 21 01:28:04 Starting candle/set-theory
May 21 01:28:33 Finished candle/set-theory                                       29s 742MB
May 21 01:28:34 Starting candle/syntax-lib
May 21 01:28:45 Finished candle/syntax-lib                                       11s 506MB
May 21 01:28:45 Starting candle/standard/syntax
May 21 01:30:42 Finished candle/standard/syntax                                1m56s 991MB
May 21 01:30:42 Starting candle/standard/semantics
May 21 01:32:32 Finished candle/standard/semantics                             1m49s 975MB
May 21 01:32:33 Starting candle/standard/monadic
May 21 01:34:24 Finished candle/standard/monadic                               1m50s   1GB
May 21 01:34:24 Starting candle/standard/ml_kernel
May 21 01:40:37 Finished candle/standard/ml_kernel                             6m12s   5GB
May 21 01:40:37 Starting candle/overloading/syntax
May 21 01:44:00 Finished candle/overloading/syntax                             3m22s 922MB
May 21 01:44:00 Starting candle/overloading/semantics
May 21 01:56:45 Finished candle/overloading/semantics                         12m44s   5GB
May 21 01:56:45 Starting characteristic/examples
May 21 01:58:09 Finished characteristic/examples                               1m23s   2GB
May 21 01:58:09 Starting tutorial/solutions
May 21 02:14:20 Finished tutorial/solutions                                   16m10s   9GB
May 21 02:14:20 Starting translator/monadic/examples
May 21 02:17:44 Finished translator/monadic/examples                           3m24s   3GB
May 21 02:17:45 Starting examples
May 21 02:26:52 Finished examples                                              9m06s   4GB
May 21 02:26:52 Starting examples/compilation/x64
May 21 04:58:15 Finished examples/compilation/x64                           2h31m23s  13GB
May 21 04:58:15 Starting examples/compilation/x64/proofs
May 21 05:00:08 Finished examples/compilation/x64/proofs                       1m52s   3GB
May 21 05:00:08 Starting examples/compilation/ag32
May 21 05:35:07 Finished examples/compilation/ag32                            34m58s   8GB
May 21 05:35:07 Starting examples/compilation/ag32/proofs
May 21 05:36:02 Finished examples/compilation/ag32/proofs                        54s   3GB
May 21 05:36:03 Starting examples/cost
May 21 05:50:29 FAILED: examples/cost
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
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 $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                       real:    0s  user:    0s     OK
miniBasisProgTheory                             real:   30s  user:   29s     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                              real:   31s  user:   30s     OK
costPropsTheory                                 real:   84s  user:   80s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  657s  user:  721s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  635s  user:  688s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  670s  user:  725s     OK
Starting work on allProofTheory
allProofTheory                                  real:  109s  user:  105sFAIL<1>
 Saved definition __ "repbool_to_tsl_def"
 Saved induction ___ "repbool_to_tsl_ind"
 Saved theorem _____ "repbool_list_to_tsl_SOME"
 Saved definition __ "repbool_list_safe_def"
 Saved definition __ "repbool_safe_heap_def"
 Saved theorem _____ "repbool_list_size_of_rm"
 Saved theorem _____ "repbool_list_seen_MEM"
 error in quse /home/cake/oven/regression/cakeml-1534/examples/cost/allProofScript.sml : HOL_ERR {message = "\"state_locals_fupd\" not found in theory \"dataSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 error in load /home/cake/oven/regression/cakeml-1534/examples/cost/allProofScript : HOL_ERR {message = "\"state_locals_fupd\" not found in theory \"dataSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}
 Uncaught exception: HOL_ERR {message = "\"state_locals_fupd\" not found in theory \"dataSem\"", origin_function = "prim_mk_const", origin_structure = "Term"}
cyesProgTheory                                                          M-KILLED
lcgLoopProofTheory                                                      M-KILLED
pureLoopProofTheory                                                     M-KILLED