Job 2267

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:c4c8009f7184d24a396e2e2022881013a002dd10
  Lift, tweak and publish some tailrecLib code [Jan 08 05:49:29]
Machine:pavlova

Jan 10 21:13:46 Claimed job
Jan 10 21:13:51 Building HOL
Jan 10 21:28:28 Starting developers
Jan 10 21:28:31 Finished developers                                               2s 213MB
Jan 10 21:28:32 Starting developers/bin
Jan 10 21:28:43 Finished developers/bin                                           9s   1GB
Jan 10 21:28:44 Starting compiler/proofs
Jan 10 23:13:46 Finished compiler/proofs                                    1h45m00s  29GB
Jan 10 23:13:47 Starting compiler/bootstrap/translation
Jan 11 07:25:14 Finished compiler/bootstrap/translation                     8h11m26s  69GB
Jan 11 07:25:15 Starting semantics/ffi
Jan 11 07:25:24 Finished semantics/ffi                                            7s 580MB
Jan 11 07:25:25 Starting semantics
Jan 11 07:25:26 Finished semantics                                                0s  60MB
Jan 11 07:25:27 Starting semantics/proofs
Jan 11 07:26:01 Finished semantics/proofs                                        33s   1GB
Jan 11 07:26:02 Starting semantics/alt_semantics
Jan 11 07:26:42 Finished semantics/alt_semantics                                 38s   1GB
Jan 11 07:26:43 Starting semantics/alt_semantics/proofs
Jan 11 07:37:44 Finished semantics/alt_semantics/proofs                       11m00s   5GB
Jan 11 07:37:45 Starting basis/pure
Jan 11 07:37:46 Finished basis/pure                                               0s  66MB
Jan 11 07:37:47 Starting translator
Jan 11 07:39:35 Finished translator                                            1m47s   4GB
Jan 11 07:39:36 Starting compiler/parsing
Jan 11 07:39:38 Finished compiler/parsing                                         0s  73MB
Jan 11 07:39:38 Starting characteristic
Jan 11 07:39:40 Finished characteristic                                           0s  90MB
Jan 11 07:39:41 Starting translator/monadic
Jan 11 07:39:42 Finished translator/monadic                                       0s  90MB
Jan 11 07:39:43 Starting basis
Jan 11 07:43:20 Finished basis                                                 3m35s   5GB
Jan 11 07:43:21 Starting compiler/inference
Jan 11 07:43:22 Finished compiler/inference                                       0s  85MB
Jan 11 07:43:23 Starting compiler/backend/reg_alloc
Jan 11 07:43:24 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 11 07:43:25 Starting compiler/backend/gc
Jan 11 07:43:27 Finished compiler/backend/gc                                      0s 138MB
Jan 11 07:43:27 Starting compiler/backend
Jan 11 07:43:45 Finished compiler/backend                                        16s   1GB
Jan 11 07:43:46 Starting compiler/encoders/asm
Jan 11 07:43:47 Finished compiler/encoders/asm                                    0s  91MB
Jan 11 07:43:48 Starting compiler/encoders/x64
Jan 11 07:43:49 Finished compiler/encoders/x64                                    0s  93MB
Jan 11 07:43:50 Starting compiler/encoders/arm7
Jan 11 07:43:52 Finished compiler/encoders/arm7                                   0s  95MB
Jan 11 07:43:52 Starting compiler/encoders/arm8
Jan 11 07:43:54 Finished compiler/encoders/arm8                                   0s  91MB
Jan 11 07:43:55 Starting compiler/encoders/arm8_asl
Jan 11 10:04:03 Finished compiler/encoders/arm8_asl                         2h20m07s  44GB
Jan 11 10:04:04 Starting compiler/encoders/mips
Jan 11 10:04:06 Finished compiler/encoders/mips                                   0s  87MB
Jan 11 10:04:06 Starting compiler/encoders/riscv
Jan 11 10:04:08 Finished compiler/encoders/riscv                                  0s  88MB
Jan 11 10:04:09 Starting compiler/encoders/ag32
Jan 11 10:04:10 Finished compiler/encoders/ag32                                   0s  85MB
Jan 11 10:04:11 Starting compiler/backend/x64
Jan 11 10:04:13 Finished compiler/backend/x64                                     0s 129MB
Jan 11 10:04:13 Starting compiler/backend/arm7
Jan 11 10:04:15 Finished compiler/backend/arm7                                    0s 129MB
Jan 11 10:04:16 Starting compiler/backend/arm8
Jan 11 10:04:18 Finished compiler/backend/arm8                                    0s 129MB
Jan 11 10:04:18 Starting compiler/backend/mips
Jan 11 10:04:20 Finished compiler/backend/mips                                    0s 129MB
Jan 11 10:04:21 Starting compiler/backend/riscv
Jan 11 10:04:23 Finished compiler/backend/riscv                                   0s 129MB
Jan 11 10:04:23 Starting compiler/backend/ag32
Jan 11 10:05:44 Finished compiler/backend/ag32                                 1m19s   2GB
Jan 11 10:05:45 Starting compiler/parsing/proofs
Jan 11 10:05:46 Finished compiler/parsing/proofs                                  0s  75MB
Jan 11 10:05:47 Starting compiler/inference/proofs
Jan 11 10:05:49 Finished compiler/inference/proofs                                0s  86MB
Jan 11 10:05:49 Starting compiler/backend/semantics
Jan 11 10:07:17 Finished compiler/backend/semantics                            1m26s   3GB
Jan 11 10:07:18 Starting compiler/backend/reg_alloc/proofs
Jan 11 10:07:19 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jan 11 10:07:20 Starting compiler/backend/proofs
Jan 11 10:08:23 Finished compiler/backend/proofs                               1m01s   3GB
Jan 11 10:08:24 Starting compiler/backend/serialiser
Jan 11 10:08:26 Finished compiler/backend/serialiser                              1s 183MB
Jan 11 10:08:27 Starting compiler/encoders/x64/proofs
Jan 11 10:17:57 Finished compiler/encoders/x64/proofs                          9m29s   5GB
Jan 11 10:17:58 Starting compiler/encoders/arm7/proofs
Jan 11 10:30:44 Finished compiler/encoders/arm7/proofs                        12m45s   5GB
Jan 11 10:30:45 Starting compiler/encoders/arm8/proofs
Jan 11 10:37:16 Finished compiler/encoders/arm8/proofs                         6m30s   4GB
Jan 11 10:37:17 Starting compiler/encoders/arm8_asl/proofs
Jan 11 11:25:06 Finished compiler/encoders/arm8_asl/proofs                    47m47s  12GB
Jan 11 11:25:07 Starting compiler/encoders/mips/proofs
Jan 11 11:35:05 Finished compiler/encoders/mips/proofs                         9m57s   7GB
Jan 11 11:35:06 Starting compiler/encoders/riscv/proofs
Jan 11 11:43:36 Finished compiler/encoders/riscv/proofs                        8m29s   4GB
Jan 11 11:43:37 Starting compiler/encoders/ag32/proofs
Jan 11 11:45:59 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Jan 11 11:46:00 Starting compiler/backend/x64/proofs
Jan 11 11:46:41 Finished compiler/backend/x64/proofs                             39s   2GB
Jan 11 11:46:42 Starting compiler/backend/arm7/proofs
Jan 11 11:47:24 Finished compiler/backend/arm7/proofs                            41s   2GB
Jan 11 11:47:25 Starting compiler/backend/arm8/proofs
Jan 11 11:48:03 Finished compiler/backend/arm8/proofs                            37s   2GB
Jan 11 11:48:04 Starting compiler/backend/arm8_asl
Jan 11 11:48:33 Finished compiler/backend/arm8_asl                               27s   2GB
Jan 11 11:48:34 Starting compiler/backend/mips/proofs
Jan 11 11:49:16 Finished compiler/backend/mips/proofs                            41s   3GB
Jan 11 11:49:17 Starting compiler/backend/riscv/proofs
Jan 11 11:50:07 Finished compiler/backend/riscv/proofs                           48s   4GB
Jan 11 11:50:07 Starting compiler/backend/ag32/proofs
Jan 11 12:03:20 Finished compiler/backend/ag32/proofs                         13m11s   6GB
Jan 11 12:03:21 Starting candle/set-theory
Jan 11 12:04:06 Finished candle/set-theory                                       44s   1GB
Jan 11 12:04:07 Starting candle/syntax-lib
Jan 11 12:04:08 Finished candle/syntax-lib                                        0s  67MB
Jan 11 12:04:09 Starting candle/standard/syntax
Jan 11 12:04:25 Finished candle/standard/syntax                                  15s   1GB
Jan 11 12:04:26 Starting candle/standard/semantics
Jan 11 12:06:49 Finished candle/standard/semantics                             2m21s   3GB
Jan 11 12:06:50 Starting candle/standard/monadic
Jan 11 12:06:51 Finished candle/standard/monadic                                  0s 104MB
Jan 11 12:06:52 Starting candle/standard/ml_kernel
Jan 11 12:08:41 Finished candle/standard/ml_kernel                             1m47s   5GB
Jan 11 12:08:42 Starting candle/overloading/syntax
Jan 11 12:12:03 Finished candle/overloading/syntax                             3m20s   3GB
Jan 11 12:12:04 Starting candle/overloading/semantics
Jan 11 12:23:21 Finished candle/overloading/semantics                         11m15s   6GB
Jan 11 12:23:22 Starting candle/overloading/monadic
Jan 11 12:25:52 Finished candle/overloading/monadic                            2m29s   2GB
Jan 11 12:25:53 Starting candle/overloading/ml_kernel
Jan 11 12:33:28 Finished candle/overloading/ml_kernel                          7m34s   6GB
Jan 11 12:33:29 Starting candle/overloading/ml_checker
Jan 11 12:36:02 Finished candle/overloading/ml_checker                         2m31s   6GB
Jan 11 12:36:03 Starting candle/prover
Jan 11 12:45:56 Finished candle/prover                                         9m52s   5GB
Jan 11 12:45:57 Starting pancake
Jan 11 12:46:57 Finished pancake                                                 59s   1GB
Jan 11 12:46:58 Starting pancake/ffi
Jan 11 12:46:59 Finished pancake/ffi                                              0s  20MB
Jan 11 12:47:00 Starting pancake/semantics
Jan 11 12:49:29 Finished pancake/semantics                                     2m28s   2GB
Jan 11 12:49:30 Starting pancake/parser
Jan 11 12:49:57 Finished pancake/parser                                          26s   2GB
Jan 11 12:49:58 Starting pancake/proofs
Jan 11 13:19:32 Finished pancake/proofs                                       29m33s   8GB
Jan 11 13:19:33 Starting characteristic/examples
Jan 11 13:21:08 Finished characteristic/examples                               1m34s   6GB
Jan 11 13:21:09 Starting tutorial/solutions
Jan 11 13:37:06 Finished tutorial/solutions                                   15m55s  17GB
Jan 11 13:37:07 Starting translator/monadic/examples
Jan 11 13:40:50 Finished translator/monadic/examples                           3m41s   4GB
Jan 11 13:40:50 Starting examples
Jan 11 13:55:22 Finished examples                                             14m30s   7GB
Jan 11 13:55:23 Starting examples/compilation/x64
Jan 11 15:52:24 Finished examples/compilation/x64                           1h57m00s  34GB
Jan 11 15:52:25 Starting examples/compilation/x64/proofs
Jan 11 15:56:15 Finished examples/compilation/x64/proofs                       3m49s   6GB
Jan 11 15:56:16 Starting examples/compilation/ag32
Jan 11 16:25:41 Finished examples/compilation/ag32                            29m23s  10GB
Jan 11 16:25:42 Starting examples/compilation/ag32/proofs
Jan 11 16:27:13 Finished examples/compilation/ag32/proofs                      1m29s   6GB
Jan 11 16:27:14 Starting examples/compilation/to_word
Jan 11 16:31:02 Finished examples/compilation/to_word                          3m47s  11GB
Jan 11 16:31:03 Starting examples/lpr_checker
Jan 11 16:32:19 Finished examples/lpr_checker                                  1m15s   2GB
Jan 11 16:32:20 Starting examples/lpr_checker/array
Jan 11 17:01:37 Finished examples/lpr_checker/array                           29m15s   8GB
Jan 11 17:01:38 Starting examples/lpr_checker/array/compilation
Jan 11 17:35:29 Finished examples/lpr_checker/array/compilation               33m50s  76GB
Jan 11 17:35:30 Starting examples/lpr_checker/array/compilation/proofs
Jan 11 17:37:22 Finished examples/lpr_checker/array/compilation/proofs         1m50s   9GB
Jan 11 17:37:22 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 11 17:50:26 Finished examples/lpr_checker/array/compilation/proofsARM8    13m02s  38GB
Jan 11 17:50:27 Starting examples/pseudo_bool
Jan 11 17:52:23 Finished examples/pseudo_bool                                  1m55s   1GB
Jan 11 17:52:24 Starting examples/pseudo_bool/cnf_encoding
Jan 11 17:52:58 Finished examples/pseudo_bool/cnf_encoding                       33s   1GB
Jan 11 17:52:59 Starting examples/pseudo_bool/graph_encoding
Jan 11 17:53:48 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Jan 11 17:53:49 Starting examples/pseudo_bool/array
Jan 11 18:44:10 Finished examples/pseudo_bool/array                           50m20s  16GB
Jan 11 18:44:11 Starting examples/pseudo_bool/array/compilation
Jan 11 20:29:20 Finished examples/pseudo_bool/array/compilation             1h45m07s  85GB
Jan 11 20:29:21 Starting examples/pseudo_bool/array/compilation/proofs
Jan 11 20:32:28 Finished examples/pseudo_bool/array/compilation/proofs         3m06s   7GB
Jan 11 20:32:29 Starting examples/opentheory
Jan 11 20:42:59 Finished examples/opentheory                                  10m28s   4GB
Jan 11 20:42:59 Starting examples/opentheory
Jan 11 20:43:01 Finished examples/opentheory                                      0s 123MB
Jan 11 20:43:02 Starting examples/opentheory/compilation
Jan 11 21:18:29 Finished examples/opentheory/compilation                      35m25s  50GB
Jan 11 21:18:30 Starting examples/opentheory/compilation/proofs
Jan 11 21:19:55 Finished examples/opentheory/compilation/proofs                1m24s   6GB
Jan 11 21:19:55 Starting examples/opentheory/compilation/ag32
Jan 11 21:52:03 Finished examples/opentheory/compilation/ag32                 32m07s  56GB
Jan 11 21:52:04 Starting examples/opentheory/compilation/ag32/proofs
Jan 11 21:54:21 Finished examples/opentheory/compilation/ag32/proofs           2m16s  11GB
Jan 11 21:54:22 Starting examples/sat_encodings
Jan 11 21:56:59 Finished examples/sat_encodings                                2m35s   1GB
Jan 11 21:56:59 Starting examples/sat_encodings/case_studies
Jan 11 21:58:58 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Jan 11 21:58:58 Starting examples/sat_encodings/translation
Jan 11 22:05:02 Finished examples/sat_encodings/translation                    6m02s   7GB
Jan 11 22:05:03 Starting examples/sat_encodings/translation/compilation
Jan 11 22:40:33 Finished examples/sat_encodings/translation/compilation       35m28s  34GB
Jan 11 22:40:33 Starting examples/deflate
Jan 11 22:41:47 Finished examples/deflate                                      1m12s   1GB
Jan 11 22:41:48 Starting examples/deflate/translation
Jan 11 22:43:30 Finished examples/deflate/translation                          1m41s   7GB
Jan 11 22:43:31 Starting examples/deflate/translation/compilation
Jan 11 23:00:15 Finished examples/deflate/translation/compilation             16m42s  21GB
Jan 11 23:00:16 Starting examples/vipr
Jan 11 23:04:19 Finished examples/vipr                                         4m01s   7GB
Jan 11 23:04:19 Starting examples/vipr/compilation
Jan 11 23:24:05 Finished examples/vipr/compilation                            19m44s  21GB
Jan 11 23:24:06 Starting translator/okasaki-examples
Jan 11 23:29:08 Finished translator/okasaki-examples                           5m00s   3GB
Jan 11 23:29:08 Starting translator/other-examples
Jan 11 23:32:47 Finished translator/other-examples                             3m38s   3GB
Jan 11 23:32:48 Starting compiler/parsing/tests
Jan 11 23:33:22 Finished compiler/parsing/tests                                  33s   1GB
Jan 11 23:33:23 Starting compiler/inference/tests
Jan 11 23:40:53 Finished compiler/inference/tests                              7m28s   5GB
Jan 11 23:40:54 Starting compiler/printing/test
Jan 11 23:44:22 Finished compiler/printing/test                                3m27s   6GB
Jan 11 23:44:23 Starting icing/flover
Jan 12 00:20:02 Finished icing/flover                                         35m38s   4GB
Jan 12 00:20:03 Starting icing/
Jan 12 01:16:22 Finished icing/                                               56m18s  32GB
Jan 12 01:16:23 Starting icing/examples
Jan 12 01:18:05 Finished icing/examples                                        1m41s   8GB
Jan 12 01:18:06 Starting compiler/repl
Jan 12 01:26:50 Finished compiler/repl                                         8m42s  10GB
Jan 12 01:26:51 Starting unverified/sexpr-bootstrap/x64/64
Jan 12 01:37:48 Finished unverified/sexpr-bootstrap/x64/64                    10m55s  15GB
Jan 12 01:37:49 Starting unverified/sexpr-bootstrap/x64/32
Jan 12 01:46:46 Finished unverified/sexpr-bootstrap/x64/32                     8m56s  14GB
Jan 12 01:46:47 Starting compiler/benchmarks
Jan 12 01:47:31 Finished compiler/benchmarks                                     43s 713MB
Jan 12 01:47:32 Starting compiler/bootstrap/compilation/x64/64
Jan 12 16:24:01 Finished compiler/bootstrap/compilation/x64/64             14h36m27s 150GB
Jan 12 16:24:02 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 12 16:44:49 Finished compiler/bootstrap/compilation/x64/64/proofs         20m46s  36GB
Jan 12 16:44:50 Starting compiler/bootstrap/compilation/x64/32
Jan 12 23:52:10 Finished compiler/bootstrap/compilation/x64/32              7h07m18s 123GB
Jan 12 23:52:11 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 12 23:55:43 Finished compiler/bootstrap/compilation/x64/32/proofs          3m31s  19GB
Jan 12 23:55:44 Starting compiler/bootstrap/compilation/ag32/32
Jan 13 07:42:34 Finished compiler/bootstrap/compilation/ag32/32             7h46m49s 134GB
Jan 13 07:42:35 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 13 07:49:49 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                                          (388s)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-2267/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-2267/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"}