CakeML Regression Test

Job 1470

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:684b665d7eb337ccab2173351f6356213e6d7e54
  Adjust signature names [Feb 05 04:46:20]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 08 18:55:37 Claimed job
Feb 08 18:55:41 Reusing HOL
Feb 08 18:56:29 Starting developers
Feb 08 18:56:33 Finished developers                                               4s 108MB
Feb 08 18:56:33 Starting developers/bin
Feb 08 18:56:40 Finished developers/bin                                           6s   1GB
Feb 08 18:56:40 Starting semantics/ffi
Feb 08 18:56:52 Finished semantics/ffi                                           11s 222MB
Feb 08 18:56:52 Starting semantics
Feb 08 18:58:19 Finished semantics                                             1m27s   1GB
Feb 08 18:58:20 Starting semantics/proofs
Feb 08 19:02:13 Finished semantics/proofs                                      3m53s   1GB
Feb 08 19:02:13 Starting basis/pure
Feb 08 19:03:05 Finished basis/pure                                              51s 817MB
Feb 08 19:03:05 Starting translator
Feb 08 19:06:43 Finished translator                                            3m37s   2GB
Feb 08 19:06:43 Starting compiler/parsing
Feb 08 19:07:59 Finished compiler/parsing                                      1m15s   2GB
Feb 08 19:07:59 Starting characteristic
Feb 08 19:13:52 Finished characteristic                                        5m52s   1GB
Feb 08 19:13:52 Starting translator/monadic
Feb 08 19:15:35 Finished translator/monadic                                    1m43s   1GB
Feb 08 19:15:35 Starting basis
Feb 08 20:03:46 Finished basis                                                48m09s  14GB
Feb 08 20:03:46 Starting compiler/inference
Feb 08 20:04:55 Finished compiler/inference                                    1m09s 992MB
Feb 08 20:04:55 Starting compiler/backend/reg_alloc
Feb 08 20:06:03 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 08 20:06:03 Starting compiler/backend/gc
Feb 08 20:09:37 Finished compiler/backend/gc                                   3m34s   2GB
Feb 08 20:09:37 Starting compiler/backend
Feb 08 20:14:45 Finished compiler/backend                                      5m07s   3GB
Feb 08 20:14:45 Starting compiler/encoders/asm
Feb 08 20:15:09 Finished compiler/encoders/asm                                   23s 706MB
Feb 08 20:15:09 Starting compiler/encoders/x64
Feb 08 20:15:35 Finished compiler/encoders/x64                                   26s 997MB
Feb 08 20:15:35 Starting compiler/encoders/arm7
Feb 08 20:16:29 Finished compiler/encoders/arm7                                  53s 951MB
Feb 08 20:16:29 Starting compiler/encoders/arm8
Feb 08 20:16:43 Finished compiler/encoders/arm8                                  13s 929MB
Feb 08 20:16:43 Starting compiler/encoders/mips
Feb 08 20:17:01 Finished compiler/encoders/mips                                  17s   1GB
Feb 08 20:17:01 Starting compiler/encoders/riscv
Feb 08 20:17:17 Finished compiler/encoders/riscv                                 16s 750MB
Feb 08 20:17:18 Starting compiler/encoders/ag32
Feb 08 20:17:36 Finished compiler/encoders/ag32                                  18s 851MB
Feb 08 20:17:36 Starting compiler/backend/x64
Feb 08 20:17:56 Finished compiler/backend/x64                                    19s   1GB
Feb 08 20:17:56 Starting compiler/backend/arm7
Feb 08 20:18:17 Finished compiler/backend/arm7                                   21s   1GB
Feb 08 20:18:17 Starting compiler/backend/arm8
Feb 08 20:18:37 Finished compiler/backend/arm8                                   19s   1GB
Feb 08 20:18:38 Starting compiler/backend/mips
Feb 08 20:18:59 Finished compiler/backend/mips                                   20s   1GB
Feb 08 20:18:59 Starting compiler/backend/riscv
Feb 08 20:19:19 Finished compiler/backend/riscv                                  20s   1GB
Feb 08 20:19:19 Starting compiler/backend/ag32
Feb 08 20:20:33 Finished compiler/backend/ag32                                 1m13s   1GB
Feb 08 20:20:33 Starting compiler/parsing/proofs
Feb 08 20:26:44 Finished compiler/parsing/proofs                               6m10s   1GB
Feb 08 20:26:44 Starting compiler/inference/proofs
Feb 08 20:29:23 Finished compiler/inference/proofs                             2m38s   1GB
Feb 08 20:29:23 Starting compiler/backend/semantics
Feb 08 21:03:01 Finished compiler/backend/semantics                           33m37s   1GB
Feb 08 21:03:01 Starting compiler/backend/reg_alloc/proofs
Feb 08 21:06:48 Finished compiler/backend/reg_alloc/proofs                     3m47s   1GB
Feb 08 21:06:49 Starting compiler/backend/proofs
Feb 08 22:06:03 Finished compiler/backend/proofs                              59m13s  25GB
Feb 08 22:06:03 Starting compiler/encoders/x64/proofs
Feb 08 22:16:28 Finished compiler/encoders/x64/proofs                         10m23s   6GB
Feb 08 22:16:28 Starting compiler/encoders/arm7/proofs
Feb 08 22:30:27 Finished compiler/encoders/arm7/proofs                        13m58s   7GB
Feb 08 22:30:27 Starting compiler/encoders/arm8/proofs
Feb 08 22:37:33 Finished compiler/encoders/arm8/proofs                         7m05s   1GB
Feb 08 22:37:33 Starting compiler/encoders/mips/proofs
Feb 08 22:48:26 Finished compiler/encoders/mips/proofs                        10m52s   2GB
Feb 08 22:48:26 Starting compiler/encoders/riscv/proofs
Feb 08 22:58:05 Finished compiler/encoders/riscv/proofs                        9m38s   1GB
Feb 08 22:58:05 Starting compiler/encoders/ag32/proofs
Feb 08 23:00:52 Finished compiler/encoders/ag32/proofs                         2m46s   1GB
Feb 08 23:00:52 Starting compiler/backend/x64/proofs
Feb 08 23:01:14 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 08 23:01:15 Starting compiler/backend/arm7/proofs
Feb 08 23:01:38 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 08 23:01:38 Starting compiler/backend/arm8/proofs
Feb 08 23:01:59 Finished compiler/backend/arm8/proofs                            21s   1GB
Feb 08 23:02:00 Starting compiler/backend/mips/proofs
Feb 08 23:02:24 Finished compiler/backend/mips/proofs                            23s   1GB
Feb 08 23:02:24 Starting compiler/backend/riscv/proofs
Feb 08 23:02:46 Finished compiler/backend/riscv/proofs                           22s   1GB
Feb 08 23:02:46 Starting compiler/backend/ag32/proofs
Feb 08 23:16:34 Finished compiler/backend/ag32/proofs                         13m46s   2GB
Feb 08 23:16:34 Starting compiler/proofs
Feb 08 23:18:15 Finished compiler/proofs                                       1m40s   4GB
Feb 08 23:18:15 Starting candle/set-theory
Feb 08 23:18:45 Finished candle/set-theory                                       29s 922MB
Feb 08 23:18:45 Starting candle/syntax-lib
Feb 08 23:18:56 Finished candle/syntax-lib                                       11s 680MB
Feb 08 23:18:57 Starting candle/standard/syntax
Feb 08 23:20:51 Finished candle/standard/syntax                                1m54s 940MB
Feb 08 23:20:51 Starting candle/standard/semantics
Feb 08 23:22:41 Finished candle/standard/semantics                             1m49s   1GB
Feb 08 23:22:41 Starting candle/standard/monadic
Feb 08 23:24:31 Finished candle/standard/monadic                               1m49s   1GB
Feb 08 23:24:32 Starting candle/standard/ml_kernel
Feb 08 23:30:46 Finished candle/standard/ml_kernel                             6m14s   5GB
Feb 08 23:30:46 Starting candle/overloading/syntax
Feb 08 23:34:08 Finished candle/overloading/syntax                             3m21s   1GB
Feb 08 23:34:08 Starting candle/overloading/semantics
Feb 08 23:47:07 Finished candle/overloading/semantics                         12m59s   4GB
Feb 08 23:47:08 Starting characteristic/examples
Feb 08 23:48:32 Finished characteristic/examples                               1m24s   3GB
Feb 08 23:48:32 Starting tutorial/solutions
Feb 09 00:05:03 Finished tutorial/solutions                                   16m29s   7GB
Feb 09 00:05:03 Starting translator/monadic/examples
Feb 09 00:08:22 Finished translator/monadic/examples                           3m19s   3GB
Feb 09 00:08:22 Starting examples
Feb 09 00:17:40 Finished examples                                              9m16s   5GB
Feb 09 00:17:40 Starting examples/compilation/x64
Feb 09 02:49:43 Finished examples/compilation/x64                           2h32m02s  15GB
Feb 09 02:49:43 Starting examples/compilation/x64/proofs
Feb 09 02:51:37 Finished examples/compilation/x64/proofs                       1m53s   3GB
Feb 09 02:51:37 Starting examples/compilation/ag32
Feb 09 03:27:17 Finished examples/compilation/ag32                            35m39s   7GB
Feb 09 03:27:17 Starting examples/compilation/ag32/proofs
Feb 09 03:28:05 Finished examples/compilation/ag32/proofs                        47s   3GB
Feb 09 03:28:05 Starting examples/cost
Feb 09 03:42:39 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:   30s  user:   29s     OK
miniBasisProgTheory                             real:   30s  user:   29s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                 real:   97s  user:   94s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  656s  user:  723s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  626s  user:  678s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  661s  user:  712s     OK
Starting work on allProofTheory
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