Job 1620

CakeML: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 04 19:30:35 Claimed job
Nov 04 19:30:40 Building HOL
Nov 04 19:41:49 Starting developers
Nov 04 19:41:51 Finished developers                                               2s 112MB
Nov 04 19:41:52 Starting developers/bin
Nov 04 19:41:58 Finished developers/bin                                           6s   1GB
Nov 04 19:41:58 Starting semantics/ffi
Nov 04 19:42:09 Finished semantics/ffi                                           10s 266MB
Nov 04 19:42:09 Starting semantics
Nov 04 19:43:44 Finished semantics                                             1m34s   1GB
Nov 04 19:43:44 Starting semantics/proofs
Nov 04 19:47:14 Finished semantics/proofs                                      3m30s   1GB
Nov 04 19:47:15 Starting semantics/alt_semantics
Nov 04 19:47:26 Finished semantics/alt_semantics                                 11s 549MB
Nov 04 19:47:26 Starting semantics/alt_semantics/proofs
Nov 04 19:49:49 Finished semantics/alt_semantics/proofs                        2m22s   2GB
Nov 04 19:49:49 Starting basis/pure
Nov 04 19:52:32 Finished basis/pure                                            2m42s   1GB
Nov 04 19:52:32 Starting translator
Nov 04 19:55:53 Finished translator                                            3m20s   2GB
Nov 04 19:55:53 Starting compiler/parsing
Nov 04 19:57:04 Finished compiler/parsing                                      1m10s   3GB
Nov 04 19:57:04 Starting characteristic
Nov 04 20:02:47 Finished characteristic                                        5m43s   3GB
Nov 04 20:02:48 Starting translator/monadic
Nov 04 20:04:40 Finished translator/monadic                                    1m51s   3GB
Nov 04 20:04:40 Starting basis
Nov 04 20:50:47 Finished basis                                                46m07s  45GB
Nov 04 20:50:47 Starting compiler/inference
Nov 04 20:52:02 Finished compiler/inference                                    1m14s   1GB
Nov 04 20:52:02 Starting compiler/backend/reg_alloc
Nov 04 20:53:09 Finished compiler/backend/reg_alloc                            1m06s   2GB
Nov 04 20:53:09 Starting compiler/backend/gc
Nov 04 20:56:50 Finished compiler/backend/gc                                   3m40s   3GB
Nov 04 20:56:50 Starting compiler/backend
Nov 04 21:02:18 Finished compiler/backend                                      5m28s   5GB
Nov 04 21:02:18 Starting compiler/encoders/asm
Nov 04 21:02:42 Finished compiler/encoders/asm                                   23s   1GB
Nov 04 21:02:42 Starting compiler/encoders/x64
Nov 04 21:03:47 Finished compiler/encoders/x64                                 1m04s   1GB
Nov 04 21:03:47 Starting compiler/encoders/arm7
Nov 04 21:05:53 Finished compiler/encoders/arm7                                2m05s   1GB
Nov 04 21:05:53 Starting compiler/encoders/arm8
Nov 04 21:06:34 Finished compiler/encoders/arm8                                  40s   1GB
Nov 04 21:06:34 Starting compiler/encoders/mips
Nov 04 21:08:02 Finished compiler/encoders/mips                                1m27s   1GB
Nov 04 21:08:02 Starting compiler/encoders/riscv
Nov 04 21:09:43 Finished compiler/encoders/riscv                               1m40s   1GB
Nov 04 21:09:43 Starting compiler/encoders/ag32
Nov 04 21:10:02 Finished compiler/encoders/ag32                                  19s 939MB
Nov 04 21:10:02 Starting compiler/backend/x64
Nov 04 21:10:22 Finished compiler/backend/x64                                    19s   1GB
Nov 04 21:10:22 Starting compiler/backend/arm7
Nov 04 21:10:44 Finished compiler/backend/arm7                                   21s   1GB
Nov 04 21:10:44 Starting compiler/backend/arm8
Nov 04 21:11:06 Finished compiler/backend/arm8                                   21s   1GB
Nov 04 21:11:06 Starting compiler/backend/mips
Nov 04 21:11:28 Finished compiler/backend/mips                                   22s   1GB
Nov 04 21:11:28 Starting compiler/backend/riscv
Nov 04 21:11:50 Finished compiler/backend/riscv                                  21s   1GB
Nov 04 21:11:50 Starting compiler/backend/ag32
Nov 04 21:13:04 Finished compiler/backend/ag32                                 1m13s   2GB
Nov 04 21:13:04 Starting compiler/parsing/proofs
Nov 04 21:15:38 Finished compiler/parsing/proofs                               2m33s   2GB
Nov 04 21:15:38 Starting compiler/inference/proofs
Nov 04 21:18:05 Finished compiler/inference/proofs                             2m26s   2GB
Nov 04 21:18:05 Starting compiler/backend/semantics
Nov 04 21:45:38 Finished compiler/backend/semantics                           27m32s   3GB
Nov 04 21:45:38 Starting compiler/backend/reg_alloc/proofs
Nov 04 21:48:56 Finished compiler/backend/reg_alloc/proofs                     3m17s   2GB
Nov 04 21:48:56 Starting compiler/backend/proofs
Nov 04 22:41:18 Finished compiler/backend/proofs                              52m21s  30GB
Nov 04 22:41:18 Starting compiler/backend/serialiser
Nov 04 22:42:27 Finished compiler/backend/serialiser                           1m08s   2GB
Nov 04 22:42:27 Starting compiler/encoders/x64/proofs
Nov 04 22:51:51 Finished compiler/encoders/x64/proofs                          9m23s   5GB
Nov 04 22:51:51 Starting compiler/encoders/arm7/proofs
Nov 04 23:04:48 Finished compiler/encoders/arm7/proofs                        12m56s   9GB
Nov 04 23:04:48 Starting compiler/encoders/arm8/proofs
Nov 04 23:11:23 Finished compiler/encoders/arm8/proofs                         6m34s   4GB
Nov 04 23:11:23 Starting compiler/encoders/mips/proofs
Nov 04 23:21:23 Finished compiler/encoders/mips/proofs                         9m59s   7GB
Nov 04 23:21:23 Starting compiler/encoders/riscv/proofs
Nov 04 23:29:56 Finished compiler/encoders/riscv/proofs                        8m33s   3GB
Nov 04 23:29:56 Starting compiler/encoders/ag32/proofs
Nov 04 23:32:19 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Nov 04 23:32:19 Starting compiler/backend/x64/proofs
Nov 04 23:32:42 Finished compiler/backend/x64/proofs                             22s   2GB
Nov 04 23:32:42 Starting compiler/backend/arm7/proofs
Nov 04 23:33:07 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 04 23:33:07 Starting compiler/backend/arm8/proofs
Nov 04 23:33:29 Finished compiler/backend/arm8/proofs                            21s   1GB
Nov 04 23:33:29 Starting compiler/backend/mips/proofs
Nov 04 23:33:53 Finished compiler/backend/mips/proofs                            23s   1GB
Nov 04 23:33:53 Starting compiler/backend/riscv/proofs
Nov 04 23:34:18 Finished compiler/backend/riscv/proofs                           25s   2GB
Nov 04 23:34:19 Starting compiler/backend/ag32/proofs
Nov 04 23:46:15 Finished compiler/backend/ag32/proofs                         11m56s   3GB
Nov 04 23:46:15 Starting compiler/proofs
Nov 04 23:48:20 Finished compiler/proofs                                       2m04s   6GB
Nov 04 23:48:20 Starting candle/set-theory
Nov 04 23:48:51 Finished candle/set-theory                                       30s 937MB
Nov 04 23:48:51 Starting candle/syntax-lib
Nov 04 23:49:02 Finished candle/syntax-lib                                       11s 808MB
Nov 04 23:49:03 Starting candle/standard/syntax
Nov 04 23:50:54 Finished candle/standard/syntax                                1m50s   1GB
Nov 04 23:50:54 Starting candle/standard/semantics
Nov 04 23:52:40 Finished candle/standard/semantics                             1m46s   1GB
Nov 04 23:52:41 Starting candle/standard/monadic
Nov 04 23:54:25 Finished candle/standard/monadic                               1m44s   1GB
Nov 04 23:54:25 Starting candle/standard/ml_kernel
Nov 05 00:00:00 Finished candle/standard/ml_kernel                             5m34s   6GB
Nov 05 00:00:00 Starting candle/overloading/syntax
Nov 05 00:03:23 Finished candle/overloading/syntax                             3m22s   2GB
Nov 05 00:03:23 Starting candle/overloading/semantics
Nov 05 00:19:12 Finished candle/overloading/semantics                         15m48s   6GB
Nov 05 00:19:12 Starting pancake
Nov 05 00:21:31 Finished pancake                                               2m19s   3GB
Nov 05 00:21:31 Starting pancake/ffi
Nov 05 00:21:32 Finished pancake/ffi                                              0s   6MB
Nov 05 00:21:32 Starting pancake/semantics
Nov 05 00:23:56 Finished pancake/semantics                                     2m24s   1GB
Nov 05 00:23:56 Starting pancake/proofs
Nov 05 00:36:31 Finished pancake/proofs                                       12m34s   8GB
Nov 05 00:36:31 Starting characteristic/examples
Nov 05 00:38:01 Finished characteristic/examples                               1m29s   5GB
Nov 05 00:38:01 Starting tutorial/solutions
Nov 05 00:55:36 Finished tutorial/solutions                                   17m34s  13GB
Nov 05 00:55:36 Starting translator/monadic/examples
Nov 05 00:59:37 Finished translator/monadic/examples                           4m00s   3GB
Nov 05 00:59:37 Starting examples
Nov 05 01:15:33 Finished examples                                             15m55s   6GB
Nov 05 01:15:33 Starting examples/compilation/x64
Nov 05 03:58:34 Finished examples/compilation/x64                           2h43m01s  23GB
Nov 05 03:58:34 Starting examples/compilation/x64/proofs
Nov 05 04:00:40 Finished examples/compilation/x64/proofs                       2m05s   3GB
Nov 05 04:00:40 Starting examples/compilation/ag32
Nov 05 04:36:39 Finished examples/compilation/ag32                            35m58s  13GB
Nov 05 04:36:40 Starting examples/compilation/ag32/proofs
Nov 05 04:37:36 Finished examples/compilation/ag32/proofs                        56s   5GB
Nov 05 04:37:36 Starting examples/cost
Nov 05 05:33:48 Finished examples/cost                                        56m11s  12GB
Nov 05 05:33:48 Starting examples/lpr_checker
Nov 05 05:34:38 Finished examples/lpr_checker                                    49s   1GB
Nov 05 05:34:38 Starting examples/lpr_checker/array
Nov 05 06:01:34 Finished examples/lpr_checker/array                           26m55s   8GB
Nov 05 06:01:35 Starting examples/lpr_checker/array/compilation
Nov 05 07:29:39 Finished examples/lpr_checker/array/compilation             1h28m04s  55GB
Nov 05 07:29:39 Starting examples/lpr_checker/array/compilation/proofs
Nov 05 07:30:55 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Nov 05 07:30:55 Starting examples/opentheory
Nov 05 07:40:12 Finished examples/opentheory                                   9m16s   6GB
Nov 05 07:40:12 Starting examples/opentheory
Nov 05 07:40:13 Finished examples/opentheory                                      1s 122MB
Nov 05 07:40:14 Starting examples/opentheory/compilation
Nov 05 08:17:29 Finished examples/opentheory/compilation                      37m15s  30GB
Nov 05 08:17:29 Starting examples/opentheory/compilation/proofs
Nov 05 08:18:17 Finished examples/opentheory/compilation/proofs                  47s   4GB
Nov 05 08:18:17 Starting examples/opentheory/compilation/ag32
Nov 05 08:56:45 Finished examples/opentheory/compilation/ag32                 38m27s  34GB
Nov 05 08:56:45 Starting examples/opentheory/compilation/ag32/proofs
Nov 05 08:58:21 Finished examples/opentheory/compilation/ag32/proofs           1m35s   7GB
Nov 05 08:58:21 Starting examples/sat_encodings
Nov 05 09:00:16 Finished examples/sat_encodings                                1m55s   1GB
Nov 05 09:00:17 Starting examples/sat_encodings/case_studies
Nov 05 09:01:52 Finished examples/sat_encodings/case_studies                   1m35s   1GB
Nov 05 09:01:52 Starting examples/sat_encodings/translation
Nov 05 09:07:30 Finished examples/sat_encodings/translation                    5m37s   5GB
Nov 05 09:07:30 Starting examples/sat_encodings/translation/compilation
Nov 05 10:03:50 Finished examples/sat_encodings/translation/compilation       56m19s  28GB
Nov 05 10:03:51 Starting translator/okasaki-examples
Nov 05 10:08:15 Finished translator/okasaki-examples                           4m23s   3GB
Nov 05 10:08:15 Starting translator/other-examples
Nov 05 10:10:07 Finished translator/other-examples                             1m51s   2GB
Nov 05 10:10:07 Starting compiler/parsing/tests
Nov 05 10:10:35 Finished compiler/parsing/tests                                  28s 640MB
Nov 05 10:10:35 Starting compiler/inference/tests
Nov 05 10:18:08 Finished compiler/inference/tests                              7m32s   5GB
Nov 05 10:18:08 Starting compiler/bootstrap/translation
Nov 05 12:09:59 FAILED: compiler/bootstrap/translation
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)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/topology[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$(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)/src/coalgebras[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)/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$(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/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)/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 README.md
Starting work on to_flatProgTheory
README.md                                                                                                                                compiler/bootstrap/translation  (0s)     OK
monadic_encTheory                                                                                                                         compiler/encoders/monadic_enc (10s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                                                                                       compiler/encoders/monadic_enc (15s)     OK
monadic_enc32Theory                                                                                                                       compiler/encoders/monadic_enc (15s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]                                                                                                         (42.350s) 
to_flatProgTheory                                                                                                                        compiler/bootstrap/translation(296s)     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                        compiler/bootstrap/translation(446s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                         compiler/bootstrap/translation(360s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                         compiler/bootstrap/translation(318s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                        compiler/bootstrap/translation(171s)     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                          compiler/bootstrap/translation(228s)     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                         compiler/bootstrap/translation(439s)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                      compiler/bootstrap/translation(883s)     OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                          compiler/bootstrap/translation(986s)     OK
Starting work on explorerProgTheory
explorerProgTheory                                                                                                                       compiler/bootstrap/translation(694s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                                                                                    compiler/bootstrap/translation(158s)     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                                                                                      compiler/bootstrap/translation (17m)     OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                                                                                      compiler/bootstrap/translation (17m)     OK
Starting work on to_target32ProgTheory
to_target64ProgTheory                                                                                                                    compiler/bootstrap/translation(569s)     OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                                                                                    compiler/bootstrap/translation(568s)     OK
Starting work on arm7ProgTheory
x64ProgTheory                                                                                                                            compiler/bootstrap/translation (26s)FAIL<1>
 Run out of store - interrupting threads
 Failed to recover - exiting
arm7ProgTheory                                                                                                                           compiler/bootstrap/translation (16s)MKILLED