Job 441

CakeML:67888c8644eea9202881e21dfa7c351539fc8a29
  Update EqualityType proof [Aug 21 13:10:21]
#512 (translator-module-ctors)
Merging into:e12dc542637af6649c97ecf8b12bc490db3840e1
  Fix more missing ERRs [Aug 19 08:01:39]
HOL:86ff704677ae31e64e05944c653f5f95e62afa1a
  Use UTF8 functions for fiddling with strings in testutil output [Aug 21 07:18:54]
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Aug 21 13:17:56 Claimed job
Aug 21 13:18:07 Building HOL
Aug 21 13:26:55 Starting developers/bin
Aug 21 13:27:30 Finished developers/bin                                          34s 911MB
Aug 21 13:27:31 Starting semantics/ffi
Aug 21 13:28:10 Finished semantics/ffi                                           38s 372MB
Aug 21 13:28:10 Starting semantics
Aug 21 13:29:36 Finished semantics                                             1m24s 913MB
Aug 21 13:29:37 Starting semantics/proofs
Aug 21 13:32:16 Finished semantics/proofs                                      2m38s   1GB
Aug 21 13:32:16 Starting basis/pure
Aug 21 13:35:48 Finished basis/pure                                            3m31s 717MB
Aug 21 13:35:49 Starting translator
Aug 21 13:36:54 Finished translator                                            1m04s 997MB
Aug 21 13:36:55 Starting compiler/parsing
Aug 21 13:38:29 Finished compiler/parsing                                      1m33s   3GB
Aug 21 13:38:29 Starting characteristic
Aug 21 13:40:51 Finished characteristic                                        2m21s   1GB
Aug 21 13:40:52 Starting translator/monadic
Aug 21 13:42:18 Finished translator/monadic                                    1m25s   1GB
Aug 21 13:42:18 Starting basis
Aug 21 13:58:09 Finished basis                                                15m49s   2GB
Aug 21 13:58:09 Starting compiler/inference
Aug 21 13:59:51 Finished compiler/inference                                    1m40s   1GB
Aug 21 13:59:52 Starting compiler/backend/reg_alloc
Aug 21 14:00:25 Finished compiler/backend/reg_alloc                              32s 893MB
Aug 21 14:00:26 Starting compiler/backend/gc
Aug 21 14:09:09 Finished compiler/backend/gc                                   8m42s   3GB
Aug 21 14:09:10 Starting compiler/backend
Aug 21 14:09:14 Finished compiler/backend                                         2s  16MB
Aug 21 14:09:14 Starting compiler/encoders/asm
Aug 21 14:09:16 Finished compiler/encoders/asm                                    1s  15MB
Aug 21 14:09:17 Starting compiler/encoders/x64
Aug 21 14:10:09 Finished compiler/encoders/x64                                   51s 632MB
Aug 21 14:10:09 Starting compiler/encoders/arm6
Aug 21 14:11:52 Finished compiler/encoders/arm6                                1m42s   1GB
Aug 21 14:11:53 Starting compiler/encoders/arm8
Aug 21 14:12:20 Finished compiler/encoders/arm8                                  25s 471MB
Aug 21 14:12:20 Starting compiler/encoders/mips
Aug 21 14:13:19 Finished compiler/encoders/mips                                  57s 822MB
Aug 21 14:13:19 Starting compiler/encoders/riscv
Aug 21 14:14:20 Finished compiler/encoders/riscv                               1m00s 776MB
Aug 21 14:14:21 Starting compiler/backend/x64
Aug 21 14:14:39 Finished compiler/backend/x64                                    17s   1GB
Aug 21 14:14:39 Starting compiler/backend/arm6
Aug 21 14:14:59 Finished compiler/backend/arm6                                   19s   1GB
Aug 21 14:14:59 Starting compiler/backend/arm8
Aug 21 14:15:18 Finished compiler/backend/arm8                                   18s   1GB
Aug 21 14:15:19 Starting compiler/backend/mips
Aug 21 14:15:38 Finished compiler/backend/mips                                   18s   1GB
Aug 21 14:15:39 Starting compiler/backend/riscv
Aug 21 14:15:59 Finished compiler/backend/riscv                                  18s   1GB
Aug 21 14:15:59 Starting compiler/parsing/proofs
Aug 21 14:21:56 Finished compiler/parsing/proofs                               5m56s   1GB
Aug 21 14:21:57 Starting compiler/inference/proofs
Aug 21 14:24:45 Finished compiler/inference/proofs                             2m47s   1GB
Aug 21 14:24:46 Starting compiler/backend/semantics
Aug 21 14:33:41 Finished compiler/backend/semantics                            8m54s   2GB
Aug 21 14:33:42 Starting compiler/backend/reg_alloc/proofs
Aug 21 14:34:30 Finished compiler/backend/reg_alloc/proofs                       47s 539MB
Aug 21 14:34:31 Starting compiler/backend/proofs
Aug 21 15:09:46 Finished compiler/backend/proofs                              35m14s   3GB
Aug 21 15:09:47 Starting compiler/encoders/x64/proofs
Aug 21 15:17:07 Finished compiler/encoders/x64/proofs                          7m19s   4GB
Aug 21 15:17:08 Starting compiler/encoders/arm6/proofs
Aug 21 15:24:20 Finished compiler/encoders/arm6/proofs                         7m12s   3GB
Aug 21 15:24:21 Starting compiler/encoders/arm8/proofs
Aug 21 15:29:40 Finished compiler/encoders/arm8/proofs                         5m18s 931MB
Aug 21 15:29:41 Starting compiler/encoders/mips/proofs
Aug 21 15:36:52 Finished compiler/encoders/mips/proofs                         7m10s   2GB
Aug 21 15:36:53 Starting compiler/encoders/riscv/proofs
Aug 21 15:44:58 Finished compiler/encoders/riscv/proofs                        8m03s 771MB
Aug 21 15:44:58 Starting compiler/backend/x64/proofs
Aug 21 15:45:19 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 21 15:45:19 Starting compiler/backend/arm6/proofs
Aug 21 15:45:42 Finished compiler/backend/arm6/proofs                            21s 825MB
Aug 21 15:45:42 Starting compiler/backend/arm8/proofs
Aug 21 15:46:04 Finished compiler/backend/arm8/proofs                            20s 842MB
Aug 21 15:46:05 Starting compiler/backend/mips/proofs
Aug 21 15:46:27 Finished compiler/backend/mips/proofs                            21s   1GB
Aug 21 15:46:27 Starting compiler/backend/riscv/proofs
Aug 21 15:46:48 Finished compiler/backend/riscv/proofs                           20s   1GB
Aug 21 15:46:49 Starting compiler/proofs
Aug 21 15:48:06 Finished compiler/proofs                                       1m16s   2GB
Aug 21 15:48:07 Starting candle/set-theory
Aug 21 15:48:39 Finished candle/set-theory                                       30s 604MB
Aug 21 15:48:39 Starting candle/syntax-lib
Aug 21 15:48:50 Finished candle/syntax-lib                                       10s 661MB
Aug 21 15:48:51 Starting candle/standard/syntax
Aug 21 15:50:24 Finished candle/standard/syntax                                1m32s 620MB
Aug 21 15:50:24 Starting candle/standard/semantics
Aug 21 15:51:44 Finished candle/standard/semantics                             1m19s   1GB
Aug 21 15:51:45 Starting candle/standard/monadic
Aug 21 15:53:11 Finished candle/standard/monadic                               1m25s 973MB
Aug 21 15:53:12 Starting candle/standard/ml_kernel
Aug 21 15:56:29 Finished candle/standard/ml_kernel                             3m16s   2GB
Aug 21 15:56:30 Starting candle/standard/opentheory
Aug 21 15:56:46 Finished candle/standard/opentheory                              15s 618MB
Aug 21 15:56:47 Starting characteristic/examples
Aug 21 15:58:20 Finished characteristic/examples                               1m32s   2GB
Aug 21 15:58:21 Starting tutorial/solutions
Aug 21 16:11:40 Finished tutorial/solutions                                   13m17s   6GB
Aug 21 16:11:41 Starting translator/monadic/examples
Aug 21 16:13:24 Finished translator/monadic/examples                           1m42s   2GB
Aug 21 16:13:24 Starting examples
Aug 21 16:18:46 Finished examples                                              5m21s   4GB
Aug 21 16:18:47 Starting examples/compilation
Aug 21 18:13:23 Finished examples/compilation                               1h54m35s   9GB
Aug 21 18:13:24 Starting examples/compilation/proofs
Aug 21 18:15:13 Finished examples/compilation/proofs                           1m48s   2GB
Aug 21 18:15:14 Starting compiler/benchmarks
Aug 21 18:15:15 Finished compiler/benchmarks                                      0s   4MB
Aug 21 18:15:16 Starting translator/okasaki-examples
Aug 21 18:18:42 Finished translator/okasaki-examples                           3m25s   1GB
Aug 21 18:18:43 Starting translator/other-examples
Aug 21 18:22:12 Finished translator/other-examples                             3m28s 750MB
Aug 21 18:22:13 Starting compiler/parsing/tests
Aug 21 18:22:38 Finished compiler/parsing/tests                                  25s 311MB
Aug 21 18:22:39 Starting compiler/inference/tests
Aug 21 18:23:32 Finished compiler/inference/tests                                52s   1GB
Aug 21 18:23:33 Starting compiler/bootstrap/translation
Aug 21 21:10:46 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/common]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/hoare-triple]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/common]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/lib]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/mips/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/x64/model]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/balanced_bst]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/multiword]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/decompiler]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/mips/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/l3-machine-code/x64/step]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/unification/triangular/first-order]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/unification/triangular]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/examples/unification/triangular/first-order]0;Holmake: ~/regression_2/HOL-86ff704677ae31e64e05944c653f5f95e62afa1a/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                                                                                                            FAILED! <1>
 Saved induction ___ "GRAMMAR_PARSETREE_TYPE_ind"
 Saved theorem _____ "GRAMMAR_PARSETREE_TYPE_def"
 Saved theorem _____ "nsLookup_auto_env_1"
 Adding type :MMLnonT
 Saved definition __ "GRAM_MMLNONT_TYPE_def"
 Saved theorem _____ "GRAM_MMLNONT_TYPE_def"
 Saved theorem _____ "nsLookup_auto_env_2"
 error in quse /home/cake/regression_2/cakeml-441/compiler/bootstrap/translation/parserProgScript.sml : HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}
 error in load parserProgScript : HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}
 Uncaught exception: HOL_ERR {message = "unsatisfied predicate", origin_function = "first", origin_structure = "Lib"}