Job 1499

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:9c2de3ee5f524d70e727448b250ce0f8f085ee53
  Merge pull request #820 from CakeML/fix-export-x64-macos [Mar 22 20:43:15]
HOL:ab03cec5200c8b23f9ba60c5cea958cfcd0cd158
  Make all string overloads "inferior" [Mar 23 06:14:09]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 25 10:25:23 Claimed job
Mar 25 10:25:28 Building HOL
Mar 25 10:41:47 Starting developers
Mar 25 10:41:51 Finished developers                                               4s 109MB
Mar 25 10:41:51 Starting developers/bin
Mar 25 10:41:58 Finished developers/bin                                           6s   1GB
Mar 25 10:41:59 Starting semantics/ffi
Mar 25 10:42:10 Finished semantics/ffi                                           11s 237MB
Mar 25 10:42:10 Starting semantics
Mar 25 10:43:47 Finished semantics                                             1m36s   1GB
Mar 25 10:43:47 Starting semantics/proofs
Mar 25 10:47:38 Finished semantics/proofs                                      3m50s   1GB
Mar 25 10:47:39 Starting basis/pure
Mar 25 10:50:47 Finished basis/pure                                            3m08s 875MB
Mar 25 10:50:47 Starting translator
Mar 25 10:54:26 Finished translator                                            3m39s   1GB
Mar 25 10:54:27 Starting compiler/parsing
Mar 25 10:55:42 Finished compiler/parsing                                      1m15s   2GB
Mar 25 10:55:43 Starting characteristic
Mar 25 11:01:41 Finished characteristic                                        5m58s   2GB
Mar 25 11:01:42 Starting translator/monadic
Mar 25 11:03:26 Finished translator/monadic                                    1m43s   1GB
Mar 25 11:03:26 Starting basis
Mar 25 11:50:58 Finished basis                                                47m31s  10GB
Mar 25 11:50:58 Starting compiler/inference
Mar 25 11:52:16 Finished compiler/inference                                    1m17s   1GB
Mar 25 11:52:17 Starting compiler/backend/reg_alloc
Mar 25 11:53:26 Finished compiler/backend/reg_alloc                            1m09s   1GB
Mar 25 11:53:26 Starting compiler/backend/gc
Mar 25 11:57:17 Finished compiler/backend/gc                                   3m50s   2GB
Mar 25 11:57:17 Starting compiler/backend
Mar 25 12:02:30 Finished compiler/backend                                      5m12s   4GB
Mar 25 12:02:30 Starting compiler/encoders/asm
Mar 25 12:02:54 Finished compiler/encoders/asm                                   23s 757MB
Mar 25 12:02:54 Starting compiler/encoders/x64
Mar 25 12:04:00 Finished compiler/encoders/x64                                 1m05s 995MB
Mar 25 12:04:00 Starting compiler/encoders/arm7
Mar 25 12:06:13 Finished compiler/encoders/arm7                                2m12s   1GB
Mar 25 12:06:13 Starting compiler/encoders/arm8
Mar 25 12:06:53 Finished compiler/encoders/arm8                                  40s 584MB
Mar 25 12:06:54 Starting compiler/encoders/mips
Mar 25 12:08:30 Finished compiler/encoders/mips                                1m36s   1GB
Mar 25 12:08:31 Starting compiler/encoders/riscv
Mar 25 12:10:19 Finished compiler/encoders/riscv                               1m48s   1GB
Mar 25 12:10:20 Starting compiler/encoders/ag32
Mar 25 12:10:39 Finished compiler/encoders/ag32                                  18s 830MB
Mar 25 12:10:39 Starting compiler/backend/x64
Mar 25 12:10:59 Finished compiler/backend/x64                                    19s   1GB
Mar 25 12:10:59 Starting compiler/backend/arm7
Mar 25 12:11:21 Finished compiler/backend/arm7                                   21s   1GB
Mar 25 12:11:21 Starting compiler/backend/arm8
Mar 25 12:11:41 Finished compiler/backend/arm8                                   19s   1GB
Mar 25 12:11:41 Starting compiler/backend/mips
Mar 25 12:12:03 Finished compiler/backend/mips                                   20s   1GB
Mar 25 12:12:03 Starting compiler/backend/riscv
Mar 25 12:12:22 Finished compiler/backend/riscv                                  18s   1GB
Mar 25 12:12:22 Starting compiler/backend/ag32
Mar 25 12:13:35 Finished compiler/backend/ag32                                 1m13s   1GB
Mar 25 12:13:36 Starting compiler/parsing/proofs
Mar 25 12:19:46 Finished compiler/parsing/proofs                               6m10s   1GB
Mar 25 12:19:46 Starting compiler/inference/proofs
Mar 25 12:22:25 Finished compiler/inference/proofs                             2m38s   1GB
Mar 25 12:22:25 Starting compiler/backend/semantics
Mar 25 12:55:33 Finished compiler/backend/semantics                           33m07s   2GB
Mar 25 12:55:34 Starting compiler/backend/reg_alloc/proofs
Mar 25 12:59:26 Finished compiler/backend/reg_alloc/proofs                     3m52s 795MB
Mar 25 12:59:26 Starting compiler/backend/proofs
Mar 25 13:58:19 Finished compiler/backend/proofs                              58m50s  17GB
Mar 25 13:58:19 Starting compiler/encoders/x64/proofs
Mar 25 14:08:47 Finished compiler/encoders/x64/proofs                         10m27s   4GB
Mar 25 14:08:47 Starting compiler/encoders/arm7/proofs
Mar 25 14:23:03 Finished compiler/encoders/arm7/proofs                        14m15s   6GB
Mar 25 14:23:03 Starting compiler/encoders/arm8/proofs
Mar 25 14:30:10 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Mar 25 14:30:10 Starting compiler/encoders/mips/proofs
Mar 25 14:40:48 Finished compiler/encoders/mips/proofs                        10m37s   3GB
Mar 25 14:40:49 Starting compiler/encoders/riscv/proofs
Mar 25 14:50:19 Finished compiler/encoders/riscv/proofs                        9m30s   1GB
Mar 25 14:50:19 Starting compiler/encoders/ag32/proofs
Mar 25 14:53:09 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Mar 25 14:53:09 Starting compiler/backend/x64/proofs
Mar 25 14:53:32 Finished compiler/backend/x64/proofs                             23s   1GB
Mar 25 14:53:32 Starting compiler/backend/arm7/proofs
Mar 25 14:53:56 Finished compiler/backend/arm7/proofs                            23s   1GB
Mar 25 14:53:56 Starting compiler/backend/arm8/proofs
Mar 25 14:54:18 Finished compiler/backend/arm8/proofs                            21s   1GB
Mar 25 14:54:18 Starting compiler/backend/mips/proofs
Mar 25 14:54:42 Finished compiler/backend/mips/proofs                            23s   1GB
Mar 25 14:54:42 Starting compiler/backend/riscv/proofs
Mar 25 14:55:04 Finished compiler/backend/riscv/proofs                           22s   1GB
Mar 25 14:55:04 Starting compiler/backend/ag32/proofs
Mar 25 15:08:43 Finished compiler/backend/ag32/proofs                         13m37s   2GB
Mar 25 15:08:43 Starting compiler/proofs
Mar 25 15:10:42 Finished compiler/proofs                                       1m58s   2GB
Mar 25 15:10:42 Starting candle/set-theory
Mar 25 15:11:11 Finished candle/set-theory                                       29s 861MB
Mar 25 15:11:12 Starting candle/syntax-lib
Mar 25 15:11:23 Finished candle/syntax-lib                                       11s 449MB
Mar 25 15:11:23 Starting candle/standard/syntax
Mar 25 15:13:19 Finished candle/standard/syntax                                1m55s 947MB
Mar 25 15:13:19 Starting candle/standard/semantics
Mar 25 15:15:08 Finished candle/standard/semantics                             1m48s   1GB
Mar 25 15:15:08 Starting candle/standard/monadic
Mar 25 15:17:00 Finished candle/standard/monadic                               1m51s   1GB
Mar 25 15:17:00 Starting candle/standard/ml_kernel
Mar 25 15:23:10 Finished candle/standard/ml_kernel                             6m09s   4GB
Mar 25 15:23:10 Starting candle/overloading/syntax
Mar 25 15:26:32 Finished candle/overloading/syntax                             3m21s   1GB
Mar 25 15:26:32 Starting candle/overloading/semantics
Mar 25 15:39:37 Finished candle/overloading/semantics                         13m04s   2GB
Mar 25 15:39:38 Starting characteristic/examples
Mar 25 15:41:01 Finished characteristic/examples                               1m23s   3GB
Mar 25 15:41:01 Starting tutorial/solutions
Mar 25 15:57:07 Finished tutorial/solutions                                   16m05s   8GB
Mar 25 15:57:07 Starting translator/monadic/examples
Mar 25 16:00:31 Finished translator/monadic/examples                           3m23s   2GB
Mar 25 16:00:31 Starting examples
Mar 25 16:09:40 Finished examples                                              9m08s   4GB
Mar 25 16:09:40 Starting examples/compilation/x64
Mar 25 18:40:01 Finished examples/compilation/x64                           2h30m20s  15GB
Mar 25 18:40:02 Starting examples/compilation/x64/proofs
Mar 25 18:41:56 Finished examples/compilation/x64/proofs                       1m54s   3GB
Mar 25 18:41:56 Starting examples/compilation/ag32
Mar 25 19:17:08 Finished examples/compilation/ag32                            35m11s   7GB
Mar 25 19:17:08 Starting examples/compilation/ag32/proofs
Mar 25 19:17:58 Finished examples/compilation/ag32/proofs                        49s   4GB
Mar 25 19:17:58 Starting examples/cost
Mar 25 19:32:44 FAILED: examples/cost
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)/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)/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                                       real:    0s  user:    0s     OK
size_ofPropsTheory                              real:   31s  user:   29s     OK
miniBasisProgTheory                             real:   31s  user:   29s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                 real:   97s  user:   94s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  662s  user:  731s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  633s  user:  682s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  658s  user:  706s     OK
Starting work on allProofTheory
pureLoopProofTheory                             real:  150s  user:  146sFAIL<1>
           <|row := 1; col := 41; offset := 0|>)
        [("pureLoop","x",App Opapp [Var (Short "pureLoop"); Var (Short "x")])];
      Dlet
        (Locs <|row := 2; col := 4; offset := 0|>
           <|row := 2; col := 21; offset := 0|>) Pany
        (App Opapp [Var (Short "pureLoop"); Lit (IntLit 1)])] (1000,1000)
 
 failed.
 Failed to prove theorem data_safe_pureLoop.
 Uncaught exception: HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
cyesProgTheory                                                          M-KILLED
lcgLoopProofTheory                                                      M-KILLED
allProofTheory                                                          M-KILLED