Job 417

CakeML:1b0dbd2c9a766be60ba0bcc0f671d2186b25550d
  Dummy commit to test ulimit on regression servers [Aug 01 07:48:35]
#505 (test-ulimit)
Merging into:c791fec924f529f0ad0fd488321c7936b6e24533
  Add two theorems to semantics/proofs [Aug 09 14:35:27]
HOL:f243fe78da5dcc426046ce1b6a0f756e6aa524b9
  Hide vim scratch buffer from the list of buffers [Aug 08 03:52:48]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Aug 10 00:06:03 Claimed job
Aug 10 00:06:10 Reusing HOL
Aug 10 00:06:36 Starting developers/bin
Aug 10 00:06:46 Finished developers/bin                                           8s 224MB
Aug 10 00:06:48 Starting semantics/ffi
Aug 10 00:07:06 Finished semantics/ffi                                           16s 248MB
Aug 10 00:07:08 Starting semantics
Aug 10 00:09:06 Finished semantics                                             1m56s 760MB
Aug 10 00:09:08 Starting semantics/proofs
Aug 10 00:14:29 Finished semantics/proofs                                      5m18s   1GB
Aug 10 00:14:31 Starting basis/pure
Aug 10 00:20:23 Finished basis/pure                                            5m48s 715MB
Aug 10 00:20:25 Starting translator
Aug 10 00:23:13 Finished translator                                            2m45s 885MB
Aug 10 00:23:15 Starting compiler/parsing
Aug 10 00:25:39 Finished compiler/parsing                                      2m21s   2GB
Aug 10 00:25:41 Starting characteristic
Aug 10 00:30:10 Finished characteristic                                        4m26s   1GB
Aug 10 00:30:12 Starting translator/monadic
Aug 10 00:32:48 Finished translator/monadic                                    2m34s   1GB
Aug 10 00:32:50 Starting basis
Aug 10 00:59:37 Finished basis                                                26m45s   3GB
Aug 10 00:59:39 Starting compiler/inference
Aug 10 01:02:29 Finished compiler/inference                                    2m47s   1GB
Aug 10 01:02:31 Starting compiler/backend/reg_alloc
Aug 10 01:03:28 Finished compiler/backend/reg_alloc                              55s   1GB
Aug 10 01:03:30 Starting compiler/backend/gc
Aug 10 01:18:38 Finished compiler/backend/gc                                  15m06s   3GB
Aug 10 01:18:40 Starting compiler/backend
Aug 10 01:18:46 Finished compiler/backend                                         3s  20MB
Aug 10 01:18:48 Starting compiler/encoders/asm
Aug 10 01:18:51 Finished compiler/encoders/asm                                    0s  25MB
Aug 10 01:18:53 Starting compiler/encoders/x64
Aug 10 01:20:21 Finished compiler/encoders/x64                                 1m26s 594MB
Aug 10 01:20:24 Starting compiler/encoders/arm6
Aug 10 01:23:30 Finished compiler/encoders/arm6                                3m03s   1GB
Aug 10 01:23:32 Starting compiler/encoders/arm8
Aug 10 01:24:17 Finished compiler/encoders/arm8                                  43s 404MB
Aug 10 01:24:19 Starting compiler/encoders/mips
Aug 10 01:25:56 Finished compiler/encoders/mips                                1m35s 722MB
Aug 10 01:25:58 Starting compiler/encoders/riscv
Aug 10 01:27:36 Finished compiler/encoders/riscv                               1m35s 464MB
Aug 10 01:27:38 Starting compiler/backend/x64
Aug 10 01:28:08 Finished compiler/backend/x64                                    27s 748MB
Aug 10 01:28:10 Starting compiler/backend/arm6
Aug 10 01:28:44 Finished compiler/backend/arm6                                   31s   1GB
Aug 10 01:28:46 Starting compiler/backend/arm8
Aug 10 01:29:18 Finished compiler/backend/arm8                                   30s   1GB
Aug 10 01:29:20 Starting compiler/backend/mips
Aug 10 01:29:53 Finished compiler/backend/mips                                   30s   1GB
Aug 10 01:29:55 Starting compiler/backend/riscv
Aug 10 01:30:27 Finished compiler/backend/riscv                                  30s   1GB
Aug 10 01:30:29 Starting compiler/parsing/proofs
Aug 10 01:34:34 Finished compiler/parsing/proofs                               4m02s 799MB
Aug 10 01:34:36 Starting compiler/inference/proofs
Aug 10 01:39:26 Finished compiler/inference/proofs                             4m48s   1GB
Aug 10 01:39:28 Starting compiler/backend/semantics
Aug 10 01:53:59 Finished compiler/backend/semantics                           14m28s   2GB
Aug 10 01:54:01 Starting compiler/backend/reg_alloc/proofs
Aug 10 01:55:26 Finished compiler/backend/reg_alloc/proofs                     1m22s 411MB
Aug 10 01:55:28 Starting compiler/backend/proofs
Aug 10 02:50:09 Finished compiler/backend/proofs                              54m38s   2GB
Aug 10 02:50:11 Starting compiler/encoders/x64/proofs
Aug 10 03:01:56 Finished compiler/encoders/x64/proofs                         11m42s   1GB
Aug 10 03:01:58 Starting compiler/encoders/arm6/proofs
Aug 10 03:14:11 Finished compiler/encoders/arm6/proofs                        12m10s   2GB
Aug 10 03:14:13 Starting compiler/encoders/arm8/proofs
Aug 10 03:22:41 Finished compiler/encoders/arm8/proofs                         8m26s   1GB
Aug 10 03:22:43 Starting compiler/encoders/mips/proofs
Aug 10 03:34:15 Finished compiler/encoders/mips/proofs                        11m29s   2GB
Aug 10 03:34:17 Starting compiler/encoders/riscv/proofs
Aug 10 03:46:51 Finished compiler/encoders/riscv/proofs                       12m31s   1GB
Aug 10 03:46:52 Starting compiler/backend/x64/proofs
Aug 10 03:47:29 Finished compiler/backend/x64/proofs                             34s   1GB
Aug 10 03:47:31 Starting compiler/backend/arm6/proofs
Aug 10 03:48:10 Finished compiler/backend/arm6/proofs                            37s 995MB
Aug 10 03:48:12 Starting compiler/backend/arm8/proofs
Aug 10 03:48:46 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 10 03:48:48 Starting compiler/backend/mips/proofs
Aug 10 03:49:25 Finished compiler/backend/mips/proofs                            34s   1GB
Aug 10 03:49:27 Starting compiler/backend/riscv/proofs
Aug 10 03:50:02 Finished compiler/backend/riscv/proofs                           33s   1GB
Aug 10 03:50:04 Starting compiler/proofs
Aug 10 03:52:30 Finished compiler/proofs                                       2m23s   2GB
Aug 10 03:52:32 Starting candle/set-theory
Aug 10 03:53:18 Finished candle/set-theory                                       44s 566MB
Aug 10 03:53:20 Starting candle/syntax-lib
Aug 10 03:53:39 Finished candle/syntax-lib                                       17s 563MB
Aug 10 03:53:41 Starting candle/standard/syntax
Aug 10 03:56:24 Finished candle/standard/syntax                                2m40s 602MB
Aug 10 03:56:26 Starting candle/standard/semantics
Aug 10 03:58:42 Finished candle/standard/semantics                             2m14s 943MB
Aug 10 03:58:44 Starting candle/standard/monadic
Aug 10 04:01:07 Finished candle/standard/monadic                               2m21s 995MB
Aug 10 04:01:09 Starting candle/standard/ml_kernel
Aug 10 04:06:58 Finished candle/standard/ml_kernel                             5m46s   2GB
Aug 10 04:07:00 Starting candle/standard/opentheory
Aug 10 04:07:27 Finished candle/standard/opentheory                              25s 554MB
Aug 10 04:07:29 Starting characteristic/examples
Aug 10 04:10:01 Finished characteristic/examples                               2m29s   1GB
Aug 10 04:10:03 Starting tutorial/solutions
Aug 10 04:30:49 Finished tutorial/solutions                                   20m43s   8GB
Aug 10 04:30:51 Starting translator/monadic/examples
Aug 10 04:33:39 Finished translator/monadic/examples                           2m46s   2GB
Aug 10 04:33:41 Starting examples
Aug 10 04:41:30 Finished examples                                              7m47s   5GB
Aug 10 04:41:32 Starting examples/compilation
Aug 10 07:36:50 Finished examples/compilation                               2h55m15s   8GB
Aug 10 07:36:52 Starting examples/compilation/proofs
Aug 10 07:40:22 Finished examples/compilation/proofs                           3m28s   3GB
Aug 10 07:40:24 Starting compiler/benchmarks
Aug 10 07:40:26 Finished compiler/benchmarks                                      0s   4MB
Aug 10 07:40:28 Starting translator/okasaki-examples
Aug 10 07:46:59 Finished translator/okasaki-examples                           6m28s   1GB
Aug 10 07:47:01 Starting translator/other-examples
Aug 10 07:53:41 Finished translator/other-examples                             6m37s   1GB
Aug 10 07:53:43 Starting compiler/parsing/tests
Aug 10 07:54:25 Finished compiler/parsing/tests                                  40s 336MB
Aug 10 07:54:27 Starting compiler/inference/tests
Aug 10 08:00:38 Finished compiler/inference/tests                              6m08s   4GB
Aug 10 08:00:40 Starting compiler/bootstrap/translation
Aug 10 16:14:53 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/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_word64ProgTheory                                                                                           OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                                                           OK
Starting work on to_target32ProgTheory
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>
 Saved theorem _____ "nsLookup_auto_env_42"
 Saved theorem _____ "compiler_config_skip_type_inference_fupd_v_thm"
 Adding type :compile_error
 Saved definition __ "COMPILER_COMPILE_ERROR_TYPE_def"
 Saved theorem _____ "COMPILER_COMPILE_ERROR_TYPE_def"
 Saved theorem _____ "nsLookup_auto_env_43"
 Translating compiler_compile
 Saved theorem _____ "nsLookup_auto_env_44"
 Saved theorem _____ "compiler_compile_v_thm"
 Translating basisprog_basis
compiler64ProgTheory                                                                                    M-KILLED