Job 436

CakeML:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:086d621de511411ec077f271bd7a73f3f37f99d6
  Another missing ERR definition [Aug 20 07:01:20]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Aug 20 12:49:18 Claimed job
Aug 20 12:49:29 Building HOL
Aug 20 13:01:50 Starting developers/bin
Aug 20 13:02:00 Finished developers/bin                                           7s 142MB
Aug 20 13:02:02 Starting semantics/ffi
Aug 20 13:03:03 Finished semantics/ffi                                           59s 321MB
Aug 20 13:03:05 Starting semantics
Aug 20 13:05:27 Finished semantics                                             2m20s 715MB
Aug 20 13:05:29 Starting semantics/proofs
Aug 20 13:10:42 Finished semantics/proofs                                      5m10s   1GB
Aug 20 13:10:44 Starting basis/pure
Aug 20 13:16:29 Finished basis/pure                                            5m43s 697MB
Aug 20 13:16:31 Starting translator
Aug 20 13:19:17 Finished translator                                            2m43s 917MB
Aug 20 13:19:18 Starting compiler/parsing
Aug 20 13:21:42 Finished compiler/parsing                                      2m21s   2GB
Aug 20 13:21:44 Starting characteristic
Aug 20 13:26:12 Finished characteristic                                        4m25s   1GB
Aug 20 13:26:14 Starting translator/monadic
Aug 20 13:28:52 Finished translator/monadic                                    2m35s   1GB
Aug 20 13:28:54 Starting basis
Aug 20 13:55:38 Finished basis                                                26m41s   2GB
Aug 20 13:55:40 Starting compiler/inference
Aug 20 13:58:29 Finished compiler/inference                                    2m46s   1GB
Aug 20 13:58:31 Starting compiler/backend/reg_alloc
Aug 20 13:59:28 Finished compiler/backend/reg_alloc                              54s   1GB
Aug 20 13:59:29 Starting compiler/backend/gc
Aug 20 14:14:07 Finished compiler/backend/gc                                  14m35s   3GB
Aug 20 14:14:09 Starting compiler/backend
Aug 20 14:14:14 Finished compiler/backend                                         3s  18MB
Aug 20 14:14:16 Starting compiler/encoders/asm
Aug 20 14:14:19 Finished compiler/encoders/asm                                    0s  11MB
Aug 20 14:14:21 Starting compiler/encoders/x64
Aug 20 14:15:47 Finished compiler/encoders/x64                                 1m24s 506MB
Aug 20 14:15:49 Starting compiler/encoders/arm6
Aug 20 14:18:52 Finished compiler/encoders/arm6                                3m00s   1GB
Aug 20 14:18:54 Starting compiler/encoders/arm8
Aug 20 14:19:38 Finished compiler/encoders/arm8                                  41s 390MB
Aug 20 14:19:40 Starting compiler/encoders/mips
Aug 20 14:21:17 Finished compiler/encoders/mips                                1m35s 705MB
Aug 20 14:21:19 Starting compiler/encoders/riscv
Aug 20 14:22:55 Finished compiler/encoders/riscv                               1m33s 523MB
Aug 20 14:22:57 Starting compiler/backend/x64
Aug 20 14:23:28 Finished compiler/backend/x64                                    28s 796MB
Aug 20 14:23:30 Starting compiler/backend/arm6
Aug 20 14:24:04 Finished compiler/backend/arm6                                   32s   1GB
Aug 20 14:24:05 Starting compiler/backend/arm8
Aug 20 14:24:39 Finished compiler/backend/arm8                                   31s   1GB
Aug 20 14:24:41 Starting compiler/backend/mips
Aug 20 14:25:16 Finished compiler/backend/mips                                   33s 918MB
Aug 20 14:25:18 Starting compiler/backend/riscv
Aug 20 14:25:50 Finished compiler/backend/riscv                                  30s   1GB
Aug 20 14:25:52 Starting compiler/parsing/proofs
Aug 20 14:29:56 Finished compiler/parsing/proofs                               4m01s 856MB
Aug 20 14:29:57 Starting compiler/inference/proofs
Aug 20 14:34:48 Finished compiler/inference/proofs                             4m48s   1GB
Aug 20 14:34:50 Starting compiler/backend/semantics
Aug 20 14:49:20 Finished compiler/backend/semantics                           14m27s   2GB
Aug 20 14:49:22 Starting compiler/backend/reg_alloc/proofs
Aug 20 14:50:45 Finished compiler/backend/reg_alloc/proofs                     1m21s 394MB
Aug 20 14:50:47 Starting compiler/backend/proofs
Aug 20 15:45:00 Finished compiler/backend/proofs                              54m10s   3GB
Aug 20 15:45:02 Starting compiler/encoders/x64/proofs
Aug 20 15:56:28 Finished compiler/encoders/x64/proofs                         11m23s   1GB
Aug 20 15:56:30 Starting compiler/encoders/arm6/proofs
Aug 20 16:08:33 Finished compiler/encoders/arm6/proofs                        12m01s   3GB
Aug 20 16:08:34 Starting compiler/encoders/arm8/proofs
Aug 20 16:16:53 Finished compiler/encoders/arm8/proofs                         8m16s   1GB
Aug 20 16:16:55 Starting compiler/encoders/mips/proofs
Aug 20 16:28:28 Finished compiler/encoders/mips/proofs                        11m31s   2GB
Aug 20 16:28:30 Starting compiler/encoders/riscv/proofs
Aug 20 16:41:07 Finished compiler/encoders/riscv/proofs                       12m34s   1GB
Aug 20 16:41:09 Starting compiler/backend/x64/proofs
Aug 20 16:41:45 Finished compiler/backend/x64/proofs                             34s   1GB
Aug 20 16:41:47 Starting compiler/backend/arm6/proofs
Aug 20 16:42:27 Finished compiler/backend/arm6/proofs                            37s   1GB
Aug 20 16:42:29 Starting compiler/backend/arm8/proofs
Aug 20 16:43:03 Finished compiler/backend/arm8/proofs                            32s   1GB
Aug 20 16:43:05 Starting compiler/backend/mips/proofs
Aug 20 16:43:42 Finished compiler/backend/mips/proofs                            34s   1GB
Aug 20 16:43:44 Starting compiler/backend/riscv/proofs
Aug 20 16:44:19 Finished compiler/backend/riscv/proofs                           33s   1GB
Aug 20 16:44:21 Starting compiler/proofs
Aug 20 16:46:45 Finished compiler/proofs                                       2m22s   1GB
Aug 20 16:46:47 Starting candle/set-theory
Aug 20 16:47:44 Finished candle/set-theory                                       54s 607MB
Aug 20 16:47:46 Starting candle/syntax-lib
Aug 20 16:48:05 Finished candle/syntax-lib                                       17s 589MB
Aug 20 16:48:07 Starting candle/standard/syntax
Aug 20 16:50:51 Finished candle/standard/syntax                                2m41s 786MB
Aug 20 16:50:53 Starting candle/standard/semantics
Aug 20 16:53:07 Finished candle/standard/semantics                             2m12s 684MB
Aug 20 16:53:09 Starting candle/standard/monadic
Aug 20 16:55:30 Finished candle/standard/monadic                               2m19s 958MB
Aug 20 16:55:32 Starting candle/standard/ml_kernel
Aug 20 17:01:22 Finished candle/standard/ml_kernel                             5m47s   2GB
Aug 20 17:01:24 Starting candle/standard/opentheory
Aug 20 17:01:51 Finished candle/standard/opentheory                              24s 671MB
Aug 20 17:01:53 Starting characteristic/examples
Aug 20 17:04:28 Finished characteristic/examples                               2m33s   1GB
Aug 20 17:04:30 Starting tutorial/solutions
Aug 20 17:25:12 Finished tutorial/solutions                                   20m39s   9GB
Aug 20 17:25:14 Starting translator/monadic/examples
Aug 20 17:28:02 Finished translator/monadic/examples                           2m46s   2GB
Aug 20 17:28:04 Starting examples
Aug 20 17:36:04 Finished examples                                              7m58s   3GB
Aug 20 17:36:06 Starting examples/compilation
Aug 20 20:30:08 Finished examples/compilation                               2h53m59s  11GB
Aug 20 20:30:10 Starting examples/compilation/proofs
Aug 20 20:33:40 Finished examples/compilation/proofs                           3m27s   2GB
Aug 20 20:33:42 Starting compiler/benchmarks
Aug 20 20:33:44 Finished compiler/benchmarks                                      0s   4MB
Aug 20 20:33:46 Starting translator/okasaki-examples
Aug 20 20:40:16 Finished translator/okasaki-examples                           6m28s   1GB
Aug 20 20:40:18 Starting translator/other-examples
Aug 20 20:46:47 Finished translator/other-examples                             6m26s   1GB
Aug 20 20:46:49 Starting compiler/parsing/tests
Aug 20 20:47:30 Finished compiler/parsing/tests                                  38s 351MB
Aug 20 20:47:32 Starting compiler/inference/tests
Aug 20 20:53:59 Finished compiler/inference/tests                              6m24s   7GB
Aug 20 20:54:01 Starting compiler/bootstrap/translation
Aug 21 04:56:22 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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-086d621de511411ec077f271bd7a73f3f37f99d6/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-086d621de511411ec077f271bd7a73f3f37f99d6/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_target32ProgTheory                                                                                                                                     OK
Starting work on arm6ProgTheory
to_target64ProgTheory                                                                                                                                     OK
Starting work on x64ProgTheory
arm6ProgTheory                                                                                                                                            OK
Starting work on compiler32ProgTheory
x64ProgTheory                                                                                                                                             OK
Starting work on arm8ProgTheory
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