Job 1490

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:92800175372782848a933d973527fc7f4dda27c6
  Merge pull request #817 from CakeML/reset_translation-fix [Mar 10 21:00:30]
HOL:39e109dd10927cd1557767a5db42c9845571fbee
  Clean minisat and zc2hs directories when bin/build clean* happens [Mar 11 00:07:46]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 12 21:10:09 Claimed job
Mar 12 21:10:12 Building HOL
Mar 12 21:26:30 Starting developers
Mar 12 21:26:35 Finished developers                                               4s  93MB
Mar 12 21:26:35 Starting developers/bin
Mar 12 21:26:42 Finished developers/bin                                           6s   1GB
Mar 12 21:26:42 Starting semantics/ffi
Mar 12 21:26:53 Finished semantics/ffi                                           11s 245MB
Mar 12 21:26:54 Starting semantics
Mar 12 21:28:31 Finished semantics                                             1m37s   1GB
Mar 12 21:28:32 Starting semantics/proofs
Mar 12 21:32:27 Finished semantics/proofs                                      3m55s 979MB
Mar 12 21:32:27 Starting basis/pure
Mar 12 21:35:37 Finished basis/pure                                            3m09s 929MB
Mar 12 21:35:37 Starting translator
Mar 12 21:39:18 Finished translator                                            3m40s   1GB
Mar 12 21:39:18 Starting compiler/parsing
Mar 12 21:40:36 Finished compiler/parsing                                      1m17s   2GB
Mar 12 21:40:36 Starting characteristic
Mar 12 21:46:33 Finished characteristic                                        5m56s   1GB
Mar 12 21:46:33 Starting translator/monadic
Mar 12 21:48:16 Finished translator/monadic                                    1m42s   1GB
Mar 12 21:48:16 Starting basis
Mar 12 22:35:59 Finished basis                                                47m42s  14GB
Mar 12 22:35:59 Starting compiler/inference
Mar 12 22:37:19 Finished compiler/inference                                    1m19s   1GB
Mar 12 22:37:19 Starting compiler/backend/reg_alloc
Mar 12 22:38:27 Finished compiler/backend/reg_alloc                            1m08s   1GB
Mar 12 22:38:28 Starting compiler/backend/gc
Mar 12 22:42:17 Finished compiler/backend/gc                                   3m49s   2GB
Mar 12 22:42:17 Starting compiler/backend
Mar 12 22:47:29 Finished compiler/backend                                      5m11s   4GB
Mar 12 22:47:29 Starting compiler/encoders/asm
Mar 12 22:47:52 Finished compiler/encoders/asm                                   22s 869MB
Mar 12 22:47:52 Starting compiler/encoders/x64
Mar 12 22:48:58 Finished compiler/encoders/x64                                 1m05s 857MB
Mar 12 22:48:58 Starting compiler/encoders/arm7
Mar 12 22:51:12 Finished compiler/encoders/arm7                                2m13s   1GB
Mar 12 22:51:12 Starting compiler/encoders/arm8
Mar 12 22:51:52 Finished compiler/encoders/arm8                                  39s 950MB
Mar 12 22:51:52 Starting compiler/encoders/mips
Mar 12 22:53:30 Finished compiler/encoders/mips                                1m37s 833MB
Mar 12 22:53:30 Starting compiler/encoders/riscv
Mar 12 22:55:21 Finished compiler/encoders/riscv                               1m51s 912MB
Mar 12 22:55:22 Starting compiler/encoders/ag32
Mar 12 22:55:41 Finished compiler/encoders/ag32                                  18s 843MB
Mar 12 22:55:41 Starting compiler/backend/x64
Mar 12 22:56:00 Finished compiler/backend/x64                                    18s   1GB
Mar 12 22:56:00 Starting compiler/backend/arm7
Mar 12 22:56:22 Finished compiler/backend/arm7                                   21s   1GB
Mar 12 22:56:22 Starting compiler/backend/arm8
Mar 12 22:56:43 Finished compiler/backend/arm8                                   20s   1GB
Mar 12 22:56:43 Starting compiler/backend/mips
Mar 12 22:57:03 Finished compiler/backend/mips                                   20s   1GB
Mar 12 22:57:03 Starting compiler/backend/riscv
Mar 12 22:57:26 Finished compiler/backend/riscv                                  22s   1GB
Mar 12 22:57:26 Starting compiler/backend/ag32
Mar 12 22:58:41 Finished compiler/backend/ag32                                 1m15s   1GB
Mar 12 22:58:42 Starting compiler/parsing/proofs
Mar 12 23:04:49 Finished compiler/parsing/proofs                               6m07s   1GB
Mar 12 23:04:49 Starting compiler/inference/proofs
Mar 12 23:07:29 Finished compiler/inference/proofs                             2m39s 945MB
Mar 12 23:07:29 Starting compiler/backend/semantics
Mar 12 23:40:08 Finished compiler/backend/semantics                           32m38s   2GB
Mar 12 23:40:08 Starting compiler/backend/reg_alloc/proofs
Mar 12 23:43:55 Finished compiler/backend/reg_alloc/proofs                     3m46s 846MB
Mar 12 23:43:55 Starting compiler/backend/proofs
Mar 13 00:42:58 Finished compiler/backend/proofs                              59m01s  17GB
Mar 13 00:42:58 Starting compiler/encoders/x64/proofs
Mar 13 00:53:24 Finished compiler/encoders/x64/proofs                         10m25s   4GB
Mar 13 00:53:24 Starting compiler/encoders/arm7/proofs
Mar 13 01:07:47 Finished compiler/encoders/arm7/proofs                        14m22s   3GB
Mar 13 01:07:47 Starting compiler/encoders/arm8/proofs
Mar 13 01:14:57 Finished compiler/encoders/arm8/proofs                         7m09s   1GB
Mar 13 01:14:57 Starting compiler/encoders/mips/proofs
Mar 13 01:25:40 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Mar 13 01:25:40 Starting compiler/encoders/riscv/proofs
Mar 13 01:35:27 Finished compiler/encoders/riscv/proofs                        9m47s   1GB
Mar 13 01:35:28 Starting compiler/encoders/ag32/proofs
Mar 13 01:38:16 Finished compiler/encoders/ag32/proofs                         2m48s 683MB
Mar 13 01:38:16 Starting compiler/backend/x64/proofs
Mar 13 01:38:39 Finished compiler/backend/x64/proofs                             22s   1GB
Mar 13 01:38:39 Starting compiler/backend/arm7/proofs
Mar 13 01:39:03 Finished compiler/backend/arm7/proofs                            23s   1GB
Mar 13 01:39:03 Starting compiler/backend/arm8/proofs
Mar 13 01:39:27 Finished compiler/backend/arm8/proofs                            23s   1GB
Mar 13 01:39:27 Starting compiler/backend/mips/proofs
Mar 13 01:39:49 Finished compiler/backend/mips/proofs                            22s   1GB
Mar 13 01:39:50 Starting compiler/backend/riscv/proofs
Mar 13 01:40:13 Finished compiler/backend/riscv/proofs                           23s   1GB
Mar 13 01:40:14 Starting compiler/backend/ag32/proofs
Mar 13 01:53:59 Finished compiler/backend/ag32/proofs                         13m45s   3GB
Mar 13 01:53:59 Starting compiler/proofs
Mar 13 01:56:01 Finished compiler/proofs                                       2m01s   6GB
Mar 13 01:56:02 Starting candle/set-theory
Mar 13 01:56:32 Finished candle/set-theory                                       29s 689MB
Mar 13 01:56:32 Starting candle/syntax-lib
Mar 13 01:56:43 Finished candle/syntax-lib                                       10s 728MB
Mar 13 01:56:43 Starting candle/standard/syntax
Mar 13 01:58:39 Finished candle/standard/syntax                                1m55s   1GB
Mar 13 01:58:39 Starting candle/standard/semantics
Mar 13 02:00:27 Finished candle/standard/semantics                             1m47s   1GB
Mar 13 02:00:28 Starting candle/standard/monadic
Mar 13 02:02:19 Finished candle/standard/monadic                               1m51s   1GB
Mar 13 02:02:19 Starting candle/standard/ml_kernel
Mar 13 02:08:44 Finished candle/standard/ml_kernel                             6m24s   3GB
Mar 13 02:08:44 Starting candle/overloading/syntax
Mar 13 02:12:06 Finished candle/overloading/syntax                             3m22s   1GB
Mar 13 02:12:06 Starting candle/overloading/semantics
Mar 13 02:24:55 Finished candle/overloading/semantics                         12m48s   4GB
Mar 13 02:24:55 Starting characteristic/examples
Mar 13 02:26:19 Finished characteristic/examples                               1m23s   2GB
Mar 13 02:26:19 Starting tutorial/solutions
Mar 13 02:42:47 Finished tutorial/solutions                                   16m28s   7GB
Mar 13 02:42:48 Starting translator/monadic/examples
Mar 13 02:46:13 Finished translator/monadic/examples                           3m25s   2GB
Mar 13 02:46:13 Starting examples
Mar 13 02:55:36 Finished examples                                              9m21s   5GB
Mar 13 02:55:36 Starting examples/compilation/x64
Mar 13 05:26:48 Finished examples/compilation/x64                           2h31m11s  20GB
Mar 13 05:26:48 Starting examples/compilation/x64/proofs
Mar 13 05:28:58 Finished examples/compilation/x64/proofs                       2m09s   2GB
Mar 13 05:28:58 Starting examples/compilation/ag32
Mar 13 06:04:37 Finished examples/compilation/ag32                            35m38s   7GB
Mar 13 06:04:37 Starting examples/compilation/ag32/proofs
Mar 13 06:05:26 Finished examples/compilation/ag32/proofs                        48s   3GB
Mar 13 06:05:27 Starting examples/cost
Mar 13 06:20:31 FAILED: examples/cost
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
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
miniBasisProgTheory                             real:   29s  user:   27s     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                              real:   30s  user:   29s     OK
costPropsTheory                                 real:   97s  user:   93s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  660s  user:  724s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  654s  user:  701s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  662s  user:  710s     OK
Starting work on allProofTheory
pureLoopProofTheory                             real:  149s  user:  145sFAIL<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