Job 305

CakeML:20fcc03bb38a9470e04a987155e3a7f0d88b75aa
  Change >> to \\ in bvl_constProof [Apr 26 08:28:20]
#485 (better-constant-folding)
Merging into:a2189a6940aa40c618029d8663874246e88029d1
  Merge pull request #482 from zapashcanon/pp [Apr 23 05:19:11]
HOL:2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1
  Merge pull request #528 from AndreasLoow/theory-graph-svg-target-fix [Apr 27 01:40:56]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Apr 28 14:43:37 Claimed job
Apr 28 14:43:46 Building HOL
Apr 28 14:51:55 Starting developers/bin
Apr 28 14:52:32 Finished developers/bin                                          35s 922MB
Apr 28 14:52:32 Starting semantics/ffi
Apr 28 14:53:12 Finished semantics/ffi                                           38s 514MB
Apr 28 14:53:12 Starting semantics
Apr 28 14:54:36 Finished semantics                                             1m22s   1GB
Apr 28 14:54:36 Starting semantics/proofs
Apr 28 14:56:26 Finished semantics/proofs                                      1m48s   1GB
Apr 28 14:56:26 Starting basis/pure
Apr 28 14:59:55 Finished basis/pure                                            3m28s 723MB
Apr 28 14:59:56 Starting translator
Apr 28 15:03:44 Finished translator                                            3m47s 908MB
Apr 28 15:03:45 Starting compiler/parsing
Apr 28 15:05:12 Finished compiler/parsing                                      1m26s   2GB
Apr 28 15:05:12 Starting characteristic
Apr 28 15:07:34 Finished characteristic                                        2m21s   1GB
Apr 28 15:07:35 Starting basis
Apr 28 15:24:17 Finished basis                                                16m41s   2GB
Apr 28 15:24:18 Starting translator/monadic
Apr 28 15:24:20 Finished translator/monadic                                       1s  19MB
Apr 28 15:24:21 Starting compiler/inference
Apr 28 15:25:54 Finished compiler/inference                                    1m32s   1GB
Apr 28 15:25:55 Starting compiler/backend/reg_alloc
Apr 28 15:26:21 Finished compiler/backend/reg_alloc                              25s 805MB
Apr 28 15:26:21 Starting compiler/backend/gc
Apr 28 15:35:01 Finished compiler/backend/gc                                   8m39s   3GB
Apr 28 15:35:02 Starting compiler/backend
Apr 28 15:35:05 Finished compiler/backend                                         2s  16MB
Apr 28 15:35:06 Starting compiler/encoders/asm
Apr 28 15:35:07 Finished compiler/encoders/asm                                    0s  13MB
Apr 28 15:35:08 Starting compiler/encoders/x64
Apr 28 15:35:59 Finished compiler/encoders/x64                                   50s 587MB
Apr 28 15:35:59 Starting compiler/encoders/arm6
Apr 28 15:37:42 Finished compiler/encoders/arm6                                1m42s   1GB
Apr 28 15:37:43 Starting compiler/encoders/arm8
Apr 28 15:38:09 Finished compiler/encoders/arm8                                  25s 452MB
Apr 28 15:38:10 Starting compiler/encoders/mips
Apr 28 15:39:07 Finished compiler/encoders/mips                                  56s 839MB
Apr 28 15:39:08 Starting compiler/encoders/riscv
Apr 28 15:40:08 Finished compiler/encoders/riscv                                 59s 707MB
Apr 28 15:40:08 Starting compiler/backend/x64
Apr 28 15:40:27 Finished compiler/backend/x64                                    17s   1GB
Apr 28 15:40:27 Starting compiler/backend/arm6
Apr 28 15:40:48 Finished compiler/backend/arm6                                   20s   1GB
Apr 28 15:40:49 Starting compiler/backend/arm8
Apr 28 15:41:08 Finished compiler/backend/arm8                                   18s   1GB
Apr 28 15:41:09 Starting compiler/backend/mips
Apr 28 15:41:27 Finished compiler/backend/mips                                   17s 904MB
Apr 28 15:41:28 Starting compiler/backend/riscv
Apr 28 15:41:46 Finished compiler/backend/riscv                                  17s   1GB
Apr 28 15:41:47 Starting compiler/parsing/proofs
Apr 28 15:47:55 Finished compiler/parsing/proofs                               6m07s 780MB
Apr 28 15:47:56 Starting compiler/inference/proofs
Apr 28 15:50:14 Finished compiler/inference/proofs                             2m17s   1GB
Apr 28 15:50:14 Starting compiler/backend/semantics
Apr 28 16:01:41 Finished compiler/backend/semantics                           11m26s   2GB
Apr 28 16:01:42 Starting compiler/backend/reg_alloc/proofs
Apr 28 16:02:20 Finished compiler/backend/reg_alloc/proofs                       37s 611MB
Apr 28 16:02:20 Starting compiler/backend/proofs
Apr 28 16:38:23 Finished compiler/backend/proofs                              36m01s   4GB
Apr 28 16:38:23 Starting compiler/encoders/x64/proofs
Apr 28 16:45:41 Finished compiler/encoders/x64/proofs                          7m16s   4GB
Apr 28 16:45:41 Starting compiler/encoders/arm6/proofs
Apr 28 16:53:09 Finished compiler/encoders/arm6/proofs                         7m27s   2GB
Apr 28 16:53:10 Starting compiler/encoders/arm8/proofs
Apr 28 16:58:31 Finished compiler/encoders/arm8/proofs                         5m20s   1GB
Apr 28 16:58:32 Starting compiler/encoders/mips/proofs
Apr 28 17:05:48 Finished compiler/encoders/mips/proofs                         7m15s   2GB
Apr 28 17:05:49 Starting compiler/encoders/riscv/proofs
Apr 28 17:13:52 Finished compiler/encoders/riscv/proofs                        8m02s 781MB
Apr 28 17:13:53 Starting compiler/backend/x64/proofs
Apr 28 17:14:13 Finished compiler/backend/x64/proofs                             19s 798MB
Apr 28 17:14:13 Starting compiler/backend/arm6/proofs
Apr 28 17:14:35 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 28 17:14:36 Starting compiler/backend/arm8/proofs
Apr 28 17:14:56 Finished compiler/backend/arm8/proofs                            19s   1GB
Apr 28 17:14:57 Starting compiler/backend/mips/proofs
Apr 28 17:15:18 Finished compiler/backend/mips/proofs                            19s 938MB
Apr 28 17:15:18 Starting compiler/backend/riscv/proofs
Apr 28 17:15:39 Finished compiler/backend/riscv/proofs                           20s 820MB
Apr 28 17:15:39 Starting compiler/proofs
Apr 28 17:16:53 Finished compiler/proofs                                       1m12s   2GB
Apr 28 17:16:53 Starting candle/set-theory
Apr 28 17:17:49 Finished candle/set-theory                                       55s 613MB
Apr 28 17:17:50 Starting candle/syntax-lib
Apr 28 17:18:00 Finished candle/syntax-lib                                        9s 620MB
Apr 28 17:18:01 Starting candle/standard/syntax
Apr 28 17:19:34 Finished candle/standard/syntax                                1m32s 614MB
Apr 28 17:19:35 Starting candle/standard/semantics
Apr 28 17:20:55 Finished candle/standard/semantics                             1m19s 848MB
Apr 28 17:20:56 Starting candle/standard/monadic
Apr 28 17:22:19 Finished candle/standard/monadic                               1m23s 884MB
Apr 28 17:22:20 Starting candle/standard/ml_kernel
Apr 28 17:28:36 Finished candle/standard/ml_kernel                             6m15s   1GB
Apr 28 17:28:37 Starting candle/standard/opentheory
Apr 28 17:28:52 Finished candle/standard/opentheory                              14s 687MB
Apr 28 17:28:52 Starting characteristic/examples
Apr 28 17:30:19 Finished characteristic/examples                               1m26s   2GB
Apr 28 17:30:20 Starting tutorial/solutions
Apr 28 17:53:25 Finished tutorial/solutions                                   23m03s  17GB
Apr 28 17:53:25 Starting translator/monadic/examples
Apr 28 17:55:14 Finished translator/monadic/examples                           1m48s   2GB
Apr 28 17:55:15 Starting examples
Apr 28 18:00:42 Finished examples                                              5m27s   2GB
Apr 28 18:00:43 Starting examples/compilation
Apr 28 21:59:28 Finished examples/compilation                               3h58m43s  24GB
Apr 28 21:59:29 Starting examples/compilation/proofs
Apr 28 22:02:41 Finished examples/compilation/proofs                           3m11s   6GB
Apr 28 22:02:41 Starting compiler/benchmarks
Apr 28 22:02:43 Finished compiler/benchmarks                                      0s   4MB
Apr 28 22:02:43 Starting translator/okasaki-examples
Apr 28 22:06:15 Finished translator/okasaki-examples                           3m31s   1GB
Apr 28 22:06:15 Starting translator/other-examples
Apr 28 22:09:44 Finished translator/other-examples                             3m27s 685MB
Apr 28 22:09:44 Starting compiler/parsing/tests
Apr 28 22:10:08 Finished compiler/parsing/tests                                  22s 332MB
Apr 28 22:10:08 Starting compiler/bootstrap/translation
Apr 28 22:59:15 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/balanced_bst]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languages]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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/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/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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]0;Holmake: ../../encodersWorking in $(CAKEMLDIR)/compiler/encoders
]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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/unification/triangular]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-2fbcb3a3bbe4b2ceb132d0d764bf418b78b69ff1/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                                                   FAILED! <1>
              PMATCH_ROW (v69. case v69 of (v68,v67) => (v68,v67))
                (v72. case v72 of (v71,v70) => TRUE)
                (v75. case v75 of (v74,v73) => v76)]
           else v76))
 error in quse /home/cake/regression/cakeml-305/compiler/bootstrap/translation/to_dataProgScript.sml : HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
 error in load to_dataProgScript : HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "pmatch_hol2deep failed (prove_EvalPatBind failed)", origin_function = "failwith", origin_structure = "??"}
 Failed translation: SmartOp2
 Failed translation: SmartOp
 Failed translation: compile