Job 1666

CakeML:3d15cac6c791de5a4fae0e2e67b908fc66a93e19
  Fix following changes to gs [Nov 25 21:17:42]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic [Nov 23 06:58:28]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 25 21:22:34 Claimed job
Nov 25 21:22:42 Reusing HOL
Nov 25 21:23:20 Starting developers
Nov 25 21:23:24 Finished developers                                               4s 147MB
Nov 25 21:23:24 Starting developers/bin
Nov 25 21:23:31 Finished developers/bin                                           6s   1GB
Nov 25 21:23:31 Starting semantics/ffi
Nov 25 21:23:40 Finished semantics/ffi                                            9s 225MB
Nov 25 21:23:40 Starting semantics
Nov 25 21:25:03 Finished semantics                                             1m23s   1GB
Nov 25 21:25:03 Starting semantics/proofs
Nov 25 21:28:32 Finished semantics/proofs                                      3m28s   1GB
Nov 25 21:28:32 Starting semantics/alt_semantics
Nov 25 21:28:43 Finished semantics/alt_semantics                                 11s 362MB
Nov 25 21:28:44 Starting semantics/alt_semantics/proofs
Nov 25 21:31:08 Finished semantics/alt_semantics/proofs                        2m24s 846MB
Nov 25 21:31:08 Starting basis/pure
Nov 25 21:31:58 Finished basis/pure                                              49s 924MB
Nov 25 21:31:58 Starting translator
Nov 25 21:34:46 Finished translator                                            2m47s   1GB
Nov 25 21:34:46 Starting compiler/parsing
Nov 25 21:36:01 Finished compiler/parsing                                      1m14s   2GB
Nov 25 21:36:01 Starting characteristic
Nov 25 21:41:43 Finished characteristic                                        5m41s   2GB
Nov 25 21:41:43 Starting translator/monadic
Nov 25 21:43:24 Finished translator/monadic                                    1m41s   1GB
Nov 25 21:43:25 Starting basis
Nov 25 22:29:20 Finished basis                                                45m54s  16GB
Nov 25 22:29:20 Starting compiler/inference
Nov 25 22:30:29 Finished compiler/inference                                    1m08s   1GB
Nov 25 22:30:30 Starting compiler/backend/reg_alloc
Nov 25 22:31:37 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 25 22:31:37 Starting compiler/backend/gc
Nov 25 22:34:54 Finished compiler/backend/gc                                   3m17s   2GB
Nov 25 22:34:54 Starting compiler/backend
Nov 25 22:39:09 Finished compiler/backend                                      4m15s   2GB
Nov 25 22:39:10 Starting compiler/encoders/asm
Nov 25 22:39:33 Finished compiler/encoders/asm                                   22s 731MB
Nov 25 22:39:33 Starting compiler/encoders/x64
Nov 25 22:39:59 Finished compiler/encoders/x64                                   25s 872MB
Nov 25 22:39:59 Starting compiler/encoders/arm7
Nov 25 22:40:50 Finished compiler/encoders/arm7                                  51s   1GB
Nov 25 22:40:50 Starting compiler/encoders/arm8
Nov 25 22:41:04 Finished compiler/encoders/arm8                                  13s 963MB
Nov 25 22:41:04 Starting compiler/encoders/mips
Nov 25 22:41:22 Finished compiler/encoders/mips                                  17s   1GB
Nov 25 22:41:22 Starting compiler/encoders/riscv
Nov 25 22:41:39 Finished compiler/encoders/riscv                                 16s 805MB
Nov 25 22:41:39 Starting compiler/encoders/ag32
Nov 25 22:41:57 Finished compiler/encoders/ag32                                  18s 918MB
Nov 25 22:41:57 Starting compiler/backend/x64
Nov 25 22:42:16 Finished compiler/backend/x64                                    18s   1GB
Nov 25 22:42:16 Starting compiler/backend/arm7
Nov 25 22:42:35 Finished compiler/backend/arm7                                   18s   1GB
Nov 25 22:42:35 Starting compiler/backend/arm8
Nov 25 22:42:55 Finished compiler/backend/arm8                                   19s   1GB
Nov 25 22:42:55 Starting compiler/backend/mips
Nov 25 22:43:15 Finished compiler/backend/mips                                   19s   1GB
Nov 25 22:43:15 Starting compiler/backend/riscv
Nov 25 22:43:35 Finished compiler/backend/riscv                                  19s   1GB
Nov 25 22:43:35 Starting compiler/backend/ag32
Nov 25 22:44:43 Finished compiler/backend/ag32                                 1m07s   1GB
Nov 25 22:44:43 Starting compiler/parsing/proofs
Nov 25 22:48:24 Finished compiler/parsing/proofs                               3m41s   1GB
Nov 25 22:48:25 Starting compiler/inference/proofs
Nov 25 22:50:48 Finished compiler/inference/proofs                             2m23s 908MB
Nov 25 22:50:48 Starting compiler/backend/semantics
Nov 25 23:18:39 Finished compiler/backend/semantics                           27m51s   3GB
Nov 25 23:18:39 Starting compiler/backend/reg_alloc/proofs
Nov 25 23:22:02 Finished compiler/backend/reg_alloc/proofs                     3m22s   1GB
Nov 25 23:22:02 Starting compiler/backend/proofs
Nov 26 00:12:09 Finished compiler/backend/proofs                              50m04s  19GB
Nov 26 00:12:09 Starting compiler/backend/serialiser
Nov 26 00:13:21 Finished compiler/backend/serialiser                           1m11s   1GB
Nov 26 00:13:21 Starting compiler/encoders/x64/proofs
Nov 26 00:22:58 Finished compiler/encoders/x64/proofs                          9m37s   4GB
Nov 26 00:22:59 Starting compiler/encoders/arm7/proofs
Nov 26 00:36:04 Finished compiler/encoders/arm7/proofs                        13m05s   3GB
Nov 26 00:36:04 Starting compiler/encoders/arm8/proofs
Nov 26 00:42:47 Finished compiler/encoders/arm8/proofs                         6m43s   1GB
Nov 26 00:42:48 Starting compiler/encoders/mips/proofs
Nov 26 00:52:38 Finished compiler/encoders/mips/proofs                         9m50s   2GB
Nov 26 00:52:38 Starting compiler/encoders/riscv/proofs
Nov 26 01:01:32 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Nov 26 01:01:32 Starting compiler/encoders/ag32/proofs
Nov 26 01:04:07 Finished compiler/encoders/ag32/proofs                         2m34s 659MB
Nov 26 01:04:07 Starting compiler/backend/x64/proofs
Nov 26 01:04:30 Finished compiler/backend/x64/proofs                             22s   1GB
Nov 26 01:04:30 Starting compiler/backend/arm7/proofs
Nov 26 01:04:54 Finished compiler/backend/arm7/proofs                            23s   1GB
Nov 26 01:04:54 Starting compiler/backend/arm8/proofs
Nov 26 01:05:18 Finished compiler/backend/arm8/proofs                            23s   1GB
Nov 26 01:05:18 Starting compiler/backend/mips/proofs
Nov 26 01:05:40 Finished compiler/backend/mips/proofs                            21s   1GB
Nov 26 01:05:40 Starting compiler/backend/riscv/proofs
Nov 26 01:06:03 Finished compiler/backend/riscv/proofs                           22s   1GB
Nov 26 01:06:03 Starting compiler/backend/ag32/proofs
Nov 26 01:18:54 Finished compiler/backend/ag32/proofs                         12m49s   2GB
Nov 26 01:18:54 Starting compiler/proofs
Nov 26 01:20:36 Finished compiler/proofs                                       1m42s   3GB
Nov 26 01:20:36 Starting candle/set-theory
Nov 26 01:21:06 Finished candle/set-theory                                       29s 885MB
Nov 26 01:21:06 Starting candle/syntax-lib
Nov 26 01:21:16 Finished candle/syntax-lib                                       10s 687MB
Nov 26 01:21:17 Starting candle/standard/syntax
Nov 26 01:23:05 Finished candle/standard/syntax                                1m48s 987MB
Nov 26 01:23:06 Starting candle/standard/semantics
Nov 26 01:24:48 Finished candle/standard/semantics                             1m42s   1GB
Nov 26 01:24:48 Starting candle/standard/monadic
Nov 26 01:26:31 Finished candle/standard/monadic                               1m42s   1GB
Nov 26 01:26:31 Starting candle/standard/ml_kernel
Nov 26 01:32:00 Finished candle/standard/ml_kernel                             5m29s   3GB
Nov 26 01:32:00 Starting candle/overloading/syntax
Nov 26 01:35:02 Finished candle/overloading/syntax                             3m01s   1GB
Nov 26 01:35:02 Starting candle/overloading/semantics
Nov 26 01:46:34 Finished candle/overloading/semantics                         11m31s   2GB
Nov 26 01:46:35 Starting pancake
Nov 26 01:48:28 Finished pancake                                               1m52s   2GB
Nov 26 01:48:28 Starting pancake/ffi
Nov 26 01:48:28 Finished pancake/ffi                                              0s   8MB
Nov 26 01:48:29 Starting pancake/semantics
Nov 26 01:50:41 Finished pancake/semantics                                     2m12s   1GB
Nov 26 01:50:41 Starting pancake/proofs
Nov 26 02:02:20 Finished pancake/proofs                                       11m38s   6GB
Nov 26 02:02:20 Starting characteristic/examples
Nov 26 02:03:40 Finished characteristic/examples                               1m20s   3GB
Nov 26 02:03:40 Starting tutorial/solutions
Nov 26 02:19:45 Finished tutorial/solutions                                   16m03s   9GB
Nov 26 02:19:45 Starting translator/monadic/examples
Nov 26 02:23:07 Finished translator/monadic/examples                           3m21s   2GB
Nov 26 02:23:07 Starting examples
Nov 26 02:32:24 Finished examples                                              9m16s   3GB
Nov 26 02:32:24 Starting examples/compilation/x64
Nov 26 04:59:59 Finished examples/compilation/x64                           2h27m32s  21GB
Nov 26 04:59:59 Starting examples/compilation/x64/proofs
Nov 26 05:01:42 Finished examples/compilation/x64/proofs                       1m43s   2GB
Nov 26 05:01:42 Starting examples/compilation/ag32
Nov 26 05:35:59 Finished examples/compilation/ag32                            34m16s   9GB
Nov 26 05:35:59 Starting examples/compilation/ag32/proofs
Nov 26 05:36:46 Finished examples/compilation/ag32/proofs                        46s   2GB
Nov 26 05:36:46 Starting examples/cost
Nov 26 05:52:10 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[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                                                                                        (28s)     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                                                                                         (29s)     OK
costPropsTheory                                                                                            (79s)     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                                                         (650s)     OK
Starting work on lcgLoopProofTheory
allProgTheory                                                                                             (614s)     OK
Starting work on allProofTheory
pureLoopProgTheory                                                                                        (618s)     OK
Starting work on pureLoopProofTheory
pureLoopProofTheory                                                                                       (193s)     OK
Starting work on reverseProgTheory
allProofTheory                                                                                            (243s)     OK
Starting work on sumProgTheory
lcgLoopProofTheory                                                                                        (293s)FAIL<1>
 Proof of 
 
 s x m c a.
   (s.locals = fromList [x; m; c; a]) 
   (lookup_lcgLoop s.code = SOME (4,lcgLoop_body)) 
   s' e. evaluate (lcgLoop_body,s) = (SOME (Rerr e),s')
 
 failed.
 Failed to prove theorem data_safe_lcgLoop_code_abort.
 Uncaught exception: HOL_ERR {message = "", origin_function = "GEN_COND_CASES_TAC", origin_structure = "Tactic"}
cyesProgTheory                                                                                            (853s)MKILLED
reverseProgTheory                                                                                          (61s)MKILLED
sumProgTheory                                                                                              (20s)MKILLED