Job 2109

CakeML:adddeec230d4c4733e664b5565ab4def7bdd50cc
  pancake: update translation for new conv_Shape_def [Mar 07 03:46:40]
#927 (translation_update)
Merging into:a4a3f0b318b9eef32403ec5fbcc2157b8da0f120
  Merge pull request #930 from CakeML/print_app_list [Mar 03 21:23:14]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 07 07:46:14 Claimed job
Mar 07 07:46:17 Reusing HOL
Mar 07 07:46:57 Starting developers
Mar 07 07:47:02 Finished developers                                               5s 174MB
Mar 07 07:47:02 Starting developers/bin
Mar 07 07:47:08 Finished developers/bin                                           6s   1GB
Mar 07 07:47:08 Starting compiler/proofs
Mar 07 09:37:23 Finished compiler/proofs                                    1h50m13s  15GB
Mar 07 09:37:23 Starting compiler/bootstrap/translation
Mar 07 18:26:57 Finished compiler/bootstrap/translation                     8h49m33s  31GB
Mar 07 18:26:57 Starting semantics/ffi
Mar 07 18:27:04 Finished semantics/ffi                                            6s 220MB
Mar 07 18:27:04 Starting semantics
Mar 07 18:27:05 Finished semantics                                                1s  18MB
Mar 07 18:27:06 Starting semantics/proofs
Mar 07 18:27:38 Finished semantics/proofs                                        32s 865MB
Mar 07 18:27:39 Starting semantics/alt_semantics
Mar 07 18:28:10 Finished semantics/alt_semantics                                 31s 841MB
Mar 07 18:28:11 Starting semantics/alt_semantics/proofs
Mar 07 18:40:07 Finished semantics/alt_semantics/proofs                       11m56s   2GB
Mar 07 18:40:07 Starting basis/pure
Mar 07 18:40:09 Finished basis/pure                                               1s  20MB
Mar 07 18:40:09 Starting translator
Mar 07 18:41:58 Finished translator                                            1m49s   1GB
Mar 07 18:41:59 Starting compiler/parsing
Mar 07 18:42:00 Finished compiler/parsing                                         1s  20MB
Mar 07 18:42:00 Starting characteristic
Mar 07 18:42:02 Finished characteristic                                           1s  22MB
Mar 07 18:42:02 Starting translator/monadic
Mar 07 18:42:04 Finished translator/monadic                                       1s  23MB
Mar 07 18:42:04 Starting basis
Mar 07 18:45:58 Finished basis                                                 3m53s   3GB
Mar 07 18:45:58 Starting compiler/inference
Mar 07 18:46:00 Finished compiler/inference                                       1s  25MB
Mar 07 18:46:00 Starting compiler/backend/reg_alloc
Mar 07 18:46:01 Finished compiler/backend/reg_alloc                               1s  18MB
Mar 07 18:46:02 Starting compiler/backend/gc
Mar 07 18:46:04 Finished compiler/backend/gc                                      2s  27MB
Mar 07 18:46:04 Starting compiler/backend
Mar 07 18:46:16 Finished compiler/backend                                        12s 568MB
Mar 07 18:46:17 Starting compiler/encoders/asm
Mar 07 18:46:18 Finished compiler/encoders/asm                                    1s  22MB
Mar 07 18:46:18 Starting compiler/encoders/x64
Mar 07 18:46:20 Finished compiler/encoders/x64                                    1s  22MB
Mar 07 18:46:20 Starting compiler/encoders/arm7
Mar 07 18:46:22 Finished compiler/encoders/arm7                                   1s  26MB
Mar 07 18:46:22 Starting compiler/encoders/arm8
Mar 07 18:46:24 Finished compiler/encoders/arm8                                   1s  20MB
Mar 07 18:46:24 Starting compiler/encoders/arm8_asl
Mar 07 18:49:38 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Mar 07 18:49:39 Starting compiler/encoders/mips
Mar 07 18:49:40 Finished compiler/encoders/mips                                   1s  24MB
Mar 07 18:49:40 Starting compiler/encoders/riscv
Mar 07 18:49:42 Finished compiler/encoders/riscv                                  1s  26MB
Mar 07 18:49:42 Starting compiler/encoders/ag32
Mar 07 18:49:44 Finished compiler/encoders/ag32                                   1s  22MB
Mar 07 18:49:44 Starting compiler/backend/x64
Mar 07 18:49:46 Finished compiler/backend/x64                                     2s  28MB
Mar 07 18:49:47 Starting compiler/backend/arm7
Mar 07 18:49:49 Finished compiler/backend/arm7                                    2s  22MB
Mar 07 18:49:49 Starting compiler/backend/arm8
Mar 07 18:49:51 Finished compiler/backend/arm8                                    2s  24MB
Mar 07 18:49:51 Starting compiler/backend/mips
Mar 07 18:49:53 Finished compiler/backend/mips                                    2s  27MB
Mar 07 18:49:54 Starting compiler/backend/riscv
Mar 07 18:49:56 Finished compiler/backend/riscv                                   2s  22MB
Mar 07 18:49:56 Starting compiler/backend/ag32
Mar 07 18:51:24 Finished compiler/backend/ag32                                 1m27s   1GB
Mar 07 18:51:24 Starting compiler/parsing/proofs
Mar 07 18:51:25 Finished compiler/parsing/proofs                                  1s  22MB
Mar 07 18:51:26 Starting compiler/inference/proofs
Mar 07 18:51:27 Finished compiler/inference/proofs                                1s  20MB
Mar 07 18:51:28 Starting compiler/backend/semantics
Mar 07 18:52:40 Finished compiler/backend/semantics                            1m12s   1GB
Mar 07 18:52:40 Starting compiler/backend/reg_alloc/proofs
Mar 07 18:52:42 Finished compiler/backend/reg_alloc/proofs                        1s  24MB
Mar 07 18:52:42 Starting compiler/backend/proofs
Mar 07 18:53:40 Finished compiler/backend/proofs                                 57s   3GB
Mar 07 18:53:40 Starting compiler/backend/serialiser
Mar 07 18:53:43 Finished compiler/backend/serialiser                              2s  34MB
Mar 07 18:53:43 Starting compiler/encoders/x64/proofs
Mar 07 19:03:32 Finished compiler/encoders/x64/proofs                          9m49s   5GB
Mar 07 19:03:33 Starting compiler/encoders/arm7/proofs
Mar 07 19:17:18 Finished compiler/encoders/arm7/proofs                        13m45s   4GB
Mar 07 19:17:18 Starting compiler/encoders/arm8/proofs
Mar 07 19:24:14 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Mar 07 19:24:14 Starting compiler/encoders/arm8_asl/proofs
Mar 07 19:40:00 Finished compiler/encoders/arm8_asl/proofs                    15m44s   2GB
Mar 07 19:40:00 Starting compiler/encoders/mips/proofs
Mar 07 19:50:46 Finished compiler/encoders/mips/proofs                        10m45s   2GB
Mar 07 19:50:46 Starting compiler/encoders/riscv/proofs
Mar 07 19:59:44 Finished compiler/encoders/riscv/proofs                        8m57s   2GB
Mar 07 19:59:44 Starting compiler/encoders/ag32/proofs
Mar 07 20:02:20 Finished compiler/encoders/ag32/proofs                         2m35s 992MB
Mar 07 20:02:20 Starting compiler/backend/x64/proofs
Mar 07 20:02:48 Finished compiler/backend/x64/proofs                             27s   1GB
Mar 07 20:02:48 Starting compiler/backend/arm7/proofs
Mar 07 20:03:21 Finished compiler/backend/arm7/proofs                            32s   2GB
Mar 07 20:03:21 Starting compiler/backend/arm8/proofs
Mar 07 20:03:52 Finished compiler/backend/arm8/proofs                            30s   1GB
Mar 07 20:03:52 Starting compiler/backend/arm8_asl
Mar 07 20:04:15 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 07 20:04:15 Starting compiler/backend/mips/proofs
Mar 07 20:04:46 Finished compiler/backend/mips/proofs                            30s   2GB
Mar 07 20:04:46 Starting compiler/backend/riscv/proofs
Mar 07 20:05:19 Finished compiler/backend/riscv/proofs                           32s   3GB
Mar 07 20:05:19 Starting compiler/backend/ag32/proofs
Mar 07 20:19:07 Finished compiler/backend/ag32/proofs                         13m47s   3GB
Mar 07 20:19:07 Starting candle/set-theory
Mar 07 20:19:45 Finished candle/set-theory                                       37s 922MB
Mar 07 20:19:45 Starting candle/syntax-lib
Mar 07 20:19:46 Finished candle/syntax-lib                                        1s  19MB
Mar 07 20:19:46 Starting candle/standard/syntax
Mar 07 20:19:57 Finished candle/standard/syntax                                  10s 599MB
Mar 07 20:19:57 Starting candle/standard/semantics
Mar 07 20:21:53 Finished candle/standard/semantics                             1m56s   1GB
Mar 07 20:21:53 Starting candle/standard/monadic
Mar 07 20:21:55 Finished candle/standard/monadic                                  1s  20MB
Mar 07 20:21:55 Starting candle/standard/ml_kernel
Mar 07 20:23:28 Finished candle/standard/ml_kernel                             1m32s   3GB
Mar 07 20:23:28 Starting candle/overloading/syntax
Mar 07 20:26:50 Finished candle/overloading/syntax                             3m21s   1GB
Mar 07 20:26:50 Starting candle/overloading/semantics
Mar 07 20:39:03 Finished candle/overloading/semantics                         12m12s   2GB
Mar 07 20:39:03 Starting candle/overloading/monadic
Mar 07 20:41:43 Finished candle/overloading/monadic                            2m39s   1GB
Mar 07 20:41:43 Starting candle/overloading/ml_kernel
Mar 07 20:49:28 Finished candle/overloading/ml_kernel                          7m44s   3GB
Mar 07 20:49:28 Starting candle/overloading/ml_checker
Mar 07 20:52:03 Finished candle/overloading/ml_checker                         2m34s   2GB
Mar 07 20:52:03 Starting candle/prover
Mar 07 21:01:56 Finished candle/prover                                         9m53s   3GB
Mar 07 21:01:57 Starting pancake
Mar 07 21:02:41 Finished pancake                                                 44s 885MB
Mar 07 21:02:41 Starting pancake/ffi
Mar 07 21:02:42 Finished pancake/ffi                                              0s  13MB
Mar 07 21:02:42 Starting pancake/semantics
Mar 07 21:05:12 Finished pancake/semantics                                     2m29s   1GB
Mar 07 21:05:12 Starting pancake/proofs
Mar 07 21:09:44 Finished pancake/proofs                                        4m31s   2GB
Mar 07 21:09:44 Starting characteristic/examples
Mar 07 21:11:18 Finished characteristic/examples                               1m34s   3GB
Mar 07 21:11:18 Starting tutorial/solutions
Mar 07 21:27:29 Finished tutorial/solutions                                   16m10s   9GB
Mar 07 21:27:29 Starting translator/monadic/examples
Mar 07 21:31:43 Finished translator/monadic/examples                           4m13s   3GB
Mar 07 21:31:43 Starting examples
Mar 07 21:49:55 Finished examples                                             18m11s   5GB
Mar 07 21:49:56 Starting examples/compilation/x64
Mar 07 23:57:25 Finished examples/compilation/x64                           2h07m28s  12GB
Mar 07 23:57:25 Starting examples/compilation/x64/proofs
Mar 07 23:59:57 Finished examples/compilation/x64/proofs                       2m31s   4GB
Mar 07 23:59:57 Starting examples/compilation/ag32
Mar 08 00:31:21 Finished examples/compilation/ag32                            31m23s  10GB
Mar 08 00:31:21 Starting examples/compilation/ag32/proofs
Mar 08 00:32:36 Finished examples/compilation/ag32/proofs                      1m14s   5GB
Mar 08 00:32:36 Starting examples/compilation/to_word
Mar 08 00:36:07 Finished examples/compilation/to_word                          3m30s   7GB
Mar 08 00:36:07 Starting examples/lpr_checker
Mar 08 00:37:15 Finished examples/lpr_checker                                  1m07s   1GB
Mar 08 00:37:15 Starting examples/lpr_checker/array
Mar 08 01:15:37 Finished examples/lpr_checker/array                           38m19s   6GB
Mar 08 01:15:37 Starting examples/lpr_checker/array/compilation
Mar 08 02:04:30 Finished examples/lpr_checker/array/compilation               48m53s  25GB
Mar 08 02:04:30 Starting examples/lpr_checker/array/compilation/proofs
Mar 08 02:07:04 Finished examples/lpr_checker/array/compilation/proofs         2m33s   3GB
Mar 08 02:07:04 Starting examples/opentheory
Mar 08 02:19:31 Finished examples/opentheory                                  12m25s   5GB
Mar 08 02:19:31 Starting examples/opentheory
Mar 08 02:19:33 Finished examples/opentheory                                      1s  23MB
Mar 08 02:19:33 Starting examples/opentheory/compilation
Mar 08 02:58:48 Finished examples/opentheory/compilation                      39m14s  25GB
Mar 08 02:58:48 Starting examples/opentheory/compilation/proofs
Mar 08 02:59:52 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Mar 08 02:59:52 Starting examples/opentheory/compilation/ag32
Mar 08 03:34:25 Finished examples/opentheory/compilation/ag32                 34m32s  25GB
Mar 08 03:34:26 Starting examples/opentheory/compilation/ag32/proofs
Mar 08 03:36:21 Finished examples/opentheory/compilation/ag32/proofs           1m55s   6GB
Mar 08 03:36:21 Starting examples/sat_encodings
Mar 08 03:38:26 Finished examples/sat_encodings                                2m04s 988MB
Mar 08 03:38:26 Starting examples/sat_encodings/case_studies
Mar 08 03:40:18 Finished examples/sat_encodings/case_studies                   1m51s   1GB
Mar 08 03:40:18 Starting examples/sat_encodings/translation
Mar 08 03:46:40 Finished examples/sat_encodings/translation                    6m21s   3GB
Mar 08 03:46:40 Starting examples/sat_encodings/translation/compilation
Mar 08 04:49:43 Finished examples/sat_encodings/translation/compilation     1h03m00s  11GB
Mar 08 04:49:43 Starting examples/deflate
Mar 08 04:50:59 Finished examples/deflate                                      1m15s 908MB
Mar 08 04:50:59 Starting examples/deflate/translation
Mar 08 04:53:48 Finished examples/deflate/translation                          2m48s   3GB
Mar 08 04:53:48 Starting examples/deflate/translation/compilation
Mar 08 05:17:03 Finished examples/deflate/translation/compilation             23m14s  13GB
Mar 08 05:17:03 Starting translator/okasaki-examples
Mar 08 05:23:36 Finished translator/okasaki-examples                           6m33s   3GB
Mar 08 05:23:36 Starting translator/other-examples
Mar 08 05:24:35 Finished translator/other-examples                               59s   2GB
Mar 08 05:24:36 Starting compiler/parsing/tests
Mar 08 05:25:08 Finished compiler/parsing/tests                                  32s 743MB
Mar 08 05:25:08 Starting compiler/inference/tests
Mar 08 05:33:53 Finished compiler/inference/tests                              8m44s   5GB
Mar 08 05:33:53 Starting compiler/printing/test
Mar 08 05:37:51 Finished compiler/printing/test                                3m57s   2GB
Mar 08 05:37:51 Starting icing/flover
Mar 08 06:20:52 Finished icing/flover                                         42m59s   2GB
Mar 08 06:20:52 Starting icing/
Mar 08 07:16:52 Finished icing/                                               55m59s   8GB
Mar 08 07:16:52 Starting icing/examples
Mar 08 07:18:24 Finished icing/examples                                        1m32s   6GB
Mar 08 07:18:24 Starting compiler/repl
Mar 08 07:27:08 Finished compiler/repl                                         8m40s   5GB
Mar 08 07:27:09 Starting unverified/sexpr-bootstrap/x64/64
Mar 08 07:40:31 Finished unverified/sexpr-bootstrap/x64/64                    13m22s  15GB
Mar 08 07:40:31 Starting unverified/sexpr-bootstrap/x64/32
Mar 08 07:51:22 Finished unverified/sexpr-bootstrap/x64/32                    10m50s  11GB
Mar 08 07:51:22 Starting compiler/benchmarks
Mar 08 07:51:26 Finished compiler/benchmarks                                      4s  34MB
Mar 08 07:51:26 Starting compiler/bootstrap/compilation/x64/64
Mar 08 21:03:57 Finished compiler/bootstrap/compilation/x64/64             13h12m29s  62GB
Mar 08 21:03:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 08 21:26:25 Finished compiler/bootstrap/compilation/x64/64/proofs         22m27s  44GB
Mar 08 21:26:25 Starting compiler/bootstrap/compilation/x64/32
Mar 09 05:11:19 Finished compiler/bootstrap/compilation/x64/32              7h44m53s  62GB
Mar 09 05:11:19 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 09 05:15:39 Finished compiler/bootstrap/compilation/x64/32/proofs          4m19s  13GB
Mar 09 05:15:39 Starting compiler/bootstrap/compilation/ag32/32
Mar 09 12:20:02 Finished compiler/bootstrap/compilation/ag32/32             7h04m21s  64GB
Mar 09 12:20:02 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 09 12:28:47 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[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)/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                                                                                                                                                      (492s)FAIL<1>
      out = explode current_build_info_str  err = ""
    else
      (let
         (cout,cerr) = compile_32 (TL cl) inp
       in
         out = explode (concat (append cout))  err = explode cerr))
 
 failed.
 Failed to prove theorem cake_extract_writes.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 377)", origin_function = "CONJ_TAC", origin_structure = "Tactic"}