Job 511

CakeML:0bca5648f09015518a7629441ff5c3e6174e3731
  Fix some things downstream of the tap changes. [Sep 20 15:16:47]
#526 (explorer)
Merging into:675c1da06454efcef70f62574de96a524820287f
  Merge pull request #532 from CakeML/trans-msg [Oct 03 07:58:05]
HOL:ef4c7cafab216f321b6aba91ed33c816f6b90049
  Make possible fix for uninterruptibility problem [Oct 03 07:23:22]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Oct 03 08:54:51 Claimed job
Oct 03 08:55:00 Building HOL
Oct 03 09:09:34 Starting developers/bin
Oct 03 09:09:47 Finished developers/bin                                          11s 916MB
Oct 03 09:09:48 Starting semantics/ffi
Oct 03 09:10:54 Finished semantics/ffi                                         1m03s 558MB
Oct 03 09:10:55 Starting semantics
Oct 03 09:13:19 Finished semantics                                             2m21s 987MB
Oct 03 09:13:20 Starting semantics/proofs
Oct 03 09:17:33 Finished semantics/proofs                                      4m11s   1GB
Oct 03 09:17:35 Starting basis/pure
Oct 03 09:23:11 Finished basis/pure                                            5m34s 642MB
Oct 03 09:23:13 Starting translator
Oct 03 09:25:01 Finished translator                                            1m46s 830MB
Oct 03 09:25:02 Starting compiler/parsing
Oct 03 09:27:23 Finished compiler/parsing                                      2m19s   2GB
Oct 03 09:27:25 Starting characteristic
Oct 03 09:31:23 Finished characteristic                                        3m56s   2GB
Oct 03 09:31:25 Starting translator/monadic
Oct 03 09:33:45 Finished translator/monadic                                    2m19s   1GB
Oct 03 09:33:47 Starting basis
Oct 03 09:59:50 Finished basis                                                26m01s   2GB
Oct 03 09:59:52 Starting compiler/inference
Oct 03 10:02:34 Finished compiler/inference                                    2m40s   1GB
Oct 03 10:02:35 Starting compiler/backend/reg_alloc
Oct 03 10:03:53 Finished compiler/backend/reg_alloc                            1m16s   1GB
Oct 03 10:03:55 Starting compiler/backend/gc
Oct 03 10:17:50 Finished compiler/backend/gc                                  13m54s   3GB
Oct 03 10:17:52 Starting compiler/backend
Oct 03 10:17:57 Finished compiler/backend                                         3s  14MB
Oct 03 10:17:59 Starting compiler/encoders/asm
Oct 03 10:18:02 Finished compiler/encoders/asm                                    1s  14MB
Oct 03 10:18:03 Starting compiler/encoders/x64
Oct 03 10:19:33 Finished compiler/encoders/x64                                 1m27s 608MB
Oct 03 10:19:35 Starting compiler/encoders/arm6
Oct 03 10:22:30 Finished compiler/encoders/arm6                                2m53s   1GB
Oct 03 10:22:32 Starting compiler/encoders/arm8
Oct 03 10:23:20 Finished compiler/encoders/arm8                                  46s 469MB
Oct 03 10:23:21 Starting compiler/encoders/mips
Oct 03 10:25:02 Finished compiler/encoders/mips                                1m39s   1GB
Oct 03 10:25:04 Starting compiler/encoders/riscv
Oct 03 10:26:42 Finished compiler/encoders/riscv                               1m36s   1GB
Oct 03 10:26:43 Starting compiler/backend/x64
Oct 03 10:27:12 Finished compiler/backend/x64                                    26s 887MB
Oct 03 10:27:14 Starting compiler/backend/arm6
Oct 03 10:27:48 Finished compiler/backend/arm6                                   33s   1GB
Oct 03 10:27:50 Starting compiler/backend/arm8
Oct 03 10:28:21 Finished compiler/backend/arm8                                   29s   1GB
Oct 03 10:28:23 Starting compiler/backend/mips
Oct 03 10:28:52 Finished compiler/backend/mips                                   27s 902MB
Oct 03 10:28:54 Starting compiler/backend/riscv
Oct 03 10:29:26 Finished compiler/backend/riscv                                  30s   1GB
Oct 03 10:29:27 Starting compiler/parsing/proofs
Oct 03 10:39:38 Finished compiler/parsing/proofs                              10m09s 820MB
Oct 03 10:39:39 Starting compiler/inference/proofs
Oct 03 10:44:10 Finished compiler/inference/proofs                             4m29s   1GB
Oct 03 10:44:12 Starting compiler/backend/semantics
Oct 03 10:57:51 Finished compiler/backend/semantics                           13m37s   1GB
Oct 03 10:57:52 Starting compiler/backend/reg_alloc/proofs
Oct 03 11:09:04 Finished compiler/backend/reg_alloc/proofs                    11m10s 580MB
Oct 03 11:09:06 Starting compiler/backend/proofs
Oct 03 12:02:29 Finished compiler/backend/proofs                              53m20s   3GB
Oct 03 12:02:30 Starting compiler/encoders/x64/proofs
Oct 03 12:14:06 Finished compiler/encoders/x64/proofs                         11m33s   4GB
Oct 03 12:14:08 Starting compiler/encoders/arm6/proofs
Oct 03 12:26:06 Finished compiler/encoders/arm6/proofs                        11m55s   3GB
Oct 03 12:26:07 Starting compiler/encoders/arm8/proofs
Oct 03 12:34:42 Finished compiler/encoders/arm8/proofs                         8m33s   1GB
Oct 03 12:34:44 Starting compiler/encoders/mips/proofs
Oct 03 12:46:31 Finished compiler/encoders/mips/proofs                        11m45s   2GB
Oct 03 12:46:33 Starting compiler/encoders/riscv/proofs
Oct 03 12:58:58 Finished compiler/encoders/riscv/proofs                       12m23s   1GB
Oct 03 12:58:59 Starting compiler/backend/x64/proofs
Oct 03 12:59:32 Finished compiler/backend/x64/proofs                             30s 858MB
Oct 03 12:59:33 Starting compiler/backend/arm6/proofs
Oct 03 13:00:10 Finished compiler/backend/arm6/proofs                            34s   1GB
Oct 03 13:00:11 Starting compiler/backend/arm8/proofs
Oct 03 13:00:45 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 03 13:00:47 Starting compiler/backend/mips/proofs
Oct 03 13:01:22 Finished compiler/backend/mips/proofs                            33s   1GB
Oct 03 13:01:24 Starting compiler/backend/riscv/proofs
Oct 03 13:01:59 Finished compiler/backend/riscv/proofs                           33s   1GB
Oct 03 13:02:00 Starting compiler/proofs
Oct 03 13:04:30 Finished compiler/proofs                                       2m27s   2GB
Oct 03 13:04:31 Starting candle/set-theory
Oct 03 13:05:25 Finished candle/set-theory                                       51s 628MB
Oct 03 13:05:26 Starting candle/syntax-lib
Oct 03 13:05:45 Finished candle/syntax-lib                                       16s 619MB
Oct 03 13:05:46 Starting candle/standard/syntax
Oct 03 13:08:23 Finished candle/standard/syntax                                2m35s 685MB
Oct 03 13:08:25 Starting candle/standard/semantics
Oct 03 13:10:36 Finished candle/standard/semantics                             2m09s 948MB
Oct 03 13:10:38 Starting candle/standard/monadic
Oct 03 13:13:11 Finished candle/standard/monadic                               2m30s 955MB
Oct 03 13:13:13 Starting candle/standard/ml_kernel
Oct 03 13:37:52 Finished candle/standard/ml_kernel                            24m37s   5GB
Oct 03 13:37:54 Starting candle/standard/opentheory
Oct 03 13:51:49 Finished candle/standard/opentheory                           13m53s   8GB
Oct 03 13:51:51 Starting candle/standard/opentheory/compilation
Oct 03 14:41:02 Finished candle/standard/opentheory/compilation               49m09s  19GB
Oct 03 14:41:04 Starting characteristic/examples
Oct 03 14:43:43 Finished characteristic/examples                               2m37s   1GB
Oct 03 14:43:44 Starting tutorial/solutions
Oct 03 15:05:24 Finished tutorial/solutions                                   21m38s   5GB
Oct 03 15:05:26 Starting translator/monadic/examples
Oct 03 15:08:00 Finished translator/monadic/examples                           2m32s   3GB
Oct 03 15:08:02 Starting examples
Oct 03 15:15:37 Finished examples                                              7m33s   4GB
Oct 03 15:15:39 Starting examples/compilation
Oct 03 18:14:37 Finished examples/compilation                               2h58m56s  10GB
Oct 03 18:14:39 Starting examples/compilation/proofs
Oct 03 18:17:56 Finished examples/compilation/proofs                           3m15s   3GB
Oct 03 18:17:57 Starting compiler/benchmarks
Oct 03 18:17:59 Finished compiler/benchmarks                                      0s   7MB
Oct 03 18:18:01 Starting translator/okasaki-examples
Oct 03 18:23:28 Finished translator/okasaki-examples                           5m24s   1GB
Oct 03 18:23:29 Starting translator/other-examples
Oct 03 18:29:12 Finished translator/other-examples                             5m41s 960MB
Oct 03 18:29:14 Starting compiler/parsing/tests
Oct 03 18:29:55 Finished compiler/parsing/tests                                  39s 370MB
Oct 03 18:29:57 Starting compiler/inference/tests
Oct 03 18:36:18 Finished compiler/inference/tests                              6m19s   5GB
Oct 03 18:36:19 Starting compiler/bootstrap/translation
Oct 04 01:42:26 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-ef4c7cafab216f321b6aba91ed33c816f6b90049/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
compiler32ProgTheory                                                                                                                              FAILED! <1>
 
 
 which has type:
 
 :32 backend$config ->
 ast$dec list ->
 (word8 list # word32 list # 32 lab_to_target$config) option # tap_data list
 
 Failed translation: compile
 Uncaught exception: UnableToTranslate (Const (?, GRND (Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 0), [])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 0), []), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 0), []), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])])]), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])])])])]), Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])]))))
mipsProgTheory                                                                                                                                       M-KILLED