Job 1480

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:8b4b25e299c212b467006f5971532007b18ad96c
  Merge pull request #816 from arolle/cyclicity-check [Feb 21 11:01:26]
HOL:466ca124556d0d92defbe6ca514c428ca12727c9
  Prove theorems for Euler phi function, and a simple Chinese Remainder [Feb 17 00:14:31]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 23 09:39:48 Claimed job
Feb 23 09:39:53 Building HOL
Feb 23 09:54:09 Starting developers
Feb 23 09:54:11 Finished developers                                               2s 104MB
Feb 23 09:54:11 Starting developers/bin
Feb 23 09:54:18 Finished developers/bin                                           6s   1GB
Feb 23 09:54:18 Starting semantics/ffi
Feb 23 09:54:28 Finished semantics/ffi                                           10s 286MB
Feb 23 09:54:28 Starting semantics
Feb 23 09:56:01 Finished semantics                                             1m31s   1GB
Feb 23 09:56:01 Starting semantics/proofs
Feb 23 09:59:31 Finished semantics/proofs                                      3m30s   1GB
Feb 23 09:59:31 Starting basis/pure
Feb 23 10:02:15 Finished basis/pure                                            2m44s   1GB
Feb 23 10:02:15 Starting translator
Feb 23 10:05:33 Finished translator                                            3m17s   2GB
Feb 23 10:05:33 Starting compiler/parsing
Feb 23 10:06:41 Finished compiler/parsing                                      1m07s   4GB
Feb 23 10:06:41 Starting characteristic
Feb 23 10:12:19 Finished characteristic                                        5m37s   3GB
Feb 23 10:12:20 Starting translator/monadic
Feb 23 10:14:06 Finished translator/monadic                                    1m46s   2GB
Feb 23 10:14:06 Starting basis
Feb 23 10:57:50 Finished basis                                                43m42s  29GB
Feb 23 10:57:50 Starting compiler/inference
Feb 23 10:59:00 Finished compiler/inference                                    1m10s   1GB
Feb 23 10:59:00 Starting compiler/backend/reg_alloc
Feb 23 11:00:04 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 23 11:00:04 Starting compiler/backend/gc
Feb 23 11:03:38 Finished compiler/backend/gc                                   3m33s   2GB
Feb 23 11:03:38 Starting compiler/backend
Feb 23 11:08:44 Finished compiler/backend                                      5m05s   4GB
Feb 23 11:08:44 Starting compiler/encoders/asm
Feb 23 11:09:06 Finished compiler/encoders/asm                                   21s   1GB
Feb 23 11:09:06 Starting compiler/encoders/x64
Feb 23 11:10:09 Finished compiler/encoders/x64                                 1m02s   1GB
Feb 23 11:10:09 Starting compiler/encoders/arm7
Feb 23 11:12:12 Finished compiler/encoders/arm7                                2m02s   1GB
Feb 23 11:12:12 Starting compiler/encoders/arm8
Feb 23 11:12:50 Finished compiler/encoders/arm8                                  37s   1GB
Feb 23 11:12:50 Starting compiler/encoders/mips
Feb 23 11:14:16 Finished compiler/encoders/mips                                1m25s   1GB
Feb 23 11:14:16 Starting compiler/encoders/riscv
Feb 23 11:15:55 Finished compiler/encoders/riscv                               1m38s   1GB
Feb 23 11:15:55 Starting compiler/encoders/ag32
Feb 23 11:16:13 Finished compiler/encoders/ag32                                  18s 938MB
Feb 23 11:16:14 Starting compiler/backend/x64
Feb 23 11:16:32 Finished compiler/backend/x64                                    18s   1GB
Feb 23 11:16:32 Starting compiler/backend/arm7
Feb 23 11:16:55 Finished compiler/backend/arm7                                   22s   1GB
Feb 23 11:16:55 Starting compiler/backend/arm8
Feb 23 11:17:15 Finished compiler/backend/arm8                                   19s   1GB
Feb 23 11:17:15 Starting compiler/backend/mips
Feb 23 11:17:36 Finished compiler/backend/mips                                   20s   1GB
Feb 23 11:17:36 Starting compiler/backend/riscv
Feb 23 11:17:57 Finished compiler/backend/riscv                                  20s   1GB
Feb 23 11:17:57 Starting compiler/backend/ag32
Feb 23 11:19:06 Finished compiler/backend/ag32                                 1m08s   2GB
Feb 23 11:19:06 Starting compiler/parsing/proofs
Feb 23 11:24:46 Finished compiler/parsing/proofs                               5m39s   2GB
Feb 23 11:24:46 Starting compiler/inference/proofs
Feb 23 11:27:19 Finished compiler/inference/proofs                             2m32s   2GB
Feb 23 11:27:19 Starting compiler/backend/semantics
Feb 23 11:54:04 Finished compiler/backend/semantics                           26m44s   3GB
Feb 23 11:54:04 Starting compiler/backend/reg_alloc/proofs
Feb 23 11:57:23 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Feb 23 11:57:23 Starting compiler/backend/proofs
Feb 23 12:50:47 Finished compiler/backend/proofs                              53m23s  16GB
Feb 23 12:50:47 Starting compiler/encoders/x64/proofs
Feb 23 13:00:08 Finished compiler/encoders/x64/proofs                          9m21s   6GB
Feb 23 13:00:09 Starting compiler/encoders/arm7/proofs
Feb 23 13:12:45 Finished compiler/encoders/arm7/proofs                        12m36s   7GB
Feb 23 13:12:45 Starting compiler/encoders/arm8/proofs
Feb 23 13:18:59 Finished compiler/encoders/arm8/proofs                         6m13s   3GB
Feb 23 13:18:59 Starting compiler/encoders/mips/proofs
Feb 23 13:28:38 Finished compiler/encoders/mips/proofs                         9m38s   5GB
Feb 23 13:28:38 Starting compiler/encoders/riscv/proofs
Feb 23 13:37:05 Finished compiler/encoders/riscv/proofs                        8m27s   3GB
Feb 23 13:37:06 Starting compiler/encoders/ag32/proofs
Feb 23 13:39:26 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Feb 23 13:39:27 Starting compiler/backend/x64/proofs
Feb 23 13:39:49 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 23 13:39:49 Starting compiler/backend/arm7/proofs
Feb 23 13:40:12 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 23 13:40:12 Starting compiler/backend/arm8/proofs
Feb 23 13:40:32 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 23 13:40:33 Starting compiler/backend/mips/proofs
Feb 23 13:40:54 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 23 13:40:54 Starting compiler/backend/riscv/proofs
Feb 23 13:41:18 Finished compiler/backend/riscv/proofs                           23s   2GB
Feb 23 13:41:18 Starting compiler/backend/ag32/proofs
Feb 23 13:53:17 Finished compiler/backend/ag32/proofs                         11m58s   4GB
Feb 23 13:53:17 Starting compiler/proofs
Feb 23 13:55:14 Finished compiler/proofs                                       1m57s   6GB
Feb 23 13:55:15 Starting candle/set-theory
Feb 23 13:55:44 Finished candle/set-theory                                       29s   1GB
Feb 23 13:55:44 Starting candle/syntax-lib
Feb 23 13:55:55 Finished candle/syntax-lib                                       10s 790MB
Feb 23 13:55:55 Starting candle/standard/syntax
Feb 23 13:57:43 Finished candle/standard/syntax                                1m47s   1GB
Feb 23 13:57:43 Starting candle/standard/semantics
Feb 23 13:59:28 Finished candle/standard/semantics                             1m45s   2GB
Feb 23 13:59:29 Starting candle/standard/monadic
Feb 23 14:01:10 Finished candle/standard/monadic                               1m41s   1GB
Feb 23 14:01:10 Starting candle/standard/ml_kernel
Feb 23 14:06:45 Finished candle/standard/ml_kernel                             5m34s   6GB
Feb 23 14:06:46 Starting candle/overloading/syntax
Feb 23 14:09:53 Finished candle/overloading/syntax                             3m07s   2GB
Feb 23 14:09:54 Starting candle/overloading/semantics
Feb 23 14:21:56 Finished candle/overloading/semantics                         12m02s   8GB
Feb 23 14:21:56 Starting characteristic/examples
Feb 23 14:23:16 Finished characteristic/examples                               1m19s   4GB
Feb 23 14:23:16 Starting tutorial/solutions
Feb 23 14:38:53 Finished tutorial/solutions                                   15m36s  16GB
Feb 23 14:38:53 Starting translator/monadic/examples
Feb 23 14:42:14 Finished translator/monadic/examples                           3m21s   4GB
Feb 23 14:42:15 Starting examples
Feb 23 14:51:07 Finished examples                                              8m52s   7GB
Feb 23 14:51:07 Starting examples/compilation/x64
Feb 23 17:13:51 Finished examples/compilation/x64                           2h22m43s  21GB
Feb 23 17:13:51 Starting examples/compilation/x64/proofs
Feb 23 17:15:52 Finished examples/compilation/x64/proofs                       2m00s   3GB
Feb 23 17:15:52 Starting examples/compilation/ag32
Feb 23 17:50:05 Finished examples/compilation/ag32                            34m12s  12GB
Feb 23 17:50:05 Starting examples/compilation/ag32/proofs
Feb 23 17:50:56 Finished examples/compilation/ag32/proofs                        50s   5GB
Feb 23 17:50:56 Starting examples/cost
Feb 23 18:05:56 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/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[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/reachability/proofs[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:   32s  user:   31s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                                               real:   96s  user:   92s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                             real:  669s  user:  727s     OK
Starting work on lcgLoopProofTheory
allProgTheory                                                                 real:  631s  user:  680s     OK
Starting work on allProofTheory
pureLoopProgTheory                                                            real:  648s  user:  689s     OK
Starting work on pureLoopProofTheory
pureLoopProofTheory                                                           real:  151s  user:  147sFAIL<1>
        (App Opapp [Var (Short "pureLoop"); Lit (IntLit 1)])] (1000,1000)
 
 failed.
 Failed to prove theorem data_safe_pureLoop.
 
 Exception raised at Q.MATCH_GOALSUB_ABBREV_TAC:
 No matching sub-term found
 error in quse /home/myreen/regression/cakeml-1480/examples/cost/pureLoopProofScript.sml : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 error in load /home/myreen/regression/cakeml-1480/examples/cost/pureLoopProofScript : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 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