Job 507

CakeML:0bca5648f09015518a7629441ff5c3e6174e3731
  Fix some things downstream of the tap changes. [Sep 20 15:16:47]
#526 (explorer)
Merging into:153ef4270fca8b5a3d6e9652f1f11edbad70406a
  Add reader compilation theories to build-sequence [Sep 26 17:48:15]
HOL:b42a4b729800b9a771bd1820e31e0ada14653ffb
  Document strange uninterruptibility of {PROVE,METIS}_TAC in comment [Oct 02 06:56:54]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Oct 02 09:36:46 Claimed job
Oct 02 09:36:54 Building HOL
Oct 02 09:51:24 Starting developers/bin
Oct 02 09:51:37 Finished developers/bin                                          11s 916MB
Oct 02 09:51:38 Starting semantics/ffi
Oct 02 09:52:44 Finished semantics/ffi                                         1m03s 527MB
Oct 02 09:52:45 Starting semantics
Oct 02 09:55:04 Finished semantics                                             2m17s 986MB
Oct 02 09:55:06 Starting semantics/proofs
Oct 02 09:59:13 Finished semantics/proofs                                      4m05s   1GB
Oct 02 09:59:15 Starting basis/pure
Oct 02 10:04:49 Finished basis/pure                                            5m32s 693MB
Oct 02 10:04:51 Starting translator
Oct 02 10:06:39 Finished translator                                            1m46s   1GB
Oct 02 10:06:40 Starting compiler/parsing
Oct 02 10:08:59 Finished compiler/parsing                                      2m17s   2GB
Oct 02 10:09:01 Starting characteristic
Oct 02 10:12:55 Finished characteristic                                        3m52s   1GB
Oct 02 10:12:57 Starting translator/monadic
Oct 02 10:15:14 Finished translator/monadic                                    2m15s   1GB
Oct 02 10:15:15 Starting basis
Oct 02 10:41:23 Finished basis                                                26m05s   3GB
Oct 02 10:41:24 Starting compiler/inference
Oct 02 10:44:08 Finished compiler/inference                                    2m41s   1GB
Oct 02 10:44:09 Starting compiler/backend/reg_alloc
Oct 02 10:45:29 Finished compiler/backend/reg_alloc                            1m18s   1GB
Oct 02 10:45:31 Starting compiler/backend/gc
Oct 02 10:59:28 Finished compiler/backend/gc                                  13m55s   3GB
Oct 02 10:59:30 Starting compiler/backend
Oct 02 10:59:35 Finished compiler/backend                                         3s  15MB
Oct 02 10:59:37 Starting compiler/encoders/asm
Oct 02 10:59:39 Finished compiler/encoders/asm                                    1s  14MB
Oct 02 10:59:41 Starting compiler/encoders/x64
Oct 02 11:01:14 Finished compiler/encoders/x64                                 1m30s 610MB
Oct 02 11:01:15 Starting compiler/encoders/arm6
Oct 02 11:04:11 Finished compiler/encoders/arm6                                2m53s   1GB
Oct 02 11:04:13 Starting compiler/encoders/arm8
Oct 02 11:04:59 Finished compiler/encoders/arm8                                  45s 472MB
Oct 02 11:05:01 Starting compiler/encoders/mips
Oct 02 11:06:40 Finished compiler/encoders/mips                                1m37s 876MB
Oct 02 11:06:42 Starting compiler/encoders/riscv
Oct 02 11:08:22 Finished compiler/encoders/riscv                               1m38s 941MB
Oct 02 11:08:23 Starting compiler/backend/x64
Oct 02 11:08:54 Finished compiler/backend/x64                                    28s   1GB
Oct 02 11:08:55 Starting compiler/backend/arm6
Oct 02 11:09:27 Finished compiler/backend/arm6                                   30s   1GB
Oct 02 11:09:29 Starting compiler/backend/arm8
Oct 02 11:09:58 Finished compiler/backend/arm8                                   27s 946MB
Oct 02 11:09:59 Starting compiler/backend/mips
Oct 02 11:10:32 Finished compiler/backend/mips                                   30s   1GB
Oct 02 11:10:33 Starting compiler/backend/riscv
Oct 02 11:11:02 Finished compiler/backend/riscv                                  26s 985MB
Oct 02 11:11:03 Starting compiler/parsing/proofs
Oct 02 11:21:22 Finished compiler/parsing/proofs                              10m17s 802MB
Oct 02 11:21:24 Starting compiler/inference/proofs
Oct 02 11:25:53 Finished compiler/inference/proofs                             4m27s   1GB
Oct 02 11:25:54 Starting compiler/backend/semantics
Oct 02 11:39:26 Finished compiler/backend/semantics                           13m30s   2GB
Oct 02 11:39:27 Starting compiler/backend/reg_alloc/proofs
Oct 02 11:50:20 Finished compiler/backend/reg_alloc/proofs                    10m51s 667MB
Oct 02 11:50:22 Starting compiler/backend/proofs
Oct 02 12:43:09 Finished compiler/backend/proofs                              52m45s   3GB
Oct 02 12:43:11 Starting compiler/encoders/x64/proofs
Oct 02 12:54:55 Finished compiler/encoders/x64/proofs                         11m43s   4GB
Oct 02 12:54:57 Starting compiler/encoders/arm6/proofs
Oct 02 13:07:02 Finished compiler/encoders/arm6/proofs                        12m03s   4GB
Oct 02 13:07:04 Starting compiler/encoders/arm8/proofs
Oct 02 13:15:35 Finished compiler/encoders/arm8/proofs                         8m30s   1GB
Oct 02 13:15:37 Starting compiler/encoders/mips/proofs
Oct 02 13:27:04 Finished compiler/encoders/mips/proofs                        11m25s   2GB
Oct 02 13:27:06 Starting compiler/encoders/riscv/proofs
Oct 02 13:39:36 Finished compiler/encoders/riscv/proofs                       12m28s   1GB
Oct 02 13:39:38 Starting compiler/backend/x64/proofs
Oct 02 13:40:11 Finished compiler/backend/x64/proofs                             31s   1GB
Oct 02 13:40:12 Starting compiler/backend/arm6/proofs
Oct 02 13:40:48 Finished compiler/backend/arm6/proofs                            34s   1GB
Oct 02 13:40:50 Starting compiler/backend/arm8/proofs
Oct 02 13:41:23 Finished compiler/backend/arm8/proofs                            31s   1GB
Oct 02 13:41:24 Starting compiler/backend/mips/proofs
Oct 02 13:41:59 Finished compiler/backend/mips/proofs                            33s   1GB
Oct 02 13:42:00 Starting compiler/backend/riscv/proofs
Oct 02 13:42:35 Finished compiler/backend/riscv/proofs                           32s   1GB
Oct 02 13:42:36 Starting compiler/proofs
Oct 02 13:45:05 Finished compiler/proofs                                       2m27s   2GB
Oct 02 13:45:07 Starting candle/set-theory
Oct 02 13:45:59 Finished candle/set-theory                                       50s 638MB
Oct 02 13:46:00 Starting candle/syntax-lib
Oct 02 13:46:18 Finished candle/syntax-lib                                       15s 505MB
Oct 02 13:46:19 Starting candle/standard/syntax
Oct 02 13:48:54 Finished candle/standard/syntax                                2m33s   1GB
Oct 02 13:48:56 Starting candle/standard/semantics
Oct 02 13:51:06 Finished candle/standard/semantics                             2m09s 954MB
Oct 02 13:51:08 Starting candle/standard/monadic
Oct 02 13:53:40 Finished candle/standard/monadic                               2m30s   1GB
Oct 02 13:53:42 Starting candle/standard/ml_kernel
Oct 02 14:18:05 Finished candle/standard/ml_kernel                            24m20s   4GB
Oct 02 14:18:07 Starting candle/standard/opentheory
Oct 02 14:32:10 Finished candle/standard/opentheory                           14m02s   5GB
Oct 02 14:32:12 Starting candle/standard/opentheory/compilation
Oct 02 15:20:42 Finished candle/standard/opentheory/compilation               48m28s  14GB
Oct 02 15:20:44 Starting characteristic/examples
Oct 02 15:23:21 Finished characteristic/examples                               2m35s   2GB
Oct 02 15:23:23 Starting tutorial/solutions
Oct 02 15:44:42 Finished tutorial/solutions                                   21m17s   6GB
Oct 02 15:44:44 Starting translator/monadic/examples
Oct 02 15:47:21 Finished translator/monadic/examples                           2m35s   2GB
Oct 02 15:47:22 Starting examples
Oct 02 15:54:59 Finished examples                                              7m34s   8GB
Oct 02 15:55:00 Starting examples/compilation
Oct 02 18:55:49 Finished examples/compilation                               3h00m46s   7GB
Oct 02 18:55:51 Starting examples/compilation/proofs
Oct 02 18:59:00 Finished examples/compilation/proofs                           3m07s   3GB
Oct 02 18:59:02 Starting compiler/benchmarks
Oct 02 18:59:04 Finished compiler/benchmarks                                      0s   7MB
Oct 02 18:59:06 Starting translator/okasaki-examples
Oct 02 19:04:30 Finished translator/okasaki-examples                           5m22s   1GB
Oct 02 19:04:32 Starting translator/other-examples
Oct 02 19:10:15 Finished translator/other-examples                             5m42s   1GB
Oct 02 19:10:17 Starting compiler/parsing/tests
Oct 02 19:10:59 Finished compiler/parsing/tests                                  39s 352MB
Oct 02 19:11:00 Starting compiler/inference/tests
Oct 02 19:17:11 Finished compiler/inference/tests                              6m08s   4GB
Oct 02 19:17:12 Starting compiler/bootstrap/translation
Oct 03 02:25:24 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-b42a4b729800b9a771bd1820e31e0ada14653ffb/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
x64ProgTheory                                                                                                                                              OK
Starting work on arm8ProgTheory
to_target32ProgTheory                                                                                                                                      OK
Starting work on arm6ProgTheory
arm8ProgTheory                                                                                                                                             OK
Starting work on riscvProgTheory
arm6ProgTheory                                                                                                                                             OK
Starting work on compiler32ProgTheory
riscvProgTheory                                                                                                                                            OK
Starting work on mipsProgTheory
mipsProgTheory                                                                                                                                             OK
Starting work on compiler64ProgTheory
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), [])])])])]))))
compiler64ProgTheory                                                                                                                                 M-KILLED