CakeML Regression Test

Job 1954

CakeML:42712c3f0757b8330cf98aaa30c0f4ed2800a50c
  Make bootstrap test ./cake --types output of basis [Jul 04 20:44:29]
#895 (issue894)
Merging into:cbf165f01258b1e3d4f325d1e849520e87d4ee71
  Fix a couple of proofs broken by recent HOL changes [Jul 04 23:33:18]
HOL:36b541e828806d911b2fee3e1cb1e3298068dfd9
  Tidy up some simpleSexp proofs [Jul 01 07:00:10]
Machine:oven3

Jul 05 06:31:04 Claimed job
Jul 05 06:31:06 Reusing HOL
Jul 05 06:31:57 Starting developers
Jul 05 06:32:07 Finished developers                                               9s 145MB
Jul 05 06:32:07 Starting developers/bin
Jul 05 06:32:19 Finished developers/bin                                          11s   1GB
Jul 05 06:32:19 Starting semantics/ffi
Jul 05 06:32:44 Finished semantics/ffi                                           24s 221MB
Jul 05 06:32:44 Starting semantics
Jul 05 06:37:51 Finished semantics                                             5m06s   1GB
Jul 05 06:37:51 Starting semantics/proofs
Jul 05 06:53:32 Finished semantics/proofs                                     15m40s   1GB
Jul 05 06:53:32 Starting semantics/alt_semantics
Jul 05 06:54:30 Finished semantics/alt_semantics                                 57s 530MB
Jul 05 06:54:30 Starting semantics/alt_semantics/proofs
Jul 05 07:20:16 Finished semantics/alt_semantics/proofs                       25m45s   2GB
Jul 05 07:20:16 Starting basis/pure
Jul 05 07:22:34 Finished basis/pure                                            2m18s 874MB
Jul 05 07:22:35 Starting translator
Jul 05 07:30:34 Finished translator                                            7m58s   1GB
Jul 05 07:30:34 Starting compiler/parsing
Jul 05 07:33:31 Finished compiler/parsing                                      2m56s   4GB
Jul 05 07:33:32 Starting characteristic
Jul 05 07:48:17 Finished characteristic                                       14m45s   2GB
Jul 05 07:48:17 Starting translator/monadic
Jul 05 07:52:29 Finished translator/monadic                                    4m11s   1GB
Jul 05 07:52:29 Starting basis
Jul 05 09:49:13 Finished basis                                              1h56m43s  19GB
Jul 05 09:49:13 Starting compiler/inference
Jul 05 09:52:48 Finished compiler/inference                                    3m34s   1GB
Jul 05 09:52:49 Starting compiler/backend/reg_alloc
Jul 05 09:55:58 Finished compiler/backend/reg_alloc                            3m09s   1GB
Jul 05 09:55:58 Starting compiler/backend/gc
Jul 05 10:04:35 Finished compiler/backend/gc                                   8m36s   2GB
Jul 05 10:04:35 Starting compiler/backend
Jul 05 10:16:45 Finished compiler/backend                                     12m09s   2GB
Jul 05 10:16:45 Starting compiler/encoders/asm
Jul 05 10:17:52 Finished compiler/encoders/asm                                 1m06s   1GB
Jul 05 10:17:52 Starting compiler/encoders/x64
Jul 05 10:20:26 Finished compiler/encoders/x64                                 2m33s   1GB
Jul 05 10:20:26 Starting compiler/encoders/arm7
Jul 05 10:25:15 Finished compiler/encoders/arm7                                4m48s   1GB
Jul 05 10:25:15 Starting compiler/encoders/arm8
Jul 05 10:26:49 Finished compiler/encoders/arm8                                1m33s   1GB
Jul 05 10:26:49 Starting compiler/encoders/arm8_asl
Jul 05 14:48:01 Finished compiler/encoders/arm8_asl                         4h21m11s  38GB
Jul 05 14:48:01 Starting compiler/encoders/mips
Jul 05 14:51:37 Finished compiler/encoders/mips                                3m36s   1GB
Jul 05 14:51:38 Starting compiler/encoders/riscv
Jul 05 14:55:31 Finished compiler/encoders/riscv                               3m53s 922MB
Jul 05 14:55:31 Starting compiler/encoders/ag32
Jul 05 14:56:20 Finished compiler/encoders/ag32                                  48s 601MB
Jul 05 14:56:20 Starting compiler/backend/x64
Jul 05 14:57:11 Finished compiler/backend/x64                                    50s   1GB
Jul 05 14:57:11 Starting compiler/backend/arm7
Jul 05 14:58:04 Finished compiler/backend/arm7                                   52s   1GB
Jul 05 14:58:05 Starting compiler/backend/arm8
Jul 05 14:58:52 Finished compiler/backend/arm8                                   47s   1GB
Jul 05 14:58:52 Starting compiler/backend/mips
Jul 05 14:59:47 Finished compiler/backend/mips                                   54s   1GB
Jul 05 14:59:47 Starting compiler/backend/riscv
Jul 05 15:00:35 Finished compiler/backend/riscv                                  47s   1GB
Jul 05 15:00:35 Starting compiler/backend/ag32
Jul 05 15:03:37 Finished compiler/backend/ag32                                 3m01s   1GB
Jul 05 15:03:37 Starting compiler/parsing/proofs
Jul 05 15:12:15 Finished compiler/parsing/proofs                               8m37s   1GB
Jul 05 15:12:15 Starting compiler/inference/proofs
Jul 05 15:18:19 Finished compiler/inference/proofs                             6m03s   1GB
Jul 05 15:18:19 Starting compiler/backend/semantics
Jul 05 16:15:17 Finished compiler/backend/semantics                           56m57s   2GB
Jul 05 16:15:18 Starting compiler/backend/reg_alloc/proofs
Jul 05 16:23:32 Finished compiler/backend/reg_alloc/proofs                     8m13s   1GB
Jul 05 16:23:32 Starting compiler/backend/proofs
Jul 05 18:15:25 Finished compiler/backend/proofs                            1h51m52s  16GB
Jul 05 18:15:25 Starting compiler/backend/serialiser
Jul 05 18:18:56 Finished compiler/backend/serialiser                           3m29s   2GB
Jul 05 18:18:56 Starting compiler/encoders/x64/proofs
Jul 05 18:40:53 Finished compiler/encoders/x64/proofs                         21m56s   4GB
Jul 05 18:40:53 Starting compiler/encoders/arm7/proofs
Jul 05 19:12:08 Finished compiler/encoders/arm7/proofs                        31m14s   3GB
Jul 05 19:12:08 Starting compiler/encoders/arm8/proofs
Jul 05 19:27:46 Finished compiler/encoders/arm8/proofs                        15m37s   1GB
Jul 05 19:27:46 Starting compiler/encoders/arm8_asl/proofs
Jul 05 21:22:08 Finished compiler/encoders/arm8_asl/proofs                  1h54m20s   9GB
Jul 05 21:22:08 Starting compiler/encoders/mips/proofs
Jul 05 21:46:14 Finished compiler/encoders/mips/proofs                        24m06s   2GB
Jul 05 21:46:14 Starting compiler/encoders/riscv/proofs
Jul 05 22:06:38 Finished compiler/encoders/riscv/proofs                       20m23s   1GB
Jul 05 22:06:38 Starting compiler/encoders/ag32/proofs
Jul 05 22:12:34 Finished compiler/encoders/ag32/proofs                         5m56s 824MB
Jul 05 22:12:34 Starting compiler/backend/x64/proofs
Jul 05 22:13:35 Finished compiler/backend/x64/proofs                           1m00s   1GB
Jul 05 22:13:36 Starting compiler/backend/arm7/proofs
Jul 05 22:14:38 Finished compiler/backend/arm7/proofs                          1m01s   1GB
Jul 05 22:14:38 Starting compiler/backend/arm8/proofs
Jul 05 22:15:42 Finished compiler/backend/arm8/proofs                          1m03s   1GB
Jul 05 22:15:42 Starting compiler/backend/arm8_asl
Jul 05 22:16:33 Finished compiler/backend/arm8_asl                               51s   1GB
Jul 05 22:16:33 Starting compiler/backend/mips/proofs
Jul 05 22:17:36 Finished compiler/backend/mips/proofs                          1m02s   1GB
Jul 05 22:17:36 Starting compiler/backend/riscv/proofs
Jul 05 22:18:38 Finished compiler/backend/riscv/proofs                         1m02s   1GB
Jul 05 22:18:39 Starting compiler/backend/ag32/proofs
Jul 05 22:50:06 Finished compiler/backend/ag32/proofs                         31m27s   2GB
Jul 05 22:50:07 Starting compiler/proofs
Jul 05 22:55:29 Finished compiler/proofs                                       5m21s   3GB
Jul 05 22:55:29 Starting candle/set-theory
Jul 05 22:56:40 Finished candle/set-theory                                     1m11s   1GB
Jul 05 22:56:41 Starting candle/syntax-lib
Jul 05 22:57:10 Finished candle/syntax-lib                                       29s 730MB
Jul 05 22:57:10 Starting candle/standard/syntax
Jul 05 23:01:38 Finished candle/standard/syntax                                4m27s   1GB
Jul 05 23:01:39 Starting candle/standard/semantics
Jul 05 23:05:46 Finished candle/standard/semantics                             4m07s   1GB
Jul 05 23:05:46 Starting candle/standard/monadic
Jul 05 23:09:51 Finished candle/standard/monadic                               4m04s   1GB
Jul 05 23:09:51 Starting candle/standard/ml_kernel
Jul 05 23:23:34 Finished candle/standard/ml_kernel                            13m42s   3GB
Jul 05 23:23:34 Starting candle/overloading/syntax
Jul 05 23:30:35 Finished candle/overloading/syntax                             7m00s   1GB
Jul 05 23:30:35 Starting candle/overloading/semantics
Jul 05 23:57:07 Finished candle/overloading/semantics                         26m31s   2GB
Jul 05 23:57:07 Starting candle/overloading/monadic
Jul 06 00:02:44 Finished candle/overloading/monadic                            5m36s   2GB
Jul 06 00:02:44 Starting candle/overloading/ml_kernel
Jul 06 00:18:40 Finished candle/overloading/ml_kernel                         15m55s   3GB
Jul 06 00:18:40 Starting candle/overloading/ml_checker
Jul 06 00:24:07 Finished candle/overloading/ml_checker                         5m27s   3GB
Jul 06 00:24:08 Starting candle/prover
Jul 06 00:48:08 Finished candle/prover                                        23m59s   2GB
Jul 06 00:48:08 Starting pancake
Jul 06 00:56:07 Finished pancake                                               7m58s   3GB
Jul 06 00:56:07 Starting pancake/ffi
Jul 06 00:56:08 Finished pancake/ffi                                              0s  34MB
Jul 06 00:56:08 Starting pancake/semantics
Jul 06 01:01:40 Finished pancake/semantics                                     5m31s   1GB
Jul 06 01:01:41 Starting pancake/proofs
Jul 06 01:28:56 Finished pancake/proofs                                       27m14s   5GB
Jul 06 01:28:56 Starting characteristic/examples
Jul 06 01:32:20 Finished characteristic/examples                               3m23s   3GB
Jul 06 01:32:20 Starting tutorial/solutions
Jul 06 02:07:00 Finished tutorial/solutions                                   34m38s   9GB
Jul 06 02:07:00 Starting translator/monadic/examples
Jul 06 02:14:16 Finished translator/monadic/examples                           7m15s   3GB
Jul 06 02:14:16 Starting examples
Jul 06 02:33:58 Finished examples                                             19m42s   3GB
Jul 06 02:33:59 Starting examples/compilation/x64
Jul 06 07:09:46 Finished examples/compilation/x64                           4h35m46s  27GB
Jul 06 07:09:46 Starting examples/compilation/x64/proofs
Jul 06 07:14:42 Finished examples/compilation/x64/proofs                       4m55s   3GB
Jul 07 10:52:55 Resuming examples/compilation/ag32
Jul 07 12:07:16 Finished examples/compilation/ag32                          1h14m21s   8GB
Jul 07 12:07:17 Starting examples/compilation/ag32/proofs
Jul 07 12:09:10 Finished examples/compilation/ag32/proofs                      1m53s   2GB
Jul 07 12:09:10 Starting examples/lpr_checker
Jul 07 12:11:25 Finished examples/lpr_checker                                  2m14s 939MB
Jul 07 12:11:25 Starting examples/lpr_checker/array
Jul 07 13:29:03 Finished examples/lpr_checker/array                         1h17m37s   6GB
Jul 07 13:29:03 Starting examples/lpr_checker/array/compilation
Jul 07 14:49:35 Finished examples/lpr_checker/array/compilation             1h20m31s  38GB
Jul 07 14:49:35 Starting examples/lpr_checker/array/compilation/proofs
Jul 07 14:52:29 Finished examples/lpr_checker/array/compilation/proofs         2m53s   5GB
Jul 07 14:52:29 Starting examples/opentheory
Jul 07 15:15:30 Finished examples/opentheory                                  23m01s   3GB
Jul 07 15:15:31 Starting examples/opentheory
Jul 07 15:15:34 Finished examples/opentheory                                      2s  32MB
Jul 07 15:15:34 Starting examples/opentheory/compilation
Jul 07 16:37:13 Finished examples/opentheory/compilation                    1h21m38s  29GB
Jul 07 16:37:14 Starting examples/opentheory/compilation/proofs
Jul 07 16:39:50 Finished examples/opentheory/compilation/proofs                2m35s   3GB
Jul 07 16:39:50 Starting examples/opentheory/compilation/ag32
Jul 07 18:03:28 Finished examples/opentheory/compilation/ag32               1h23m37s  49GB
Jul 07 18:03:28 Starting examples/opentheory/compilation/ag32/proofs
Jul 07 18:07:14 Finished examples/opentheory/compilation/ag32/proofs           3m45s   6GB
Jul 07 18:07:14 Starting examples/sat_encodings
Jul 07 18:11:42 Finished examples/sat_encodings                                4m27s   1GB
Jul 07 18:11:42 Starting examples/sat_encodings/case_studies
Jul 07 18:15:29 Finished examples/sat_encodings/case_studies                   3m46s 962MB
Jul 07 18:15:29 Starting examples/sat_encodings/translation
Jul 07 18:27:38 Finished examples/sat_encodings/translation                   12m08s   4GB
Jul 07 18:27:38 Starting examples/sat_encodings/translation/compilation
Jul 07 19:53:55 Finished examples/sat_encodings/translation/compilation     1h26m16s  23GB
Jul 07 19:53:55 Starting examples/deflate
Jul 07 19:55:55 Finished examples/deflate                                      1m59s   1GB
Jul 07 19:55:55 Starting examples/deflate/translation
Jul 07 19:58:56 Finished examples/deflate/translation                          3m00s   3GB
Jul 07 19:58:56 Starting examples/deflate/translation/compilation
Jul 07 20:27:54 FAILED: examples/deflate/translation/compilation
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/deflate[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/deflate/translation[0m
Scanned 77 directories
Starting work on README.md
Starting work on compressionCompileTheory
Starting work on decompressionCompileTheory
Starting work on deflateDecodeCompileTheory
README.md                                                                                                                                                                                             (0s)     OK
Starting work on deflateEncodeCompileTheory
compressionCompileTheory                                                                                                                                                                             (35m)     OK
decompressionCompileTheory                                                                                                                                                                           (36m)FAIL<1>
           lab_to_target real: 10m10s
           lab_to_target size: 1912764
                       export: runtime: 1.0s,    gctime: 0.19788s,     systime: 0.02663s.
 Saved theorem _______ "decompression_compiled"
 Exporting theory "decompressionCompile" ... Run out of store - interrupting threads
 error in quse /root/regression/cakeml-1954/examples/deflate/translation/compilation/decompressionCompileScript.sml : Interrupt
 error in load /root/regression/cakeml-1954/examples/deflate/translation/compilation/decompressionCompileScript : Interrupt
 
 Failure while writing theory!
 Uncaught exception: Interrupt
deflateDecodeCompileTheory                                                                                                                                                                           (40m)MKILLED
deflateEncodeCompileTheory                                                                                                                                                                           (46m)MKILLED