Job 461

CakeML:edf04ec42f9f759b4de9c4042b65197255308284
  Fix typo [Aug 27 07:48:53]
#517 (check-prog-def)
Merging into:647f4e17b2e75c7f7b7e1c9e1c3b7756121d4b0b
  Merge pull request #515 from CakeML/opentheory-reader [Aug 24 23:14:12]
HOL:f384c8dc9f93709f216559459e077b899f3071d8
  Add simple test for the Futures in the Isabelle concurrency code [Aug 27 04:04:00]
Machine:cakeml1796 4.4.0-22-generic x86_64 GNU/Linux

Aug 27 09:39:14 Claimed job
Aug 27 09:39:26 Building HOL
Aug 27 09:53:06 Starting developers/bin
Aug 27 09:53:16 Finished developers/bin                                           7s 144MB
Aug 27 09:53:18 Starting semantics/ffi
Aug 27 09:54:17 Finished semantics/ffi                                           57s 271MB
Aug 27 09:54:19 Starting semantics
Aug 27 09:56:44 Finished semantics                                             2m22s 735MB
Aug 27 09:56:46 Starting semantics/proofs
Aug 27 10:02:03 Finished semantics/proofs                                      5m14s   1GB
Aug 27 10:02:05 Starting basis/pure
Aug 27 10:07:54 Finished basis/pure                                            5m47s 703MB
Aug 27 10:07:56 Starting translator
Aug 27 10:09:53 Finished translator                                            1m55s   1GB
Aug 27 10:09:55 Starting compiler/parsing
Aug 27 10:12:16 Finished compiler/parsing                                      2m19s   2GB
Aug 27 10:12:18 Starting characteristic
Aug 27 10:16:51 Finished characteristic                                        4m30s   1GB
Aug 27 10:16:53 Starting translator/monadic
Aug 27 10:19:37 Finished translator/monadic                                    2m41s   1GB
Aug 27 10:19:39 Starting basis
Aug 27 10:47:14 Finished basis                                                27m33s   2GB
Aug 27 10:47:16 Starting compiler/inference
Aug 27 10:50:07 Finished compiler/inference                                    2m48s   2GB
Aug 27 10:50:09 Starting compiler/backend/reg_alloc
Aug 27 10:51:32 Finished compiler/backend/reg_alloc                            1m21s   1GB
Aug 27 10:51:34 Starting compiler/backend/gc
Aug 27 11:06:25 Finished compiler/backend/gc                                  14m48s   3GB
Aug 27 11:06:27 Starting compiler/backend
Aug 27 11:06:32 Finished compiler/backend                                         3s  14MB
Aug 27 11:06:34 Starting compiler/encoders/asm
Aug 27 11:06:37 Finished compiler/encoders/asm                                    0s  11MB
Aug 27 11:06:39 Starting compiler/encoders/x64
Aug 27 11:08:09 Finished compiler/encoders/x64                                 1m28s 478MB
Aug 27 11:08:11 Starting compiler/encoders/arm6
Aug 27 11:11:08 Finished compiler/encoders/arm6                                2m55s   1GB
Aug 27 11:11:10 Starting compiler/encoders/arm8
Aug 27 11:11:54 Finished compiler/encoders/arm8                                  42s 385MB
Aug 27 11:11:56 Starting compiler/encoders/mips
Aug 27 11:13:33 Finished compiler/encoders/mips                                1m34s 948MB
Aug 27 11:13:35 Starting compiler/encoders/riscv
Aug 27 11:15:11 Finished compiler/encoders/riscv                               1m33s 633MB
Aug 27 11:15:12 Starting compiler/backend/x64
Aug 27 11:15:46 Finished compiler/backend/x64                                    31s 827MB
Aug 27 11:15:48 Starting compiler/backend/arm6
Aug 27 11:16:25 Finished compiler/backend/arm6                                   35s   1GB
Aug 27 11:16:27 Starting compiler/backend/arm8
Aug 27 11:17:01 Finished compiler/backend/arm8                                   32s   1GB
Aug 27 11:17:03 Starting compiler/backend/mips
Aug 27 11:17:37 Finished compiler/backend/mips                                   31s   1GB
Aug 27 11:17:39 Starting compiler/backend/riscv
Aug 27 11:18:13 Finished compiler/backend/riscv                                  32s   1GB
Aug 27 11:18:15 Starting compiler/parsing/proofs
Aug 27 11:22:15 Finished compiler/parsing/proofs                               3m58s 829MB
Aug 27 11:22:17 Starting compiler/inference/proofs
Aug 27 11:27:06 Finished compiler/inference/proofs                             4m46s   1GB
Aug 27 11:27:08 Starting compiler/backend/semantics
Aug 27 11:41:43 Finished compiler/backend/semantics                           14m32s   2GB
Aug 27 11:41:45 Starting compiler/backend/reg_alloc/proofs
Aug 27 11:53:33 Finished compiler/backend/reg_alloc/proofs                    11m46s 555MB
Aug 27 11:53:35 Starting compiler/backend/proofs
Aug 27 12:48:31 Finished compiler/backend/proofs                              54m54s   3GB
Aug 27 12:48:33 Starting compiler/encoders/x64/proofs
Aug 27 13:00:02 Finished compiler/encoders/x64/proofs                         11m26s   1GB
Aug 27 13:00:04 Starting compiler/encoders/arm6/proofs
Aug 27 13:12:11 Finished compiler/encoders/arm6/proofs                        12m05s   3GB
Aug 27 13:12:13 Starting compiler/encoders/arm8/proofs
Aug 27 13:20:40 Finished compiler/encoders/arm8/proofs                         8m25s   1GB
Aug 27 13:20:42 Starting compiler/encoders/mips/proofs
Aug 27 13:32:11 Finished compiler/encoders/mips/proofs                        11m27s   2GB
Aug 27 13:32:13 Starting compiler/encoders/riscv/proofs
Aug 27 13:44:47 Finished compiler/encoders/riscv/proofs                       12m31s   1GB
Aug 27 13:44:49 Starting compiler/backend/x64/proofs
Aug 27 13:45:25 Finished compiler/backend/x64/proofs                             33s   1GB
Aug 27 13:45:27 Starting compiler/backend/arm6/proofs
Aug 27 13:46:08 Finished compiler/backend/arm6/proofs                            38s   1GB
Aug 27 13:46:10 Starting compiler/backend/arm8/proofs
Aug 27 13:46:44 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 27 13:46:46 Starting compiler/backend/mips/proofs
Aug 27 13:47:24 Finished compiler/backend/mips/proofs                            35s   1GB
Aug 27 13:47:26 Starting compiler/backend/riscv/proofs
Aug 27 13:48:01 Finished compiler/backend/riscv/proofs                           32s   1GB
Aug 27 13:48:03 Starting compiler/proofs
Aug 27 13:50:30 Finished compiler/proofs                                       2m25s   1GB
Aug 27 13:50:32 Starting candle/set-theory
Aug 27 13:51:28 Finished candle/set-theory                                       53s 578MB
Aug 27 13:51:30 Starting candle/syntax-lib
Aug 27 13:51:50 Finished candle/syntax-lib                                       17s 525MB
Aug 27 13:51:52 Starting candle/standard/syntax
Aug 27 13:54:35 Finished candle/standard/syntax                                2m41s 587MB
Aug 27 13:54:37 Starting candle/standard/semantics
Aug 27 13:56:53 Finished candle/standard/semantics                             2m13s 806MB
Aug 27 13:56:55 Starting candle/standard/monadic
Aug 27 13:59:31 Finished candle/standard/monadic                               2m34s   1GB
Aug 27 13:59:33 Starting candle/standard/ml_kernel
Aug 27 14:24:44 Finished candle/standard/ml_kernel                            25m09s   4GB
Aug 27 14:24:46 Starting candle/standard/opentheory
Aug 27 14:39:31 Finished candle/standard/opentheory                           14m42s   5GB
Aug 27 14:39:33 Starting characteristic/examples
Aug 27 14:42:12 Finished characteristic/examples                               2m37s   1GB
Aug 27 14:42:14 Starting tutorial/solutions
Aug 27 15:02:43 Finished tutorial/solutions                                   20m25s   8GB
Aug 27 15:02:45 Starting translator/monadic/examples
Aug 27 15:05:35 Finished translator/monadic/examples                           2m48s   2GB
Aug 27 15:05:37 Starting examples
Aug 27 15:13:55 Finished examples                                              8m16s   4GB
Aug 27 15:13:57 Starting examples/compilation
Aug 27 18:05:29 Finished examples/compilation                               2h51m29s  16GB
Aug 27 18:05:31 Starting examples/compilation/proofs
Aug 27 18:09:04 Finished examples/compilation/proofs                           3m31s   3GB
Aug 27 18:09:06 Starting compiler/benchmarks
Aug 27 18:09:08 Finished compiler/benchmarks                                      0s   4MB
Aug 27 18:09:10 Starting translator/okasaki-examples
Aug 27 18:15:36 Finished translator/okasaki-examples                           6m24s   1GB
Aug 27 18:15:38 Starting translator/other-examples
Aug 27 18:22:17 Finished translator/other-examples                             6m36s   1GB
Aug 27 18:22:19 Starting compiler/parsing/tests
Aug 27 18:23:02 Finished compiler/parsing/tests                                  40s 349MB
Aug 27 18:23:04 Starting compiler/inference/tests
Aug 27 18:29:15 Finished compiler/inference/tests                              6m08s   4GB
Aug 27 18:29:17 Starting compiler/bootstrap/translation
Aug 28 01:24:50 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f384c8dc9f93709f216559459e077b899f3071d8/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../inference]0;Holmake: ../../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on heap
heap                                                                                                          OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                             OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                               OK
Starting work on parserProgTheory
parserProgTheory                                                                                              OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                           OK
Starting work on inferProgTheory
inferProgTheory                                                                                               OK
Starting work on explorerProgTheory
explorerProgTheory                                                                                            OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                                                         OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word32ProgTheory                                                                                           OK
Starting work on to_target32ProgTheory
to_word64ProgTheory                                                                                           OK
Starting work on to_target64ProgTheory
to_target64ProgTheory                                                                                         OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                                                         OK
Starting work on arm6ProgTheory
x64ProgTheory                                                                                                 OK
Starting work on arm8ProgTheory
arm6ProgTheory                                                                                                OK
Starting work on compiler32ProgTheory
arm8ProgTheory                                                                                                OK
Starting work on riscvProgTheory
riscvProgTheory                                                                                               OK
Starting work on mipsProgTheory
mipsProgTheory                                                                                                OK
Starting work on compiler64ProgTheory
Run out of store - interrupting threads
Run out of store - interrupting threads