Job 553

CakeML:e7a4dbd0299ce9557477364496dbe70ad38ef79e
  Setup nsLookup_conv for use in eval/compute. [Nov 08 14:47:19]
#551 (translator-alist-tree)
Merging into:3fa28c85c940b4edbbe79025687e39763ee2de56
  Fix data_to_word_bignumProof for revision to simp's caching of ARITH [Nov 08 10:34:25]
HOL:2a25e6b67662cae9559c5ab0952fb64ff5aabd1a
  Put variant regression test into tfl's selftest [Nov 08 00:58:09]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 08 21:54:13 Claimed job
Nov 08 21:54:32 Building HOL
Nov 08 22:04:38 Starting developers/bin
Nov 08 22:05:53 Finished developers/bin                                        1m14s 916MB
Nov 08 22:05:54 Starting semantics/ffi
Nov 08 22:06:37 Finished semantics/ffi                                           42s 374MB
Nov 08 22:06:38 Starting semantics
Nov 08 22:08:21 Finished semantics                                             1m42s 848MB
Nov 08 22:08:22 Starting semantics/proofs
Nov 08 22:11:29 Finished semantics/proofs                                      3m06s   1GB
Nov 08 22:11:30 Starting basis/pure
Nov 08 22:15:26 Finished basis/pure                                            3m55s 754MB
Nov 08 22:15:27 Starting translator
Nov 08 22:18:51 Finished translator                                            3m23s   1GB
Nov 08 22:18:51 Starting compiler/parsing
Nov 08 22:20:36 Finished compiler/parsing                                      1m43s   1GB
Nov 08 22:20:37 Starting characteristic
Nov 08 22:23:26 Finished characteristic                                        2m48s   1GB
Nov 08 22:23:27 Starting translator/monadic
Nov 08 22:25:05 Finished translator/monadic                                    1m37s   1GB
Nov 08 22:25:05 Starting basis
Nov 08 22:43:46 Finished basis                                                18m39s   2GB
Nov 08 22:43:47 Starting compiler/inference
Nov 08 22:45:39 Finished compiler/inference                                    1m51s 965MB
Nov 08 22:45:39 Starting compiler/backend/reg_alloc
Nov 08 22:46:32 Finished compiler/backend/reg_alloc                              52s 909MB
Nov 08 22:46:33 Starting compiler/backend/gc
Nov 08 22:55:16 Finished compiler/backend/gc                                   8m42s   1GB
Nov 08 22:55:17 Starting compiler/backend
Nov 08 22:55:20 Finished compiler/backend                                         2s  28MB
Nov 08 22:55:21 Starting compiler/encoders/asm
Nov 08 22:55:23 Finished compiler/encoders/asm                                    1s  16MB
Nov 08 22:55:23 Starting compiler/encoders/x64
Nov 08 22:56:21 Finished compiler/encoders/x64                                   56s 610MB
Nov 08 22:56:21 Starting compiler/encoders/arm6
Nov 08 22:58:16 Finished compiler/encoders/arm6                                1m53s   1GB
Nov 08 22:58:17 Starting compiler/encoders/arm8
Nov 08 22:58:45 Finished compiler/encoders/arm8                                  28s 490MB
Nov 08 22:58:46 Starting compiler/encoders/mips
Nov 08 22:59:50 Finished compiler/encoders/mips                                1m03s 922MB
Nov 08 22:59:51 Starting compiler/encoders/riscv
Nov 08 23:01:00 Finished compiler/encoders/riscv                               1m07s 679MB
Nov 08 23:01:00 Starting compiler/backend/x64
Nov 08 23:01:21 Finished compiler/backend/x64                                    20s   1GB
Nov 08 23:01:22 Starting compiler/backend/arm6
Nov 08 23:01:44 Finished compiler/backend/arm6                                   21s   1GB
Nov 08 23:01:45 Starting compiler/backend/arm8
Nov 08 23:02:06 Finished compiler/backend/arm8                                   20s   1GB
Nov 08 23:02:07 Starting compiler/backend/mips
Nov 08 23:02:28 Finished compiler/backend/mips                                   20s   1GB
Nov 08 23:02:29 Starting compiler/backend/riscv
Nov 08 23:02:50 Finished compiler/backend/riscv                                  20s   1GB
Nov 08 23:02:51 Starting compiler/parsing/proofs
Nov 08 23:09:27 Finished compiler/parsing/proofs                               6m35s   1GB
Nov 08 23:09:28 Starting compiler/inference/proofs
Nov 08 23:12:42 Finished compiler/inference/proofs                             3m13s   1GB
Nov 08 23:12:43 Starting compiler/backend/semantics
Nov 08 23:23:24 Finished compiler/backend/semantics                           10m40s   2GB
Nov 08 23:23:25 Starting compiler/backend/reg_alloc/proofs
Nov 08 23:26:20 Finished compiler/backend/reg_alloc/proofs                     2m54s 924MB
Nov 08 23:26:21 Starting compiler/backend/proofs
Nov 09 00:22:39 Finished compiler/backend/proofs                              56m16s   4GB
Nov 09 00:22:39 Starting compiler/encoders/x64/proofs
Nov 09 00:31:26 Finished compiler/encoders/x64/proofs                          8m46s   5GB
Nov 09 00:31:27 Starting compiler/encoders/arm6/proofs
Nov 09 00:39:50 Finished compiler/encoders/arm6/proofs                         8m22s   3GB
Nov 09 00:39:51 Starting compiler/encoders/arm8/proofs
Nov 09 00:45:51 Finished compiler/encoders/arm8/proofs                         5m59s 972MB
Nov 09 00:45:51 Starting compiler/encoders/mips/proofs
Nov 09 00:53:51 Finished compiler/encoders/mips/proofs                         7m59s   2GB
Nov 09 00:53:52 Starting compiler/encoders/riscv/proofs
Nov 09 01:02:35 Finished compiler/encoders/riscv/proofs                        8m42s 672MB
Nov 09 01:02:36 Starting compiler/backend/x64/proofs
Nov 09 01:02:58 Finished compiler/backend/x64/proofs                             21s 851MB
Nov 09 01:02:59 Starting compiler/backend/arm6/proofs
Nov 09 01:03:23 Finished compiler/backend/arm6/proofs                            23s 865MB
Nov 09 01:03:24 Starting compiler/backend/arm8/proofs
Nov 09 01:03:46 Finished compiler/backend/arm8/proofs                            21s   1GB
Nov 09 01:03:46 Starting compiler/backend/mips/proofs
Nov 09 01:04:10 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 09 01:04:10 Starting compiler/backend/riscv/proofs
Nov 09 01:04:33 Finished compiler/backend/riscv/proofs                           22s   1GB
Nov 09 01:04:34 Starting compiler/proofs
Nov 09 01:06:08 Finished compiler/proofs                                       1m33s   2GB
Nov 09 01:06:08 Starting candle/set-theory
Nov 09 01:06:45 Finished candle/set-theory                                       35s 624MB
Nov 09 01:06:46 Starting candle/syntax-lib
Nov 09 01:06:57 Finished candle/syntax-lib                                       10s 460MB
Nov 09 01:06:58 Starting candle/standard/syntax
Nov 09 01:08:42 Finished candle/standard/syntax                                1m43s 813MB
Nov 09 01:08:43 Starting candle/standard/semantics
Nov 09 01:10:14 Finished candle/standard/semantics                             1m30s   1GB
Nov 09 01:10:14 Starting candle/standard/monadic
Nov 09 01:12:06 Finished candle/standard/monadic                               1m51s   1GB
Nov 09 01:12:07 Starting candle/standard/ml_kernel
Nov 09 01:29:56 Finished candle/standard/ml_kernel                            17m47s   2GB
Nov 09 01:29:57 Starting candle/standard/opentheory
Nov 09 01:39:06 Finished candle/standard/opentheory                            9m08s   2GB
Nov 09 01:39:07 Starting candle/standard/opentheory/compilation
Nov 09 02:26:48 Finished candle/standard/opentheory/compilation               47m41s   7GB
Nov 09 02:26:49 Starting candle/standard/opentheory/compilation/proofs
Nov 09 02:27:39 Finished candle/standard/opentheory/compilation/proofs           49s   3GB
Nov 09 02:27:40 Starting characteristic/examples
Nov 09 02:29:20 Finished characteristic/examples                               1m39s   1GB
Nov 09 02:29:21 Starting tutorial/solutions
Nov 09 02:43:30 Finished tutorial/solutions                                   14m08s   6GB
Nov 09 02:43:31 Starting translator/monadic/examples
Nov 09 02:45:35 Finished translator/monadic/examples                           2m03s   1GB
Nov 09 02:45:35 Starting examples
Nov 09 02:52:19 Finished examples                                              6m43s   2GB
Nov 09 02:52:20 Starting examples/compilation
Nov 09 04:51:55 Finished examples/compilation                               1h59m34s  13GB
Nov 09 04:51:56 Starting examples/compilation/proofs
Nov 09 04:53:57 Finished examples/compilation/proofs                           2m00s   3GB
Nov 09 04:53:58 Starting compiler/benchmarks
Nov 09 04:53:59 Finished compiler/benchmarks                                      0s   4MB
Nov 09 04:53:59 Starting translator/okasaki-examples
Nov 09 04:58:19 Finished translator/okasaki-examples                           4m18s   1GB
Nov 09 04:58:19 Starting translator/other-examples
Nov 09 05:03:26 Finished translator/other-examples                             5m05s 879MB
Nov 09 05:03:27 Starting compiler/parsing/tests
Nov 09 05:04:06 Finished compiler/parsing/tests                                  38s 274MB
Nov 09 05:04:06 Starting compiler/inference/tests
Nov 09 05:10:26 Finished compiler/inference/tests                              6m18s   3GB
Nov 09 05:10:27 Starting compiler/bootstrap/translation
Nov 09 07:43:54 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ../../backend]0;Holmake: ../../backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-2a25e6b67662cae9559c5ab0952fb64ff5aabd1a/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ../../inference]0;Holmake: ../../inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: ../..]0;Holmake: ../..Working in $(CAKEMLDIR)/compiler
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofsWorking in $(CAKEMLDIR)/compiler/inference/proofs
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/bootstrap/translation
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                                                 FAILED! <1>
 Saved theorem _____ "nsLookup_auto_env_214_pfun_eqs"
 Saved theorem _____ "asm_asm_config_cjump_offset_fupd_v_thm"
 Translating asm_asm_config_loc_offset_fupd
 Adding repr thms for [auto_env_214].
 Saved theorem _____ "nsLookup_auto_env_215_pfun_eqs"
 Saved theorem _____ "asm_asm_config_loc_offset_fupd_v_thm"
 error in quse /home/cake/oven/regression/cakeml-553/compiler/bootstrap/translation/to_word64ProgScript.sml : HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
 error in load to_word64ProgScript : HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
 Failed translation: inst_select_exp
 Uncaught exception: HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
to_word32ProgTheory                                                    M-KILLED