Job 1493

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:3d4a96b446a3347e5cb94f1b123332937de84554
  Fix reference to HOL examples theory that has moved [Mar 18 00:23:39]
HOL:94d032357d37c515713e95934557884394537da2
  Improve loop detection in simplifier [Mar 18 06:46:50]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 19 07:27:30 Claimed job
Mar 19 07:27:41 Building HOL
Mar 19 07:42:20 Starting developers
Mar 19 07:42:22 Finished developers                                               2s 136MB
Mar 19 07:42:22 Starting developers/bin
Mar 19 07:42:28 Finished developers/bin                                           5s   1GB
Mar 19 07:42:29 Starting semantics/ffi
Mar 19 07:42:39 Finished semantics/ffi                                            9s 298MB
Mar 19 07:42:39 Starting semantics
Mar 19 07:44:14 Finished semantics                                             1m35s   1GB
Mar 19 07:44:15 Starting semantics/proofs
Mar 19 07:47:46 Finished semantics/proofs                                      3m31s   1GB
Mar 19 07:47:46 Starting basis/pure
Mar 19 07:50:26 Finished basis/pure                                            2m39s   1GB
Mar 19 07:50:26 Starting translator
Mar 19 07:53:46 Finished translator                                            3m19s   2GB
Mar 19 07:53:46 Starting compiler/parsing
Mar 19 07:54:53 Finished compiler/parsing                                      1m07s   3GB
Mar 19 07:54:54 Starting characteristic
Mar 19 08:00:34 Finished characteristic                                        5m40s   3GB
Mar 19 08:00:34 Starting translator/monadic
Mar 19 08:02:23 Finished translator/monadic                                    1m48s   3GB
Mar 19 08:02:23 Starting basis
Mar 19 08:47:37 Finished basis                                                45m13s  45GB
Mar 19 08:47:37 Starting compiler/inference
Mar 19 08:48:49 Finished compiler/inference                                    1m11s   1GB
Mar 19 08:48:49 Starting compiler/backend/reg_alloc
Mar 19 08:49:55 Finished compiler/backend/reg_alloc                            1m05s   1GB
Mar 19 08:49:55 Starting compiler/backend/gc
Mar 19 08:53:32 Finished compiler/backend/gc                                   3m36s   4GB
Mar 19 08:53:32 Starting compiler/backend
Mar 19 08:58:43 Finished compiler/backend                                      5m10s   5GB
Mar 19 08:58:43 Starting compiler/encoders/asm
Mar 19 08:59:06 Finished compiler/encoders/asm                                   22s   1GB
Mar 19 08:59:06 Starting compiler/encoders/x64
Mar 19 09:00:09 Finished compiler/encoders/x64                                 1m03s   1GB
Mar 19 09:00:09 Starting compiler/encoders/arm7
Mar 19 09:02:12 Finished compiler/encoders/arm7                                2m02s   1GB
Mar 19 09:02:12 Starting compiler/encoders/arm8
Mar 19 09:02:51 Finished compiler/encoders/arm8                                  38s   1GB
Mar 19 09:02:51 Starting compiler/encoders/mips
Mar 19 09:04:19 Finished compiler/encoders/mips                                1m27s   1GB
Mar 19 09:04:19 Starting compiler/encoders/riscv
Mar 19 09:05:57 Finished compiler/encoders/riscv                               1m37s   1GB
Mar 19 09:05:57 Starting compiler/encoders/ag32
Mar 19 09:06:16 Finished compiler/encoders/ag32                                  18s 958MB
Mar 19 09:06:16 Starting compiler/backend/x64
Mar 19 09:06:37 Finished compiler/backend/x64                                    20s   1GB
Mar 19 09:06:37 Starting compiler/backend/arm7
Mar 19 09:06:58 Finished compiler/backend/arm7                                   21s   1GB
Mar 19 09:06:58 Starting compiler/backend/arm8
Mar 19 09:07:19 Finished compiler/backend/arm8                                   20s   1GB
Mar 19 09:07:19 Starting compiler/backend/mips
Mar 19 09:07:40 Finished compiler/backend/mips                                   20s   1GB
Mar 19 09:07:40 Starting compiler/backend/riscv
Mar 19 09:08:01 Finished compiler/backend/riscv                                  21s   1GB
Mar 19 09:08:02 Starting compiler/backend/ag32
Mar 19 09:09:13 Finished compiler/backend/ag32                                 1m11s   2GB
Mar 19 09:09:13 Starting compiler/parsing/proofs
Mar 19 09:15:04 Finished compiler/parsing/proofs                               5m50s   2GB
Mar 19 09:15:04 Starting compiler/inference/proofs
Mar 19 09:17:36 Finished compiler/inference/proofs                             2m32s   2GB
Mar 19 09:17:37 Starting compiler/backend/semantics
Mar 19 09:44:20 Finished compiler/backend/semantics                           26m43s   2GB
Mar 19 09:44:21 Starting compiler/backend/reg_alloc/proofs
Mar 19 09:47:42 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Mar 19 09:47:42 Starting compiler/backend/proofs
Mar 19 10:45:52 Finished compiler/backend/proofs                              58m09s  16GB
Mar 19 10:45:52 Starting compiler/encoders/x64/proofs
Mar 19 10:55:28 Finished compiler/encoders/x64/proofs                          9m35s   5GB
Mar 19 10:55:28 Starting compiler/encoders/arm7/proofs
Mar 19 11:08:09 Finished compiler/encoders/arm7/proofs                        12m41s   5GB
Mar 19 11:08:09 Starting compiler/encoders/arm8/proofs
Mar 19 11:14:23 Finished compiler/encoders/arm8/proofs                         6m13s   3GB
Mar 19 11:14:23 Starting compiler/encoders/mips/proofs
Mar 19 11:24:10 Finished compiler/encoders/mips/proofs                         9m47s   6GB
Mar 19 11:24:11 Starting compiler/encoders/riscv/proofs
Mar 19 11:32:33 Finished compiler/encoders/riscv/proofs                        8m22s   3GB
Mar 19 11:32:34 Starting compiler/encoders/ag32/proofs
Mar 19 11:34:53 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Mar 19 11:34:54 Starting compiler/backend/x64/proofs
Mar 19 11:35:16 Finished compiler/backend/x64/proofs                             22s   2GB
Mar 19 11:35:16 Starting compiler/backend/arm7/proofs
Mar 19 11:35:39 Finished compiler/backend/arm7/proofs                            22s   1GB
Mar 19 11:35:39 Starting compiler/backend/arm8/proofs
Mar 19 11:36:00 Finished compiler/backend/arm8/proofs                            20s   1GB
Mar 19 11:36:00 Starting compiler/backend/mips/proofs
Mar 19 11:36:23 Finished compiler/backend/mips/proofs                            22s   1GB
Mar 19 11:36:23 Starting compiler/backend/riscv/proofs
Mar 19 11:36:47 Finished compiler/backend/riscv/proofs                           23s   2GB
Mar 19 11:36:47 Starting compiler/backend/ag32/proofs
Mar 19 11:48:50 Finished compiler/backend/ag32/proofs                         12m02s   5GB
Mar 19 11:48:51 Starting compiler/proofs
Mar 19 11:50:48 Finished compiler/proofs                                       1m57s   6GB
Mar 19 11:50:49 Starting candle/set-theory
Mar 19 11:51:19 Finished candle/set-theory                                       29s   1GB
Mar 19 11:51:19 Starting candle/syntax-lib
Mar 19 11:51:30 Finished candle/syntax-lib                                       11s 805MB
Mar 19 11:51:31 Starting candle/standard/syntax
Mar 19 11:53:23 Finished candle/standard/syntax                                1m52s   1GB
Mar 19 11:53:23 Starting candle/standard/semantics
Mar 19 11:55:12 Finished candle/standard/semantics                             1m48s   2GB
Mar 19 11:55:12 Starting candle/standard/monadic
Mar 19 11:56:55 Finished candle/standard/monadic                               1m42s   1GB
Mar 19 11:56:55 Starting candle/standard/ml_kernel
Mar 19 12:02:24 Finished candle/standard/ml_kernel                             5m28s   7GB
Mar 19 12:02:24 Starting candle/overloading/syntax
Mar 19 12:05:36 Finished candle/overloading/syntax                             3m11s   1GB
Mar 19 12:05:36 Starting candle/overloading/semantics
Mar 19 12:17:34 Finished candle/overloading/semantics                         11m58s   8GB
Mar 19 12:17:34 Starting characteristic/examples
Mar 19 12:18:53 Finished characteristic/examples                               1m18s   4GB
Mar 19 12:18:53 Starting tutorial/solutions
Mar 19 12:34:32 Finished tutorial/solutions                                   15m38s  13GB
Mar 19 12:34:32 Starting translator/monadic/examples
Mar 19 12:37:57 Finished translator/monadic/examples                           3m25s   3GB
Mar 19 12:37:57 Starting examples
Mar 19 12:46:53 Finished examples                                              8m55s   6GB
Mar 19 12:46:54 Starting examples/compilation/x64
Mar 19 15:07:34 Finished examples/compilation/x64                           2h20m39s  46GB
Mar 19 15:07:34 Starting examples/compilation/x64/proofs
Mar 19 15:09:37 Finished examples/compilation/x64/proofs                       2m02s   3GB
Mar 19 15:09:37 Starting examples/compilation/ag32
Mar 19 15:43:21 Finished examples/compilation/ag32                            33m43s  14GB
Mar 19 15:43:21 Starting examples/compilation/ag32/proofs
Mar 19 15:44:15 Finished examples/compilation/ag32/proofs                        53s   4GB
Mar 19 15:44:15 Starting examples/cost
Mar 19 15:59:05 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:   28s  user:   28s     OK
miniBasisProgTheory                                                           real:   32s  user:   30s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                                               real:   92s  user:   89s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                             real:  652s  user:  712s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                            real:  644s  user:  689s     OK
Starting work on pureLoopProofTheory
allProgTheory                                                                 real:  660s  user:  709s     OK
Starting work on allProofTheory
pureLoopProofTheory                                                           real:  150s  user:  146sFAIL<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-1493/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-1493/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