Job 1471

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:583808f6196b34844469aa95cb78bf855a62d80a
  Provide machinery for storing ssfragments by name in global db [Feb 08 06:30:26]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 09 11:43:11 Claimed job
Feb 09 11:43:19 Building HOL
Feb 09 11:57:38 Starting developers
Feb 09 11:57:38 Finished developers                                               0s  34MB
Feb 09 11:57:38 Starting developers/bin
Feb 09 11:57:45 Finished developers/bin                                           6s   1GB
Feb 09 11:57:45 Starting semantics/ffi
Feb 09 11:57:55 Finished semantics/ffi                                           10s 318MB
Feb 09 11:57:55 Starting semantics
Feb 09 11:59:30 Finished semantics                                             1m34s   1GB
Feb 09 11:59:30 Starting semantics/proofs
Feb 09 12:03:04 Finished semantics/proofs                                      3m33s   1GB
Feb 09 12:03:04 Starting basis/pure
Feb 09 12:05:45 Finished basis/pure                                            2m41s   1GB
Feb 09 12:05:46 Starting translator
Feb 09 12:09:04 Finished translator                                            3m18s   2GB
Feb 09 12:09:04 Starting compiler/parsing
Feb 09 12:10:13 Finished compiler/parsing                                      1m08s   2GB
Feb 09 12:10:13 Starting characteristic
Feb 09 12:15:52 Finished characteristic                                        5m38s   3GB
Feb 09 12:15:52 Starting translator/monadic
Feb 09 12:17:38 Finished translator/monadic                                    1m45s   3GB
Feb 09 12:17:38 Starting basis
Feb 09 13:01:34 Finished basis                                                43m55s  31GB
Feb 09 13:01:34 Starting compiler/inference
Feb 09 13:02:48 Finished compiler/inference                                    1m13s   2GB
Feb 09 13:02:48 Starting compiler/backend/reg_alloc
Feb 09 13:03:52 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 09 13:03:52 Starting compiler/backend/gc
Feb 09 13:07:27 Finished compiler/backend/gc                                   3m34s   3GB
Feb 09 13:07:27 Starting compiler/backend
Feb 09 13:12:34 Finished compiler/backend                                      5m06s   5GB
Feb 09 13:12:34 Starting compiler/encoders/asm
Feb 09 13:12:56 Finished compiler/encoders/asm                                   22s   1GB
Feb 09 13:12:56 Starting compiler/encoders/x64
Feb 09 13:13:59 Finished compiler/encoders/x64                                 1m02s   1GB
Feb 09 13:13:59 Starting compiler/encoders/arm7
Feb 09 13:16:00 Finished compiler/encoders/arm7                                2m00s   1GB
Feb 09 13:16:00 Starting compiler/encoders/arm8
Feb 09 13:16:38 Finished compiler/encoders/arm8                                  38s   1GB
Feb 09 13:16:39 Starting compiler/encoders/mips
Feb 09 13:18:05 Finished compiler/encoders/mips                                1m25s   1GB
Feb 09 13:18:05 Starting compiler/encoders/riscv
Feb 09 13:19:42 Finished compiler/encoders/riscv                               1m36s   1GB
Feb 09 13:19:42 Starting compiler/encoders/ag32
Feb 09 13:20:00 Finished compiler/encoders/ag32                                  18s 943MB
Feb 09 13:20:00 Starting compiler/backend/x64
Feb 09 13:20:19 Finished compiler/backend/x64                                    17s   1GB
Feb 09 13:20:19 Starting compiler/backend/arm7
Feb 09 13:20:39 Finished compiler/backend/arm7                                   20s   1GB
Feb 09 13:20:39 Starting compiler/backend/arm8
Feb 09 13:20:59 Finished compiler/backend/arm8                                   19s   1GB
Feb 09 13:20:59 Starting compiler/backend/mips
Feb 09 13:21:20 Finished compiler/backend/mips                                   20s   1GB
Feb 09 13:21:20 Starting compiler/backend/riscv
Feb 09 13:21:42 Finished compiler/backend/riscv                                  21s   1GB
Feb 09 13:21:42 Starting compiler/backend/ag32
Feb 09 13:22:52 Finished compiler/backend/ag32                                 1m09s   1GB
Feb 09 13:22:52 Starting compiler/parsing/proofs
Feb 09 13:28:36 Finished compiler/parsing/proofs                               5m43s   2GB
Feb 09 13:28:36 Starting compiler/inference/proofs
Feb 09 13:31:08 Finished compiler/inference/proofs                             2m31s   2GB
Feb 09 13:31:09 Starting compiler/backend/semantics
Feb 09 13:57:47 Finished compiler/backend/semantics                           26m38s   3GB
Feb 09 13:57:48 Starting compiler/backend/reg_alloc/proofs
Feb 09 14:01:08 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Feb 09 14:01:09 Starting compiler/backend/proofs
Feb 09 14:55:15 Finished compiler/backend/proofs                              54m06s  33GB
Feb 09 14:55:15 Starting compiler/encoders/x64/proofs
Feb 09 15:04:52 Finished compiler/encoders/x64/proofs                          9m36s   5GB
Feb 09 15:04:52 Starting compiler/encoders/arm7/proofs
Feb 09 15:17:34 Finished compiler/encoders/arm7/proofs                        12m42s   5GB
Feb 09 15:17:34 Starting compiler/encoders/arm8/proofs
Feb 09 15:23:56 Finished compiler/encoders/arm8/proofs                         6m21s   4GB
Feb 09 15:23:56 Starting compiler/encoders/mips/proofs
Feb 09 15:33:39 Finished compiler/encoders/mips/proofs                         9m42s   7GB
Feb 09 15:33:39 Starting compiler/encoders/riscv/proofs
Feb 09 15:42:00 Finished compiler/encoders/riscv/proofs                        8m20s   3GB
Feb 09 15:42:00 Starting compiler/encoders/ag32/proofs
Feb 09 15:44:22 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Feb 09 15:44:22 Starting compiler/backend/x64/proofs
Feb 09 15:44:44 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 09 15:44:44 Starting compiler/backend/arm7/proofs
Feb 09 15:45:08 Finished compiler/backend/arm7/proofs                            23s   1GB
Feb 09 15:45:08 Starting compiler/backend/arm8/proofs
Feb 09 15:45:30 Finished compiler/backend/arm8/proofs                            22s   1GB
Feb 09 15:45:30 Starting compiler/backend/mips/proofs
Feb 09 15:45:52 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 09 15:45:53 Starting compiler/backend/riscv/proofs
Feb 09 15:46:17 Finished compiler/backend/riscv/proofs                           24s   2GB
Feb 09 15:46:17 Starting compiler/backend/ag32/proofs
Feb 09 15:58:20 Finished compiler/backend/ag32/proofs                         12m02s   4GB
Feb 09 15:58:20 Starting compiler/proofs
Feb 09 16:00:19 Finished compiler/proofs                                       1m57s   6GB
Feb 09 16:00:19 Starting candle/set-theory
Feb 09 16:00:49 Finished candle/set-theory                                       29s   1GB
Feb 09 16:00:49 Starting candle/syntax-lib
Feb 09 16:01:00 Finished candle/syntax-lib                                       11s 790MB
Feb 09 16:01:01 Starting candle/standard/syntax
Feb 09 16:02:52 Finished candle/standard/syntax                                1m51s   1GB
Feb 09 16:02:52 Starting candle/standard/semantics
Feb 09 16:04:39 Finished candle/standard/semantics                             1m46s   2GB
Feb 09 16:04:39 Starting candle/standard/monadic
Feb 09 16:06:23 Finished candle/standard/monadic                               1m43s   1GB
Feb 09 16:06:23 Starting candle/standard/ml_kernel
Feb 09 16:11:59 Finished candle/standard/ml_kernel                             5m35s   7GB
Feb 09 16:11:59 Starting candle/overloading/syntax
Feb 09 16:15:09 Finished candle/overloading/syntax                             3m09s   1GB
Feb 09 16:15:09 Starting candle/overloading/semantics
Feb 09 16:27:13 Finished candle/overloading/semantics                         12m04s   8GB
Feb 09 16:27:14 Starting characteristic/examples
Feb 09 16:28:34 Finished characteristic/examples                               1m20s   4GB
Feb 09 16:28:34 Starting tutorial/solutions
Feb 09 16:44:05 Finished tutorial/solutions                                   15m30s  14GB
Feb 09 16:44:05 Starting translator/monadic/examples
Feb 09 16:47:25 Finished translator/monadic/examples                           3m19s   3GB
Feb 09 16:47:25 Starting examples
Feb 09 16:56:19 Finished examples                                              8m54s   6GB
Feb 09 16:56:20 Starting examples/compilation/x64
Feb 09 19:17:46 Finished examples/compilation/x64                           2h21m26s  25GB
Feb 09 19:17:46 Starting examples/compilation/x64/proofs
Feb 09 19:19:45 Finished examples/compilation/x64/proofs                       1m58s   3GB
Feb 09 19:19:46 Starting examples/compilation/ag32
Feb 09 19:53:49 Finished examples/compilation/ag32                            34m03s  17GB
Feb 09 19:53:49 Starting examples/compilation/ag32/proofs
Feb 09 19:54:41 Finished examples/compilation/ag32/proofs                        51s   5GB
Feb 09 19:54:41 Starting examples/cost
Feb 09 20:09: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/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 costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
size_ofPropsTheory                                                            real:   28s  user:   27s     OK
miniBasisProgTheory                                                           real:   33s  user:   31s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                                               real:   93s  user:   90s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                             real:  668s  user:  726s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                            real:  642s  user:  685s     OK
Starting work on pureLoopProofTheory
allProgTheory                                                                 real:  658s  user:  704s     OK
Starting work on allProofTheory
pureLoopProofTheory                                                           real:  148s  user:  143sFAIL<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-1471/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-1471/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