CakeML Regression Test

Job 1473

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:9ff85ba156ed5501ffb3f4921ae639fb10ebb312
  Remove definitions.tex in DESCRIPTION manual's Holmakefile's EXTRA_CL [Feb 12 05:34:54]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 15 06:56:25 Claimed job
Feb 15 06:56:31 Building HOL
Feb 15 07:12:16 Starting developers
Feb 15 07:12:20 Finished developers                                               4s 134MB
Feb 15 07:12:20 Starting developers/bin
Feb 15 07:12:27 Finished developers/bin                                           6s   1GB
Feb 15 07:12:27 Starting semantics/ffi
Feb 15 07:12:39 Finished semantics/ffi                                           11s 230MB
Feb 15 07:12:39 Starting semantics
Feb 15 07:14:17 Finished semantics                                             1m38s   1GB
Feb 15 07:14:18 Starting semantics/proofs
Feb 15 07:18:12 Finished semantics/proofs                                      3m53s   1GB
Feb 15 07:18:12 Starting basis/pure
Feb 15 07:21:22 Finished basis/pure                                            3m09s 855MB
Feb 15 07:21:22 Starting translator
Feb 15 07:25:00 Finished translator                                            3m37s   1GB
Feb 15 07:25:00 Starting compiler/parsing
Feb 15 07:26:18 Finished compiler/parsing                                      1m17s   2GB
Feb 15 07:26:18 Starting characteristic
Feb 15 07:32:16 Finished characteristic                                        5m57s   1GB
Feb 15 07:32:16 Starting translator/monadic
Feb 15 07:33:59 Finished translator/monadic                                    1m43s   1GB
Feb 15 07:34:00 Starting basis
Feb 15 08:22:11 Finished basis                                                48m11s   9GB
Feb 15 08:22:11 Starting compiler/inference
Feb 15 08:23:29 Finished compiler/inference                                    1m17s   1GB
Feb 15 08:23:29 Starting compiler/backend/reg_alloc
Feb 15 08:24:36 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 15 08:24:36 Starting compiler/backend/gc
Feb 15 08:28:26 Finished compiler/backend/gc                                   3m49s   2GB
Feb 15 08:28:26 Starting compiler/backend
Feb 15 08:33:34 Finished compiler/backend                                      5m07s   3GB
Feb 15 08:33:34 Starting compiler/encoders/asm
Feb 15 08:33:57 Finished compiler/encoders/asm                                   22s 632MB
Feb 15 08:33:57 Starting compiler/encoders/x64
Feb 15 08:35:02 Finished compiler/encoders/x64                                 1m05s   1GB
Feb 15 08:35:03 Starting compiler/encoders/arm7
Feb 15 08:37:13 Finished compiler/encoders/arm7                                2m10s   1GB
Feb 15 08:37:13 Starting compiler/encoders/arm8
Feb 15 08:37:53 Finished compiler/encoders/arm8                                  39s 676MB
Feb 15 08:37:53 Starting compiler/encoders/mips
Feb 15 08:39:32 Finished compiler/encoders/mips                                1m37s   1GB
Feb 15 08:39:32 Starting compiler/encoders/riscv
Feb 15 08:41:23 Finished compiler/encoders/riscv                               1m50s   1GB
Feb 15 08:41:23 Starting compiler/encoders/ag32
Feb 15 08:41:41 Finished compiler/encoders/ag32                                  18s 880MB
Feb 15 08:41:42 Starting compiler/backend/x64
Feb 15 08:42:01 Finished compiler/backend/x64                                    19s   1GB
Feb 15 08:42:02 Starting compiler/backend/arm7
Feb 15 08:42:22 Finished compiler/backend/arm7                                   20s   1GB
Feb 15 08:42:22 Starting compiler/backend/arm8
Feb 15 08:42:42 Finished compiler/backend/arm8                                   19s   1GB
Feb 15 08:42:42 Starting compiler/backend/mips
Feb 15 08:43:03 Finished compiler/backend/mips                                   20s   1GB
Feb 15 08:43:03 Starting compiler/backend/riscv
Feb 15 08:43:24 Finished compiler/backend/riscv                                  20s   1GB
Feb 15 08:43:24 Starting compiler/backend/ag32
Feb 15 08:44:36 Finished compiler/backend/ag32                                 1m12s   1GB
Feb 15 08:44:36 Starting compiler/parsing/proofs
Feb 15 08:50:48 Finished compiler/parsing/proofs                               6m11s   1GB
Feb 15 08:50:48 Starting compiler/inference/proofs
Feb 15 08:53:26 Finished compiler/inference/proofs                             2m37s   1GB
Feb 15 08:53:26 Starting compiler/backend/semantics
Feb 15 09:26:09 Finished compiler/backend/semantics                           32m42s   2GB
Feb 15 09:26:09 Starting compiler/backend/reg_alloc/proofs
Feb 15 09:30:03 Finished compiler/backend/reg_alloc/proofs                     3m53s 740MB
Feb 15 09:30:03 Starting compiler/backend/proofs
Feb 15 10:29:00 Finished compiler/backend/proofs                              58m56s  24GB
Feb 15 10:29:00 Starting compiler/encoders/x64/proofs
Feb 15 10:39:24 Finished compiler/encoders/x64/proofs                         10m24s   4GB
Feb 15 10:39:25 Starting compiler/encoders/arm7/proofs
Feb 15 10:53:45 Finished compiler/encoders/arm7/proofs                        14m19s   3GB
Feb 15 10:53:45 Starting compiler/encoders/arm8/proofs
Feb 15 11:00:53 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Feb 15 11:00:53 Starting compiler/encoders/mips/proofs
Feb 15 11:11:53 Finished compiler/encoders/mips/proofs                        10m59s   1GB
Feb 15 11:11:53 Starting compiler/encoders/riscv/proofs
Feb 15 11:21:29 Finished compiler/encoders/riscv/proofs                        9m36s   1GB
Feb 15 11:21:30 Starting compiler/encoders/ag32/proofs
Feb 15 11:24:18 Finished compiler/encoders/ag32/proofs                         2m47s 668MB
Feb 15 11:24:18 Starting compiler/backend/x64/proofs
Feb 15 11:24:41 Finished compiler/backend/x64/proofs                             22s   1GB
Feb 15 11:24:41 Starting compiler/backend/arm7/proofs
Feb 15 11:25:05 Finished compiler/backend/arm7/proofs                            23s   1GB
Feb 15 11:25:05 Starting compiler/backend/arm8/proofs
Feb 15 11:25:28 Finished compiler/backend/arm8/proofs                            22s   1GB
Feb 15 11:25:28 Starting compiler/backend/mips/proofs
Feb 15 11:25:51 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 15 11:25:51 Starting compiler/backend/riscv/proofs
Feb 15 11:26:14 Finished compiler/backend/riscv/proofs                           22s   1GB
Feb 15 11:26:14 Starting compiler/backend/ag32/proofs
Feb 15 11:39:56 Finished compiler/backend/ag32/proofs                         13m41s   2GB
Feb 15 11:39:56 Starting compiler/proofs
Feb 17 12:55:39 Resuming compiler/proofs
Feb 17 12:57:19 Finished compiler/proofs                                       1m40s   4GB
Feb 17 12:57:20 Starting candle/set-theory
Feb 17 12:57:49 Finished candle/set-theory                                       29s 730MB
Feb 17 12:57:49 Starting candle/syntax-lib
Feb 17 12:58:00 Finished candle/syntax-lib                                       10s 680MB
Feb 17 12:58:00 Starting candle/standard/syntax
Feb 17 12:59:55 Finished candle/standard/syntax                                1m54s 969MB
Feb 17 12:59:55 Starting candle/standard/semantics
Feb 17 13:01:43 Finished candle/standard/semantics                             1m47s   1GB
Feb 17 13:01:43 Starting candle/standard/monadic
Feb 17 13:03:33 Finished candle/standard/monadic                               1m50s   1GB
Feb 17 13:03:33 Starting candle/standard/ml_kernel
Feb 17 13:09:43 Finished candle/standard/ml_kernel                             6m09s   5GB
Feb 17 13:09:43 Starting candle/overloading/syntax
Feb 17 13:13:03 Finished candle/overloading/syntax                             3m19s   1GB
Feb 17 13:13:03 Starting candle/overloading/semantics
Feb 17 13:25:55 Finished candle/overloading/semantics                         12m51s   4GB
Feb 17 13:25:55 Starting characteristic/examples
Feb 17 13:27:21 Finished characteristic/examples                               1m26s   2GB
Feb 17 13:27:22 Starting tutorial/solutions
Feb 17 13:43:40 Finished tutorial/solutions                                   16m18s   7GB
Feb 17 13:43:40 Starting translator/monadic/examples
Feb 17 13:46:57 Finished translator/monadic/examples                           3m16s   2GB
Feb 17 13:46:57 Starting examples
Feb 17 13:56:15 Finished examples                                              9m17s   3GB
Feb 17 13:56:15 Starting examples/compilation/x64
Feb 17 16:25:32 Finished examples/compilation/x64                           2h29m15s  17GB
Feb 17 16:25:32 Starting examples/compilation/x64/proofs
Feb 17 16:27:26 Finished examples/compilation/x64/proofs                       1m53s   3GB
Feb 17 16:27:26 Starting examples/compilation/ag32
Feb 17 17:02:49 Finished examples/compilation/ag32                            35m22s   6GB
Feb 17 17:02:49 Starting examples/compilation/ag32/proofs
Feb 17 17:03:38 Finished examples/compilation/ag32/proofs                        48s   3GB
Feb 17 17:03:38 Starting examples/cost
Feb 17 17:18: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
size_ofPropsTheory                              real:   29s  user:   28s     OK
miniBasisProgTheory                             real:   30s  user:   28s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                 real:   95s  user:   91s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  661s  user:  729s     OK
Starting work on lcgLoopProofTheory
allProgTheory                                   real:  642s  user:  699s     OK
Starting work on allProofTheory
pureLoopProgTheory                              real:  658s  user:  708s     OK
Starting work on pureLoopProofTheory
pureLoopProofTheory                             real:  146s  user:  142sFAIL<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