Job 835

CakeML:5cf686ad5abbd742bc3350cd7bcb954f975a3fd3
  Fix {wordcount,sort,hello}Proof [May 03 10:45:55]
#629 (vstte18)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:d3953f88ec91360cb865ace99ebbb7b8028807e2
  Emacs-mode: allow goal selection between  [May 02 02:23:56]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 03 14:39:09 Claimed job
May 03 14:39:15 Building HOL
May 03 14:46:59 Starting developers
May 03 14:46:59 Finished developers                                               0s  34MB
May 03 14:46:59 Starting developers/bin
May 03 14:47:03 Finished developers/bin                                           2s 144MB
May 03 14:47:03 Starting semantics/ffi
May 03 14:47:37 Finished semantics/ffi                                           33s 381MB
May 03 14:47:37 Starting semantics
May 03 14:49:08 Finished semantics                                             1m30s   1GB
May 03 14:49:08 Starting semantics/proofs
May 03 14:52:01 Finished semantics/proofs                                      2m52s 883MB
May 03 14:52:02 Starting basis/pure
May 03 14:55:32 Finished basis/pure                                            3m29s 820MB
May 03 14:55:32 Starting translator
May 03 14:57:09 Finished translator                                            1m36s   1GB
May 03 14:57:09 Starting compiler/parsing
May 03 14:58:06 Finished compiler/parsing                                        56s   2GB
May 03 14:58:07 Starting characteristic
May 03 15:03:11 Finished characteristic                                        5m04s   2GB
May 03 15:03:12 Starting translator/monadic
May 03 15:04:36 Finished translator/monadic                                    1m23s   1GB
May 03 15:04:36 Starting basis
May 03 15:21:25 Finished basis                                                16m48s   2GB
May 03 15:21:25 Starting compiler/inference
May 03 15:23:10 Finished compiler/inference                                    1m44s   1GB
May 03 15:23:10 Starting compiler/backend/reg_alloc
May 03 15:24:08 Finished compiler/backend/reg_alloc                              57s   1GB
May 03 15:24:08 Starting compiler/backend/gc
May 03 15:32:59 Finished compiler/backend/gc                                   8m49s   2GB
May 03 15:32:59 Starting compiler/backend
May 03 15:33:00 Finished compiler/backend                                         0s  42MB
May 03 15:33:00 Starting compiler/encoders/asm
May 03 15:33:01 Finished compiler/encoders/asm                                    0s  32MB
May 03 15:33:01 Starting compiler/encoders/x64
May 03 15:33:57 Finished compiler/encoders/x64                                   55s 701MB
May 03 15:33:57 Starting compiler/encoders/arm6
May 03 15:35:33 Finished compiler/encoders/arm6                                1m35s   1GB
May 03 15:35:34 Starting compiler/encoders/arm8
May 03 15:36:02 Finished compiler/encoders/arm8                                  28s 520MB
May 03 15:36:03 Starting compiler/encoders/mips
May 03 15:37:07 Finished compiler/encoders/mips                                1m03s   1GB
May 03 15:37:07 Starting compiler/encoders/riscv
May 03 15:38:23 Finished compiler/encoders/riscv                               1m16s 810MB
May 03 15:38:24 Starting compiler/encoders/ag32
May 03 15:38:38 Finished compiler/encoders/ag32                                  14s 657MB
May 03 15:38:39 Starting compiler/backend/x64
May 03 15:38:53 Finished compiler/backend/x64                                    14s 888MB
May 03 15:38:53 Starting compiler/backend/arm6
May 03 15:39:11 Finished compiler/backend/arm6                                   17s   1GB
May 03 15:39:11 Starting compiler/backend/arm8
May 03 15:39:28 Finished compiler/backend/arm8                                   16s   1GB
May 03 15:39:28 Starting compiler/backend/mips
May 03 15:39:43 Finished compiler/backend/mips                                   14s 826MB
May 03 15:39:44 Starting compiler/backend/riscv
May 03 15:40:00 Finished compiler/backend/riscv                                  16s   1GB
May 03 15:40:00 Starting compiler/backend/ag32
May 03 15:41:06 Finished compiler/backend/ag32                                 1m05s   1GB
May 03 15:41:06 Starting compiler/parsing/proofs
May 03 15:46:35 Finished compiler/parsing/proofs                               5m28s 800MB
May 03 15:46:35 Starting compiler/inference/proofs
May 03 15:49:11 Finished compiler/inference/proofs                             2m36s   1GB
May 03 15:49:12 Starting compiler/backend/semantics
May 03 15:56:06 Finished compiler/backend/semantics                            6m54s   1GB
May 03 15:56:06 Starting compiler/backend/reg_alloc/proofs
May 03 15:59:16 Finished compiler/backend/reg_alloc/proofs                     3m09s 700MB
May 03 15:59:16 Starting compiler/backend/proofs
May 03 16:36:38 Finished compiler/backend/proofs                              37m21s   3GB
May 03 16:36:38 Starting compiler/encoders/x64/proofs
May 03 16:46:37 Finished compiler/encoders/x64/proofs                          9m58s   5GB
May 03 16:46:38 Starting compiler/encoders/arm6/proofs
May 03 17:00:09 Finished compiler/encoders/arm6/proofs                        13m31s   3GB
May 03 17:00:09 Starting compiler/encoders/arm8/proofs
May 03 17:06:54 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
May 03 17:06:54 Starting compiler/encoders/mips/proofs
May 03 17:17:06 Finished compiler/encoders/mips/proofs                        10m11s   1GB
May 03 17:17:06 Starting compiler/encoders/riscv/proofs
May 03 17:25:23 Finished compiler/encoders/riscv/proofs                        8m16s   1GB
May 03 17:25:23 Starting compiler/encoders/ag32/proofs
May 03 17:27:50 Finished compiler/encoders/ag32/proofs                         2m26s 682MB
May 03 17:27:50 Starting compiler/backend/x64/proofs
May 03 17:28:06 Finished compiler/backend/x64/proofs                             15s 978MB
May 03 17:28:07 Starting compiler/backend/arm6/proofs
May 03 17:28:25 Finished compiler/backend/arm6/proofs                            18s   1GB
May 03 17:28:26 Starting compiler/backend/arm8/proofs
May 03 17:28:42 Finished compiler/backend/arm8/proofs                            16s   1GB
May 03 17:28:42 Starting compiler/backend/mips/proofs
May 03 17:28:59 Finished compiler/backend/mips/proofs                            16s   1GB
May 03 17:28:59 Starting compiler/backend/riscv/proofs
May 03 17:29:16 Finished compiler/backend/riscv/proofs                           16s   1GB
May 03 17:29:16 Starting compiler/backend/ag32/proofs
May 03 17:38:11 Finished compiler/backend/ag32/proofs                          8m54s   2GB
May 03 17:38:12 Starting compiler/proofs
May 03 17:39:30 Finished compiler/proofs                                       1m18s   2GB
May 03 17:39:31 Starting candle/set-theory
May 03 17:39:55 Finished candle/set-theory                                       24s 722MB
May 03 17:39:55 Starting candle/syntax-lib
May 03 17:40:04 Finished candle/syntax-lib                                        8s 661MB
May 03 17:40:05 Starting candle/standard/syntax
May 03 17:41:45 Finished candle/standard/syntax                                1m40s 901MB
May 03 17:41:45 Starting candle/standard/semantics
May 03 17:43:18 Finished candle/standard/semantics                             1m32s   1GB
May 03 17:43:18 Starting candle/standard/monadic
May 03 17:44:51 Finished candle/standard/monadic                               1m32s   1GB
May 03 17:44:51 Starting candle/standard/ml_kernel
May 03 17:48:40 Finished candle/standard/ml_kernel                             3m48s   3GB
May 03 17:48:40 Starting candle/standard/opentheory
May 03 17:56:58 Finished candle/standard/opentheory                            8m18s   3GB
May 03 17:56:59 Starting candle/standard/opentheory/compilation
May 03 18:25:32 Finished candle/standard/opentheory/compilation               28m32s  22GB
May 03 18:25:32 Starting candle/standard/opentheory/compilation/proofs
May 03 18:26:11 Finished candle/standard/opentheory/compilation/proofs           39s   2GB
May 03 18:26:12 Starting characteristic/examples
May 03 18:27:36 Finished characteristic/examples                               1m23s   2GB
May 03 18:27:36 Starting tutorial/solutions
May 03 18:40:20 Finished tutorial/solutions                                   12m43s   6GB
May 03 18:40:20 Starting translator/monadic/examples
May 03 18:43:09 Finished translator/monadic/examples                           2m48s   2GB
May 03 18:43:10 Starting examples
May 03 18:51:50 Finished examples                                              8m40s   3GB
May 03 18:51:50 Starting examples/compilation/x64
May 03 20:53:39 Finished examples/compilation/x64                           2h01m47s  19GB
May 03 20:53:39 Starting examples/compilation/x64/proofs
May 03 20:55:01 Finished examples/compilation/x64/proofs                       1m21s   3GB
May 03 20:55:01 Starting examples/compilation/ag32
May 03 21:22:23 Finished examples/compilation/ag32                            27m21s   6GB
May 03 21:22:23 Starting examples/compilation/ag32/proofs
May 03 21:23:08 Finished examples/compilation/ag32/proofs                        44s   2GB
May 03 21:23:08 Starting translator/okasaki-examples
May 03 21:27:13 Finished translator/okasaki-examples                           4m03s   1GB
May 03 21:27:13 Starting translator/other-examples
May 03 21:30:29 Finished translator/other-examples                             3m15s   1GB
May 03 21:30:29 Starting compiler/parsing/tests
May 03 21:30:53 Finished compiler/parsing/tests                                  24s 478MB
May 03 21:30:54 Starting compiler/inference/tests
May 03 21:34:58 Finished compiler/inference/tests                              4m04s   4GB
May 03 21:34:58 Starting compiler/bootstrap/translation
May 04 00:01:14 Finished compiler/bootstrap/translation                     2h26m14s  40GB
May 04 00:01:14 Starting unverified/sexpr-bootstrap/x64/64
May 04 00:08:16 Finished unverified/sexpr-bootstrap/x64/64                     7m02s   3GB
May 04 00:08:17 Starting unverified/sexpr-bootstrap/x64/32
May 04 00:12:34 Finished unverified/sexpr-bootstrap/x64/32                     4m16s   7GB
May 04 00:12:34 Starting compiler/benchmarks
May 04 00:49:13 Finished compiler/benchmarks                                  36m38s   2GB
May 04 00:49:13 Starting compiler/bootstrap/compilation/x64/64
May 04 10:45:22 Finished compiler/bootstrap/compilation/x64/64              9h56m08s  64GB
May 04 10:45:22 Starting compiler/bootstrap/compilation/x64/64/proofs
May 04 10:48:42 Finished compiler/bootstrap/compilation/x64/64/proofs          3m19s   5GB
May 04 10:48:42 Starting compiler/bootstrap/compilation/x64/32
May 04 20:53:04 Finished compiler/bootstrap/compilation/x64/32             10h04m21s  64GB
May 04 20:53:05 Starting compiler/bootstrap/compilation/x64/32/proofs
May 04 20:55:51 Finished compiler/bootstrap/compilation/x64/32/proofs          2m46s   5GB
May 04 20:55:52 Starting compiler/bootstrap/compilation/ag32/32
May 05 06:22:14 Finished compiler/bootstrap/compilation/ag32/32             9h26m21s  64GB
May 05 06:22:14 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 05 06:43:53 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ~/regression/cakeml-835/basis]0;Holmake: ~/regression/cakeml-835/basis/pure]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/balanced_bst]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-835/basis/pure]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-835/basis/pure]0;Holmake: ~/regression/cakeml-835/misc]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-835/misc]0;Holmake: ~/regression/cakeml-835/developers]0;Holmake: ~/regression/cakeml-835/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-835/misc]0;Holmake: ~/regression/cakeml-835/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-835/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-835/misc]0;Holmake: ~/regression/cakeml-835/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-835/basis/pure]0;Holmake: ~/regression/cakeml-835/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-835/basis]0;Holmake: ~/regression/cakeml-835/characteristic]0;Holmake: ~/regression/cakeml-835/compiler/parsing]0;Holmake: ~/regression/cakeml-835/semantics]0;Holmake: ~/regression/cakeml-835/semantics/ffi]0;Holmake: ~/regression/cakeml-835/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-835/semantics]0;Holmake: ~/regression/cakeml-835/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-835/compiler/parsing]0;Holmake: ~/regression/cakeml-835/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-835/characteristic]0;Holmake: ~/regression/cakeml-835/semantics/proofs]0;Holmake: ~/regression/cakeml-835/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-835/characteristic]0;Holmake: ~/regression/cakeml-835/translator]0;Holmake: ~/regression/cakeml-835/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-835/characteristic]0;Holmake: ~/regression/cakeml-835/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-835/basis]0;Holmake: ~/regression/cakeml-835/translator/monadic]0;Holmake: ~/regression/cakeml-835/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-835/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-835/translator/monadic]0;Holmake: ~/regression/cakeml-835/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-835/basis]0;Holmake: ~/regression/cakeml-835/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/ag32]0;Holmake: ../../../../../backend]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../../../../backend]0;Holmake: ../../../../../backend/reg_alloc]0;Holmake: ~/regression/cakeml-835/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-835/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: ../../../../../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: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/gc]0;Holmake: ../../../../../backend/gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/reg_alloc/proofs]0;Holmake: ../../../../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/semantics]0;Holmake: ../../../../../backend/semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../encoders/ag32/proofs]0;Holmake: ../../../../../encoders/ag32/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/ag32/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../../..]0;Holmake: ../../../../../backend/arm6]0;Holmake: ../../../../../encoders/arm6]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ../../../../../encoders/arm6]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: ../../../../../encoders/arm8]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: ../../../../../encoders/mips]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ../../../../../encoders/riscv]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ../../../../../encoders/x64]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/unification/triangular]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-d3953f88ec91360cb865ace99ebbb7b8028807e2/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: ../../../../translation]0;Holmake: ../../../../../encoders/monadic_enc]0;Holmake: ../../../../../encoders/monadic_enc[1mWorking in $(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
]0;Holmake: ../../../../translation]0;Holmake: ../../../../../inference/proofs]0;Holmake: ../../../../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: ../../../../translation]0;Holmake: ../../../../translation[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs[0m
Starting work on ag32BootstrapProofTheory
Starting work on README.md
README.md                                                                    OK
ag32BootstrapProofTheory                                            FAILED! <1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "ag32BootstrapProof">>
 Saved theorem _____ "target_state_rel_cake_start_asm_state"
 Saved theorem _____ "cake_installed"
 Saved theorem _____ "cake_machine_sem"
 Saved theorem _____ "get_stdin_stdin_fs"
 Saved theorem _____ "inFS_fname_fastForwardFD"
 error in quse /home/myreen/regression/cakeml-835/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load ag32BootstrapProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}