Job 435

CakeML:de7418a383680d661e4993cd2a960c75cc36787d
  Move register_type into Map structure [Aug 19 17:57:59]
#512 (translator-module-ctors)
Merging into:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:f59f1264f77465a8321b6b7c9115f007db7d2bc1
  Fix a missing ERR definition [Aug 18 19:10:45]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Aug 19 19:13:03 Claimed job
Aug 19 19:13:11 Reusing HOL
Aug 19 19:13:25 Starting developers/bin
Aug 19 19:13:39 Finished developers/bin                                          12s 142MB
Aug 19 19:13:41 Starting semantics/ffi
Aug 19 19:14:00 Finished semantics/ffi                                           16s 256MB
Aug 19 19:14:02 Starting semantics
Aug 19 19:16:01 Finished semantics                                             1m57s 855MB
Aug 19 19:16:03 Starting semantics/proofs
Aug 19 19:21:16 Finished semantics/proofs                                      5m10s   1GB
Aug 19 19:21:18 Starting basis/pure
Aug 19 19:22:51 Finished basis/pure                                            1m31s 831MB
Aug 19 19:22:53 Starting translator
Aug 19 19:24:59 Finished translator                                            2m03s 939MB
Aug 19 19:25:01 Starting compiler/parsing
Aug 19 19:27:23 Finished compiler/parsing                                      2m20s   2GB
Aug 19 19:27:25 Starting characteristic
Aug 19 19:31:49 Finished characteristic                                        4m21s   2GB
Aug 19 19:31:51 Starting translator/monadic
Aug 19 19:34:30 Finished translator/monadic                                    2m37s   1GB
Aug 19 19:34:32 Starting basis
Aug 19 20:01:19 Finished basis                                                26m44s   2GB
Aug 19 20:01:21 Starting compiler/inference
Aug 19 20:03:38 Finished compiler/inference                                    2m15s   1GB
Aug 19 20:03:40 Starting compiler/backend/reg_alloc
Aug 19 20:04:38 Finished compiler/backend/reg_alloc                              56s   1GB
Aug 19 20:04:40 Starting compiler/backend/gc
Aug 19 20:18:01 Finished compiler/backend/gc                                  13m18s   3GB
Aug 19 20:18:03 Starting compiler/backend
Aug 19 20:18:08 Finished compiler/backend                                         3s  18MB
Aug 19 20:18:10 Starting compiler/encoders/asm
Aug 19 20:18:13 Finished compiler/encoders/asm                                    0s  11MB
Aug 19 20:18:15 Starting compiler/encoders/x64
Aug 19 20:18:42 Finished compiler/encoders/x64                                   24s 404MB
Aug 19 20:18:44 Starting compiler/encoders/arm6
Aug 19 20:19:55 Finished compiler/encoders/arm6                                1m08s 398MB
Aug 19 20:19:57 Starting compiler/encoders/arm8
Aug 19 20:20:10 Finished compiler/encoders/arm8                                  11s 397MB
Aug 19 20:20:12 Starting compiler/encoders/mips
Aug 19 20:20:29 Finished compiler/encoders/mips                                  14s 505MB
Aug 19 20:20:31 Starting compiler/encoders/riscv
Aug 19 20:20:46 Finished compiler/encoders/riscv                                 12s 378MB
Aug 19 20:20:48 Starting compiler/backend/x64
Aug 19 20:21:21 Finished compiler/backend/x64                                    30s 828MB
Aug 19 20:21:23 Starting compiler/backend/arm6
Aug 19 20:21:59 Finished compiler/backend/arm6                                   33s   1GB
Aug 19 20:22:01 Starting compiler/backend/arm8
Aug 19 20:22:34 Finished compiler/backend/arm8                                   31s 862MB
Aug 19 20:22:36 Starting compiler/backend/mips
Aug 19 20:23:07 Finished compiler/backend/mips                                   28s 845MB
Aug 19 20:23:09 Starting compiler/backend/riscv
Aug 19 20:23:40 Finished compiler/backend/riscv                                  29s   1GB
Aug 19 20:23:42 Starting compiler/parsing/proofs
Aug 19 20:27:46 Finished compiler/parsing/proofs                               4m02s 829MB
Aug 19 20:27:48 Starting compiler/inference/proofs
Aug 19 20:32:38 Finished compiler/inference/proofs                             4m47s   1GB
Aug 19 20:32:40 Starting compiler/backend/semantics
Aug 19 20:47:11 Finished compiler/backend/semantics                           14m28s   2GB
Aug 19 20:47:13 Starting compiler/backend/reg_alloc/proofs
Aug 19 20:48:36 Finished compiler/backend/reg_alloc/proofs                     1m21s 572MB
Aug 19 20:48:38 Starting compiler/backend/proofs
Aug 19 21:43:29 Finished compiler/backend/proofs                              54m48s   3GB
Aug 19 21:43:31 Starting compiler/encoders/x64/proofs
Aug 19 21:53:23 Finished compiler/encoders/x64/proofs                          9m50s   1GB
Aug 19 21:53:25 Starting compiler/encoders/arm6/proofs
Aug 19 22:03:20 Finished compiler/encoders/arm6/proofs                         9m53s   1GB
Aug 19 22:03:22 Starting compiler/encoders/arm8/proofs
Aug 19 22:11:27 Finished compiler/encoders/arm8/proofs                         8m00s 935MB
Aug 19 22:11:29 Starting compiler/encoders/mips/proofs
Aug 19 22:21:53 Finished compiler/encoders/mips/proofs                        10m22s   2GB
Aug 19 22:21:55 Starting compiler/encoders/riscv/proofs
Aug 19 22:34:16 Finished compiler/encoders/riscv/proofs                       12m18s   1GB
Aug 19 22:34:18 Starting compiler/backend/x64/proofs
Aug 19 22:34:54 Finished compiler/backend/x64/proofs                             33s   1GB
Aug 19 22:34:56 Starting compiler/backend/arm6/proofs
Aug 19 22:35:32 Finished compiler/backend/arm6/proofs                            34s   1GB
Aug 19 22:35:34 Starting compiler/backend/arm8/proofs
Aug 19 22:36:10 Finished compiler/backend/arm8/proofs                            33s   1GB
Aug 19 22:36:11 Starting compiler/backend/mips/proofs
Aug 19 22:36:47 Finished compiler/backend/mips/proofs                            33s   1GB
Aug 19 22:36:49 Starting compiler/backend/riscv/proofs
Aug 19 22:37:25 Finished compiler/backend/riscv/proofs                           33s   1GB
Aug 19 22:37:26 Starting compiler/proofs
Aug 19 22:39:54 Finished compiler/proofs                                       2m25s   2GB
Aug 19 22:39:56 Starting candle/set-theory
Aug 19 22:40:43 Finished candle/set-theory                                       44s 787MB
Aug 19 22:40:45 Starting candle/syntax-lib
Aug 19 22:41:03 Finished candle/syntax-lib                                       16s 529MB
Aug 19 22:41:05 Starting candle/standard/syntax
Aug 19 22:43:51 Finished candle/standard/syntax                                2m43s 670MB
Aug 19 22:43:53 Starting candle/standard/semantics
Aug 19 22:46:09 Finished candle/standard/semantics                             2m13s 833MB
Aug 19 22:46:11 Starting candle/standard/monadic
Aug 19 22:48:37 Finished candle/standard/monadic                               2m24s 929MB
Aug 19 22:48:39 Starting candle/standard/ml_kernel
Aug 19 22:54:21 Finished candle/standard/ml_kernel                             5m39s   2GB
Aug 19 22:54:22 Starting candle/standard/opentheory
Aug 19 22:54:50 Finished candle/standard/opentheory                              25s 609MB
Aug 19 22:54:52 Starting characteristic/examples
Aug 19 22:57:28 Finished characteristic/examples                               2m33s   1GB
Aug 19 22:57:30 Starting tutorial/solutions
Aug 19 23:18:12 Finished tutorial/solutions                                   20m40s   8GB
Aug 19 23:18:14 Starting translator/monadic/examples
Aug 19 23:21:05 Finished translator/monadic/examples                           2m49s   2GB
Aug 19 23:21:07 Starting examples
Aug 19 23:29:16 Finished examples                                              8m05s   3GB
Aug 19 23:29:18 Starting examples/compilation
Aug 20 02:23:15 Finished examples/compilation                               2h53m54s  12GB
Aug 20 02:23:17 Starting examples/compilation/proofs
Aug 20 02:26:47 Finished examples/compilation/proofs                           3m28s   3GB
Aug 20 02:26:49 Starting compiler/benchmarks
Aug 20 02:26:51 Finished compiler/benchmarks                                      0s   4MB
Aug 20 02:26:53 Starting translator/okasaki-examples
Aug 20 02:33:23 Finished translator/okasaki-examples                           6m27s   1GB
Aug 20 02:33:25 Starting translator/other-examples
Aug 20 02:39:54 Finished translator/other-examples                             6m26s 920MB
Aug 20 02:39:56 Starting compiler/parsing/tests
Aug 20 02:40:37 Finished compiler/parsing/tests                                  39s 353MB
Aug 20 02:40:39 Starting compiler/inference/tests
Aug 20 02:42:06 Finished compiler/inference/tests                              1m25s   1GB
Aug 20 02:42:08 Starting compiler/bootstrap/translation
Aug 20 05:22:25 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-f59f1264f77465a8321b6b7c9115f007db7d2bc1/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                                                                                                                              FAILED! <1>
 Saved theorem _____ "ra_state_stack_fupd_v_thm"
 Adding type :(, ) exc
 Saved definition __ "ML_MONADBASE_EXC_TYPE_def"
 Saved theorem _____ "ML_MONADBASE_EXC_TYPE_def"
 Saved theorem _____ "nsLookup_auto_env_72"
 Translating monadic run: reg_alloc_aux
 Defining local functions: 57 56 55 54 53 52 51 50 49 48 47 46 45 44 43 42 41 40 39 38 37 36 35 34 33 32 31 30 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1 
 error in quse /scratch/cakeml/regression/cakeml-435/compiler/bootstrap/translation/reg_allocProgScript.sml : HOL_ERR {message = "between beginning of frag 0 and end of frag 0:\nat Defn.prim_mk_defn:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"%%list%%list%%[]%%\", \"%%option%%option%%NONE%%\", \"%%reg_alloc%%tag%%Atemp%%\"", origin_function = "Define", origin_structure = "TotalDefn"}
 error in load reg_allocProgScript : HOL_ERR {message = "between beginning of frag 0 and end of frag 0:\nat Defn.prim_mk_defn:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"%%list%%list%%[]%%\", \"%%option%%option%%NONE%%\", \"%%reg_alloc%%tag%%Atemp%%\"", origin_function = "Define", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "between beginning of frag 0 and end of frag 0:\nat Defn.prim_mk_defn:\nat Defn.prim_mk_defn:\nSimple definition failed with message: Definition.new_definition: at Thm.new_specification:\nFree variables in rhs of definition: \"%%list%%list%%[]%%\", \"%%option%%option%%NONE%%\", \"%%reg_alloc%%tag%%Atemp%%\"", origin_function = "Define", origin_structure = "TotalDefn"}