CakeML Regression Test

Job 1488

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
Merging into:d799d23caefc9c1971792072350c9dd7c1779c53
  Update COPYING [Mar 02 09:44:55]
HOL:9bceeb0943cf71103527d68d69a659cb3c78c74e
  Print diagnostic about value of Int.maxInt in configure's output [Mar 09 05:51:19]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 10 20:45:01 Claimed job
Mar 10 20:45:06 Building HOL
Mar 10 21:01:22 Starting developers
Mar 10 21:01:27 Finished developers                                               4s 157MB
Mar 10 21:01:27 Starting developers/bin
Mar 10 21:01:34 Finished developers/bin                                           6s   1GB
Mar 10 21:01:34 Starting semantics/ffi
Mar 10 21:01:45 Finished semantics/ffi                                           11s 246MB
Mar 10 21:01:46 Starting semantics
Mar 10 21:03:23 Finished semantics                                             1m36s   1GB
Mar 10 21:03:23 Starting semantics/proofs
Mar 10 21:07:14 Finished semantics/proofs                                      3m50s 939MB
Mar 10 21:07:14 Starting basis/pure
Mar 10 21:10:24 Finished basis/pure                                            3m09s 892MB
Mar 10 21:10:24 Starting translator
Mar 10 21:14:06 Finished translator                                            3m40s   1GB
Mar 10 21:14:06 Starting compiler/parsing
Mar 10 21:15:22 Finished compiler/parsing                                      1m16s   2GB
Mar 10 21:15:22 Starting characteristic
Mar 10 21:21:19 Finished characteristic                                        5m56s   1GB
Mar 10 21:21:20 Starting translator/monadic
Mar 10 21:23:03 Finished translator/monadic                                    1m43s   1GB
Mar 10 21:23:03 Starting basis
Mar 10 22:10:58 Finished basis                                                47m54s  16GB
Mar 10 22:10:58 Starting compiler/inference
Mar 10 22:12:18 Finished compiler/inference                                    1m19s   1GB
Mar 10 22:12:19 Starting compiler/backend/reg_alloc
Mar 10 22:13:28 Finished compiler/backend/reg_alloc                            1m09s   1GB
Mar 10 22:13:28 Starting compiler/backend/gc
Mar 10 22:17:18 Finished compiler/backend/gc                                   3m49s   2GB
Mar 10 22:17:18 Starting compiler/backend
Mar 10 22:22:27 Finished compiler/backend                                      5m08s   4GB
Mar 10 22:22:27 Starting compiler/encoders/asm
Mar 10 22:22:50 Finished compiler/encoders/asm                                   22s 732MB
Mar 10 22:22:50 Starting compiler/encoders/x64
Mar 10 22:23:56 Finished compiler/encoders/x64                                 1m05s 811MB
Mar 10 22:23:56 Starting compiler/encoders/arm7
Mar 10 22:26:10 Finished compiler/encoders/arm7                                2m13s   1GB
Mar 10 22:26:10 Starting compiler/encoders/arm8
Mar 10 22:26:50 Finished compiler/encoders/arm8                                  40s 942MB
Mar 10 22:26:51 Starting compiler/encoders/mips
Mar 10 22:28:27 Finished compiler/encoders/mips                                1m36s   1GB
Mar 10 22:28:28 Starting compiler/encoders/riscv
Mar 10 22:30:19 Finished compiler/encoders/riscv                               1m50s 885MB
Mar 10 22:30:19 Starting compiler/encoders/ag32
Mar 10 22:30:37 Finished compiler/encoders/ag32                                  18s 866MB
Mar 10 22:30:38 Starting compiler/backend/x64
Mar 10 22:30:57 Finished compiler/backend/x64                                    19s   1GB
Mar 10 22:30:58 Starting compiler/backend/arm7
Mar 10 22:31:19 Finished compiler/backend/arm7                                   20s   1GB
Mar 10 22:31:19 Starting compiler/backend/arm8
Mar 10 22:31:39 Finished compiler/backend/arm8                                   19s   1GB
Mar 10 22:31:39 Starting compiler/backend/mips
Mar 10 22:31:59 Finished compiler/backend/mips                                   19s   1GB
Mar 10 22:31:59 Starting compiler/backend/riscv
Mar 10 22:32:18 Finished compiler/backend/riscv                                  18s   1GB
Mar 10 22:32:18 Starting compiler/backend/ag32
Mar 10 22:33:32 Finished compiler/backend/ag32                                 1m13s   1GB
Mar 10 22:33:32 Starting compiler/parsing/proofs
Mar 10 22:39:44 Finished compiler/parsing/proofs                               6m11s 914MB
Mar 10 22:39:44 Starting compiler/inference/proofs
Mar 10 22:42:24 Finished compiler/inference/proofs                             2m39s 987MB
Mar 10 22:42:24 Starting compiler/backend/semantics
Mar 10 23:15:38 Finished compiler/backend/semantics                           33m13s   2GB
Mar 10 23:15:38 Starting compiler/backend/reg_alloc/proofs
Mar 10 23:19:30 Finished compiler/backend/reg_alloc/proofs                     3m51s 738MB
Mar 10 23:19:30 Starting compiler/backend/proofs
Mar 11 00:18:37 Finished compiler/backend/proofs                              59m06s  21GB
Mar 11 00:18:37 Starting compiler/encoders/x64/proofs
Mar 11 00:28:59 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Mar 11 00:28:59 Starting compiler/encoders/arm7/proofs
Mar 11 00:43:12 Finished compiler/encoders/arm7/proofs                        14m12s   5GB
Mar 11 00:43:12 Starting compiler/encoders/arm8/proofs
Mar 11 00:50:21 Finished compiler/encoders/arm8/proofs                         7m08s   1GB
Mar 11 00:50:21 Starting compiler/encoders/mips/proofs
Mar 11 01:01:12 Finished compiler/encoders/mips/proofs                        10m51s   2GB
Mar 11 01:01:13 Starting compiler/encoders/riscv/proofs
Mar 12 08:44:29 Resuming compiler/encoders/riscv/proofs
Mar 12 08:44:30 Finished compiler/encoders/riscv/proofs                           0s  13MB
Mar 12 08:44:30 Starting compiler/encoders/ag32/proofs
Mar 12 08:47:18 Finished compiler/encoders/ag32/proofs                         2m47s 683MB
Mar 12 08:47:18 Starting compiler/backend/x64/proofs
Mar 12 08:47:41 Finished compiler/backend/x64/proofs                             22s   1GB
Mar 12 08:47:41 Starting compiler/backend/arm7/proofs
Mar 12 08:48:05 Finished compiler/backend/arm7/proofs                            23s   1GB
Mar 12 08:48:06 Starting compiler/backend/arm8/proofs
Mar 12 08:48:29 Finished compiler/backend/arm8/proofs                            23s   1GB
Mar 12 08:48:29 Starting compiler/backend/mips/proofs
Mar 12 08:48:52 Finished compiler/backend/mips/proofs                            22s   1GB
Mar 12 08:48:52 Starting compiler/backend/riscv/proofs
Mar 12 08:49:15 Finished compiler/backend/riscv/proofs                           22s   1GB
Mar 12 08:49:15 Starting compiler/backend/ag32/proofs
Mar 12 09:02:51 Finished compiler/backend/ag32/proofs                         13m35s   3GB
Mar 12 09:02:51 Starting compiler/proofs
Mar 12 09:04:50 Finished compiler/proofs                                       1m58s   3GB
Mar 12 09:04:50 Starting candle/set-theory
Mar 12 09:05:20 Finished candle/set-theory                                       29s 844MB
Mar 12 09:05:20 Starting candle/syntax-lib
Mar 12 09:05:31 Finished candle/syntax-lib                                       11s 476MB
Mar 12 09:05:32 Starting candle/standard/syntax
Mar 12 09:07:28 Finished candle/standard/syntax                                1m56s   1GB
Mar 12 09:07:29 Starting candle/standard/semantics
Mar 12 09:09:17 Finished candle/standard/semantics                             1m48s   1GB
Mar 12 09:09:18 Starting candle/standard/monadic
Mar 12 09:11:09 Finished candle/standard/monadic                               1m51s   1GB
Mar 12 09:11:09 Starting candle/standard/ml_kernel
Mar 12 09:17:22 Finished candle/standard/ml_kernel                             6m13s   4GB
Mar 12 09:17:23 Starting candle/overloading/syntax
Mar 12 09:20:43 Finished candle/overloading/syntax                             3m20s   1GB
Mar 12 09:20:43 Starting candle/overloading/semantics
Mar 12 09:33:47 Finished candle/overloading/semantics                         13m03s   3GB
Mar 12 09:33:47 Starting characteristic/examples
Mar 12 09:35:12 Finished characteristic/examples                               1m24s   2GB
Mar 12 09:35:12 Starting tutorial/solutions
Mar 12 09:51:02 Finished tutorial/solutions                                   15m49s   8GB
Mar 12 09:51:02 Starting translator/monadic/examples
Mar 12 09:54:29 Finished translator/monadic/examples                           3m26s   3GB
Mar 12 09:54:29 Starting examples
Mar 12 10:03:46 Finished examples                                              9m16s   4GB
Mar 12 10:03:46 Starting examples/compilation/x64
Mar 12 12:32:55 Finished examples/compilation/x64                           2h29m08s  13GB
Mar 12 12:32:55 Starting examples/compilation/x64/proofs
Mar 12 12:34:42 Finished examples/compilation/x64/proofs                       1m46s   3GB
Mar 12 12:34:42 Starting examples/compilation/ag32
Mar 12 13:09:36 Finished examples/compilation/ag32                            34m53s   7GB
Mar 12 13:09:36 Starting examples/compilation/ag32/proofs
Mar 12 13:10:24 Finished examples/compilation/ag32/proofs                        47s   2GB
Mar 12 13:10:24 Starting examples/cost
Mar 12 13:25:11 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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/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:   29s  user:   28s     OK
miniBasisProgTheory                             real:   30s  user:   29s     OK
Starting work on lcgLoopProgTheory
costPropsTheory                                 real:   99s  user:   96s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                               real:  638s  user:  708s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                              real:  633s  user:  680s     OK
Starting work on pureLoopProofTheory
allProgTheory                                   real:  660s  user:  714s     OK
Starting work on allProofTheory
pureLoopProofTheory                             real:  151s  user:  147sFAIL<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