Job 652

CakeML:bd211e2702a5c6788c4e88b9751017244d766fcb
  Commit a few generated README.md files [Dec 27 19:41:46]
#590 (howto)
Merging into:2e9c8e4f622247379354a7408d480f5a67333abc
  Tweak gitignores [Dec 27 16:58:19]
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
  Fix bug: TypeBase.simpls_of not being filled in on load [Dec 21 04:04:45]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 27 20:02:39 Claimed job
Dec 27 20:02:43 Reusing HOL
Dec 27 20:03:34 Starting developers
Dec 27 20:03:36 Finished developers                                               2s  21MB
Dec 27 20:03:37 Starting developers/bin
Dec 27 20:04:48 Finished developers/bin                                        1m09s 916MB
Dec 27 20:04:48 Starting semantics/ffi
Dec 27 20:04:59 Finished semantics/ffi                                           10s 254MB
Dec 27 20:05:00 Starting semantics
Dec 27 20:06:24 Finished semantics                                             1m23s   1GB
Dec 27 20:06:25 Starting semantics/proofs
Dec 27 20:09:48 Finished semantics/proofs                                      3m22s   1GB
Dec 27 20:09:49 Starting basis/pure
Dec 27 20:10:42 Finished basis/pure                                              52s 736MB
Dec 27 20:10:43 Starting translator
Dec 27 20:12:25 Finished translator                                            1m41s   1GB
Dec 27 20:12:26 Starting compiler/parsing
Dec 27 20:13:31 Finished compiler/parsing                                      1m04s   2GB
Dec 27 20:13:32 Starting characteristic
Dec 27 20:16:53 Finished characteristic                                        3m21s   1GB
Dec 27 20:16:54 Starting translator/monadic
Dec 27 20:18:26 Finished translator/monadic                                    1m31s   1GB
Dec 27 20:18:27 Starting basis
Dec 27 20:35:07 Finished basis                                                16m39s   2GB
Dec 27 20:35:08 Starting compiler/inference
Dec 27 20:36:49 Finished compiler/inference                                    1m41s   1GB
Dec 27 20:36:50 Starting compiler/backend/reg_alloc
Dec 27 20:37:44 Finished compiler/backend/reg_alloc                              53s   1GB
Dec 27 20:37:45 Starting compiler/backend/gc
Dec 27 20:45:46 Finished compiler/backend/gc                                   8m00s   1GB
Dec 27 20:45:47 Starting compiler/backend
Dec 27 20:45:50 Finished compiler/backend                                         2s  15MB
Dec 27 20:45:50 Starting compiler/encoders/asm
Dec 27 20:45:52 Finished compiler/encoders/asm                                    1s  15MB
Dec 27 20:45:53 Starting compiler/encoders/x64
Dec 27 20:46:19 Finished compiler/encoders/x64                                   25s 814MB
Dec 27 20:46:20 Starting compiler/encoders/arm6
Dec 27 20:47:13 Finished compiler/encoders/arm6                                  52s 761MB
Dec 27 20:47:13 Starting compiler/encoders/arm8
Dec 27 20:47:27 Finished compiler/encoders/arm8                                  13s 647MB
Dec 27 20:47:28 Starting compiler/encoders/mips
Dec 27 20:47:46 Finished compiler/encoders/mips                                  17s   1GB
Dec 27 20:47:46 Starting compiler/encoders/riscv
Dec 27 20:48:02 Finished compiler/encoders/riscv                                 15s 845MB
Dec 27 20:48:03 Starting compiler/encoders/ag32
Dec 27 20:48:21 Finished compiler/encoders/ag32                                  17s 806MB
Dec 27 20:48:21 Starting compiler/backend/x64
Dec 27 20:48:40 Finished compiler/backend/x64                                    17s   1GB
Dec 27 20:48:41 Starting compiler/backend/arm6
Dec 27 20:49:02 Finished compiler/backend/arm6                                   20s   1GB
Dec 27 20:49:02 Starting compiler/backend/arm8
Dec 27 20:49:21 Finished compiler/backend/arm8                                   18s 916MB
Dec 27 20:49:22 Starting compiler/backend/mips
Dec 27 20:49:41 Finished compiler/backend/mips                                   18s   1GB
Dec 27 20:49:42 Starting compiler/backend/riscv
Dec 27 20:50:02 Finished compiler/backend/riscv                                  19s   1GB
Dec 27 20:50:03 Starting compiler/backend/ag32
Dec 27 20:51:16 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 27 20:51:16 Starting compiler/parsing/proofs
Dec 27 20:57:37 Finished compiler/parsing/proofs                               6m19s 854MB
Dec 27 20:57:37 Starting compiler/inference/proofs
Dec 27 21:00:32 Finished compiler/inference/proofs                             2m54s   1GB
Dec 27 21:00:33 Starting compiler/backend/semantics
Dec 27 21:08:07 Finished compiler/backend/semantics                            7m32s   1GB
Dec 27 21:08:07 Starting compiler/backend/reg_alloc/proofs
Dec 27 21:10:57 Finished compiler/backend/reg_alloc/proofs                     2m49s 744MB
Dec 27 21:10:57 Starting compiler/backend/proofs
Dec 27 21:49:46 Finished compiler/backend/proofs                              38m47s   3GB
Dec 27 21:49:46 Starting compiler/encoders/x64/proofs
Dec 27 21:59:31 Finished compiler/encoders/x64/proofs                          9m43s   5GB
Dec 27 21:59:31 Starting compiler/encoders/arm6/proofs
Dec 27 22:13:30 Finished compiler/encoders/arm6/proofs                        13m57s   3GB
Dec 27 22:13:31 Starting compiler/encoders/arm8/proofs
Dec 27 22:19:32 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
Dec 27 22:19:33 Starting compiler/encoders/mips/proofs
Dec 27 22:30:11 Finished compiler/encoders/mips/proofs                        10m36s   2GB
Dec 27 22:30:11 Starting compiler/encoders/riscv/proofs
Dec 27 22:38:06 Finished compiler/encoders/riscv/proofs                        7m53s   1GB
Dec 27 22:38:06 Starting compiler/encoders/ag32/proofs
Dec 27 22:40:51 Finished compiler/encoders/ag32/proofs                         2m43s 580MB
Dec 27 22:40:51 Starting compiler/backend/x64/proofs
Dec 27 22:41:12 Finished compiler/backend/x64/proofs                             20s   1GB
Dec 27 22:41:13 Starting compiler/backend/arm6/proofs
Dec 27 22:41:35 Finished compiler/backend/arm6/proofs                            21s   1GB
Dec 27 22:41:35 Starting compiler/backend/arm8/proofs
Dec 27 22:41:56 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 27 22:41:57 Starting compiler/backend/mips/proofs
Dec 27 22:42:19 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 27 22:42:19 Starting compiler/backend/riscv/proofs
Dec 27 22:42:41 Finished compiler/backend/riscv/proofs                           20s   1GB
Dec 27 22:42:41 Starting compiler/backend/ag32/proofs
Dec 27 22:52:01 Finished compiler/backend/ag32/proofs                          9m19s   2GB
Dec 27 22:52:02 Starting compiler/proofs
Dec 28 11:41:30 Resuming compiler/proofs
Dec 28 11:41:37 Finished compiler/proofs                                          5s  24MB
Dec 28 11:41:37 Starting candle/set-theory
Dec 28 11:42:05 Finished candle/set-theory                                       27s 678MB
Dec 28 11:42:05 Starting candle/syntax-lib
Dec 28 11:42:17 Finished candle/syntax-lib                                       10s 672MB
Dec 28 11:42:17 Starting candle/standard/syntax
Dec 28 11:44:09 Finished candle/standard/syntax                                1m50s 825MB
Dec 28 11:44:09 Starting candle/standard/semantics
Dec 28 11:45:53 Finished candle/standard/semantics                             1m42s   1GB
Dec 28 11:45:53 Starting candle/standard/monadic
Dec 28 11:47:39 Finished candle/standard/monadic                               1m44s   1GB
Dec 28 11:47:40 Starting candle/standard/ml_kernel
Dec 28 12:02:50 Finished candle/standard/ml_kernel                            15m09s   3GB
Dec 28 12:02:50 Starting candle/standard/opentheory
Dec 28 12:11:43 Finished candle/standard/opentheory                            8m52s   4GB
Dec 28 12:11:44 Starting candle/standard/opentheory/compilation
Dec 28 12:40:36 Finished candle/standard/opentheory/compilation               28m51s  15GB
Dec 28 12:40:37 Starting candle/standard/opentheory/compilation/proofs
Dec 28 12:41:28 Finished candle/standard/opentheory/compilation/proofs           49s   5GB
Dec 28 12:41:28 Starting characteristic/examples
Dec 28 12:43:01 Finished characteristic/examples                               1m31s   2GB
Dec 28 12:43:01 Starting tutorial/solutions
Dec 28 12:56:21 Finished tutorial/solutions                                   13m18s   7GB
Dec 28 12:56:21 Starting translator/monadic/examples
Dec 28 12:58:34 Finished translator/monadic/examples                           2m12s   2GB
Dec 28 12:58:35 Starting examples
Dec 28 13:06:21 Finished examples                                              7m45s   3GB
Dec 28 13:06:22 Starting examples/compilation/x64
Dec 28 15:09:25 Finished examples/compilation/x64                           2h03m01s  12GB
Dec 28 15:09:25 Starting examples/compilation/x64/proofs
Dec 28 15:11:19 Finished examples/compilation/x64/proofs                       1m52s   4GB
Dec 28 15:11:19 Starting examples/compilation/ag32
Dec 28 15:38:35 Finished examples/compilation/ag32                            27m15s   7GB
Dec 28 15:38:36 Starting examples/compilation/ag32/proofs
Dec 28 15:39:26 Finished examples/compilation/ag32/proofs                        49s   3GB
Dec 28 15:39:27 Starting translator/okasaki-examples
Dec 28 15:43:29 Finished translator/okasaki-examples                           4m01s   1GB
Dec 28 15:43:29 Starting translator/other-examples
Dec 28 15:44:12 Finished translator/other-examples                               42s   1GB
Dec 28 15:44:13 Starting compiler/parsing/tests
Dec 28 15:44:40 Finished compiler/parsing/tests                                  26s 547MB
Dec 28 15:44:41 Starting compiler/inference/tests
Dec 28 15:48:42 Finished compiler/inference/tests                              4m00s   3GB
Dec 28 15:48:42 Starting compiler/bootstrap/translation
Dec 28 19:17:59 Finished compiler/bootstrap/translation                     3h29m15s  52GB
Dec 28 19:18:00 Starting unverified/sexpr-bootstrap/x64/64
Dec 28 19:26:10 Finished unverified/sexpr-bootstrap/x64/64                     8m09s  15GB
Dec 28 19:26:11 Starting unverified/sexpr-bootstrap/x64/32
Dec 28 19:31:09 FAILED: unverified/sexpr-bootstrap/x64/32
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/cakeml-652/basis]0;Holmake: ~/oven/regression/cakeml-652/basis/pure]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/oven/regression/cakeml-652/basis/pure]0;Holmake: ~/oven/regression/cakeml-652/misc]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/oven/regression/cakeml-652/misc]0;Holmake: ~/oven/regression/cakeml-652/developers]0;Holmake: ~/oven/regression/cakeml-652/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-652/misc]0;Holmake: ~/oven/regression/cakeml-652/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-652/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-652/misc]0;Holmake: ~/oven/regression/cakeml-652/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/oven/regression/cakeml-652/basis/pure]0;Holmake: ~/oven/regression/cakeml-652/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/oven/regression/cakeml-652/basis]0;Holmake: ~/oven/regression/cakeml-652/characteristic]0;Holmake: ~/oven/regression/cakeml-652/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-652/semantics]0;Holmake: ~/oven/regression/cakeml-652/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-652/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-652/semantics]0;Holmake: ~/oven/regression/cakeml-652/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-652/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/oven/regression/cakeml-652/characteristic]0;Holmake: ~/oven/regression/cakeml-652/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-652/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/oven/regression/cakeml-652/characteristic]0;Holmake: ~/oven/regression/cakeml-652/translator]0;Holmake: ~/oven/regression/cakeml-652/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/oven/regression/cakeml-652/characteristic]0;Holmake: ~/oven/regression/cakeml-652/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/oven/regression/cakeml-652/basis]0;Holmake: ~/oven/regression/cakeml-652/translator/monadic]0;Holmake: ~/oven/regression/cakeml-652/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-652/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/oven/regression/cakeml-652/translator/monadic]0;Holmake: ~/oven/regression/cakeml-652/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/oven/regression/cakeml-652/basis]0;Holmake: ~/oven/regression/cakeml-652/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-652/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-652/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/asm]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/ag32]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm6]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm6]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm8]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm8]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/mips]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/mips]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/riscv]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/riscv]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/x64]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/x64]0;Holmake: ~/oven/regression/cakeml-652/compiler/encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler/inference]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/inference]0;Holmake: ~/oven/regression/cakeml-652/compiler/inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler]0;Holmake: ~/oven/regression/cakeml-652/compiler[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/reg_alloc/proofs]0;Holmake: ~/oven/regression/cakeml-652/compiler/backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/cakeml-652/compiler/inference/proofs]0;Holmake: ~/oven/regression/cakeml-652/compiler/inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation]0;Holmake: ~/oven/regression/cakeml-652/compiler/bootstrap/translation[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-652/developers/bin]0;Holmake: ~/oven/regression/cakeml-652/developers/bin[1mWorking in $(CAKEMLDIR)/developers/bin[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32[0m
Starting work on x64SexprTheory
Starting work on README.md
README.md                                                                    OK
x64SexprTheory                                                               OK
Starting work on cake.S
cake.S                                                                       OK
Don't know how to build necessary target(s): how-to.output