Job 2268

CakeML:57af409c48bbfc4c3103e2702259d492ce97b29a
  Attempt at a fix [Jan 11 10:19:07]
#976 (ffiname)
Merging into:45534e558612704f938386fc12b79bc991c3afa3
  Update for new year [Jan 01 02:20:21]
HOL:c4c8009f7184d24a396e2e2022881013a002dd10
  Lift, tweak and publish some tailrecLib code [Jan 08 05:49:29]
Machine:pavlova

Jan 13 07:49:54 Claimed job
Jan 13 07:49:59 Reusing HOL
Jan 13 07:50:09 Starting developers
Jan 13 07:50:13 Finished developers                                               2s 197MB
Jan 13 07:50:13 Starting developers/bin
Jan 13 07:50:24 Finished developers/bin                                           9s   1GB
Jan 13 07:50:25 Starting compiler/proofs
Jan 13 09:32:21 Finished compiler/proofs                                    1h41m54s  30GB
Jan 13 09:32:21 Starting compiler/bootstrap/translation
Jan 13 17:34:41 Finished compiler/bootstrap/translation                     8h02m18s  72GB
Jan 13 17:34:42 Starting semantics/ffi
Jan 13 17:34:51 Finished semantics/ffi                                            7s 584MB
Jan 13 17:34:51 Starting semantics
Jan 13 17:34:53 Finished semantics                                                0s  60MB
Jan 13 17:34:54 Starting semantics/proofs
Jan 13 17:35:29 Finished semantics/proofs                                        34s   2GB
Jan 13 17:35:30 Starting semantics/alt_semantics
Jan 13 17:36:10 Finished semantics/alt_semantics                                 39s   1GB
Jan 13 17:36:11 Starting semantics/alt_semantics/proofs
Jan 13 17:47:12 Finished semantics/alt_semantics/proofs                       11m00s   4GB
Jan 13 17:47:13 Starting basis/pure
Jan 13 17:47:14 Finished basis/pure                                               0s  66MB
Jan 13 17:47:15 Starting translator
Jan 13 17:48:56 Finished translator                                            1m40s   3GB
Jan 13 17:48:57 Starting compiler/parsing
Jan 13 17:48:58 Finished compiler/parsing                                         0s  73MB
Jan 13 17:48:59 Starting characteristic
Jan 13 17:49:01 Finished characteristic                                           0s  88MB
Jan 13 17:49:02 Starting translator/monadic
Jan 13 17:49:03 Finished translator/monadic                                       0s  95MB
Jan 13 17:49:04 Starting basis
Jan 13 17:52:40 Finished basis                                                 3m34s   5GB
Jan 13 17:52:41 Starting compiler/inference
Jan 13 17:52:42 Finished compiler/inference                                       0s  79MB
Jan 13 17:52:43 Starting compiler/backend/reg_alloc
Jan 13 17:52:44 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 13 17:52:45 Starting compiler/backend/gc
Jan 13 17:52:47 Finished compiler/backend/gc                                      0s 137MB
Jan 13 17:52:48 Starting compiler/backend
Jan 13 17:53:04 Finished compiler/backend                                        15s   1GB
Jan 13 17:53:05 Starting compiler/encoders/asm
Jan 13 17:53:06 Finished compiler/encoders/asm                                    0s  91MB
Jan 13 17:53:07 Starting compiler/encoders/x64
Jan 13 17:53:09 Finished compiler/encoders/x64                                    0s  94MB
Jan 13 17:53:10 Starting compiler/encoders/arm7
Jan 13 17:53:11 Finished compiler/encoders/arm7                                   0s  94MB
Jan 13 17:53:12 Starting compiler/encoders/arm8
Jan 13 17:53:13 Finished compiler/encoders/arm8                                   0s  93MB
Jan 13 17:53:14 Starting compiler/encoders/arm8_asl
Jan 13 17:55:33 Finished compiler/encoders/arm8_asl                            2m17s   1GB
Jan 13 17:55:34 Starting compiler/encoders/mips
Jan 13 17:55:35 Finished compiler/encoders/mips                                   0s  92MB
Jan 13 17:55:36 Starting compiler/encoders/riscv
Jan 13 17:55:37 Finished compiler/encoders/riscv                                  0s  91MB
Jan 13 17:55:38 Starting compiler/encoders/ag32
Jan 13 17:55:40 Finished compiler/encoders/ag32                                   0s  85MB
Jan 13 17:55:41 Starting compiler/backend/x64
Jan 13 17:55:42 Finished compiler/backend/x64                                     0s 128MB
Jan 13 17:55:43 Starting compiler/backend/arm7
Jan 13 17:55:45 Finished compiler/backend/arm7                                    0s 128MB
Jan 13 17:55:46 Starting compiler/backend/arm8
Jan 13 17:55:47 Finished compiler/backend/arm8                                    0s 121MB
Jan 13 17:55:48 Starting compiler/backend/mips
Jan 13 17:55:50 Finished compiler/backend/mips                                    0s 121MB
Jan 13 17:55:51 Starting compiler/backend/riscv
Jan 13 17:55:52 Finished compiler/backend/riscv                                   0s 121MB
Jan 13 17:55:53 Starting compiler/backend/ag32
Jan 13 17:57:11 Finished compiler/backend/ag32                                 1m16s   2GB
Jan 13 17:57:12 Starting compiler/parsing/proofs
Jan 13 17:57:13 Finished compiler/parsing/proofs                                  0s  75MB
Jan 13 17:57:14 Starting compiler/inference/proofs
Jan 13 17:57:15 Finished compiler/inference/proofs                                0s  85MB
Jan 13 17:57:16 Starting compiler/backend/semantics
Jan 13 17:58:43 Finished compiler/backend/semantics                            1m25s   3GB
Jan 13 17:58:44 Starting compiler/backend/reg_alloc/proofs
Jan 13 17:58:46 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Jan 13 17:58:46 Starting compiler/backend/proofs
Jan 13 17:59:48 Finished compiler/backend/proofs                               1m00s   3GB
Jan 13 17:59:49 Starting compiler/backend/serialiser
Jan 13 17:59:51 Finished compiler/backend/serialiser                              1s 201MB
Jan 13 17:59:52 Starting compiler/encoders/x64/proofs
Jan 13 18:09:13 Finished compiler/encoders/x64/proofs                          9m20s   5GB
Jan 13 18:09:14 Starting compiler/encoders/arm7/proofs
Jan 13 18:21:59 Finished compiler/encoders/arm7/proofs                        12m43s   9GB
Jan 13 18:21:59 Starting compiler/encoders/arm8/proofs
Jan 13 18:28:43 Finished compiler/encoders/arm8/proofs                         6m42s   5GB
Jan 13 18:28:44 Starting compiler/encoders/arm8_asl/proofs
Jan 13 18:42:51 Finished compiler/encoders/arm8_asl/proofs                    14m05s   4GB
Jan 13 18:42:52 Starting compiler/encoders/mips/proofs
Jan 13 18:52:53 Finished compiler/encoders/mips/proofs                        10m00s   6GB
Jan 13 18:52:54 Starting compiler/encoders/riscv/proofs
Jan 13 19:01:21 Finished compiler/encoders/riscv/proofs                        8m26s   7GB
Jan 13 19:01:22 Starting compiler/encoders/ag32/proofs
Jan 13 19:03:45 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Jan 13 19:03:45 Starting compiler/backend/x64/proofs
Jan 13 19:04:25 Finished compiler/backend/x64/proofs                             39s   3GB
Jan 13 19:04:26 Starting compiler/backend/arm7/proofs
Jan 13 19:05:08 Finished compiler/backend/arm7/proofs                            41s   2GB
Jan 13 19:05:09 Starting compiler/backend/arm8/proofs
Jan 13 19:05:50 Finished compiler/backend/arm8/proofs                            39s   3GB
Jan 13 19:05:50 Starting compiler/backend/arm8_asl
Jan 13 19:06:20 Finished compiler/backend/arm8_asl                               28s   2GB
Jan 13 19:06:21 Starting compiler/backend/mips/proofs
Jan 13 19:07:04 Finished compiler/backend/mips/proofs                            41s   3GB
Jan 13 19:07:05 Starting compiler/backend/riscv/proofs
Jan 13 19:07:53 Finished compiler/backend/riscv/proofs                           47s   4GB
Jan 13 19:07:54 Starting compiler/backend/ag32/proofs
Jan 13 19:21:04 Finished compiler/backend/ag32/proofs                         13m08s   6GB
Jan 13 19:21:05 Starting candle/set-theory
Jan 13 19:21:49 Finished candle/set-theory                                       43s   1GB
Jan 13 19:21:50 Starting candle/syntax-lib
Jan 13 19:21:51 Finished candle/syntax-lib                                        0s  72MB
Jan 13 19:21:52 Starting candle/standard/syntax
Jan 13 19:22:08 Finished candle/standard/syntax                                  15s   1GB
Jan 13 19:22:09 Starting candle/standard/semantics
Jan 13 19:24:31 Finished candle/standard/semantics                             2m20s   2GB
Jan 13 19:24:32 Starting candle/standard/monadic
Jan 13 19:24:33 Finished candle/standard/monadic                                  0s 104MB
Jan 13 19:24:34 Starting candle/standard/ml_kernel
Jan 13 19:26:22 Finished candle/standard/ml_kernel                             1m47s   5GB
Jan 13 19:26:23 Starting candle/overloading/syntax
Jan 13 19:29:44 Finished candle/overloading/syntax                             3m19s   3GB
Jan 13 19:29:44 Starting candle/overloading/semantics
Jan 13 19:40:59 Finished candle/overloading/semantics                         11m13s   5GB
Jan 13 19:41:00 Starting candle/overloading/monadic
Jan 13 19:43:32 Finished candle/overloading/monadic                            2m30s   2GB
Jan 13 19:43:33 Starting candle/overloading/ml_kernel
Jan 13 19:51:10 Finished candle/overloading/ml_kernel                          7m35s   7GB
Jan 13 19:51:10 Starting candle/overloading/ml_checker
Jan 13 19:53:43 Finished candle/overloading/ml_checker                         2m31s   6GB
Jan 13 19:53:44 Starting candle/prover
Jan 13 20:03:36 Finished candle/prover                                         9m51s   5GB
Jan 13 20:03:37 Starting pancake
Jan 13 20:04:39 Finished pancake                                               1m00s   1GB
Jan 13 20:04:39 Starting pancake/ffi
Jan 13 20:04:40 Finished pancake/ffi                                              0s  21MB
Jan 13 20:04:41 Starting pancake/semantics
Jan 13 20:07:07 Finished pancake/semantics                                     2m24s   2GB
Jan 13 20:07:08 Starting pancake/parser
Jan 13 20:07:35 Finished pancake/parser                                          26s   2GB
Jan 13 20:07:36 Starting pancake/proofs
Jan 13 20:37:13 Finished pancake/proofs                                       29m36s   9GB
Jan 13 20:37:14 Starting characteristic/examples
Jan 13 20:38:51 Finished characteristic/examples                               1m35s   6GB
Jan 13 20:38:51 Starting tutorial/solutions
Jan 13 20:54:26 Finished tutorial/solutions                                   15m33s  17GB
Jan 13 20:54:27 Starting translator/monadic/examples
Jan 13 20:58:09 Finished translator/monadic/examples                           3m41s   5GB
Jan 13 20:58:10 Starting examples
Jan 13 21:12:27 Finished examples                                             14m15s   8GB
Jan 13 21:12:27 Starting examples/compilation/x64
Jan 13 23:10:21 Finished examples/compilation/x64                           1h57m52s  35GB
Jan 13 23:10:22 Starting examples/compilation/x64/proofs
Jan 13 23:14:08 Finished examples/compilation/x64/proofs                       3m44s   6GB
Jan 13 23:14:09 Starting examples/compilation/ag32
Jan 13 23:43:48 Finished examples/compilation/ag32                            29m38s   9GB
Jan 13 23:43:49 Starting examples/compilation/ag32/proofs
Jan 13 23:45:16 Finished examples/compilation/ag32/proofs                      1m25s   7GB
Jan 13 23:45:16 Starting examples/compilation/to_word
Jan 13 23:49:12 Finished examples/compilation/to_word                          3m54s  13GB
Jan 13 23:49:13 Starting examples/lpr_checker
Jan 13 23:50:29 Finished examples/lpr_checker                                  1m15s   2GB
Jan 13 23:50:30 Starting examples/lpr_checker/array
Jan 14 00:19:37 Finished examples/lpr_checker/array                           29m05s  11GB
Jan 14 00:19:38 Starting examples/lpr_checker/array/compilation
Jan 14 00:53:22 Finished examples/lpr_checker/array/compilation               33m43s  49GB
Jan 14 00:53:23 Starting examples/lpr_checker/array/compilation/proofs
Jan 14 00:55:16 Finished examples/lpr_checker/array/compilation/proofs         1m52s  10GB
Jan 14 00:55:17 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 14 01:07:57 Finished examples/lpr_checker/array/compilation/proofsARM8    12m38s  38GB
Jan 14 01:07:57 Starting examples/pseudo_bool
Jan 14 01:09:57 Finished examples/pseudo_bool                                  1m58s   2GB
Jan 14 01:09:58 Starting examples/pseudo_bool/cnf_encoding
Jan 14 01:10:33 Finished examples/pseudo_bool/cnf_encoding                       33s   1GB
Jan 14 01:10:34 Starting examples/pseudo_bool/graph_encoding
Jan 14 01:11:22 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Jan 14 01:11:23 Starting examples/pseudo_bool/array
Jan 14 02:01:33 Finished examples/pseudo_bool/array                           50m09s  15GB
Jan 14 02:01:34 Starting examples/pseudo_bool/array/compilation
Jan 14 03:49:37 Finished examples/pseudo_bool/array/compilation             1h48m02s 131GB
Jan 14 03:49:38 Starting examples/pseudo_bool/array/compilation/proofs
Jan 14 03:52:42 Finished examples/pseudo_bool/array/compilation/proofs         3m02s   7GB
Jan 14 03:52:43 Starting examples/opentheory
Jan 14 04:03:17 Finished examples/opentheory                                  10m33s   8GB
Jan 14 04:03:18 Starting examples/opentheory
Jan 14 04:03:20 Finished examples/opentheory                                      0s 133MB
Jan 14 04:03:21 Starting examples/opentheory/compilation
Jan 14 04:38:55 Finished examples/opentheory/compilation                      35m33s  54GB
Jan 14 04:38:56 Starting examples/opentheory/compilation/proofs
Jan 14 04:40:28 Finished examples/opentheory/compilation/proofs                1m30s   5GB
Jan 14 04:40:29 Starting examples/opentheory/compilation/ag32
Jan 14 05:11:57 Finished examples/opentheory/compilation/ag32                 31m26s  46GB
Jan 14 05:11:57 Starting examples/opentheory/compilation/ag32/proofs
Jan 14 05:14:23 Finished examples/opentheory/compilation/ag32/proofs           2m24s   9GB
Jan 14 05:14:23 Starting examples/sat_encodings
Jan 14 05:16:58 Finished examples/sat_encodings                                2m33s   1GB
Jan 14 05:16:59 Starting examples/sat_encodings/case_studies
Jan 14 05:18:56 Finished examples/sat_encodings/case_studies                   1m55s   2GB
Jan 14 05:18:57 Starting examples/sat_encodings/translation
Jan 14 05:25:04 Finished examples/sat_encodings/translation                    6m06s   7GB
Jan 14 05:25:05 Starting examples/sat_encodings/translation/compilation
Jan 14 05:59:54 Finished examples/sat_encodings/translation/compilation       34m47s  46GB
Jan 14 05:59:54 Starting examples/deflate
Jan 14 06:01:10 Finished examples/deflate                                      1m14s   1GB
Jan 14 06:01:11 Starting examples/deflate/translation
Jan 14 06:02:47 Finished examples/deflate/translation                          1m35s   7GB
Jan 14 06:02:48 Starting examples/deflate/translation/compilation
Jan 14 06:19:41 Finished examples/deflate/translation/compilation             16m52s  22GB
Jan 14 06:19:42 Starting examples/vipr
Jan 14 06:23:42 Finished examples/vipr                                         3m59s   7GB
Jan 14 06:23:43 Starting examples/vipr/compilation
Jan 14 06:43:55 Finished examples/vipr/compilation                            20m11s  39GB
Jan 14 06:43:56 Starting translator/okasaki-examples
Jan 14 06:48:57 Finished translator/okasaki-examples                           5m00s   4GB
Jan 14 06:48:58 Starting translator/other-examples
Jan 14 06:50:07 Finished translator/other-examples                             1m07s   3GB
Jan 14 06:50:08 Starting compiler/parsing/tests
Jan 14 06:50:42 Finished compiler/parsing/tests                                  33s   1GB
Jan 14 06:50:43 Starting compiler/inference/tests
Jan 14 06:58:17 Finished compiler/inference/tests                              7m33s   7GB
Jan 14 06:58:18 Starting compiler/printing/test
Jan 14 07:01:48 Finished compiler/printing/test                                3m29s   5GB
Jan 14 07:01:49 Starting icing/flover
Jan 14 07:37:34 Finished icing/flover                                         35m44s   4GB
Jan 14 07:37:35 Starting icing/
Jan 14 08:32:57 Finished icing/                                               55m21s  34GB
Jan 14 08:32:58 Starting icing/examples
Jan 14 08:34:41 Finished icing/examples                                        1m41s   8GB
Jan 14 08:34:41 Starting compiler/repl
Jan 14 08:43:23 Finished compiler/repl                                         8m40s  10GB
Jan 14 08:43:24 Starting unverified/sexpr-bootstrap/x64/64
Jan 14 08:54:25 Finished unverified/sexpr-bootstrap/x64/64                    11m00s  16GB
Jan 14 08:54:26 Starting unverified/sexpr-bootstrap/x64/32
Jan 14 09:03:21 Finished unverified/sexpr-bootstrap/x64/32                     8m54s  13GB
Jan 14 09:03:22 Starting compiler/benchmarks
Jan 14 09:04:07 Finished compiler/benchmarks                                     43s 713MB
Jan 14 09:04:08 Starting compiler/bootstrap/compilation/x64/64
Jan 14 23:21:43 Finished compiler/bootstrap/compilation/x64/64             14h17m33s 154GB
Jan 14 23:21:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 14 23:42:33 Finished compiler/bootstrap/compilation/x64/64/proofs         20m48s  41GB
Jan 14 23:42:34 Starting compiler/bootstrap/compilation/x64/32
Jan 15 06:55:41 Finished compiler/bootstrap/compilation/x64/32              7h13m05s 129GB
Jan 15 06:55:42 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 15 06:59:15 Finished compiler/bootstrap/compilation/x64/32/proofs          3m32s  19GB
Jan 15 06:59:16 Starting compiler/bootstrap/compilation/ag32/32
Jan 15 14:38:35 Finished compiler/bootstrap/compilation/ag32/32             7h39m18s 138GB
Jan 15 14:38:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 15 14:45:26 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                                          (371s)FAIL<1>
   (FUNPOW Next (cake_startup_clock ms0 inp cl) ms0)
 
 failed.
 Failed to prove theorem cake_installed.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match (THEN1 on line 154)
 error in quse /scratch/cakeml/regression/cakeml-2268/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml : HOL_ERR {message = "No match (THEN1 on line 154)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /scratch/cakeml/regression/cakeml-2268/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript : HOL_ERR {message = "No match (THEN1 on line 154)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 154)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}