Job 602

CakeML:8be407f160d23d58a787b3ff5149961930ec5168
  Use set_grammar_ancestry to solve parsing issue in VectorProg [Dec 02 01:31:12]
HOL:393360fdb468d3686efdee941152538a9d59d35d
  Move some theorems into pred_setTheory from CakeML [Dec 01 10:59:28]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Dec 02 05:05:17 Claimed job
Dec 02 05:07:07 Building HOL
Dec 02 05:14:47 Starting developers
Dec 02 05:14:48 Finished developers                                               0s  32MB
Dec 02 05:14:48 Starting developers/bin
Dec 02 05:15:25 Finished developers/bin                                          35s 202MB
Dec 02 05:15:26 Starting semantics/ffi
Dec 02 05:16:02 Finished semantics/ffi                                           35s 483MB
Dec 02 05:16:02 Starting semantics
Dec 02 05:17:37 Finished semantics                                             1m33s 896MB
Dec 02 05:17:38 Starting semantics/proofs
Dec 02 05:20:41 Finished semantics/proofs                                      3m03s   1GB
Dec 02 05:20:42 Starting basis/pure
Dec 02 05:24:26 Finished basis/pure                                            3m43s 636MB
Dec 02 05:24:27 Starting translator
Dec 02 05:25:42 Finished translator                                            1m14s 905MB
Dec 02 05:25:43 Starting compiler/parsing
Dec 02 05:27:11 Finished compiler/parsing                                      1m26s   2GB
Dec 02 05:27:11 Starting characteristic
Dec 02 05:29:47 Finished characteristic                                        2m34s   1GB
Dec 02 05:29:47 Starting translator/monadic
Dec 02 05:31:17 Finished translator/monadic                                    1m28s   1GB
Dec 02 05:31:18 Starting basis
Dec 02 05:48:12 Finished basis                                                16m53s   2GB
Dec 02 05:48:13 Starting compiler/inference
Dec 02 05:49:58 Finished compiler/inference                                    1m44s   1GB
Dec 02 05:49:59 Starting compiler/backend/reg_alloc
Dec 02 05:50:48 Finished compiler/backend/reg_alloc                              47s   1GB
Dec 02 05:50:48 Starting compiler/backend/gc
Dec 03 04:30:09 Resuming compiler/backend/gc
Dec 03 04:34:59 Finished compiler/backend/gc                                   4m48s   1GB
Dec 03 04:34:59 Starting compiler/backend
Dec 03 04:35:01 Finished compiler/backend                                         1s  17MB
Dec 03 04:35:02 Starting compiler/encoders/asm
Dec 03 04:35:03 Finished compiler/encoders/asm                                    0s  16MB
Dec 03 04:35:04 Starting compiler/encoders/x64
Dec 03 04:35:59 Finished compiler/encoders/x64                                   54s 577MB
Dec 03 04:36:00 Starting compiler/encoders/arm6
Dec 03 04:37:45 Finished compiler/encoders/arm6                                1m44s   1GB
Dec 03 04:37:46 Starting compiler/encoders/arm8
Dec 03 04:38:11 Finished compiler/encoders/arm8                                  24s 454MB
Dec 03 04:38:12 Starting compiler/encoders/mips
Dec 03 04:39:11 Finished compiler/encoders/mips                                  57s 602MB
Dec 03 04:39:11 Starting compiler/encoders/riscv
Dec 03 04:40:15 Finished compiler/encoders/riscv                               1m03s 894MB
Dec 03 04:40:16 Starting compiler/encoders/ag32
Dec 03 04:40:34 Finished compiler/encoders/ag32                                  17s 786MB
Dec 03 04:40:35 Starting compiler/backend/x64
Dec 03 04:40:53 Finished compiler/backend/x64                                    17s   1GB
Dec 03 04:40:54 Starting compiler/backend/arm6
Dec 03 04:41:13 Finished compiler/backend/arm6                                   19s   1GB
Dec 03 04:41:14 Starting compiler/backend/arm8
Dec 03 04:41:32 Finished compiler/backend/arm8                                   16s 869MB
Dec 03 04:41:33 Starting compiler/backend/mips
Dec 03 04:41:52 Finished compiler/backend/mips                                   18s   1GB
Dec 03 04:41:52 Starting compiler/backend/riscv
Dec 03 04:42:13 Finished compiler/backend/riscv                                  19s   1GB
Dec 03 04:42:14 Starting compiler/backend/ag32
Dec 03 04:43:35 Finished compiler/backend/ag32                                 1m20s   1GB
Dec 03 04:43:36 Starting compiler/parsing/proofs
Dec 03 04:49:52 Finished compiler/parsing/proofs                               6m15s   1GB
Dec 03 04:49:53 Starting compiler/inference/proofs
Dec 03 04:53:00 Finished compiler/inference/proofs                             3m06s 997MB
Dec 03 04:53:01 Starting compiler/backend/semantics
Dec 03 05:04:11 Finished compiler/backend/semantics                           11m09s   1GB
Dec 03 05:04:12 Starting compiler/backend/reg_alloc/proofs
Dec 03 05:07:02 Finished compiler/backend/reg_alloc/proofs                     2m49s 505MB
Dec 03 05:07:02 Starting compiler/backend/proofs
Dec 03 05:57:54 Finished compiler/backend/proofs                              50m50s   3GB
Dec 03 05:57:55 Starting compiler/encoders/x64/proofs
Dec 03 06:08:54 Finished compiler/encoders/x64/proofs                         10m58s   5GB
Dec 03 06:08:55 Starting compiler/encoders/arm6/proofs
Dec 03 06:24:36 Finished compiler/encoders/arm6/proofs                        15m40s   3GB
Dec 03 06:24:37 Starting compiler/encoders/arm8/proofs
Dec 03 06:31:07 Finished compiler/encoders/arm8/proofs                         6m28s 980MB
Dec 03 06:31:08 Starting compiler/encoders/mips/proofs
Dec 03 06:42:18 Finished compiler/encoders/mips/proofs                        11m10s   2GB
Dec 03 06:42:19 Starting compiler/encoders/riscv/proofs
Dec 03 06:50:44 Finished compiler/encoders/riscv/proofs                        8m23s 826MB
Dec 03 06:50:45 Starting compiler/encoders/ag32/proofs
Dec 03 06:53:40 Finished compiler/encoders/ag32/proofs                         2m54s 615MB
Dec 03 06:53:40 Starting compiler/backend/x64/proofs
Dec 03 06:54:00 Finished compiler/backend/x64/proofs                             18s   1GB
Dec 03 06:54:01 Starting compiler/backend/arm6/proofs
Dec 03 06:54:22 Finished compiler/backend/arm6/proofs                            20s   1GB
Dec 03 06:54:23 Starting compiler/backend/arm8/proofs
Dec 03 06:54:42 Finished compiler/backend/arm8/proofs                            18s   1GB
Dec 03 06:54:43 Starting compiler/backend/mips/proofs
Dec 03 06:55:03 Finished compiler/backend/mips/proofs                            19s   1GB
Dec 03 06:55:04 Starting compiler/backend/riscv/proofs
Dec 03 06:55:24 Finished compiler/backend/riscv/proofs                           19s   1GB
Dec 03 06:55:25 Starting compiler/backend/ag32/proofs
Dec 03 07:05:30 Finished compiler/backend/ag32/proofs                         10m02s   2GB
Dec 03 07:05:30 Starting compiler/proofs
Dec 03 07:06:54 Finished compiler/proofs                                       1m22s   1GB
Dec 03 07:06:54 Starting candle/set-theory
Dec 03 07:07:25 Finished candle/set-theory                                       30s 622MB
Dec 03 07:07:26 Starting candle/syntax-lib
Dec 03 07:07:36 Finished candle/syntax-lib                                        9s 488MB
Dec 03 07:07:37 Starting candle/standard/syntax
Dec 03 07:09:13 Finished candle/standard/syntax                                1m35s 600MB
Dec 03 07:09:14 Starting candle/standard/semantics
Dec 03 07:10:35 Finished candle/standard/semantics                             1m20s 794MB
Dec 03 07:10:36 Starting candle/standard/monadic
Dec 03 07:12:14 Finished candle/standard/monadic                               1m36s 774MB
Dec 03 07:12:14 Starting candle/standard/ml_kernel
Dec 03 07:27:51 Finished candle/standard/ml_kernel                            15m36s   3GB
Dec 03 07:27:52 Starting candle/standard/opentheory
Dec 03 07:36:16 Finished candle/standard/opentheory                            8m23s   2GB
Dec 03 07:36:17 Starting candle/standard/opentheory/compilation
Dec 03 08:08:14 Finished candle/standard/opentheory/compilation               31m55s  22GB
Dec 03 08:08:14 Starting candle/standard/opentheory/compilation/proofs
Dec 03 08:08:50 Finished candle/standard/opentheory/compilation/proofs           34s   5GB
Dec 03 08:08:50 Starting characteristic/examples
Dec 03 08:10:24 Finished characteristic/examples                               1m32s   1GB
Dec 03 08:10:24 Starting tutorial/solutions
Dec 03 08:24:20 Finished tutorial/solutions                                   13m55s   5GB
Dec 03 08:24:21 Starting translator/monadic/examples
Dec 03 08:26:26 Finished translator/monadic/examples                           2m04s   2GB
Dec 03 08:26:27 Starting examples
Dec 03 08:34:22 Finished examples                                              7m53s   2GB
Dec 03 08:34:22 Starting examples/compilation/x64
Dec 03 10:37:06 Finished examples/compilation/x64                           2h02m42s  10GB
Dec 03 10:37:07 Starting examples/compilation/x64/proofs
Dec 03 10:39:00 Finished examples/compilation/x64/proofs                       1m52s   3GB
Dec 03 10:39:01 Starting examples/compilation/ag32
Dec 03 11:05:48 Finished examples/compilation/ag32                            26m45s   3GB
Dec 03 11:05:49 Starting examples/compilation/ag32/proofs
Dec 03 11:06:15 Finished examples/compilation/ag32/proofs                        25s   2GB
Dec 03 11:06:16 Starting compiler/benchmarks
Dec 03 11:06:16 Finished compiler/benchmarks                                      0s   4MB
Dec 03 11:06:17 Starting translator/okasaki-examples
Dec 03 11:09:47 Finished translator/okasaki-examples                           3m28s   1GB
Dec 03 11:09:48 Starting translator/other-examples
Dec 03 11:12:58 Finished translator/other-examples                             3m09s 796MB
Dec 03 11:12:59 Starting compiler/parsing/tests
Dec 03 11:13:25 Finished compiler/parsing/tests                                  24s 283MB
Dec 03 11:13:25 Starting compiler/inference/tests
Dec 03 11:17:28 Finished compiler/inference/tests                              4m01s   4GB
Dec 03 11:17:29 Starting compiler/bootstrap/translation
Dec 03 12:54:51 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/balanced_bst]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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 $(CAKEMLDIR)/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: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../characteristic]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/monad_base]0;Holmake: ../../../translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/ag32]0;Holmake: ../../encoders/ag32]0;Holmake: ../../encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ../../backend/ag32]0;Holmake: ../../backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/unification/triangular]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-393360fdb468d3686efdee941152538a9d59d35d/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
Starting work on README.md
README.md                                                                                                  OK
heap                                                                                                       OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                          OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                            OK
Starting work on parserProgTheory
parserProgTheory                                                                                           OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                        OK
Starting work on inferProgTheory
inferProgTheory                                                                                            OK
Starting work on explorerProgTheory
explorerProgTheory                                  OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                               OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word32ProgTheory                        FAILED! <1>
 Saved theorem _____ "data_to_word_get_gen_size_v_thm"
 Translating data_to_word_tag_mask
 Adding nsLookup representation thms for [auto_env_26]
 Saved theorem _____ "nsLookup_auto_env_27_pfun_eqs"
 Saved theorem _____ "data_to_word_tag_mask_v_thm"
 Translating data_to_word_encode_header
 Adding nsLookup representation thms for [auto_env_27]
 error in quse /home/myreen/regression/cakeml-602/compiler/bootstrap/translation/to_word32ProgScript.sml : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
 error in load to_word32ProgScript : HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
 Uncaught exception: HOL_ERR {message = "not a comb", origin_function = "RATOR_CONV", origin_structure = "Conv"}
to_word64ProgTheory                           M-KILLED