Job 1650

CakeML:e920b3bfbf7b1f18d4e84575a9bee4aaf66ecb2a
  Fix a typo to get bootstrap translation to work [Nov 21 20:50:55]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:bdb437dfa109a22361c4d539c736d12e5828dbb8
  Add two utility shell scripts to developers [Nov 19 06:33:56]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 22 08:06:32 Claimed job
Nov 22 08:06:42 Building HOL
Nov 22 08:16:13 Starting developers
Nov 22 08:16:16 Finished developers                                               2s 135MB
Nov 22 08:16:16 Starting developers/bin
Nov 22 08:16:22 Finished developers/bin                                           6s   1GB
Nov 22 08:16:22 Starting semantics/ffi
Nov 22 08:16:34 Finished semantics/ffi                                           11s 262MB
Nov 22 08:16:34 Starting semantics
Nov 22 08:18:19 Finished semantics                                             1m44s   1GB
Nov 22 08:18:19 Starting semantics/proofs
Nov 22 08:22:05 Finished semantics/proofs                                      3m45s   1GB
Nov 22 08:22:05 Starting semantics/alt_semantics
Nov 22 08:22:16 Finished semantics/alt_semantics                                 10s 423MB
Nov 22 08:22:16 Starting semantics/alt_semantics/proofs
Nov 22 08:24:37 Finished semantics/alt_semantics/proofs                        2m20s   1GB
Nov 22 08:24:37 Starting basis/pure
Nov 22 08:27:24 Finished basis/pure                                            2m46s   1GB
Nov 22 08:27:24 Starting translator
Nov 22 08:30:23 Finished translator                                            2m58s   2GB
Nov 22 08:30:23 Starting compiler/parsing
Nov 22 08:31:36 Finished compiler/parsing                                      1m12s   4GB
Nov 22 08:31:36 Starting characteristic
Nov 22 08:37:25 Finished characteristic                                        5m49s   3GB
Nov 22 08:37:26 Starting translator/monadic
Nov 22 08:39:20 Finished translator/monadic                                    1m54s   2GB
Nov 22 08:39:21 Starting basis
Nov 22 09:25:59 Finished basis                                                46m37s  24GB
Nov 22 09:25:59 Starting compiler/inference
Nov 22 09:27:14 Finished compiler/inference                                    1m14s   2GB
Nov 22 09:27:15 Starting compiler/backend/reg_alloc
Nov 22 09:28:24 Finished compiler/backend/reg_alloc                            1m09s   1GB
Nov 22 09:28:24 Starting compiler/backend/gc
Nov 22 09:32:05 Finished compiler/backend/gc                                   3m40s   4GB
Nov 22 09:32:05 Starting compiler/backend
Nov 22 09:37:25 Finished compiler/backend                                      5m19s   5GB
Nov 22 09:37:26 Starting compiler/encoders/asm
Nov 22 09:37:49 Finished compiler/encoders/asm                                   23s   1GB
Nov 22 09:37:49 Starting compiler/encoders/x64
Nov 22 09:38:54 Finished compiler/encoders/x64                                 1m04s   1GB
Nov 22 09:38:54 Starting compiler/encoders/arm7
Nov 22 09:41:01 Finished compiler/encoders/arm7                                2m07s   1GB
Nov 22 09:41:01 Starting compiler/encoders/arm8
Nov 22 09:41:43 Finished compiler/encoders/arm8                                  41s   1GB
Nov 22 09:41:43 Starting compiler/encoders/mips
Nov 22 09:43:11 Finished compiler/encoders/mips                                1m28s   1GB
Nov 22 09:43:11 Starting compiler/encoders/riscv
Nov 22 09:44:53 Finished compiler/encoders/riscv                               1m41s   1GB
Nov 22 09:44:53 Starting compiler/encoders/ag32
Nov 22 09:45:13 Finished compiler/encoders/ag32                                  19s 942MB
Nov 22 09:45:13 Starting compiler/backend/x64
Nov 22 09:45:34 Finished compiler/backend/x64                                    20s   1GB
Nov 22 09:45:34 Starting compiler/backend/arm7
Nov 22 09:45:57 Finished compiler/backend/arm7                                   23s   1GB
Nov 22 09:45:57 Starting compiler/backend/arm8
Nov 22 09:46:19 Finished compiler/backend/arm8                                   21s   1GB
Nov 22 09:46:19 Starting compiler/backend/mips
Nov 22 09:46:40 Finished compiler/backend/mips                                   20s   1GB
Nov 22 09:46:40 Starting compiler/backend/riscv
Nov 22 09:47:03 Finished compiler/backend/riscv                                  22s   1GB
Nov 22 09:47:03 Starting compiler/backend/ag32
Nov 22 09:48:15 Finished compiler/backend/ag32                                 1m11s   2GB
Nov 22 09:48:15 Starting compiler/parsing/proofs
Nov 22 09:50:56 Finished compiler/parsing/proofs                               2m40s   2GB
Nov 22 09:50:56 Starting compiler/inference/proofs
Nov 22 09:53:24 Finished compiler/inference/proofs                             2m27s   1GB
Nov 22 09:53:24 Starting compiler/backend/semantics
Nov 22 10:20:52 Finished compiler/backend/semantics                           27m27s   4GB
Nov 22 10:20:52 Starting compiler/backend/reg_alloc/proofs
Nov 22 10:24:12 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Nov 22 10:24:12 Starting compiler/backend/proofs
Nov 22 11:26:14 Finished compiler/backend/proofs                            1h02m01s  17GB
Nov 22 11:26:14 Starting compiler/backend/serialiser
Nov 22 11:27:30 Finished compiler/backend/serialiser                           1m15s   2GB
Nov 22 11:27:31 Starting compiler/encoders/x64/proofs
Nov 22 11:37:30 Finished compiler/encoders/x64/proofs                          9m59s   4GB
Nov 22 11:37:30 Starting compiler/encoders/arm7/proofs
Nov 22 11:51:10 Finished compiler/encoders/arm7/proofs                        13m39s   8GB
Nov 22 11:51:10 Starting compiler/encoders/arm8/proofs
Nov 22 11:57:56 Finished compiler/encoders/arm8/proofs                         6m45s   3GB
Nov 22 11:57:56 Starting compiler/encoders/mips/proofs
Nov 22 12:08:05 Finished compiler/encoders/mips/proofs                        10m08s   3GB
Nov 22 12:08:05 Starting compiler/encoders/riscv/proofs
Nov 22 12:16:27 Finished compiler/encoders/riscv/proofs                        8m21s   3GB
Nov 22 12:16:27 Starting compiler/encoders/ag32/proofs
Nov 22 12:18:48 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Nov 22 12:18:49 Starting compiler/backend/x64/proofs
Nov 22 12:19:12 Finished compiler/backend/x64/proofs                             22s   1GB
Nov 22 12:19:12 Starting compiler/backend/arm7/proofs
Nov 22 12:19:36 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 22 12:19:36 Starting compiler/backend/arm8/proofs
Nov 22 12:20:00 Finished compiler/backend/arm8/proofs                            23s   1GB
Nov 22 12:20:00 Starting compiler/backend/mips/proofs
Nov 22 12:20:24 Finished compiler/backend/mips/proofs                            23s   1GB
Nov 22 12:20:24 Starting compiler/backend/riscv/proofs
Nov 22 12:20:48 Finished compiler/backend/riscv/proofs                           24s   2GB
Nov 22 12:20:49 Starting compiler/backend/ag32/proofs
Nov 22 12:33:50 Finished compiler/backend/ag32/proofs                         13m00s   4GB
Nov 22 12:33:50 Starting compiler/proofs
Nov 22 12:36:03 Finished compiler/proofs                                       2m13s   6GB
Nov 22 12:36:03 Starting candle/set-theory
Nov 22 12:36:37 Finished candle/set-theory                                       33s   1GB
Nov 22 12:36:37 Starting candle/syntax-lib
Nov 22 12:36:49 Finished candle/syntax-lib                                       11s 816MB
Nov 22 12:36:49 Starting candle/standard/syntax
Nov 22 12:38:48 Finished candle/standard/syntax                                1m58s   1GB
Nov 22 12:38:49 Starting candle/standard/semantics
Nov 22 12:40:42 Finished candle/standard/semantics                             1m53s   2GB
Nov 22 12:40:42 Starting candle/standard/monadic
Nov 22 12:42:30 Finished candle/standard/monadic                               1m47s   1GB
Nov 22 12:42:30 Starting candle/standard/ml_kernel
Nov 22 12:48:25 Finished candle/standard/ml_kernel                             5m54s   7GB
Nov 22 12:48:25 Starting candle/overloading/syntax
Nov 22 12:51:45 Finished candle/overloading/syntax                             3m19s   1GB
Nov 22 12:51:45 Starting candle/overloading/semantics
Nov 22 13:03:07 Finished candle/overloading/semantics                         11m21s   6GB
Nov 22 13:03:07 Starting pancake
Nov 22 13:05:23 Finished pancake                                               2m15s   3GB
Nov 22 13:05:23 Starting pancake/ffi
Nov 22 13:05:24 Finished pancake/ffi                                              0s   6MB
Nov 22 13:05:24 Starting pancake/semantics
Nov 22 13:07:43 Finished pancake/semantics                                     2m19s   1GB
Nov 22 13:07:44 Starting pancake/proofs
Nov 22 13:18:58 Finished pancake/proofs                                       11m14s   6GB
Nov 22 13:18:59 Starting characteristic/examples
Nov 22 13:20:22 Finished characteristic/examples                               1m23s   4GB
Nov 22 13:20:22 Starting tutorial/solutions
Nov 22 13:36:47 Finished tutorial/solutions                                   16m24s  16GB
Nov 22 13:36:48 Starting translator/monadic/examples
Nov 22 13:40:17 Finished translator/monadic/examples                           3m28s   3GB
Nov 22 13:40:17 Starting examples
Nov 22 13:50:17 Finished examples                                              9m59s   6GB
Nov 22 13:50:17 Starting examples/compilation/x64
Nov 22 16:25:03 Finished examples/compilation/x64                           2h34m44s  28GB
Nov 22 16:25:03 Starting examples/compilation/x64/proofs
Nov 22 16:27:53 Finished examples/compilation/x64/proofs                       2m50s   3GB
Nov 22 16:27:53 Starting examples/compilation/ag32
Nov 22 17:03:54 Finished examples/compilation/ag32                            36m00s  14GB
Nov 22 17:03:54 Starting examples/compilation/ag32/proofs
Nov 22 17:04:50 Finished examples/compilation/ag32/proofs                        55s   5GB
Nov 22 17:04:50 Starting examples/cost
Nov 22 18:01:50 Finished examples/cost                                        56m59s  15GB
Nov 22 18:01:51 Starting examples/lpr_checker
Nov 22 18:02:41 Finished examples/lpr_checker                                    50s   2GB
Nov 22 18:02:41 Starting examples/lpr_checker/array
Nov 22 18:30:35 Finished examples/lpr_checker/array                           27m53s  12GB
Nov 22 18:30:35 Starting examples/lpr_checker/array/compilation
Nov 22 19:58:30 Finished examples/lpr_checker/array/compilation             1h27m54s  37GB
Nov 22 19:58:30 Starting examples/lpr_checker/array/compilation/proofs
Nov 22 19:59:46 Finished examples/lpr_checker/array/compilation/proofs         1m15s   5GB
Nov 22 19:59:46 Starting examples/opentheory
Nov 22 20:09:02 Finished examples/opentheory                                   9m15s   6GB
Nov 22 20:09:02 Starting examples/opentheory
Nov 22 20:09:04 Finished examples/opentheory                                      1s 135MB
Nov 22 20:09:04 Starting examples/opentheory/compilation
Nov 22 20:46:08 Finished examples/opentheory/compilation                      37m04s  35GB
Nov 22 20:46:08 Starting examples/opentheory/compilation/proofs
Nov 22 20:46:55 Finished examples/opentheory/compilation/proofs                  46s   4GB
Nov 22 20:46:55 Starting examples/opentheory/compilation/ag32
Nov 22 21:26:19 Finished examples/opentheory/compilation/ag32                 39m23s  31GB
Nov 22 21:26:19 Starting examples/opentheory/compilation/ag32/proofs
Nov 22 21:28:00 Finished examples/opentheory/compilation/ag32/proofs           1m40s   6GB
Nov 22 21:28:00 Starting examples/sat_encodings
Nov 22 21:29:58 Finished examples/sat_encodings                                1m58s   1GB
Nov 22 21:29:58 Starting examples/sat_encodings/case_studies
Nov 22 21:31:33 Finished examples/sat_encodings/case_studies                   1m34s   1GB
Nov 22 21:31:33 Starting examples/sat_encodings/translation
Nov 22 21:37:10 Finished examples/sat_encodings/translation                    5m36s   6GB
Nov 22 21:37:10 Starting examples/sat_encodings/translation/compilation
Nov 22 22:28:55 Finished examples/sat_encodings/translation/compilation       51m43s  26GB
Nov 22 22:28:55 Starting translator/okasaki-examples
Nov 22 22:33:25 Finished translator/okasaki-examples                           4m29s   3GB
Nov 22 22:33:25 Starting translator/other-examples
Nov 22 22:35:14 Finished translator/other-examples                             1m48s   1GB
Nov 22 22:35:14 Starting compiler/parsing/tests
Nov 22 22:35:42 Finished compiler/parsing/tests                                  28s 741MB
Nov 22 22:35:43 Starting compiler/inference/tests
Nov 22 22:43:12 Finished compiler/inference/tests                              7m28s   5GB
Nov 22 22:43:12 Starting compiler/bootstrap/translation
Nov 23 01:27:10 Finished compiler/bootstrap/translation                     2h43m58s  55GB
Nov 23 01:27:11 Starting unverified/sexpr-bootstrap/x64/64
Nov 23 01:40:00 Finished unverified/sexpr-bootstrap/x64/64                    12m49s   8GB
Nov 23 01:40:01 Starting unverified/sexpr-bootstrap/x64/32
Nov 23 01:51:10 Finished unverified/sexpr-bootstrap/x64/32                    11m08s   8GB
Nov 23 01:51:10 Starting compiler/benchmarks
Nov 23 02:31:28 Finished compiler/benchmarks                                  40m18s   2GB
Nov 23 02:31:29 Starting compiler/bootstrap/compilation/x64/64
Nov 23 02:32:58 FAILED: compiler/bootstrap/compilation/x64/64
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$(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$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[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$(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)/compiler/backend/serialiser[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
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                                                                                                                                (0s)     OK
cake-sexpr-32                                                                                                                                                           (81s)FAIL<1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-1650/compiler/bootstrap/translation/compiler32ProgTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/compiler32ProgTheory : Interrupt
 error in load /home/myreen/regression/cakeml-1650/compiler/bootstrap/compilation/x64/64/sexprBootstrap32Script : Interrupt
 Uncaught exception: Interrupt
cake-sexpr-64                                                                                                                                                           (81s)MKILLED
to_dataBootstrapTheory                                                                                                                                                  (82s)MKILLED