Job 836

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:7b9343ee31f1202a7efd349e7ff291eef8311133
  Document some changes to emacs mode [May 03 00:36:20]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 06 01:55:56 Claimed job
May 06 01:56:40 Building HOL
May 06 02:05:59 Starting developers
May 06 02:06:02 Finished developers                                               2s  21MB
May 06 02:06:02 Starting developers/bin
May 06 02:07:13 Finished developers/bin                                        1m10s 919MB
May 06 02:07:13 Starting semantics/ffi
May 06 02:07:51 Finished semantics/ffi                                           37s 483MB
May 06 02:07:51 Starting semantics
May 06 02:09:27 Finished semantics                                             1m35s   1GB
May 06 02:09:27 Starting semantics/proofs
May 06 02:12:22 Finished semantics/proofs                                      2m55s   1GB
May 06 02:12:23 Starting basis/pure
May 06 02:15:58 Finished basis/pure                                            3m34s 632MB
May 06 02:15:58 Starting translator
May 06 02:17:38 Finished translator                                            1m40s   1GB
May 06 02:17:39 Starting compiler/parsing
May 06 02:18:36 Finished compiler/parsing                                        57s   2GB
May 06 02:18:36 Starting characteristic
May 06 02:23:49 Finished characteristic                                        5m12s   1GB
May 06 02:23:50 Starting translator/monadic
May 06 02:25:21 Finished translator/monadic                                    1m30s   1GB
May 06 02:25:21 Starting basis
May 06 02:42:07 Finished basis                                                16m46s   2GB
May 06 02:42:08 Starting compiler/inference
May 06 02:43:58 Finished compiler/inference                                    1m50s   1GB
May 06 02:43:58 Starting compiler/backend/reg_alloc
May 06 02:44:58 Finished compiler/backend/reg_alloc                              59s   1GB
May 06 02:44:59 Starting compiler/backend/gc
May 06 02:54:06 Finished compiler/backend/gc                                   9m07s   2GB
May 06 02:54:06 Starting compiler/backend
May 06 02:54:09 Finished compiler/backend                                         2s  15MB
May 06 02:54:09 Starting compiler/encoders/asm
May 06 02:54:11 Finished compiler/encoders/asm                                    1s  24MB
May 06 02:54:11 Starting compiler/encoders/x64
May 06 02:55:12 Finished compiler/encoders/x64                                 1m01s 947MB
May 06 02:55:13 Starting compiler/encoders/arm6
May 06 02:56:51 Finished compiler/encoders/arm6                                1m38s   1GB
May 06 02:56:51 Starting compiler/encoders/arm8
May 06 02:57:24 Finished compiler/encoders/arm8                                  32s 798MB
May 06 02:57:24 Starting compiler/encoders/mips
May 06 02:58:32 Finished compiler/encoders/mips                                1m08s 978MB
May 06 02:58:33 Starting compiler/encoders/riscv
May 06 02:59:53 Finished compiler/encoders/riscv                               1m20s   1GB
May 06 02:59:54 Starting compiler/encoders/ag32
May 06 03:00:11 Finished compiler/encoders/ag32                                  16s 781MB
May 06 03:00:11 Starting compiler/backend/x64
May 06 03:00:30 Finished compiler/backend/x64                                    18s   1GB
May 06 03:00:30 Starting compiler/backend/arm6
May 06 03:00:49 Finished compiler/backend/arm6                                   18s   1GB
May 06 03:00:49 Starting compiler/backend/arm8
May 06 03:01:08 Finished compiler/backend/arm8                                   18s   1GB
May 06 03:01:08 Starting compiler/backend/mips
May 06 03:01:28 Finished compiler/backend/mips                                   19s   1GB
May 06 03:01:28 Starting compiler/backend/riscv
May 06 03:01:47 Finished compiler/backend/riscv                                  19s   1GB
May 06 03:01:48 Starting compiler/backend/ag32
May 06 03:02:55 Finished compiler/backend/ag32                                 1m07s   1GB
May 06 03:02:55 Starting compiler/parsing/proofs
May 06 03:08:29 Finished compiler/parsing/proofs                               5m33s   1GB
May 06 03:08:30 Starting compiler/inference/proofs
May 06 03:11:11 Finished compiler/inference/proofs                             2m41s   1GB
May 06 03:11:12 Starting compiler/backend/semantics
May 06 03:18:03 Finished compiler/backend/semantics                            6m51s   2GB
May 06 03:18:03 Starting compiler/backend/reg_alloc/proofs
May 06 03:21:20 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
May 06 03:21:20 Starting compiler/backend/proofs
May 06 03:58:22 Finished compiler/backend/proofs                              37m01s   3GB
May 06 03:58:22 Starting compiler/encoders/x64/proofs
May 06 04:08:20 Finished compiler/encoders/x64/proofs                          9m57s   4GB
May 06 04:08:20 Starting compiler/encoders/arm6/proofs
May 06 04:21:54 Finished compiler/encoders/arm6/proofs                        13m33s   3GB
May 06 04:21:54 Starting compiler/encoders/arm8/proofs
May 06 04:28:32 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
May 06 04:28:32 Starting compiler/encoders/mips/proofs
May 06 04:38:16 Finished compiler/encoders/mips/proofs                         9m43s   2GB
May 06 04:38:16 Starting compiler/encoders/riscv/proofs
May 06 04:46:37 Finished compiler/encoders/riscv/proofs                        8m21s   1GB
May 06 04:46:38 Starting compiler/encoders/ag32/proofs
May 06 04:49:05 Finished compiler/encoders/ag32/proofs                         2m26s 899MB
May 06 04:49:05 Starting compiler/backend/x64/proofs
May 06 04:49:25 Finished compiler/backend/x64/proofs                             20s 884MB
May 06 04:49:26 Starting compiler/backend/arm6/proofs
May 06 04:49:48 Finished compiler/backend/arm6/proofs                            22s   1GB
May 06 04:49:48 Starting compiler/backend/arm8/proofs
May 06 04:50:07 Finished compiler/backend/arm8/proofs                            18s 812MB
May 06 04:50:07 Starting compiler/backend/mips/proofs
May 06 04:50:28 Finished compiler/backend/mips/proofs                            20s   1GB
May 06 04:50:28 Starting compiler/backend/riscv/proofs
May 06 04:50:47 Finished compiler/backend/riscv/proofs                           19s 814MB
May 06 04:50:47 Starting compiler/backend/ag32/proofs
May 06 04:59:37 Finished compiler/backend/ag32/proofs                          8m49s   2GB
May 06 04:59:37 Starting compiler/proofs
May 06 05:01:16 Finished compiler/proofs                                       1m38s   2GB
May 06 05:01:17 Starting candle/set-theory
May 06 05:01:44 Finished candle/set-theory                                       26s 687MB
May 06 05:01:44 Starting candle/syntax-lib
May 06 05:01:55 Finished candle/syntax-lib                                       11s 595MB
May 06 05:01:56 Starting candle/standard/syntax
May 06 05:03:39 Finished candle/standard/syntax                                1m43s   1GB
May 06 05:03:40 Starting candle/standard/semantics
May 06 05:05:18 Finished candle/standard/semantics                             1m37s   1GB
May 06 05:05:18 Starting candle/standard/monadic
May 06 05:06:51 Finished candle/standard/monadic                               1m32s   1GB
May 06 05:06:51 Starting candle/standard/ml_kernel
May 06 05:10:43 Finished candle/standard/ml_kernel                             3m51s   3GB
May 06 05:10:43 Starting candle/standard/opentheory
May 06 05:19:05 Finished candle/standard/opentheory                            8m21s   3GB
May 06 05:19:05 Starting candle/standard/opentheory/compilation
May 06 05:48:14 Finished candle/standard/opentheory/compilation               29m08s  22GB
May 06 05:48:14 Starting candle/standard/opentheory/compilation/proofs
May 06 05:49:07 Finished candle/standard/opentheory/compilation/proofs           52s   2GB
May 06 05:49:07 Starting characteristic/examples
May 06 05:50:31 Finished characteristic/examples                               1m23s   2GB
May 06 05:50:31 Starting tutorial/solutions
May 06 06:03:29 Finished tutorial/solutions                                   12m56s   6GB
May 06 06:03:29 Starting translator/monadic/examples
May 06 06:06:22 Finished translator/monadic/examples                           2m52s   2GB
May 06 06:06:22 Starting examples
May 06 06:14:58 Finished examples                                              8m36s   4GB
May 06 06:14:59 Starting examples/compilation/x64
May 06 08:16:24 Finished examples/compilation/x64                           2h01m24s  14GB
May 06 08:16:24 Starting examples/compilation/x64/proofs
May 06 08:17:51 Finished examples/compilation/x64/proofs                       1m26s   2GB
May 06 08:17:51 Starting examples/compilation/ag32
May 06 08:45:36 Finished examples/compilation/ag32                            27m45s   6GB
May 06 08:45:37 Starting examples/compilation/ag32/proofs
May 06 08:46:36 Finished examples/compilation/ag32/proofs                        59s   2GB
May 06 08:46:36 Starting translator/okasaki-examples
May 06 08:50:35 Finished translator/okasaki-examples                           3m58s   1GB
May 06 08:50:36 Starting translator/other-examples
May 06 08:54:12 Finished translator/other-examples                             3m35s   1GB
May 06 08:54:12 Starting compiler/parsing/tests
May 06 08:54:37 Finished compiler/parsing/tests                                  25s 579MB
May 06 08:54:38 Starting compiler/inference/tests
May 06 08:58:44 Finished compiler/inference/tests                              4m05s   5GB
May 06 08:58:44 Starting compiler/bootstrap/translation
May 06 11:27:39 Finished compiler/bootstrap/translation                     2h28m54s  40GB
May 06 11:27:39 Starting unverified/sexpr-bootstrap/x64/64
May 06 11:35:13 Finished unverified/sexpr-bootstrap/x64/64                     7m33s   3GB
May 06 11:35:14 Starting unverified/sexpr-bootstrap/x64/32
May 06 11:39:48 Finished unverified/sexpr-bootstrap/x64/32                     4m34s   6GB
May 06 11:39:49 Starting compiler/benchmarks
May 06 11:39:56 Finished compiler/benchmarks                                      6s  23MB
May 06 11:39:56 Starting compiler/bootstrap/compilation/x64/64
May 06 21:44:13 Finished compiler/bootstrap/compilation/x64/64             10h04m16s  64GB
May 06 21:44:13 Starting compiler/bootstrap/compilation/x64/64/proofs
May 06 21:47:34 Finished compiler/bootstrap/compilation/x64/64/proofs          3m20s   5GB
May 06 21:47:34 Starting compiler/bootstrap/compilation/x64/32
May 07 07:41:38 Finished compiler/bootstrap/compilation/x64/32              9h54m03s  63GB
May 07 07:41:39 Starting compiler/bootstrap/compilation/x64/32/proofs
May 07 07:45:09 Finished compiler/bootstrap/compilation/x64/32/proofs          3m30s   5GB
May 07 07:45:09 Starting compiler/bootstrap/compilation/ag32/32
May 07 17:45:34 Finished compiler/bootstrap/compilation/ag32/32            10h00m24s  64GB
May 07 17:45:35 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 07 18:00:00 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ~/oven/regression/cakeml-836/basis]0;Holmake: ~/oven/regression/cakeml-836/basis/pure]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/cakeml-836/basis/pure]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-836/basis/pure]0;Holmake: ~/oven/regression/cakeml-836/misc]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-836/misc]0;Holmake: ~/oven/regression/cakeml-836/developers]0;Holmake: ~/oven/regression/cakeml-836/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-836/misc]0;Holmake: ~/oven/regression/cakeml-836/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-836/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-836/misc]0;Holmake: ~/oven/regression/cakeml-836/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-836/basis/pure]0;Holmake: ~/oven/regression/cakeml-836/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-836/basis]0;Holmake: ~/oven/regression/cakeml-836/characteristic]0;Holmake: ~/oven/regression/cakeml-836/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-836/semantics]0;Holmake: ~/oven/regression/cakeml-836/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-836/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-836/semantics]0;Holmake: ~/oven/regression/cakeml-836/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-836/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-836/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-836/characteristic]0;Holmake: ~/oven/regression/cakeml-836/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-836/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-836/characteristic]0;Holmake: ~/oven/regression/cakeml-836/translator]0;Holmake: ~/oven/regression/cakeml-836/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-836/characteristic]0;Holmake: ~/oven/regression/cakeml-836/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-836/basis]0;Holmake: ~/oven/regression/cakeml-836/translator/monadic]0;Holmake: ~/oven/regression/cakeml-836/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-836/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-836/translator/monadic]0;Holmake: ~/oven/regression/cakeml-836/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-836/basis]0;Holmake: ~/oven/regression/cakeml-836/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/ag32]0;Holmake: ../../../../../backend]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../../../../../backend]0;Holmake: ../../../../../backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-836/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-836/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: ../../../../../backend/ag32]0;Holmake: ../../../../../encoders/ag32]0;Holmake: ../../../../../encoders/ag32Working in $(CAKEMLDIR)/compiler/encoders/ag32
]0;Holmake: ../../../../../backend/ag32]0;Holmake: ../../../../../backend/ag32Working in $(CAKEMLDIR)/compiler/backend/ag32
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/gc]0;Holmake: ../../../../../backend/gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/reg_alloc/proofs]0;Holmake: ../../../../../backend/reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/semantics]0;Holmake: ../../../../../backend/semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: ../../../../../backend/proofs]0;Holmake: ../../../../../backend/proofsWorking in $(CAKEMLDIR)/compiler/backend/proofs
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../encoders/ag32/proofs]0;Holmake: ../../../../../encoders/ag32/proofsWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs
]0;Holmake: ../../../../../backend/ag32/proofs]0;Holmake: ../../../../../backend/ag32/proofsWorking in $(CAKEMLDIR)/compiler/backend/ag32/proofs
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../../..]0;Holmake: ../../../../../backend/arm6]0;Holmake: ../../../../../encoders/arm6]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: ../../../../../encoders/arm6]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: ../../../../../encoders/arm8]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: ../../../../../encoders/mips]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: ../../../../../encoders/riscv]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: ../../../../../encoders/x64]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-7b9343ee31f1202a7efd349e7ff291eef8311133/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: ../../../../translation]0;Holmake: ../../../../../encoders/monadic_enc]0;Holmake: ../../../../../encoders/monadic_encWorking in $(CAKEMLDIR)/compiler/encoders/monadic_enc
]0;Holmake: ../../../../translation]0;Holmake: ../../../../../inference/proofs]0;Holmake: ../../../../../inference/proofsWorking in $(CAKEMLDIR)/compiler/inference/proofs
]0;Holmake: ../../../../translation]0;Holmake: ../../../../translationWorking in $(CAKEMLDIR)/compiler/bootstrap/translation
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
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"
 error in quse /home/cake/oven/regression/cakeml-836/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"}
 Saved theorem _____ "inFS_fname_fastForwardFD"
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}