Job 1622

CakeML:11ce5f9be7a62a7a9d1e8fc232d385c48c16d833
  Hook up decoder to bootstrap translation [Oct 21 06:45:24]
#841 (eval)
Merging into:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
  Merge pull request #839 from CakeML/lpr_transform [Oct 03 11:04:50]
HOL:56617180468ec5da8a1c0cfa582a16877f54a29b
  Make Theorem/Definition syntax slightly more liberal [Nov 03 04:51:40]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 08 18:46:42 Claimed job
Nov 08 18:46:45 Reusing HOL
Nov 08 18:46:55 Starting developers
Nov 08 18:46:58 Finished developers                                               2s 116MB
Nov 08 18:46:58 Starting developers/bin
Nov 08 18:47:04 Finished developers/bin                                           6s   1GB
Nov 08 18:47:05 Starting semantics/ffi
Nov 08 18:47:16 Finished semantics/ffi                                           11s 298MB
Nov 08 18:47:16 Starting semantics
Nov 08 18:48:52 Finished semantics                                             1m36s   1GB
Nov 08 18:48:53 Starting semantics/proofs
Nov 08 18:53:20 Finished semantics/proofs                                      4m27s   1GB
Nov 08 18:53:20 Starting semantics/alt_semantics
Nov 08 18:53:32 Finished semantics/alt_semantics                                 11s 461MB
Nov 08 18:53:32 Starting semantics/alt_semantics/proofs
Nov 08 18:56:01 Finished semantics/alt_semantics/proofs                        2m28s   2GB
Nov 08 18:56:01 Starting basis/pure
Nov 08 18:56:58 Finished basis/pure                                              56s   1GB
Nov 08 18:56:58 Starting translator
Nov 08 19:00:33 Finished translator                                            3m35s   2GB
Nov 08 19:00:33 Starting compiler/parsing
Nov 08 19:01:44 Finished compiler/parsing                                      1m10s   3GB
Nov 08 19:01:44 Starting characteristic
Nov 08 19:07:27 Finished characteristic                                        5m43s   3GB
Nov 08 19:07:28 Starting translator/monadic
Nov 08 19:09:20 Finished translator/monadic                                    1m52s   3GB
Nov 08 19:09:20 Starting basis
Nov 08 19:55:36 Finished basis                                                46m15s  36GB
Nov 08 19:55:36 Starting compiler/inference
Nov 08 19:56:46 Finished compiler/inference                                    1m09s   2GB
Nov 08 19:56:46 Starting compiler/backend/reg_alloc
Nov 08 19:57:54 Finished compiler/backend/reg_alloc                            1m07s   2GB
Nov 08 19:57:54 Starting compiler/backend/gc
Nov 08 20:01:23 Finished compiler/backend/gc                                   3m28s   3GB
Nov 08 20:01:23 Starting compiler/backend
Nov 08 20:06:48 Finished compiler/backend                                      5m24s   5GB
Nov 08 20:06:48 Starting compiler/encoders/asm
Nov 08 20:07:11 Finished compiler/encoders/asm                                   23s   1GB
Nov 08 20:07:11 Starting compiler/encoders/x64
Nov 08 20:07:39 Finished compiler/encoders/x64                                   27s   1GB
Nov 08 20:07:39 Starting compiler/encoders/arm7
Nov 08 20:08:35 Finished compiler/encoders/arm7                                  55s   1GB
Nov 08 20:08:35 Starting compiler/encoders/arm8
Nov 08 20:08:50 Finished compiler/encoders/arm8                                  14s   1GB
Nov 08 20:08:50 Starting compiler/encoders/mips
Nov 08 20:09:09 Finished compiler/encoders/mips                                  19s   1GB
Nov 08 20:09:10 Starting compiler/encoders/riscv
Nov 08 20:09:27 Finished compiler/encoders/riscv                                 17s   1GB
Nov 08 20:09:28 Starting compiler/encoders/ag32
Nov 08 20:09:49 Finished compiler/encoders/ag32                                  20s 935MB
Nov 08 20:09:49 Starting compiler/backend/x64
Nov 08 20:10:12 Finished compiler/backend/x64                                    23s   1GB
Nov 08 20:10:12 Starting compiler/backend/arm7
Nov 08 20:10:38 Finished compiler/backend/arm7                                   25s   1GB
Nov 08 20:10:38 Starting compiler/backend/arm8
Nov 08 20:11:05 Finished compiler/backend/arm8                                   26s   1GB
Nov 08 20:11:05 Starting compiler/backend/mips
Nov 08 20:11:29 Finished compiler/backend/mips                                   23s   1GB
Nov 08 20:11:29 Starting compiler/backend/riscv
Nov 08 20:11:50 Finished compiler/backend/riscv                                  20s   1GB
Nov 08 20:11:50 Starting compiler/backend/ag32
Nov 08 20:13:03 Finished compiler/backend/ag32                                 1m12s   2GB
Nov 08 20:13:03 Starting compiler/parsing/proofs
Nov 08 20:15:36 Finished compiler/parsing/proofs                               2m32s   1GB
Nov 08 20:15:36 Starting compiler/inference/proofs
Nov 08 20:18:06 Finished compiler/inference/proofs                             2m29s   2GB
Nov 08 20:18:06 Starting compiler/backend/semantics
Nov 08 20:45:32 Finished compiler/backend/semantics                           27m25s   3GB
Nov 08 20:45:32 Starting compiler/backend/reg_alloc/proofs
Nov 08 20:48:49 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Nov 08 20:48:49 Starting compiler/backend/proofs
Nov 08 21:42:07 Finished compiler/backend/proofs                              53m17s  17GB
Nov 08 21:42:07 Starting compiler/backend/serialiser
Nov 08 21:43:20 Finished compiler/backend/serialiser                           1m11s   2GB
Nov 08 21:43:20 Starting compiler/encoders/x64/proofs
Nov 08 21:52:41 Finished compiler/encoders/x64/proofs                          9m20s   4GB
Nov 08 21:52:41 Starting compiler/encoders/arm7/proofs
Nov 08 22:05:33 Finished compiler/encoders/arm7/proofs                        12m51s   4GB
Nov 08 22:05:33 Starting compiler/encoders/arm8/proofs
Nov 08 22:12:23 Finished compiler/encoders/arm8/proofs                         6m50s   3GB
Nov 08 22:12:23 Starting compiler/encoders/mips/proofs
Nov 08 22:22:23 Finished compiler/encoders/mips/proofs                         9m59s   6GB
Nov 08 22:22:23 Starting compiler/encoders/riscv/proofs
Nov 08 22:30:44 Finished compiler/encoders/riscv/proofs                        8m21s   4GB
Nov 08 22:30:45 Starting compiler/encoders/ag32/proofs
Nov 08 22:33:08 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Nov 08 22:33:08 Starting compiler/backend/x64/proofs
Nov 08 22:33:31 Finished compiler/backend/x64/proofs                             23s   2GB
Nov 08 22:33:31 Starting compiler/backend/arm7/proofs
Nov 08 22:33:56 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 08 22:33:56 Starting compiler/backend/arm8/proofs
Nov 08 22:34:20 Finished compiler/backend/arm8/proofs                            23s   1GB
Nov 08 22:34:20 Starting compiler/backend/mips/proofs
Nov 08 22:34:43 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 08 22:34:43 Starting compiler/backend/riscv/proofs
Nov 08 22:35:08 Finished compiler/backend/riscv/proofs                           24s   2GB
Nov 08 22:35:08 Starting compiler/backend/ag32/proofs
Nov 08 22:47:05 Finished compiler/backend/ag32/proofs                         11m56s   3GB
Nov 08 22:47:05 Starting compiler/proofs
Nov 08 22:48:57 Finished compiler/proofs                                       1m51s   6GB
Nov 08 22:48:58 Starting candle/set-theory
Nov 08 22:49:28 Finished candle/set-theory                                       30s   1GB
Nov 08 22:49:28 Starting candle/syntax-lib
Nov 08 22:49:40 Finished candle/syntax-lib                                       11s 802MB
Nov 08 22:49:40 Starting candle/standard/syntax
Nov 08 22:51:33 Finished candle/standard/syntax                                1m52s   1GB
Nov 08 22:51:33 Starting candle/standard/semantics
Nov 08 22:53:21 Finished candle/standard/semantics                             1m47s   2GB
Nov 08 22:53:21 Starting candle/standard/monadic
Nov 08 22:55:05 Finished candle/standard/monadic                               1m43s   1GB
Nov 08 22:55:05 Starting candle/standard/ml_kernel
Nov 08 23:00:38 Finished candle/standard/ml_kernel                             5m33s   5GB
Nov 08 23:00:39 Starting candle/overloading/syntax
Nov 08 23:03:53 Finished candle/overloading/syntax                             3m13s   2GB
Nov 08 23:03:53 Starting candle/overloading/semantics
Nov 08 23:14:43 Finished candle/overloading/semantics                         10m49s   6GB
Nov 08 23:14:43 Starting pancake
Nov 08 23:16:49 Finished pancake                                               2m05s   3GB
Nov 08 23:16:49 Starting pancake/ffi
Nov 08 23:16:49 Finished pancake/ffi                                              0s   7MB
Nov 08 23:16:49 Starting pancake/semantics
Nov 08 23:19:06 Finished pancake/semantics                                     2m16s   1GB
Nov 08 23:19:06 Starting pancake/proofs
Nov 08 23:30:32 Finished pancake/proofs                                       11m26s   7GB
Nov 08 23:30:32 Starting characteristic/examples
Nov 08 23:31:56 Finished characteristic/examples                               1m23s   4GB
Nov 08 23:31:56 Starting tutorial/solutions
Nov 08 23:48:50 Finished tutorial/solutions                                   16m53s  14GB
Nov 08 23:48:50 Starting translator/monadic/examples
Nov 08 23:52:16 Finished translator/monadic/examples                           3m26s   4GB
Nov 08 23:52:16 Starting examples
Nov 09 00:02:27 Finished examples                                             10m10s   6GB
Nov 09 00:02:27 Starting examples/compilation/x64
Nov 09 02:56:15 Finished examples/compilation/x64                           2h53m46s  31GB
Nov 09 02:56:15 Starting examples/compilation/x64/proofs
Nov 09 02:58:45 Finished examples/compilation/x64/proofs                       2m30s   3GB
Nov 09 02:58:45 Starting examples/compilation/ag32
Nov 09 03:38:46 Finished examples/compilation/ag32                            40m00s  13GB
Nov 09 03:38:46 Starting examples/compilation/ag32/proofs
Nov 09 03:39:47 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Nov 09 03:39:47 Starting examples/cost
Nov 09 04:35:52 Finished examples/cost                                        56m03s  13GB
Nov 09 04:35:52 Starting examples/lpr_checker
Nov 09 04:36:45 Finished examples/lpr_checker                                    52s   2GB
Nov 09 04:36:45 Starting examples/lpr_checker/array
Nov 09 05:03:36 Finished examples/lpr_checker/array                           26m50s  14GB
Nov 09 05:03:36 Starting examples/lpr_checker/array/compilation
Nov 09 06:29:43 Finished examples/lpr_checker/array/compilation             1h26m06s  39GB
Nov 09 06:29:44 Starting examples/lpr_checker/array/compilation/proofs
Nov 09 06:30:56 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Nov 09 06:30:56 Starting examples/opentheory
Nov 09 06:31:31 FAILED: examples/opentheory
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/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/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$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Starting work on README.md
Starting work on prettyTheory
README.md                                                                                         (0s)     OK
prettyTheory                                                                                     (20s)     OK
Starting work on readerTheory
readerTheory                                                                                     (11s)FAIL<1>
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-1622/candle/standard/ml_kernel/ml_hol_kernelProgTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/candle/standard/ml_kernel/ml_hol_kernelProgTheory : Interrupt
 error in load /home/myreen/regression/cakeml-1622/examples/opentheory/readerScript : Interrupt
 Uncaught exception: Interrupt