Job 1326

CakeML:0b23296d34495457ed119cb1a4a27c60dd8758d0
  Get some examples to build again [Aug 06 17:28:40]
HOL:e514bb277bd566e9c2e8622df374e923e3aac2fc
  Update documentation of Holmake's recursive behaviours [Aug 20 04:35:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 21 14:51:46 Claimed job
Aug 21 14:51:55 Building HOL
Aug 21 15:04:20 Starting developers
Aug 21 15:04:21 Finished developers                                               0s  34MB
Aug 21 15:04:21 Starting developers/bin
Aug 21 15:04:27 Finished developers/bin                                           6s   1GB
Aug 21 15:04:27 Starting semantics/ffi
Aug 21 15:04:38 Finished semantics/ffi                                           10s 300MB
Aug 21 15:04:38 Starting semantics
Aug 21 15:06:11 Finished semantics                                             1m33s   1GB
Aug 21 15:06:11 Starting semantics/proofs
Aug 21 15:09:30 Finished semantics/proofs                                      3m18s   2GB
Aug 21 15:09:30 Starting semantics/alt_semantics
Aug 21 15:09:39 Finished semantics/alt_semantics                                  8s 460MB
Aug 21 15:09:39 Starting semantics/alt_semantics/proofs
Aug 21 15:11:39 Finished semantics/alt_semantics/proofs                        2m00s   1GB
Aug 21 15:11:39 Starting basis/pure
Aug 21 15:14:24 Finished basis/pure                                            2m44s   1GB
Aug 21 15:14:24 Starting translator
Aug 21 15:16:59 Finished translator                                            2m35s   1GB
Aug 21 15:16:59 Starting compiler/parsing
Aug 21 15:18:09 Finished compiler/parsing                                      1m09s   3GB
Aug 21 15:18:09 Starting characteristic
Aug 21 15:23:55 Finished characteristic                                        5m45s   3GB
Aug 21 15:23:55 Starting translator/monadic
Aug 21 15:25:33 Finished translator/monadic                                    1m38s   3GB
Aug 21 15:25:33 Starting basis
Aug 21 15:57:46 Finished basis                                                32m12s  23GB
Aug 21 15:57:46 Starting compiler/inference
Aug 21 15:58:54 Finished compiler/inference                                    1m07s   1GB
Aug 21 15:58:54 Starting compiler/backend/reg_alloc
Aug 21 16:00:00 Finished compiler/backend/reg_alloc                            1m05s   2GB
Aug 21 16:00:00 Starting compiler/backend/gc
Aug 21 16:03:34 Finished compiler/backend/gc                                   3m33s   3GB
Aug 21 16:03:34 Starting compiler/backend
Aug 21 16:08:21 Finished compiler/backend                                      4m46s   5GB
Aug 21 16:08:21 Starting compiler/encoders/asm
Aug 21 16:08:44 Finished compiler/encoders/asm                                   22s   1GB
Aug 21 16:08:44 Starting compiler/encoders/x64
Aug 21 16:09:45 Finished compiler/encoders/x64                                 1m00s   1GB
Aug 21 16:09:45 Starting compiler/encoders/arm7
Aug 21 16:11:32 Finished compiler/encoders/arm7                                1m46s   1GB
Aug 21 16:11:32 Starting compiler/encoders/arm8
Aug 21 16:12:09 Finished compiler/encoders/arm8                                  36s   1GB
Aug 21 16:12:09 Starting compiler/encoders/mips
Aug 21 16:13:22 Finished compiler/encoders/mips                                1m12s   1GB
Aug 21 16:13:22 Starting compiler/encoders/riscv
Aug 21 16:14:51 Finished compiler/encoders/riscv                               1m28s   1GB
Aug 21 16:14:51 Starting compiler/encoders/ag32
Aug 21 16:15:10 Finished compiler/encoders/ag32                                  18s 975MB
Aug 21 16:15:10 Starting compiler/backend/x64
Aug 21 16:15:27 Finished compiler/backend/x64                                    17s   1GB
Aug 21 16:15:27 Starting compiler/backend/arm7
Aug 21 16:15:48 Finished compiler/backend/arm7                                   20s   1GB
Aug 21 16:15:48 Starting compiler/backend/arm8
Aug 21 16:16:07 Finished compiler/backend/arm8                                   18s   1GB
Aug 21 16:16:07 Starting compiler/backend/mips
Aug 21 16:16:27 Finished compiler/backend/mips                                   19s   1GB
Aug 21 16:16:27 Starting compiler/backend/riscv
Aug 21 16:16:47 Finished compiler/backend/riscv                                  19s   1GB
Aug 21 16:16:48 Starting compiler/backend/ag32
Aug 21 16:17:56 Finished compiler/backend/ag32                                 1m07s   3GB
Aug 21 16:17:56 Starting compiler/parsing/proofs
Aug 21 16:20:05 Finished compiler/parsing/proofs                               2m08s   1GB
Aug 21 16:20:05 Starting compiler/inference/proofs
Aug 21 16:22:22 Finished compiler/inference/proofs                             2m16s   1GB
Aug 21 16:22:22 Starting compiler/backend/semantics
Aug 21 16:48:22 Finished compiler/backend/semantics                           25m59s   5GB
Aug 21 16:48:22 Starting compiler/backend/reg_alloc/proofs
Aug 21 16:51:35 Finished compiler/backend/reg_alloc/proofs                     3m13s   1GB
Aug 21 16:51:35 Starting compiler/backend/proofs
Aug 21 17:42:37 Finished compiler/backend/proofs                              51m01s  29GB
Aug 21 17:42:37 Starting compiler/encoders/x64/proofs
Aug 21 17:51:57 Finished compiler/encoders/x64/proofs                          9m19s   4GB
Aug 21 17:51:57 Starting compiler/encoders/arm7/proofs
Aug 21 18:04:23 Finished compiler/encoders/arm7/proofs                        12m25s   5GB
Aug 21 18:04:23 Starting compiler/encoders/arm8/proofs
Aug 21 18:10:30 Finished compiler/encoders/arm8/proofs                         6m06s   3GB
Aug 21 18:10:30 Starting compiler/encoders/mips/proofs
Aug 21 18:20:17 Finished compiler/encoders/mips/proofs                         9m47s   5GB
Aug 21 18:20:17 Starting compiler/encoders/riscv/proofs
Aug 21 18:28:13 Finished compiler/encoders/riscv/proofs                        7m55s   4GB
Aug 21 18:28:13 Starting compiler/encoders/ag32/proofs
Aug 21 18:30:33 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Aug 21 18:30:33 Starting compiler/backend/x64/proofs
Aug 21 18:30:54 Finished compiler/backend/x64/proofs                             20s   1GB
Aug 21 18:30:54 Starting compiler/backend/arm7/proofs
Aug 21 18:31:15 Finished compiler/backend/arm7/proofs                            21s   1GB
Aug 21 18:31:15 Starting compiler/backend/arm8/proofs
Aug 21 18:31:33 Finished compiler/backend/arm8/proofs                            18s   1GB
Aug 21 18:31:33 Starting compiler/backend/mips/proofs
Aug 21 18:31:54 Finished compiler/backend/mips/proofs                            20s   1GB
Aug 21 18:31:55 Starting compiler/backend/riscv/proofs
Aug 21 18:32:17 Finished compiler/backend/riscv/proofs                           21s   1GB
Aug 21 18:32:17 Starting compiler/backend/ag32/proofs
Aug 21 18:44:15 Finished compiler/backend/ag32/proofs                         11m57s   3GB
Aug 21 18:44:15 Starting compiler/proofs
Aug 21 18:46:05 Finished compiler/proofs                                       1m50s   5GB
Aug 21 18:46:06 Starting candle/set-theory
Aug 21 18:46:36 Finished candle/set-theory                                       30s   1GB
Aug 21 18:46:37 Starting candle/syntax-lib
Aug 21 18:46:48 Finished candle/syntax-lib                                       11s 836MB
Aug 21 18:46:48 Starting candle/standard/syntax
Aug 21 18:48:40 Finished candle/standard/syntax                                1m51s   1GB
Aug 21 18:48:40 Starting candle/standard/semantics
Aug 21 18:50:23 Finished candle/standard/semantics                             1m43s   2GB
Aug 21 18:50:24 Starting candle/standard/monadic
Aug 21 18:52:06 Finished candle/standard/monadic                               1m42s   2GB
Aug 21 18:52:06 Starting candle/standard/ml_kernel
Aug 21 18:57:11 Finished candle/standard/ml_kernel                             5m04s   6GB
Aug 21 18:57:11 Starting candle/overloading/syntax
Aug 21 19:00:18 Finished candle/overloading/syntax                             3m06s   2GB
Aug 21 19:00:18 Starting candle/overloading/semantics
Aug 21 19:06:47 Finished candle/overloading/semantics                          6m29s   3GB
Aug 21 19:06:48 Starting characteristic/examples
Aug 21 19:08:02 Finished characteristic/examples                               1m13s   4GB
Aug 21 19:08:02 Starting tutorial/solutions
Aug 21 19:22:08 Finished tutorial/solutions                                   14m06s  19GB
Aug 21 19:22:09 Starting translator/monadic/examples
Aug 21 19:25:26 Finished translator/monadic/examples                           3m17s   3GB
Aug 21 19:25:26 Starting examples
Aug 21 19:33:50 Finished examples                                              8m23s   6GB
Aug 21 19:33:50 Starting examples/compilation/x64
Aug 21 21:43:26 Finished examples/compilation/x64                           2h09m35s  26GB
Aug 21 21:43:26 Starting examples/compilation/x64/proofs
Aug 21 21:45:12 Finished examples/compilation/x64/proofs                       1m45s   3GB
Aug 21 21:45:12 Starting examples/compilation/ag32
Aug 21 22:15:38 Finished examples/compilation/ag32                            30m25s   8GB
Aug 21 22:15:38 Starting examples/compilation/ag32/proofs
Aug 21 22:16:26 Finished examples/compilation/ag32/proofs                        47s   4GB
Aug 21 22:16:26 Starting examples/cost
Aug 21 23:01:20 Finished examples/cost                                        44m53s  10GB
Aug 21 23:01:20 Starting examples/lpr_checker
Aug 21 23:05:01 Finished examples/lpr_checker                                  3m40s   5GB
Aug 21 23:05:01 Starting examples/lpr_checker/compilation
Aug 21 23:21:53 Finished examples/lpr_checker/compilation                     16m52s  11GB
Aug 21 23:21:53 Starting examples/lpr_checker/compilation/proofs
Aug 21 23:22:32 Finished examples/lpr_checker/compilation/proofs                 38s   3GB
Aug 21 23:22:32 Starting examples/lpr_checker/array
Aug 21 23:34:53 Finished examples/lpr_checker/array                           12m20s   4GB
Aug 21 23:34:53 Starting examples/lpr_checker/array/compilation
Aug 21 23:52:30 Finished examples/lpr_checker/array/compilation               17m36s  22GB
Aug 21 23:52:30 Starting examples/lpr_checker/array/compilation/proofs
Aug 21 23:53:16 Finished examples/lpr_checker/array/compilation/proofs           45s   3GB
Aug 21 23:53:16 Starting examples/opentheory
Aug 22 00:02:23 Finished examples/opentheory                                   9m05s   6GB
Aug 22 00:02:23 Starting examples/opentheory
Aug 22 00:02:24 Finished examples/opentheory                                      0s  98MB
Aug 22 00:02:24 Starting examples/opentheory/compilation
Aug 22 00:34:29 Finished examples/opentheory/compilation                      32m04s  26GB
Aug 22 00:34:29 Starting examples/opentheory/compilation/proofs
Aug 22 00:35:08 Finished examples/opentheory/compilation/proofs                  39s   3GB
Aug 22 00:35:08 Starting examples/opentheory/compilation/ag32
Aug 22 01:06:45 Finished examples/opentheory/compilation/ag32                 31m36s  25GB
Aug 22 01:06:46 Starting examples/opentheory/compilation/ag32/proofs
Aug 22 01:08:12 Finished examples/opentheory/compilation/ag32/proofs           1m26s   5GB
Aug 22 01:08:12 Starting translator/okasaki-examples
Aug 22 01:12:20 Finished translator/okasaki-examples                           4m07s   2GB
Aug 22 01:12:20 Starting translator/other-examples
Aug 22 01:14:18 Finished translator/other-examples                             1m57s   1GB
Aug 22 01:14:18 Starting compiler/parsing/tests
Aug 22 01:14:42 Finished compiler/parsing/tests                                  24s 619MB
Aug 22 01:14:42 Starting compiler/inference/tests
Aug 22 01:18:59 Finished compiler/inference/tests                              4m17s   5GB
Aug 22 01:18:59 Starting compiler/bootstrap/translation
Aug 22 02:12:26 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[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)/examples/fun-op-sem/lprefix_lub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on to_flatProgTheory
monadic_encTheory                                                             real:   11s  user:   10s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                           real:   15s  user:   15s     OK
monadic_enc32Theory                                                           real:   17s  user:   15s     OK
to_flatProgTheory                                                             real:  384s  user:  378s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                             real:  384s  user:  379s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                              real:  361s  user:  353s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                              real:  309s  user:  304s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                             real:  166s  user:  163s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                               real:  233s  user:  230s     OK
Starting work on parserProgTheory
parserProgTheory                                                              real:  466s  user:  458s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                           real:  879s  user:  869s     OK
Starting work on inferProgTheory
inferProgTheory                                                               real:   19s  user:   17sFAIL<1>
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-1326/compiler/bootstrap/translation/reg_allocProgTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/reg_allocProgTheory : Interrupt
 error in load /home/myreen/regression/cakeml-1326/compiler/bootstrap/translation/inferProgScript : Interrupt
 Uncaught exception: Interrupt