Job 1963

CakeML:971151a653e5a0c840aedc3747ca44c56a19300c
  Merge pull request #895 from CakeML/issue894 [Jul 13 08:19:06]
HOL:ba57e7156c32864446a2ef4c200a8ef296977a2e
  Get new contig example to build as part of -t1 [Jul 15 07:20:25]
Machine:oven3

Jul 18 08:00:43 Claimed job
Jul 18 08:00:49 Building HOL
Jul 18 08:24:18 Starting developers
Jul 18 08:24:28 Finished developers                                               9s 135MB
Jul 18 08:24:28 Starting developers/bin
Jul 18 08:24:41 Finished developers/bin                                          12s   1GB
Jul 18 08:24:41 Starting semantics/ffi
Jul 18 08:25:06 Finished semantics/ffi                                           24s 251MB
Jul 18 08:25:06 Starting semantics
Jul 18 08:30:27 Finished semantics                                             5m20s   1GB
Jul 18 08:30:28 Starting semantics/proofs
Jul 18 08:46:39 Finished semantics/proofs                                     16m10s   1GB
Jul 18 08:46:39 Starting semantics/alt_semantics
Jul 18 08:47:37 Finished semantics/alt_semantics                                 57s 543MB
Jul 18 08:47:37 Starting semantics/alt_semantics/proofs
Jul 18 09:13:08 Finished semantics/alt_semantics/proofs                       25m30s   2GB
Jul 18 09:13:08 Starting basis/pure
Jul 18 09:20:43 Finished basis/pure                                            7m34s 900MB
Jul 18 09:20:44 Starting translator
Jul 18 09:28:40 Finished translator                                            7m56s   2GB
Jul 18 09:28:40 Starting compiler/parsing
Jul 18 09:31:50 Finished compiler/parsing                                      3m09s   4GB
Jul 18 09:31:50 Starting characteristic
Jul 18 09:46:32 Finished characteristic                                       14m41s   2GB
Jul 18 09:46:32 Starting translator/monadic
Jul 18 09:50:51 Finished translator/monadic                                    4m18s   1GB
Jul 18 09:50:51 Starting basis
Jul 18 11:48:24 Finished basis                                              1h57m32s  17GB
Jul 18 11:48:24 Starting compiler/inference
Jul 18 11:51:59 Finished compiler/inference                                    3m34s   1GB
Jul 18 11:51:59 Starting compiler/backend/reg_alloc
Jul 18 11:55:14 Finished compiler/backend/reg_alloc                            3m14s   1GB
Jul 18 11:55:14 Starting compiler/backend/gc
Jul 18 12:04:03 Finished compiler/backend/gc                                   8m48s   2GB
Jul 18 12:04:04 Starting compiler/backend
Jul 18 12:16:15 Finished compiler/backend                                     12m10s   2GB
Jul 18 12:16:15 Starting compiler/encoders/asm
Jul 18 12:17:20 Finished compiler/encoders/asm                                 1m04s 746MB
Jul 18 12:17:20 Starting compiler/encoders/x64
Jul 18 12:19:54 Finished compiler/encoders/x64                                 2m34s 728MB
Jul 18 12:19:55 Starting compiler/encoders/arm7
Jul 18 12:24:47 Finished compiler/encoders/arm7                                4m52s   1GB
Jul 18 12:24:48 Starting compiler/encoders/arm8
Jul 18 12:26:25 Finished compiler/encoders/arm8                                1m36s 789MB
Jul 18 12:26:25 Starting compiler/encoders/arm8_asl
Jul 18 16:43:29 Finished compiler/encoders/arm8_asl                         4h17m03s  23GB
Jul 18 16:43:29 Starting compiler/encoders/mips
Jul 18 16:46:53 Finished compiler/encoders/mips                                3m23s   1GB
Jul 18 16:46:53 Starting compiler/encoders/riscv
Jul 18 16:50:52 Finished compiler/encoders/riscv                               3m58s   1GB
Jul 18 16:50:52 Starting compiler/encoders/ag32
Jul 18 16:51:44 Finished compiler/encoders/ag32                                  51s 963MB
Jul 18 16:51:44 Starting compiler/backend/x64
Jul 18 16:52:31 Finished compiler/backend/x64                                    46s   1GB
Jul 18 16:52:32 Starting compiler/backend/arm7
Jul 18 16:53:28 Finished compiler/backend/arm7                                   55s   1GB
Jul 18 16:53:28 Starting compiler/backend/arm8
Jul 18 16:54:18 Finished compiler/backend/arm8                                   50s   1GB
Jul 18 16:54:19 Starting compiler/backend/mips
Jul 18 16:55:10 Finished compiler/backend/mips                                   50s   1GB
Jul 18 16:55:10 Starting compiler/backend/riscv
Jul 18 16:56:01 Finished compiler/backend/riscv                                  50s   1GB
Jul 18 16:56:01 Starting compiler/backend/ag32
Jul 18 16:59:06 Finished compiler/backend/ag32                                 3m05s   1GB
Jul 18 16:59:07 Starting compiler/parsing/proofs
Jul 18 17:07:39 Finished compiler/parsing/proofs                               8m31s   1GB
Jul 18 17:07:39 Starting compiler/inference/proofs
Jul 18 17:13:51 Finished compiler/inference/proofs                             6m12s   1GB
Jul 18 17:13:52 Starting compiler/backend/semantics
Jul 18 18:12:40 Finished compiler/backend/semantics                           58m48s   2GB
Jul 18 18:12:40 Starting compiler/backend/reg_alloc/proofs
Jul 18 18:21:04 Finished compiler/backend/reg_alloc/proofs                     8m23s 993MB
Jul 18 18:21:05 Starting compiler/backend/proofs
Jul 18 20:14:45 Finished compiler/backend/proofs                            1h53m39s  14GB
Jul 18 20:14:45 Starting compiler/backend/serialiser
Jul 18 20:18:17 Finished compiler/backend/serialiser                           3m31s   1GB
Jul 18 20:18:17 Starting compiler/encoders/x64/proofs
Jul 18 20:40:14 Finished compiler/encoders/x64/proofs                         21m57s   5GB
Jul 18 20:40:15 Starting compiler/encoders/arm7/proofs
Jul 18 21:11:27 Finished compiler/encoders/arm7/proofs                        31m12s   4GB
Jul 18 21:11:27 Starting compiler/encoders/arm8/proofs
Jul 18 21:27:13 Finished compiler/encoders/arm8/proofs                        15m45s   1GB
Jul 18 21:27:13 Starting compiler/encoders/arm8_asl/proofs
Jul 18 23:24:24 Finished compiler/encoders/arm8_asl/proofs                  1h57m10s   6GB
Jul 18 23:24:24 Starting compiler/encoders/mips/proofs
Jul 18 23:48:06 Finished compiler/encoders/mips/proofs                        23m41s   2GB
Jul 18 23:48:06 Starting compiler/encoders/riscv/proofs
Jul 19 00:08:35 Finished compiler/encoders/riscv/proofs                       20m28s   1GB
Jul 19 00:08:35 Starting compiler/encoders/ag32/proofs
Jul 19 00:14:27 Finished compiler/encoders/ag32/proofs                         5m51s 862MB
Jul 19 00:14:27 Starting compiler/backend/x64/proofs
Jul 19 00:15:30 Finished compiler/backend/x64/proofs                           1m03s   1GB
Jul 19 00:15:31 Starting compiler/backend/arm7/proofs
Jul 19 00:16:35 Finished compiler/backend/arm7/proofs                          1m04s   1GB
Jul 19 00:16:35 Starting compiler/backend/arm8/proofs
Jul 19 00:17:38 Finished compiler/backend/arm8/proofs                          1m02s   1GB
Jul 19 00:17:38 Starting compiler/backend/arm8_asl
Jul 19 00:18:33 Finished compiler/backend/arm8_asl                               54s   1GB
Jul 19 00:18:33 Starting compiler/backend/mips/proofs
Jul 19 00:19:38 Finished compiler/backend/mips/proofs                          1m04s   1GB
Jul 19 00:19:38 Starting compiler/backend/riscv/proofs
Jul 19 00:20:41 Finished compiler/backend/riscv/proofs                         1m02s   1GB
Jul 19 00:20:41 Starting compiler/backend/ag32/proofs
Jul 19 00:51:13 Finished compiler/backend/ag32/proofs                         30m31s   3GB
Jul 19 00:51:13 Starting compiler/proofs
Jul 19 00:56:52 Finished compiler/proofs                                       5m38s   4GB
Jul 19 00:56:52 Starting candle/set-theory
Jul 19 00:58:01 Finished candle/set-theory                                     1m08s   1GB
Jul 19 00:58:01 Starting candle/syntax-lib
Jul 19 00:58:30 Finished candle/syntax-lib                                       28s 685MB
Jul 19 00:58:30 Starting candle/standard/syntax
Jul 19 01:02:58 Finished candle/standard/syntax                                4m27s   1GB
Jul 19 01:02:58 Starting candle/standard/semantics
Jul 19 01:07:02 Finished candle/standard/semantics                             4m03s   1GB
Jul 19 01:07:02 Starting candle/standard/monadic
Jul 19 01:11:07 Finished candle/standard/monadic                               4m04s   2GB
Jul 19 01:11:08 Starting candle/standard/ml_kernel
Jul 19 01:24:48 Finished candle/standard/ml_kernel                            13m40s   4GB
Jul 19 01:24:48 Starting candle/overloading/syntax
Jul 19 01:31:51 Finished candle/overloading/syntax                             7m02s   1GB
Jul 19 01:31:52 Starting candle/overloading/semantics
Jul 19 01:58:59 Finished candle/overloading/semantics                         27m06s   2GB
Jul 19 01:58:59 Starting candle/overloading/monadic
Jul 19 02:04:51 Finished candle/overloading/monadic                            5m52s   1GB
Jul 19 02:04:52 Starting candle/overloading/ml_kernel
Jul 19 02:20:38 Finished candle/overloading/ml_kernel                         15m45s   3GB
Jul 19 02:20:38 Starting candle/overloading/ml_checker
Jul 19 02:26:02 Finished candle/overloading/ml_checker                         5m24s   3GB
Jul 19 02:26:03 Starting candle/prover
Jul 19 02:51:41 Finished candle/prover                                        25m38s   3GB
Jul 19 02:51:41 Starting pancake
Jul 19 02:59:36 Finished pancake                                               7m53s   3GB
Jul 19 02:59:36 Starting pancake/ffi
Jul 19 02:59:37 Finished pancake/ffi                                              0s  40MB
Jul 19 02:59:38 Starting pancake/semantics
Jul 19 03:05:29 Finished pancake/semantics                                     5m50s   1GB
Jul 19 03:05:29 Starting pancake/proofs
Jul 19 03:32:58 Finished pancake/proofs                                       27m28s   6GB
Jul 19 03:32:58 Starting characteristic/examples
Jul 19 03:36:02 Finished characteristic/examples                               3m03s   3GB
Jul 19 03:36:02 Starting tutorial/solutions
Jul 19 04:11:20 Finished tutorial/solutions                                   35m18s   7GB
Jul 19 04:11:21 Starting translator/monadic/examples
Jul 19 04:18:30 Finished translator/monadic/examples                           7m09s   3GB
Jul 19 04:18:30 Starting examples
Jul 19 04:38:28 Finished examples                                             19m57s   3GB
Jul 19 04:38:29 Starting examples/compilation/x64
Jul 19 09:12:49 Finished examples/compilation/x64                           4h34m19s  22GB
Jul 19 09:12:50 Starting examples/compilation/x64/proofs
Jul 19 09:17:15 Finished examples/compilation/x64/proofs                       4m24s   3GB
Jul 19 09:17:15 Starting examples/compilation/ag32
Jul 19 10:31:01 Finished examples/compilation/ag32                          1h13m45s   8GB
Jul 19 10:31:02 Starting examples/compilation/ag32/proofs
Jul 19 10:32:55 Finished examples/compilation/ag32/proofs                      1m52s   2GB
Jul 19 10:32:55 Starting examples/lpr_checker
Jul 19 10:35:05 Finished examples/lpr_checker                                  2m09s   1GB
Jul 19 10:35:05 Starting examples/lpr_checker/array
Jul 19 11:52:46 Finished examples/lpr_checker/array                         1h17m41s  10GB
Jul 19 11:52:46 Starting examples/lpr_checker/array/compilation
Jul 19 13:12:42 Finished examples/lpr_checker/array/compilation             1h19m55s  37GB
Jul 19 13:12:42 Starting examples/lpr_checker/array/compilation/proofs
Jul 19 13:15:43 Finished examples/lpr_checker/array/compilation/proofs         3m00s   6GB
Jul 19 13:15:44 Starting examples/opentheory
Jul 19 13:38:49 Finished examples/opentheory                                  23m05s   3GB
Jul 19 13:38:49 Starting examples/opentheory
Jul 19 13:38:53 Finished examples/opentheory                                      2s  32MB
Jul 19 13:38:53 Starting examples/opentheory/compilation
Jul 19 15:07:18 Finished examples/opentheory/compilation                    1h28m22s  41GB
Jul 19 15:07:18 Starting examples/opentheory/compilation/proofs
Jul 19 15:09:12 Finished examples/opentheory/compilation/proofs                1m54s   4GB
Jul 19 15:09:12 Starting examples/opentheory/compilation/ag32
Jul 19 16:31:02 Finished examples/opentheory/compilation/ag32               1h21m49s  41GB
Jul 19 16:31:03 Starting examples/opentheory/compilation/ag32/proofs
Jul 19 16:35:34 Finished examples/opentheory/compilation/ag32/proofs           4m31s   3GB
Jul 19 16:35:35 Starting examples/sat_encodings
Jul 19 16:39:59 Finished examples/sat_encodings                                4m23s 919MB
Jul 19 16:39:59 Starting examples/sat_encodings/case_studies
Jul 19 16:43:45 Finished examples/sat_encodings/case_studies                   3m45s 707MB
Jul 19 16:43:45 Starting examples/sat_encodings/translation
Jul 19 16:55:52 Finished examples/sat_encodings/translation                   12m06s   5GB
Jul 19 16:55:52 Starting examples/sat_encodings/translation/compilation
Jul 19 18:22:12 Finished examples/sat_encodings/translation/compilation     1h26m18s  22GB
Jul 19 18:22:12 Starting examples/deflate
Jul 19 18:24:14 Finished examples/deflate                                      2m02s 699MB
Jul 19 18:24:15 Starting examples/deflate/translation
Jul 19 18:27:29 Finished examples/deflate/translation                          3m13s   3GB
Jul 19 18:27:29 Starting examples/deflate/translation/compilation
Jul 19 18:56:30 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
decompressionCompileTheory                                                                                                                                                                           (35m)     OK
compressionCompileTheory                                                                                                                                                                             (35m)FAIL<1>
           lab_to_target real: 10m44s
           lab_to_target size: 1914752
                       export: runtime: 1.1s,    gctime: 0.21771s,     systime: 0.06332s.
 Saved theorem _______ "compression_compiled"
 Exporting theory "compressionCompile" ... Run out of store - interrupting threads
 error in quse /local/regression_new/cakeml-1963/examples/deflate/translation/compilation/compressionCompileScript.sml : Interrupt
 error in load /local/regression_new/cakeml-1963/examples/deflate/translation/compilation/compressionCompileScript : Interrupt
 
 Failure while writing theory!
 Uncaught exception: Interrupt
deflateDecodeCompileTheory                                                                                                                                                                           (39m)MKILLED
deflateEncodeCompileTheory                                                                                                                                                                           (46m)MKILLED