Job 1482

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:773a7927a5af89e94a1c3bda992bdd7afb8fbb02
  Merge pull request #815 from hrutvik/master [Feb 23 15:27:11]
HOL:466ca124556d0d92defbe6ca514c428ca12727c9
  Prove theorems for Euler phi function, and a simple Chinese Remainder [Feb 17 00:14:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 24 10:52:54 Claimed job
Feb 24 10:52:58 Building HOL
Feb 24 11:08:44 Starting developers
Feb 24 11:08:48 Finished developers                                               4s 101MB
Feb 24 11:08:48 Starting developers/bin
Feb 24 11:08:56 Finished developers/bin                                           6s   1GB
Feb 24 11:08:56 Starting semantics/ffi
Feb 24 11:09:07 Finished semantics/ffi                                           11s 225MB
Feb 24 11:09:07 Starting semantics
Feb 24 11:10:44 Finished semantics                                             1m36s   1GB
Feb 24 11:10:44 Starting semantics/proofs
Feb 24 11:14:38 Finished semantics/proofs                                      3m53s   1GB
Feb 24 11:14:38 Starting basis/pure
Feb 24 11:17:44 Finished basis/pure                                            3m06s 925MB
Feb 24 11:17:45 Starting translator
Feb 24 11:21:21 Finished translator                                            3m36s   1GB
Feb 24 11:21:21 Starting compiler/parsing
Feb 24 11:22:38 Finished compiler/parsing                                      1m16s   2GB
Feb 24 11:22:38 Starting characteristic
Feb 24 11:28:33 Finished characteristic                                        5m54s   1GB
Feb 24 11:28:33 Starting translator/monadic
Feb 24 11:30:17 Finished translator/monadic                                    1m43s   1GB
Feb 24 11:30:17 Starting basis
Feb 24 12:19:21 Finished basis                                                49m03s  12GB
Feb 24 12:19:21 Starting compiler/inference
Feb 24 12:20:38 Finished compiler/inference                                    1m17s   1GB
Feb 24 12:20:39 Starting compiler/backend/reg_alloc
Feb 24 12:21:46 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 24 12:21:46 Starting compiler/backend/gc
Feb 24 12:25:40 Finished compiler/backend/gc                                   3m53s   2GB
Feb 24 12:25:40 Starting compiler/backend
Feb 24 12:30:46 Finished compiler/backend                                      5m05s   3GB
Feb 24 12:30:46 Starting compiler/encoders/asm
Feb 24 12:31:09 Finished compiler/encoders/asm                                   22s 717MB
Feb 24 12:31:09 Starting compiler/encoders/x64
Feb 24 12:32:15 Finished compiler/encoders/x64                                 1m06s 747MB
Feb 24 12:32:16 Starting compiler/encoders/arm7
Feb 24 12:34:26 Finished compiler/encoders/arm7                                2m10s   1GB
Feb 24 12:34:27 Starting compiler/encoders/arm8
Feb 24 12:35:06 Finished compiler/encoders/arm8                                  39s 698MB
Feb 24 12:35:07 Starting compiler/encoders/mips
Feb 24 12:36:43 Finished compiler/encoders/mips                                1m35s   1GB
Feb 24 12:36:43 Starting compiler/encoders/riscv
Feb 24 12:38:33 Finished compiler/encoders/riscv                               1m49s 971MB
Feb 24 12:38:33 Starting compiler/encoders/ag32
Feb 24 12:38:51 Finished compiler/encoders/ag32                                  18s 870MB
Feb 24 12:38:51 Starting compiler/backend/x64
Feb 24 12:39:12 Finished compiler/backend/x64                                    20s   1GB
Feb 24 12:39:12 Starting compiler/backend/arm7
Feb 24 12:39:34 Finished compiler/backend/arm7                                   21s   1GB
Feb 24 12:39:34 Starting compiler/backend/arm8
Feb 24 12:39:54 Finished compiler/backend/arm8                                   19s   1GB
Feb 24 12:39:54 Starting compiler/backend/mips
Feb 24 12:40:14 Finished compiler/backend/mips                                   19s   1GB
Feb 24 12:40:14 Starting compiler/backend/riscv
Feb 24 12:40:35 Finished compiler/backend/riscv                                  20s   1GB
Feb 24 12:40:35 Starting compiler/backend/ag32
Feb 24 12:41:48 Finished compiler/backend/ag32                                 1m13s   1GB
Feb 24 12:41:48 Starting compiler/parsing/proofs
Feb 24 12:48:00 Finished compiler/parsing/proofs                               6m11s   1GB
Feb 24 12:48:00 Starting compiler/inference/proofs
Feb 24 12:50:40 Finished compiler/inference/proofs                             2m39s   1GB
Feb 24 12:50:40 Starting compiler/backend/semantics
Feb 24 13:23:06 Finished compiler/backend/semantics                           32m25s   2GB
Feb 24 13:23:06 Starting compiler/backend/reg_alloc/proofs
Feb 24 13:26:54 Finished compiler/backend/reg_alloc/proofs                     3m48s 788MB
Feb 24 13:26:54 Starting compiler/backend/proofs
Feb 24 14:25:33 Finished compiler/backend/proofs                              58m37s  16GB
Feb 24 14:25:33 Starting compiler/encoders/x64/proofs
Feb 24 14:35:56 Finished compiler/encoders/x64/proofs                         10m23s   4GB
Feb 24 14:35:56 Starting compiler/encoders/arm7/proofs
Feb 24 14:50:06 Finished compiler/encoders/arm7/proofs                        14m09s   7GB
Feb 24 14:50:06 Starting compiler/encoders/arm8/proofs
Feb 24 14:57:06 Finished compiler/encoders/arm8/proofs                         7m00s   1GB
Feb 24 14:57:07 Starting compiler/encoders/mips/proofs
Feb 24 15:08:08 Finished compiler/encoders/mips/proofs                        11m01s   1GB
Feb 24 15:08:08 Starting compiler/encoders/riscv/proofs
Feb 24 15:17:40 Finished compiler/encoders/riscv/proofs                        9m31s   1GB
Feb 24 15:17:40 Starting compiler/encoders/ag32/proofs
Feb 24 15:20:30 Finished compiler/encoders/ag32/proofs                         2m49s 816MB
Feb 24 15:20:30 Starting compiler/backend/x64/proofs
Feb 24 15:20:52 Finished compiler/backend/x64/proofs                             22s   1GB
Feb 24 15:20:53 Starting compiler/backend/arm7/proofs
Feb 24 15:21:16 Finished compiler/backend/arm7/proofs                            23s   1GB
Feb 24 15:21:16 Starting compiler/backend/arm8/proofs
Feb 24 15:21:39 Finished compiler/backend/arm8/proofs                            22s   1GB
Feb 24 15:21:39 Starting compiler/backend/mips/proofs
Feb 24 15:22:02 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 24 15:22:02 Starting compiler/backend/riscv/proofs
Feb 24 15:22:25 Finished compiler/backend/riscv/proofs                           23s   1GB
Feb 24 15:22:25 Starting compiler/backend/ag32/proofs
Feb 24 15:36:01 Finished compiler/backend/ag32/proofs                         13m35s   2GB
Feb 24 15:36:01 Starting compiler/proofs
Feb 24 15:38:00 Finished compiler/proofs                                       1m58s   4GB
Feb 24 15:38:00 Starting candle/set-theory
Feb 24 15:38:29 Finished candle/set-theory                                       28s 739MB
Feb 24 15:38:29 Starting candle/syntax-lib
Feb 24 15:38:40 Finished candle/syntax-lib                                       10s 537MB
Feb 24 15:38:40 Starting candle/standard/syntax
Feb 24 15:40:35 Finished candle/standard/syntax                                1m54s 924MB
Feb 24 15:40:36 Starting candle/standard/semantics
Feb 24 15:42:25 Finished candle/standard/semantics                             1m49s   1GB
Feb 24 15:42:25 Starting candle/standard/monadic
Feb 24 15:44:15 Finished candle/standard/monadic                               1m50s   1GB
Feb 24 15:44:16 Starting candle/standard/ml_kernel
Feb 24 15:50:28 Finished candle/standard/ml_kernel                             6m12s   5GB
Feb 24 15:50:28 Starting candle/overloading/syntax
Feb 24 15:53:47 Finished candle/overloading/syntax                             3m18s   1GB
Feb 24 15:53:47 Starting candle/overloading/semantics
Feb 24 16:06:31 Finished candle/overloading/semantics                         12m43s   5GB
Feb 24 16:06:31 Starting characteristic/examples
Feb 24 16:07:56 Finished characteristic/examples                               1m24s   2GB
Feb 24 16:07:56 Starting tutorial/solutions
Feb 24 16:24:27 Finished tutorial/solutions                                   16m30s   8GB
Feb 24 16:24:27 Starting translator/monadic/examples
Feb 24 16:27:45 Finished translator/monadic/examples                           3m18s   2GB
Feb 24 16:27:45 Starting examples
Feb 24 16:36:57 Finished examples                                              9m11s   4GB
Feb 24 16:36:57 Starting examples/compilation/x64
Feb 24 19:06:59 Finished examples/compilation/x64                           2h30m01s  22GB
Feb 24 19:06:59 Starting examples/compilation/x64/proofs
Feb 24 19:09:00 Finished examples/compilation/x64/proofs                       2m00s   3GB
Feb 24 19:09:00 Starting examples/compilation/ag32
Feb 24 19:44:55 Finished examples/compilation/ag32                            35m54s   7GB
Feb 24 19:44:55 Starting examples/compilation/ag32/proofs
Feb 24 19:45:44 Finished examples/compilation/ag32/proofs                        48s   3GB
Feb 24 19:45:44 Starting examples/cost
Feb 24 20:00:28 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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/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:   29s  user:   28s     OK
miniBasisProgTheory                             real:   30s  user:   29s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                 real:   99s  user:   95s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  659s  user:  725s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  635s  user:  688s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  648s  user:  706s     OK
Starting work on allProofTheory
pureLoopProofTheory                             real:  147s  user:  143sFAIL<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