Job 1411

CakeML:35ccb3262271f64bfdd9c2f81e80236a52ff8e3b
  Fix a proof broken by merge [Dec 04 07:49:22]
#807 (issue797)
Merging into:3157c56dfe1eab23ef37b3cefb8fca2cced396c5
  Merge pull request #804 from CakeML/currheap [Nov 17 07:22:18]
HOL:77016ef7b01f987f1f684e825ac1d79feb8d454a
  emacs-mode: fix bug in previous caused by variable masking [Nov 27 05:03:03]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 05 23:45:02 Claimed job
Dec 05 23:45:05 Reusing HOL
Dec 05 23:45:54 Starting developers
Dec 05 23:45:59 Finished developers                                               4s 106MB
Dec 05 23:45:59 Starting developers/bin
Dec 05 23:46:06 Finished developers/bin                                           6s   1GB
Dec 05 23:46:06 Starting semantics/ffi
Dec 05 23:46:18 Finished semantics/ffi                                           11s 260MB
Dec 05 23:46:18 Starting semantics
Dec 05 23:47:45 Finished semantics                                             1m27s   1GB
Dec 05 23:47:45 Starting semantics/proofs
Dec 05 23:51:22 Finished semantics/proofs                                      3m36s 975MB
Dec 05 23:51:22 Starting semantics/alt_semantics
Dec 05 23:51:32 Finished semantics/alt_semantics                                  9s 320MB
Dec 05 23:51:32 Starting semantics/alt_semantics/proofs
Dec 05 23:53:48 Finished semantics/alt_semantics/proofs                        2m16s   1GB
Dec 05 23:53:48 Starting basis/pure
Dec 05 23:54:40 Finished basis/pure                                              51s 876MB
Dec 05 23:54:41 Starting translator
Dec 05 23:57:30 Finished translator                                            2m49s   1GB
Dec 05 23:57:31 Starting compiler/parsing
Dec 05 23:58:43 Finished compiler/parsing                                      1m12s   2GB
Dec 05 23:58:44 Starting characteristic
Dec 06 00:05:02 Finished characteristic                                        6m18s   1GB
Dec 06 00:05:03 Starting translator/monadic
Dec 06 00:06:45 Finished translator/monadic                                    1m42s   1GB
Dec 06 00:06:45 Starting basis
Dec 06 00:43:08 Finished basis                                                36m22s  12GB
Dec 06 00:43:08 Starting compiler/inference
Dec 06 00:44:14 Finished compiler/inference                                    1m05s   1GB
Dec 06 00:44:14 Starting compiler/backend/reg_alloc
Dec 06 00:45:22 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 06 00:45:22 Starting compiler/backend/gc
Dec 06 00:48:56 Finished compiler/backend/gc                                   3m34s   2GB
Dec 06 00:48:56 Starting compiler/backend
Dec 06 00:53:52 Finished compiler/backend                                      4m55s   4GB
Dec 06 00:53:52 Starting compiler/encoders/asm
Dec 06 00:54:15 Finished compiler/encoders/asm                                   23s 901MB
Dec 06 00:54:16 Starting compiler/encoders/x64
Dec 06 00:54:42 Finished compiler/encoders/x64                                   25s 879MB
Dec 06 00:54:42 Starting compiler/encoders/arm7
Dec 06 00:55:34 Finished compiler/encoders/arm7                                  51s 715MB
Dec 06 00:55:34 Starting compiler/encoders/arm8
Dec 06 00:55:47 Finished compiler/encoders/arm8                                  13s 929MB
Dec 06 00:55:48 Starting compiler/encoders/mips
Dec 06 00:56:05 Finished compiler/encoders/mips                                  17s   1GB
Dec 06 00:56:05 Starting compiler/encoders/riscv
Dec 06 00:56:22 Finished compiler/encoders/riscv                                 16s 761MB
Dec 06 00:56:22 Starting compiler/encoders/ag32
Dec 06 00:56:41 Finished compiler/encoders/ag32                                  18s 867MB
Dec 06 00:56:41 Starting compiler/backend/x64
Dec 06 00:57:01 Finished compiler/backend/x64                                    19s   1GB
Dec 06 00:57:01 Starting compiler/backend/arm7
Dec 06 00:57:21 Finished compiler/backend/arm7                                   20s   1GB
Dec 06 00:57:21 Starting compiler/backend/arm8
Dec 06 00:57:40 Finished compiler/backend/arm8                                   18s   1GB
Dec 06 00:57:40 Starting compiler/backend/mips
Dec 06 00:58:00 Finished compiler/backend/mips                                   19s   1GB
Dec 06 00:58:00 Starting compiler/backend/riscv
Dec 06 00:58:21 Finished compiler/backend/riscv                                  20s   1GB
Dec 06 00:58:21 Starting compiler/backend/ag32
Dec 06 00:59:34 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 06 00:59:34 Starting compiler/parsing/proofs
Dec 06 01:05:21 Finished compiler/parsing/proofs                               5m46s   2GB
Dec 06 01:05:21 Starting compiler/inference/proofs
Dec 06 01:07:59 Finished compiler/inference/proofs                             2m37s   1GB
Dec 06 01:07:59 Starting compiler/backend/semantics
Dec 06 01:41:04 Finished compiler/backend/semantics                           33m04s   3GB
Dec 06 01:41:04 Starting compiler/backend/reg_alloc/proofs
Dec 06 01:44:50 Finished compiler/backend/reg_alloc/proofs                     3m45s 847MB
Dec 06 01:44:50 Starting compiler/backend/proofs
Dec 06 02:43:08 Finished compiler/backend/proofs                              58m17s  17GB
Dec 06 02:43:09 Starting compiler/encoders/x64/proofs
Dec 06 02:53:29 Finished compiler/encoders/x64/proofs                         10m19s   4GB
Dec 06 02:53:29 Starting compiler/encoders/arm7/proofs
Dec 06 03:07:23 Finished compiler/encoders/arm7/proofs                        13m53s   3GB
Dec 06 03:07:23 Starting compiler/encoders/arm8/proofs
Dec 06 03:14:25 Finished compiler/encoders/arm8/proofs                         7m02s   1GB
Dec 06 03:14:26 Starting compiler/encoders/mips/proofs
Dec 06 03:25:16 Finished compiler/encoders/mips/proofs                        10m49s   2GB
Dec 06 03:25:16 Starting compiler/encoders/riscv/proofs
Dec 06 03:35:02 Finished compiler/encoders/riscv/proofs                        9m45s 963MB
Dec 06 03:35:02 Starting compiler/encoders/ag32/proofs
Dec 06 03:37:49 Finished compiler/encoders/ag32/proofs                         2m46s 801MB
Dec 06 03:37:49 Starting compiler/backend/x64/proofs
Dec 06 03:38:11 Finished compiler/backend/x64/proofs                             21s   1GB
Dec 06 03:38:11 Starting compiler/backend/arm7/proofs
Dec 06 03:38:35 Finished compiler/backend/arm7/proofs                            23s   1GB
Dec 06 03:38:35 Starting compiler/backend/arm8/proofs
Dec 06 03:38:57 Finished compiler/backend/arm8/proofs                            22s   1GB
Dec 06 03:38:57 Starting compiler/backend/mips/proofs
Dec 06 03:39:19 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 06 03:39:19 Starting compiler/backend/riscv/proofs
Dec 06 03:39:41 Finished compiler/backend/riscv/proofs                           21s   1GB
Dec 06 03:39:41 Starting compiler/backend/ag32/proofs
Dec 06 03:53:24 Finished compiler/backend/ag32/proofs                         13m43s   3GB
Dec 06 03:53:24 Starting compiler/proofs
Dec 06 03:55:03 Finished compiler/proofs                                       1m37s   2GB
Dec 06 03:55:03 Starting candle/set-theory
Dec 06 03:55:32 Finished candle/set-theory                                       29s 689MB
Dec 06 03:55:33 Starting candle/syntax-lib
Dec 06 03:55:44 Finished candle/syntax-lib                                       10s 648MB
Dec 06 03:55:44 Starting candle/standard/syntax
Dec 06 03:57:38 Finished candle/standard/syntax                                1m53s   1GB
Dec 06 03:57:38 Starting candle/standard/semantics
Dec 06 03:59:26 Finished candle/standard/semantics                             1m47s   1GB
Dec 06 03:59:26 Starting candle/standard/monadic
Dec 06 04:01:14 Finished candle/standard/monadic                               1m47s   1GB
Dec 06 04:01:15 Starting candle/standard/ml_kernel
Dec 06 04:07:06 Finished candle/standard/ml_kernel                             5m51s   5GB
Dec 06 04:07:06 Starting candle/overloading/syntax
Dec 06 04:10:26 Finished candle/overloading/syntax                             3m19s 974MB
Dec 06 04:10:26 Starting candle/overloading/semantics
Dec 06 04:23:27 Finished candle/overloading/semantics                         13m00s   3GB
Dec 06 04:23:27 Starting characteristic/examples
Dec 06 04:24:47 Finished characteristic/examples                               1m20s   2GB
Dec 06 04:24:48 Starting tutorial/solutions
Dec 06 04:39:45 Finished tutorial/solutions                                   14m57s   6GB
Dec 06 04:39:46 Starting translator/monadic/examples
Dec 06 04:43:05 Finished translator/monadic/examples                           3m19s   2GB
Dec 06 04:43:05 Starting examples
Dec 06 04:51:58 Finished examples                                              8m52s   3GB
Dec 06 04:51:58 Starting examples/compilation/x64
Dec 06 07:07:25 Finished examples/compilation/x64                           2h15m26s  14GB
Dec 06 07:07:26 Starting examples/compilation/x64/proofs
Dec 06 07:09:26 Finished examples/compilation/x64/proofs                       2m00s   3GB
Dec 06 07:09:27 Starting examples/compilation/ag32
Dec 06 07:42:16 Finished examples/compilation/ag32                            32m48s   6GB
Dec 06 07:42:16 Starting examples/compilation/ag32/proofs
Dec 06 07:43:02 Finished examples/compilation/ag32/proofs                        46s   2GB
Dec 06 07:43:03 Starting examples/cost
Dec 06 07:57:41 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/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
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/reachability/proofs
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:   28s  user:   27s     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                              real:   29s  user:   28s     OK
costPropsTheory                                 real:   89s  user:   86s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  658s  user:  722s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  653s  user:  705s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  660s  user:  715s     OK
Starting work on allProofTheory
pureLoopProofTheory                             real:  133s  user:  128sFAIL<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