Job 462

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:98d718b2599e89f71200ee47e9077ea1cfaba444
  Merge pull request #577 from binghe/topology_merge.2 [Aug 27 23:16:27]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Aug 28 07:26:58 Claimed job
Aug 28 07:27:08 Building HOL
Aug 28 07:40:27 Starting developers/bin
Aug 28 07:40:37 Finished developers/bin                                           7s 144MB
Aug 28 07:40:38 Starting semantics/ffi
Aug 28 07:41:41 Finished semantics/ffi                                         1m00s 306MB
Aug 28 07:41:43 Starting semantics
Aug 28 07:44:04 Finished semantics                                             2m19s 947MB
Aug 28 07:44:06 Starting semantics/proofs
Aug 28 07:49:22 Finished semantics/proofs                                      5m13s   1GB
Aug 28 07:49:24 Starting basis/pure
Aug 28 07:55:14 Finished basis/pure                                            5m47s 751MB
Aug 28 07:55:16 Starting translator
Aug 28 07:57:09 Finished translator                                            1m51s 807MB
Aug 28 07:57:11 Starting compiler/parsing
Aug 28 07:59:30 Finished compiler/parsing                                      2m16s   2GB
Aug 28 07:59:32 Starting characteristic
Aug 28 08:04:12 Finished characteristic                                        4m38s   1GB
Aug 28 08:04:14 Starting translator/monadic
Aug 28 08:06:52 Finished translator/monadic                                    2m35s   1GB
Aug 28 08:06:54 Starting basis
Aug 28 08:34:30 Finished basis                                                27m33s   3GB
Aug 28 08:34:32 Starting compiler/inference
Aug 28 08:37:19 Finished compiler/inference                                    2m45s   1GB
Aug 28 08:37:21 Starting compiler/backend/reg_alloc
Aug 28 08:38:42 Finished compiler/backend/reg_alloc                            1m19s   1GB
Aug 28 08:38:44 Starting compiler/backend/gc
Aug 28 08:53:46 Finished compiler/backend/gc                                  15m00s   3GB
Aug 28 08:53:48 Starting compiler/backend
Aug 28 08:53:53 Finished compiler/backend                                         3s  22MB
Aug 28 08:53:55 Starting compiler/encoders/asm
Aug 28 08:53:58 Finished compiler/encoders/asm                                    0s  11MB
Aug 28 08:54:00 Starting compiler/encoders/x64
Aug 28 08:55:25 Finished compiler/encoders/x64                                 1m23s 509MB
Aug 28 08:55:27 Starting compiler/encoders/arm6
Aug 28 08:58:20 Finished compiler/encoders/arm6                                2m51s   1GB
Aug 28 08:58:22 Starting compiler/encoders/arm8
Aug 28 08:59:04 Finished compiler/encoders/arm8                                  39s 400MB
Aug 28 08:59:06 Starting compiler/encoders/mips
Aug 28 09:00:46 Finished compiler/encoders/mips                                1m38s 703MB
Aug 28 09:00:48 Starting compiler/encoders/riscv
Aug 28 09:02:27 Finished compiler/encoders/riscv                               1m37s 579MB
Aug 28 09:02:29 Starting compiler/backend/x64
Aug 28 09:03:01 Finished compiler/backend/x64                                    30s   1GB
Aug 28 09:03:03 Starting compiler/backend/arm6
Aug 28 09:03:37 Finished compiler/backend/arm6                                   32s 971MB
Aug 28 09:03:39 Starting compiler/backend/arm8
Aug 28 09:04:12 Finished compiler/backend/arm8                                   30s   1GB
Aug 28 09:04:14 Starting compiler/backend/mips
Aug 28 09:04:48 Finished compiler/backend/mips                                   31s   1GB
Aug 28 09:04:50 Starting compiler/backend/riscv
Aug 28 09:05:21 Finished compiler/backend/riscv                                  28s 761MB
Aug 28 09:05:23 Starting compiler/parsing/proofs
Aug 28 09:09:23 Finished compiler/parsing/proofs                               3m58s 975MB
Aug 28 09:09:25 Starting compiler/inference/proofs
Aug 28 09:14:14 Finished compiler/inference/proofs                             4m46s   1GB
Aug 28 09:14:16 Starting compiler/backend/semantics
Aug 28 09:28:46 Finished compiler/backend/semantics                           14m28s   2GB
Aug 28 09:28:48 Starting compiler/backend/reg_alloc/proofs
Aug 28 09:40:48 Finished compiler/backend/reg_alloc/proofs                    11m57s 550MB
Aug 28 09:40:50 Starting compiler/backend/proofs
Aug 28 10:35:29 Finished compiler/backend/proofs                              54m37s   3GB
Aug 28 10:35:31 Starting compiler/encoders/x64/proofs
Aug 28 10:47:14 Finished compiler/encoders/x64/proofs                         11m40s   1GB
Aug 28 10:47:16 Starting compiler/encoders/arm6/proofs
Aug 28 10:59:26 Finished compiler/encoders/arm6/proofs                        12m08s   2GB
Aug 28 10:59:28 Starting compiler/encoders/arm8/proofs
Aug 28 11:07:48 Finished compiler/encoders/arm8/proofs                         8m17s   1GB
Aug 28 11:07:50 Starting compiler/encoders/mips/proofs
Aug 28 11:19:32 Finished compiler/encoders/mips/proofs                        11m40s   1GB
Aug 28 11:19:34 Starting compiler/encoders/riscv/proofs
Aug 28 11:32:02 Finished compiler/encoders/riscv/proofs                       12m25s   1GB
Aug 28 11:32:04 Starting compiler/backend/x64/proofs
Aug 28 11:32:40 Finished compiler/backend/x64/proofs                             34s   1GB
Aug 28 11:32:42 Starting compiler/backend/arm6/proofs
Aug 28 11:33:21 Finished compiler/backend/arm6/proofs                            36s   1GB
Aug 28 11:33:23 Starting compiler/backend/arm8/proofs
Aug 28 11:33:59 Finished compiler/backend/arm8/proofs                            34s   1GB
Aug 28 11:34:01 Starting compiler/backend/mips/proofs
Aug 28 11:34:37 Finished compiler/backend/mips/proofs                            33s   1GB
Aug 28 11:34:39 Starting compiler/backend/riscv/proofs
Aug 28 11:35:15 Finished compiler/backend/riscv/proofs                           34s   1GB
Aug 28 11:35:17 Starting compiler/proofs
Aug 28 11:37:44 Finished compiler/proofs                                       2m24s   2GB
Aug 28 11:37:46 Starting candle/set-theory
Aug 28 11:38:38 Finished candle/set-theory                                       49s 548MB
Aug 28 11:38:40 Starting candle/syntax-lib
Aug 28 11:38:58 Finished candle/syntax-lib                                       16s 437MB
Aug 28 11:39:00 Starting candle/standard/syntax
Aug 28 11:41:41 Finished candle/standard/syntax                                2m39s   1GB
Aug 28 11:41:43 Starting candle/standard/semantics
Aug 28 11:43:59 Finished candle/standard/semantics                             2m13s 749MB
Aug 28 11:44:01 Starting candle/standard/monadic
Aug 28 11:46:35 Finished candle/standard/monadic                               2m32s   1GB
Aug 28 11:46:37 Starting candle/standard/ml_kernel
Aug 28 12:11:43 Finished candle/standard/ml_kernel                            25m03s   3GB
Aug 28 12:11:45 Starting candle/standard/opentheory
Aug 28 12:26:16 Finished candle/standard/opentheory                           14m28s   6GB
Aug 28 12:26:17 Starting characteristic/examples
Aug 28 12:28:54 Finished characteristic/examples                               2m34s   1GB
Aug 28 12:28:56 Starting tutorial/solutions
Aug 28 12:50:19 Finished tutorial/solutions                                   21m21s   5GB
Aug 28 12:50:21 Starting translator/monadic/examples
Aug 28 12:53:06 Finished translator/monadic/examples                           2m43s   2GB
Aug 28 12:53:08 Starting examples
Aug 28 13:01:20 Finished examples                                              8m09s   4GB
Aug 28 13:01:22 Starting examples/compilation
Aug 28 15:56:28 Finished examples/compilation                               2h55m03s  15GB
Aug 28 15:56:30 Starting examples/compilation/proofs
Aug 28 16:00:05 Finished examples/compilation/proofs                           3m32s   2GB
Aug 28 16:00:07 Starting compiler/benchmarks
Aug 28 16:00:09 Finished compiler/benchmarks                                      0s   4MB
Aug 28 16:00:11 Starting translator/okasaki-examples
Aug 28 16:06:35 Finished translator/okasaki-examples                           6m21s   1GB
Aug 28 16:06:37 Starting translator/other-examples
Aug 28 16:13:16 Finished translator/other-examples                             6m37s   1GB
Aug 28 16:13:18 Starting compiler/parsing/tests
Aug 28 16:13:59 Finished compiler/parsing/tests                                  38s 345MB
Aug 28 16:14:01 Starting compiler/inference/tests
Aug 28 16:20:24 Finished compiler/inference/tests                              6m21s   3GB
Aug 28 16:20:26 Starting compiler/bootstrap/translation
Aug 28 23:32:02 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/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
compiler32ProgTheory                                         FAILED! <Signal 9>
 Translating compiler_parse_nums
 Saved theorem _____ "nsLookup_auto_env_64"
 Saved theorem _____ "compiler_parse_nums_v_thm"
 Translating clos_known_default_inline_factor
 Saved theorem _____ "nsLookup_auto_env_65"
 Saved theorem _____ "clos_known_default_inline_factor_v_thm"
 Translating clos_known_default_max_body_size
 Saved theorem _____ "nsLookup_auto_env_66"
 Saved theorem _____ "clos_known_default_max_body_size_v_thm"
 Translating clos_known_mk_config
compiler64ProgTheory                                                   M-KILLED