Job 2263

CakeML:d14bd87d704913b4e7ffba9c0747ccfb9a6184cd
  Fixes for ffiname [Jan 03 01:49:45]
#976 (ffiname)
Merging into:45534e558612704f938386fc12b79bc991c3afa3
  Update for new year [Jan 01 02:20:21]
HOL:d587e1c70b4c059edc079ed4a529b5b7423223b8
  Add ltree_every and ltree_finite_branching (#1172) [Dec 11 22:22:54]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Jan 03 15:31:55 Claimed job
Jan 03 15:31:57 Reusing HOL
Jan 03 15:32:38 Starting developers
Jan 03 15:32:44 Finished developers                                               5s 105MB
Jan 03 15:32:44 Starting developers/bin
Jan 03 15:32:50 Finished developers/bin                                           6s   1GB
Jan 03 15:32:50 Starting compiler/proofs
Jan 04 09:11:12 Resuming compiler/proofs
Jan 04 09:14:05 Finished compiler/proofs                                       2m52s   4GB
Jan 04 09:14:05 Starting compiler/bootstrap/translation
Jan 04 17:36:37 Finished compiler/bootstrap/translation                     8h22m31s  34GB
Jan 04 17:36:37 Starting semantics/ffi
Jan 04 17:36:43 Finished semantics/ffi                                            5s 213MB
Jan 04 17:36:43 Starting semantics
Jan 04 17:36:44 Finished semantics                                                1s  18MB
Jan 04 17:36:45 Starting semantics/proofs
Jan 04 17:37:17 Finished semantics/proofs                                        31s 767MB
Jan 04 17:37:17 Starting semantics/alt_semantics
Jan 04 17:37:49 Finished semantics/alt_semantics                                 32s 921MB
Jan 04 17:37:49 Starting semantics/alt_semantics/proofs
Jan 04 17:49:53 Finished semantics/alt_semantics/proofs                       12m03s   1GB
Jan 04 17:49:53 Starting basis/pure
Jan 04 17:49:55 Finished basis/pure                                               1s  22MB
Jan 04 17:49:55 Starting translator
Jan 04 17:51:45 Finished translator                                            1m50s   2GB
Jan 04 17:51:46 Starting compiler/parsing
Jan 04 17:51:47 Finished compiler/parsing                                         1s  16MB
Jan 04 17:51:47 Starting characteristic
Jan 04 17:51:49 Finished characteristic                                           1s  22MB
Jan 04 17:51:49 Starting translator/monadic
Jan 04 17:51:51 Finished translator/monadic                                       1s  21MB
Jan 04 17:51:51 Starting basis
Jan 04 17:55:37 Finished basis                                                 3m45s   3GB
Jan 04 17:55:37 Starting compiler/inference
Jan 04 17:55:39 Finished compiler/inference                                       1s  23MB
Jan 04 17:55:39 Starting compiler/backend/reg_alloc
Jan 04 17:55:41 Finished compiler/backend/reg_alloc                               1s  21MB
Jan 04 17:55:41 Starting compiler/backend/gc
Jan 04 17:55:43 Finished compiler/backend/gc                                      2s  26MB
Jan 04 17:55:43 Starting compiler/backend
Jan 04 17:55:56 Finished compiler/backend                                        12s 775MB
Jan 04 17:55:56 Starting compiler/encoders/asm
Jan 04 17:55:57 Finished compiler/encoders/asm                                    1s  23MB
Jan 04 17:55:57 Starting compiler/encoders/x64
Jan 04 17:55:59 Finished compiler/encoders/x64                                    1s  25MB
Jan 04 17:55:59 Starting compiler/encoders/arm7
Jan 04 17:56:01 Finished compiler/encoders/arm7                                   1s  25MB
Jan 04 17:56:01 Starting compiler/encoders/arm8
Jan 04 17:56:03 Finished compiler/encoders/arm8                                   1s  24MB
Jan 04 17:56:03 Starting compiler/encoders/arm8_asl
Jan 04 17:59:15 Finished compiler/encoders/arm8_asl                            3m11s   1GB
Jan 04 17:59:15 Starting compiler/encoders/mips
Jan 04 17:59:17 Finished compiler/encoders/mips                                   1s  25MB
Jan 04 17:59:17 Starting compiler/encoders/riscv
Jan 04 17:59:19 Finished compiler/encoders/riscv                                  1s  25MB
Jan 04 17:59:19 Starting compiler/encoders/ag32
Jan 04 17:59:21 Finished compiler/encoders/ag32                                   1s  26MB
Jan 04 17:59:21 Starting compiler/backend/x64
Jan 04 17:59:23 Finished compiler/backend/x64                                     2s  23MB
Jan 04 17:59:23 Starting compiler/backend/arm7
Jan 04 17:59:25 Finished compiler/backend/arm7                                    2s  27MB
Jan 04 17:59:25 Starting compiler/backend/arm8
Jan 04 17:59:28 Finished compiler/backend/arm8                                    2s  22MB
Jan 04 17:59:28 Starting compiler/backend/mips
Jan 04 17:59:30 Finished compiler/backend/mips                                    2s  22MB
Jan 04 17:59:30 Starting compiler/backend/riscv
Jan 04 17:59:32 Finished compiler/backend/riscv                                   2s  22MB
Jan 04 17:59:32 Starting compiler/backend/ag32
Jan 04 18:00:59 Finished compiler/backend/ag32                                 1m26s   1GB
Jan 04 18:00:59 Starting compiler/parsing/proofs
Jan 04 18:01:01 Finished compiler/parsing/proofs                                  1s  20MB
Jan 04 18:01:01 Starting compiler/inference/proofs
Jan 04 18:01:03 Finished compiler/inference/proofs                                1s  22MB
Jan 04 18:01:03 Starting compiler/backend/semantics
Jan 04 18:02:18 Finished compiler/backend/semantics                            1m15s   1GB
Jan 04 18:02:18 Starting compiler/backend/reg_alloc/proofs
Jan 04 18:02:20 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Jan 04 18:02:20 Starting compiler/backend/proofs
Jan 04 18:03:20 Finished compiler/backend/proofs                               1m00s   2GB
Jan 04 18:03:20 Starting compiler/backend/serialiser
Jan 04 18:03:23 Finished compiler/backend/serialiser                              2s  41MB
Jan 04 18:03:24 Starting compiler/encoders/x64/proofs
Jan 04 18:13:10 Finished compiler/encoders/x64/proofs                          9m46s   5GB
Jan 04 18:13:10 Starting compiler/encoders/arm7/proofs
Jan 04 18:26:47 Finished compiler/encoders/arm7/proofs                        13m36s   5GB
Jan 04 18:26:47 Starting compiler/encoders/arm8/proofs
Jan 04 18:33:47 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
Jan 04 18:33:47 Starting compiler/encoders/arm8_asl/proofs
Jan 04 18:49:03 Finished compiler/encoders/arm8_asl/proofs                    15m16s   2GB
Jan 04 18:49:03 Starting compiler/encoders/mips/proofs
Jan 04 18:59:47 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Jan 04 18:59:47 Starting compiler/encoders/riscv/proofs
Jan 04 19:08:44 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
Jan 04 19:08:44 Starting compiler/encoders/ag32/proofs
Jan 04 19:11:17 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Jan 04 19:11:17 Starting compiler/backend/x64/proofs
Jan 04 19:11:47 Finished compiler/backend/x64/proofs                             30s   1GB
Jan 04 19:11:47 Starting compiler/backend/arm7/proofs
Jan 04 19:12:21 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 04 19:12:21 Starting compiler/backend/arm8/proofs
Jan 04 19:12:51 Finished compiler/backend/arm8/proofs                            29s   1GB
Jan 04 19:12:51 Starting compiler/backend/arm8_asl
Jan 04 19:13:14 Finished compiler/backend/arm8_asl                               23s   1GB
Jan 04 19:13:14 Starting compiler/backend/mips/proofs
Jan 04 19:13:45 Finished compiler/backend/mips/proofs                            31s   1GB
Jan 04 19:13:45 Starting compiler/backend/riscv/proofs
Jan 04 19:14:20 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 04 19:14:20 Starting compiler/backend/ag32/proofs
Jan 04 19:28:08 Finished compiler/backend/ag32/proofs                         13m48s   3GB
Jan 04 19:28:08 Starting candle/set-theory
Jan 04 19:28:47 Finished candle/set-theory                                       38s   1GB
Jan 04 19:28:47 Starting candle/syntax-lib
Jan 04 19:28:48 Finished candle/syntax-lib                                        1s  21MB
Jan 04 19:28:48 Starting candle/standard/syntax
Jan 04 19:29:00 Finished candle/standard/syntax                                  11s 733MB
Jan 04 19:29:00 Starting candle/standard/semantics
Jan 04 19:30:56 Finished candle/standard/semantics                             1m56s   1GB
Jan 04 19:30:56 Starting candle/standard/monadic
Jan 04 19:30:58 Finished candle/standard/monadic                                  1s  20MB
Jan 04 19:30:58 Starting candle/standard/ml_kernel
Jan 04 19:32:33 Finished candle/standard/ml_kernel                             1m34s   2GB
Jan 04 19:32:33 Starting candle/overloading/syntax
Jan 04 19:35:56 Finished candle/overloading/syntax                             3m22s   1GB
Jan 04 19:35:56 Starting candle/overloading/semantics
Jan 04 19:48:17 Finished candle/overloading/semantics                         12m20s   2GB
Jan 04 19:48:17 Starting candle/overloading/monadic
Jan 04 19:51:03 Finished candle/overloading/monadic                            2m45s   2GB
Jan 04 19:51:03 Starting candle/overloading/ml_kernel
Jan 04 19:59:02 Finished candle/overloading/ml_kernel                          7m58s   3GB
Jan 04 19:59:02 Starting candle/overloading/ml_checker
Jan 04 20:01:41 Finished candle/overloading/ml_checker                         2m39s   2GB
Jan 04 20:01:42 Starting candle/prover
Jan 04 20:11:44 Finished candle/prover                                        10m02s   4GB
Jan 04 20:11:45 Starting pancake
Jan 04 20:12:28 Finished pancake                                                 43s 916MB
Jan 04 20:12:28 Starting pancake/ffi
Jan 04 20:12:29 Finished pancake/ffi                                              0s  13MB
Jan 04 20:12:29 Starting pancake/semantics
Jan 04 20:14:59 Finished pancake/semantics                                     2m30s   1GB
Jan 04 20:15:00 Starting pancake/parser
Jan 04 20:15:22 Finished pancake/parser                                          22s 943MB
Jan 04 20:15:22 Starting pancake/proofs
Jan 04 20:49:01 Finished pancake/proofs                                       33m38s   6GB
Jan 04 20:49:01 Starting characteristic/examples
Jan 04 20:50:38 Finished characteristic/examples                               1m36s   3GB
Jan 04 20:50:38 Starting tutorial/solutions
Jan 04 21:06:01 Finished tutorial/solutions                                   15m22s   9GB
Jan 04 21:06:01 Starting translator/monadic/examples
Jan 04 21:10:08 Finished translator/monadic/examples                           4m06s   3GB
Jan 04 21:10:08 Starting examples
Jan 04 21:26:41 Finished examples                                             16m32s   4GB
Jan 04 21:26:41 Starting examples/compilation/x64
Jan 04 23:26:28 Finished examples/compilation/x64                           1h59m46s  20GB
Jan 04 23:26:28 Starting examples/compilation/x64/proofs
Jan 04 23:29:04 Finished examples/compilation/x64/proofs                       2m35s   4GB
Jan 04 23:29:04 Starting examples/compilation/ag32
Jan 04 23:59:37 Finished examples/compilation/ag32                            30m32s   9GB
Jan 04 23:59:37 Starting examples/compilation/ag32/proofs
Jan 05 00:00:40 Finished examples/compilation/ag32/proofs                      1m03s   4GB
Jan 05 00:00:40 Starting examples/compilation/to_word
Jan 05 00:04:06 Finished examples/compilation/to_word                          3m25s   6GB
Jan 05 00:04:06 Starting examples/lpr_checker
Jan 05 00:05:13 Finished examples/lpr_checker                                  1m06s   1GB
Jan 05 00:05:13 Starting examples/lpr_checker/array
Jan 05 00:36:16 Finished examples/lpr_checker/array                           31m03s   6GB
Jan 05 00:36:16 Starting examples/lpr_checker/array/compilation
Jan 05 01:25:41 Finished examples/lpr_checker/array/compilation               49m24s  25GB
Jan 05 01:25:41 Starting examples/lpr_checker/array/compilation/proofs
Jan 05 01:27:52 Finished examples/lpr_checker/array/compilation/proofs         2m10s   3GB
Jan 05 01:27:52 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 05 01:34:23 Finished examples/lpr_checker/array/compilation/proofsARM8     6m31s  20GB
Jan 05 01:34:24 Starting examples/pseudo_bool
Jan 05 01:36:18 Finished examples/pseudo_bool                                  1m54s   1GB
Jan 05 01:36:18 Starting examples/pseudo_bool/cnf_encoding
Jan 05 01:36:46 Finished examples/pseudo_bool/cnf_encoding                       27s 709MB
Jan 05 01:36:47 Starting examples/pseudo_bool/graph_encoding
Jan 05 01:37:30 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Jan 05 01:37:30 Starting examples/pseudo_bool/array
Jan 05 02:36:50 Finished examples/pseudo_bool/array                           59m19s   5GB
Jan 05 02:36:50 Starting examples/pseudo_bool/array/compilation
Jan 05 06:25:44 Finished examples/pseudo_bool/array/compilation             3h48m54s  28GB
Jan 05 06:25:44 Starting examples/pseudo_bool/array/compilation/proofs
Jan 05 06:28:40 Finished examples/pseudo_bool/array/compilation/proofs         2m55s   5GB
Jan 05 06:28:40 Starting examples/opentheory
Jan 05 06:39:49 Finished examples/opentheory                                  11m09s   4GB
Jan 05 06:39:49 Starting examples/opentheory
Jan 05 06:39:51 Finished examples/opentheory                                      1s  25MB
Jan 05 06:39:51 Starting examples/opentheory/compilation
Jan 05 07:18:06 Finished examples/opentheory/compilation                      38m14s  28GB
Jan 05 07:18:06 Starting examples/opentheory/compilation/proofs
Jan 05 07:19:12 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Jan 05 07:19:12 Starting examples/opentheory/compilation/ag32
Jan 05 07:54:06 Finished examples/opentheory/compilation/ag32                 34m53s  27GB
Jan 05 07:54:06 Starting examples/opentheory/compilation/ag32/proofs
Jan 05 07:56:02 Finished examples/opentheory/compilation/ag32/proofs           1m55s   4GB
Jan 05 07:56:02 Starting examples/sat_encodings
Jan 05 07:58:10 Finished examples/sat_encodings                                2m08s   1GB
Jan 05 07:58:10 Starting examples/sat_encodings/case_studies
Jan 05 07:59:57 Finished examples/sat_encodings/case_studies                   1m46s   1GB
Jan 05 07:59:57 Starting examples/sat_encodings/translation
Jan 05 08:06:40 Finished examples/sat_encodings/translation                    6m43s   4GB
Jan 05 08:06:40 Starting examples/sat_encodings/translation/compilation
Jan 05 09:06:40 Finished examples/sat_encodings/translation/compilation       59m59s  12GB
Jan 05 09:06:40 Starting examples/deflate
Jan 05 09:08:00 Finished examples/deflate                                      1m20s   1GB
Jan 05 09:08:00 Starting examples/deflate/translation
Jan 05 09:10:37 Finished examples/deflate/translation                          2m36s   3GB
Jan 05 09:10:37 Starting examples/deflate/translation/compilation
Jan 05 09:40:19 Finished examples/deflate/translation/compilation             29m41s   5GB
Jan 05 09:40:19 Starting examples/vipr
Jan 05 09:45:48 Finished examples/vipr                                         5m29s   3GB
Jan 05 09:45:49 Starting examples/vipr/compilation
Jan 05 10:09:30 Finished examples/vipr/compilation                            23m40s  17GB
Jan 05 10:09:30 Starting translator/okasaki-examples
Jan 05 10:17:14 Finished translator/okasaki-examples                           7m44s   2GB
Jan 05 10:17:14 Starting translator/other-examples
Jan 05 10:18:14 Finished translator/other-examples                               59s   1GB
Jan 05 10:18:14 Starting compiler/parsing/tests
Jan 05 10:18:47 Finished compiler/parsing/tests                                  32s 812MB
Jan 05 10:18:48 Starting compiler/inference/tests
Jan 05 10:27:44 Finished compiler/inference/tests                              8m55s   3GB
Jan 05 10:27:44 Starting compiler/printing/test
Jan 05 10:31:45 Finished compiler/printing/test                                4m01s   3GB
Jan 05 10:31:45 Starting icing/flover
Jan 05 11:15:32 Finished icing/flover                                         43m46s   2GB
Jan 05 11:15:32 Starting icing/
Jan 05 12:09:55 Finished icing/                                               54m22s   7GB
Jan 05 12:09:55 Starting icing/examples
Jan 05 12:11:34 Finished icing/examples                                        1m38s   3GB
Jan 05 12:11:34 Starting compiler/repl
Jan 05 12:20:21 Finished compiler/repl                                         8m45s   5GB
Jan 05 12:20:21 Starting unverified/sexpr-bootstrap/x64/64
Jan 05 12:33:52 Finished unverified/sexpr-bootstrap/x64/64                    13m31s  14GB
Jan 05 12:33:52 Starting unverified/sexpr-bootstrap/x64/32
Jan 05 12:44:52 Finished unverified/sexpr-bootstrap/x64/32                    10m59s  11GB
Jan 05 12:44:52 Starting compiler/benchmarks
Jan 05 13:00:28 Finished compiler/benchmarks                                  15m35s   2GB
Jan 05 13:00:28 Starting compiler/bootstrap/compilation/x64/64
Jan 06 01:21:43 Finished compiler/bootstrap/compilation/x64/64             12h21m15s  64GB
Jan 06 01:21:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 06 01:42:44 Finished compiler/bootstrap/compilation/x64/64/proofs         21m00s  38GB
Jan 06 01:42:44 Starting compiler/bootstrap/compilation/x64/32
Jan 06 08:53:17 Finished compiler/bootstrap/compilation/x64/32              7h10m33s  64GB
Jan 06 08:53:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 06 08:56:08 Finished compiler/bootstrap/compilation/x64/32/proofs          2m50s  14GB
Jan 06 08:56:08 Starting compiler/bootstrap/compilation/ag32/32
Jan 06 16:15:15 Finished compiler/bootstrap/compilation/ag32/32             7h19m06s  64GB
Jan 06 16:15:15 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 06 16:21:59 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover/compute[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32[0m
Scanned 100 directories
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                                                                                   (0s)     OK
ag32BootstrapProofTheory                                                                                  (374s)FAIL<1>
 is_ag32_init_state
   (init_memory code data (extcalls cake_config.lab_conf.ffi_names) (cl,inp))
   ms0 
 installed code 0 data 0 cake_config.lab_conf.ffi_names
   (heap_regs ag32_backend_config.stack_conf.reg_names) cake_machine_config
   (FUNPOW Next (cake_startup_clock ms0 inp cl) ms0)
 
 failed.
 Failed to prove theorem cake_installed.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 154)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}