Job 1653

CakeML:4ab53d65d30d390110be9933723bc3f088c6e804
  Finish clos_opProof [Nov 22 21:23:20]
#847 (clos-smart-op)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:bdb437dfa109a22361c4d539c736d12e5828dbb8
  Add two utility shell scripts to developers [Nov 19 06:33:56]
Machine:oven3 4.19.67.1.amd64-smp

Nov 22 21:29:47 Claimed job
Nov 22 21:29:54 Reusing HOL
Nov 22 21:30:46 Starting developers
Nov 22 21:30:54 Finished developers                                               8s  90MB
Nov 22 21:30:55 Starting developers/bin
Nov 22 21:31:07 Finished developers/bin                                          12s   1GB
Nov 22 21:31:07 Starting semantics/ffi
Nov 22 21:31:33 Finished semantics/ffi                                           26s 261MB
Nov 22 21:31:34 Starting semantics
Nov 22 21:34:34 Finished semantics                                             2m59s   1GB
Nov 22 21:34:34 Starting semantics/proofs
Nov 22 21:42:43 Finished semantics/proofs                                      8m08s   1GB
Nov 22 21:42:43 Starting semantics/alt_semantics
Nov 22 21:43:09 Finished semantics/alt_semantics                                 25s 421MB
Nov 22 21:43:09 Starting semantics/alt_semantics/proofs
Nov 22 21:48:31 Finished semantics/alt_semantics/proofs                        5m21s   1GB
Nov 22 21:48:31 Starting basis/pure
Nov 22 21:50:18 Finished basis/pure                                            1m46s 745MB
Nov 22 21:50:18 Starting translator
Nov 22 21:56:15 Finished translator                                            5m56s   1GB
Nov 22 21:56:15 Starting compiler/parsing
Nov 22 21:58:46 Finished compiler/parsing                                      2m30s   3GB
Nov 22 21:58:46 Starting characteristic
Nov 22 22:11:00 Finished characteristic                                       12m13s   2GB
Nov 22 22:11:00 Starting translator/monadic
Nov 22 22:14:34 Finished translator/monadic                                    3m33s   1GB
Nov 22 22:14:34 Starting basis
Nov 22 23:55:23 Finished basis                                              1h40m48s  19GB
Nov 22 23:55:23 Starting compiler/inference
Nov 22 23:57:48 Finished compiler/inference                                    2m24s   1GB
Nov 22 23:57:49 Starting compiler/backend/reg_alloc
Nov 22 23:59:59 Finished compiler/backend/reg_alloc                            2m10s   1GB
Nov 22 23:59:59 Starting compiler/backend/gc
Nov 23 00:06:47 Finished compiler/backend/gc                                   6m47s   2GB
Nov 23 00:06:48 Starting compiler/backend
Nov 23 00:17:22 Finished compiler/backend                                     10m33s   4GB
Nov 23 00:17:22 Starting compiler/encoders/asm
Nov 23 00:18:13 Finished compiler/encoders/asm                                   50s 711MB
Nov 23 00:18:13 Starting compiler/encoders/x64
Nov 23 00:19:11 Finished compiler/encoders/x64                                   57s   1GB
Nov 23 00:19:12 Starting compiler/encoders/arm7
Nov 23 00:21:10 Finished compiler/encoders/arm7                                1m57s   1GB
Nov 23 00:21:10 Starting compiler/encoders/arm8
Nov 23 00:21:40 Finished compiler/encoders/arm8                                  29s 572MB
Nov 23 00:21:40 Starting compiler/encoders/mips
Nov 23 00:22:16 Finished compiler/encoders/mips                                  35s 907MB
Nov 23 00:22:16 Starting compiler/encoders/riscv
Nov 23 00:22:53 Finished compiler/encoders/riscv                                 36s 815MB
Nov 23 00:22:53 Starting compiler/encoders/ag32
Nov 23 00:23:33 Finished compiler/encoders/ag32                                  39s 606MB
Nov 23 00:23:33 Starting compiler/backend/x64
Nov 23 00:24:17 Finished compiler/backend/x64                                    44s   1GB
Nov 23 00:24:18 Starting compiler/backend/arm7
Nov 23 00:25:03 Finished compiler/backend/arm7                                   45s   1GB
Nov 23 00:25:03 Starting compiler/backend/arm8
Nov 23 00:25:47 Finished compiler/backend/arm8                                   43s   1GB
Nov 23 00:25:47 Starting compiler/backend/mips
Nov 23 00:26:30 Finished compiler/backend/mips                                   42s   1GB
Nov 23 00:26:30 Starting compiler/backend/riscv
Nov 23 00:27:13 Finished compiler/backend/riscv                                  43s   1GB
Nov 23 00:27:14 Starting compiler/backend/ag32
Nov 23 00:29:43 Finished compiler/backend/ag32                                 2m28s   1GB
Nov 23 00:29:43 Starting compiler/parsing/proofs
Nov 23 00:44:15 Finished compiler/parsing/proofs                              14m31s   1GB
Nov 23 00:44:15 Starting compiler/inference/proofs
Nov 23 00:50:01 Finished compiler/inference/proofs                             5m45s   1GB
Nov 23 00:50:01 Starting compiler/backend/semantics
Nov 23 01:50:17 Finished compiler/backend/semantics                         1h00m15s   3GB
Nov 23 01:50:18 Starting compiler/backend/reg_alloc/proofs
Nov 23 01:58:05 Finished compiler/backend/reg_alloc/proofs                     7m46s 946MB
Nov 23 01:58:05 Starting compiler/backend/proofs
Nov 23 03:40:39 Finished compiler/backend/proofs                            1h42m33s  14GB
Nov 23 03:40:39 Starting compiler/backend/serialiser
Nov 23 03:43:09 Finished compiler/backend/serialiser                           2m29s   2GB
Nov 23 03:43:10 Starting compiler/encoders/x64/proofs
Nov 23 04:04:49 Finished compiler/encoders/x64/proofs                         21m39s   5GB
Nov 23 04:04:50 Starting compiler/encoders/arm7/proofs
Nov 23 04:34:13 Finished compiler/encoders/arm7/proofs                        29m22s   3GB
Nov 23 04:34:13 Starting compiler/encoders/arm8/proofs
Nov 23 04:49:36 Finished compiler/encoders/arm8/proofs                        15m22s   1GB
Nov 23 04:49:36 Starting compiler/encoders/mips/proofs
Nov 23 05:12:09 Finished compiler/encoders/mips/proofs                        22m32s   2GB
Nov 23 05:12:09 Starting compiler/encoders/riscv/proofs
Nov 23 05:32:29 Finished compiler/encoders/riscv/proofs                       20m19s   1GB
Nov 23 05:32:30 Starting compiler/encoders/ag32/proofs
Nov 23 05:38:15 Finished compiler/encoders/ag32/proofs                         5m45s 799MB
Nov 23 05:38:15 Starting compiler/backend/x64/proofs
Nov 23 05:39:06 Finished compiler/backend/x64/proofs                             50s   1GB
Nov 23 05:39:07 Starting compiler/backend/arm7/proofs
Nov 23 05:39:57 Finished compiler/backend/arm7/proofs                            50s   1GB
Nov 23 05:39:57 Starting compiler/backend/arm8/proofs
Nov 23 05:40:46 Finished compiler/backend/arm8/proofs                            48s   1GB
Nov 23 05:40:46 Starting compiler/backend/mips/proofs
Nov 23 05:41:37 Finished compiler/backend/mips/proofs                            50s   1GB
Nov 23 05:41:37 Starting compiler/backend/riscv/proofs
Nov 23 05:42:29 Finished compiler/backend/riscv/proofs                           51s   1GB
Nov 23 05:42:29 Starting compiler/backend/ag32/proofs
Nov 23 06:09:49 Finished compiler/backend/ag32/proofs                         27m19s   2GB
Nov 23 06:09:49 Starting compiler/proofs
Nov 23 06:13:36 Finished compiler/proofs                                       3m46s   3GB
Nov 23 06:13:36 Starting candle/set-theory
Nov 23 06:14:36 Finished candle/set-theory                                       58s 772MB
Nov 23 06:14:36 Starting candle/syntax-lib
Nov 23 06:15:00 Finished candle/syntax-lib                                       24s 459MB
Nov 23 06:15:00 Starting candle/standard/syntax
Nov 23 06:19:02 Finished candle/standard/syntax                                4m00s 988MB
Nov 23 06:19:02 Starting candle/standard/semantics
Nov 23 06:23:00 Finished candle/standard/semantics                             3m57s   1GB
Nov 23 06:23:00 Starting candle/standard/monadic
Nov 23 06:26:46 Finished candle/standard/monadic                               3m45s   1GB
Nov 23 06:26:46 Starting candle/standard/ml_kernel
Nov 23 06:39:06 Finished candle/standard/ml_kernel                            12m19s   3GB
Nov 23 06:39:06 Starting candle/overloading/syntax
Nov 23 06:45:47 Finished candle/overloading/syntax                             6m40s   1GB
Nov 23 06:45:47 Starting candle/overloading/semantics
Nov 23 07:12:05 Finished candle/overloading/semantics                         26m15s   4GB
Nov 23 07:12:05 Starting pancake
Nov 23 07:16:07 Finished pancake                                               4m01s   2GB
Nov 23 07:16:07 Starting pancake/ffi
Nov 23 07:16:08 Finished pancake/ffi                                              0s   7MB
Nov 23 07:16:08 Starting pancake/semantics
Nov 23 07:21:11 Finished pancake/semantics                                     5m03s   1GB
Nov 23 07:21:12 Starting pancake/proofs
Nov 23 07:48:01 Finished pancake/proofs                                       26m49s   6GB
Nov 23 07:48:02 Starting characteristic/examples
Nov 23 07:50:53 Finished characteristic/examples                               2m51s   2GB
Nov 23 07:50:53 Starting tutorial/solutions
Nov 23 08:25:39 Finished tutorial/solutions                                   34m45s  13GB
Nov 23 08:25:40 Starting translator/monadic/examples
Nov 23 08:31:34 Finished translator/monadic/examples                           5m54s   2GB
Nov 23 08:31:34 Starting examples
Nov 23 08:48:38 Finished examples                                             17m03s   5GB
Nov 23 08:48:38 Starting examples/compilation/x64
Nov 23 14:14:35 Finished examples/compilation/x64                           5h25m56s  20GB
Nov 23 14:14:36 Starting examples/compilation/x64/proofs
Nov 23 14:18:24 Finished examples/compilation/x64/proofs                       3m47s   3GB
Nov 23 14:18:24 Starting examples/compilation/ag32
Nov 23 15:35:25 Finished examples/compilation/ag32                          1h17m00s   9GB
Nov 23 15:35:25 Starting examples/compilation/ag32/proofs
Nov 23 15:37:26 Finished examples/compilation/ag32/proofs                      2m00s   3GB
Nov 23 15:37:27 Starting examples/cost
Nov 23 16:01:21 FAILED: examples/cost
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[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)/compiler/backend[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$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                                                                                                                                                                                                        (0s)     OK
miniBasisProgTheory                                                                                                                                                                                                             (58s)     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                                                                                                                                                                                                              (59s)     OK
costPropsTheory                                                                                                                                                                                                                (155s)     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                                                                                                                                                                               (20m)     OK
Starting work on lcgLoopProofTheory
allProgTheory                                                                                                                                                                                                                   (19m)     OK
Starting work on allProofTheory
pureLoopProgTheory                                                                                                                                                                                                              (19m)     OK
Starting work on pureLoopProofTheory
lcgLoopProofTheory                                                                                                                                                                                                             (193s)FAIL<1>
         space := 0; tstamps := SOME ts0; peak_heap_length := pkheap0;
         stack := stk|>))  clk0  s.clock 
     ((res = Rerr (Rabort Rtimeout_error)) 
      (vv tsl.
         (res = Rval vv)  repchar_list vv (k + l) ts0  (stk = s.stack) 
         (repchar_to_tsl vv = SOME tsl)  repchar_safe_heap s tsl)  ts < ts0)
 
 failed.
 Failed to prove theorem n2l_acc_evaluate.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 512) (THEN1 on line 531) (THEN1 on line 542) (THEN1 on line 550) (THEN1 on line 574) (THEN1 on line 604) (THEN1 on line 614) (THEN1 on line 627)", origin_function = "find_term", origin_structure = "HolKernel"}
cyesProgTheory                                                                                                                                                                                                                  (20m)MKILLED
allProofTheory                                                                                                                                                                                                                 (132s)MKILLED
pureLoopProofTheory                                                                                                                                                                                                            (125s)MKILLED