Job 3490

CakeML:6a7502d29e4de6f03f63f97ec6d45e17ce522a22
  Fix compiler32Prog [Aug 28 11:09:15]
#1470 (pan_news)
Merging into:74c512d96abbe45540922383388ed33bd3e4d6d7
  Adds LRUP checker (#1476) [Aug 29 14:18:07]
HOL:a390cbabd3a4521bab4ee20281e3e42933a8a3ae
  Holmake: resolve a foreign HOLHEAP in its own Holmakefile's directory [Aug 20 06:42:59]
Machine:pavlova

Aug 31 07:10:34 Claimed job
Aug 31 07:10:39 Reusing HOL
Aug 31 07:11:35 Starting developers
Aug 31 07:12:26 Finished developers                                              50s   1GB
Aug 31 07:12:27 Starting developers/bin
Aug 31 07:12:35 Finished developers/bin                                           7s   1GB
Aug 31 07:12:36 Starting misc
Aug 31 07:13:27 Finished misc                                                    49s   1GB
Aug 31 07:13:28 Starting compiler/proofs
Aug 31 08:34:32 Finished compiler/proofs                                    1h21m03s  10GB
Aug 31 08:34:33 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 31 14:57:56 Finished compiler/bootstrap/compilation/x64/64/proofs       6h23m20s  73GB
Aug 31 14:57:56 Starting semantics/ffi
Aug 31 14:58:19 Finished semantics/ffi                                           22s   1GB
Aug 31 14:58:20 Starting semantics
Aug 31 14:58:27 Finished semantics                                                5s   1GB
Aug 31 14:58:28 Starting semantics/proofs
Aug 31 14:58:57 Finished semantics/proofs                                        28s   1GB
Aug 31 14:58:58 Starting semantics/alt_semantics
Aug 31 14:59:21 Finished semantics/alt_semantics                                 22s   1GB
Aug 31 14:59:22 Starting semantics/alt_semantics/proofs
Aug 31 15:03:18 Finished semantics/alt_semantics/proofs                        3m55s   1GB
Aug 31 15:03:19 Starting basis/pure
Aug 31 15:03:26 Finished basis/pure                                               6s   1GB
Aug 31 15:03:26 Starting translator
Aug 31 15:04:39 Finished translator                                            1m12s   2GB
Aug 31 15:04:40 Starting compiler/parsing
Aug 31 15:05:34 Finished compiler/parsing                                        52s   1GB
Aug 31 15:05:34 Starting characteristic
Aug 31 15:05:41 Finished characteristic                                           5s   1GB
Aug 31 15:05:42 Starting translator/monadic
Aug 31 15:05:48 Finished translator/monadic                                       5s   1GB
Aug 31 15:05:49 Starting translator/monadic/monad_base
Aug 31 15:05:56 Finished translator/monadic/monad_base                            5s   1GB
Aug 31 15:05:56 Starting profiler
Aug 31 15:06:34 Finished profiler                                                36s   1GB
Aug 31 15:06:35 Starting basis
Aug 31 15:08:29 Finished basis                                                 1m53s   4GB
Aug 31 15:08:30 Starting compiler
Aug 31 15:08:36 Finished compiler                                                 5s   1GB
Aug 31 15:08:37 Starting compiler/inference
Aug 31 15:08:43 Finished compiler/inference                                       5s   1GB
Aug 31 15:08:44 Starting compiler/backend/reg_alloc
Aug 31 15:08:51 Finished compiler/backend/reg_alloc                               5s   1GB
Aug 31 15:08:51 Starting compiler/backend/gc
Aug 31 15:08:58 Finished compiler/backend/gc                                      5s   1GB
Aug 31 15:08:59 Starting compiler/backend
Aug 31 15:09:05 Finished compiler/backend                                         5s   1GB
Aug 31 15:09:06 Starting compiler/encoders/asm
Aug 31 15:09:12 Finished compiler/encoders/asm                                    5s   1GB
Aug 31 15:09:13 Starting compiler/encoders/x64
Aug 31 15:09:19 Finished compiler/encoders/x64                                    5s   1GB
Aug 31 15:09:20 Starting compiler/encoders/arm7
Aug 31 15:09:27 Finished compiler/encoders/arm7                                   5s   1GB
Aug 31 15:09:27 Starting compiler/encoders/arm8
Aug 31 15:09:34 Finished compiler/encoders/arm8                                   5s   1GB
Aug 31 15:09:35 Starting compiler/encoders/arm8_asl
Aug 31 15:10:00 Finished compiler/encoders/arm8_asl                              24s   1GB
Aug 31 15:10:01 Starting compiler/encoders/mips
Aug 31 15:10:08 Finished compiler/encoders/mips                                   5s   1GB
Aug 31 15:10:09 Starting compiler/encoders/riscv
Aug 31 15:10:15 Finished compiler/encoders/riscv                                  5s   1GB
Aug 31 15:10:16 Starting compiler/encoders/ag32
Aug 31 15:10:22 Finished compiler/encoders/ag32                                   5s   1GB
Aug 31 15:10:23 Starting compiler/encoders/tests
Aug 31 15:10:30 Finished compiler/encoders/tests                                  5s   1GB
Aug 31 15:10:31 Starting compiler/encoders/monadic_enc
Aug 31 15:10:58 Finished compiler/encoders/monadic_enc                           26s   1GB
Aug 31 15:10:59 Starting compiler/backend/x64
Aug 31 15:11:05 Finished compiler/backend/x64                                     5s   1GB
Aug 31 15:11:06 Starting compiler/backend/arm7
Aug 31 15:11:12 Finished compiler/backend/arm7                                    5s   1GB
Aug 31 15:11:13 Starting compiler/backend/arm8
Aug 31 15:11:20 Finished compiler/backend/arm8                                    5s   1GB
Aug 31 15:11:21 Starting compiler/backend/mips
Aug 31 15:11:27 Finished compiler/backend/mips                                    5s   1GB
Aug 31 15:11:28 Starting compiler/backend/riscv
Aug 31 15:11:34 Finished compiler/backend/riscv                                   5s   1GB
Aug 31 15:11:35 Starting compiler/backend/ag32
Aug 31 15:12:44 Finished compiler/backend/ag32                                 1m07s   1GB
Aug 31 15:12:44 Starting compiler/backend/pattern_matching
Aug 31 15:13:06 Finished compiler/backend/pattern_matching                       20s   1GB
Aug 31 15:13:07 Starting compiler/parsing/ocaml
Aug 31 15:15:28 Finished compiler/parsing/ocaml                                2m19s   1GB
Aug 31 15:15:29 Starting compiler/printing
Aug 31 15:16:31 Finished compiler/printing                                     1m01s   1GB
Aug 31 15:16:32 Starting compiler/parsing/proofs
Aug 31 15:16:38 Finished compiler/parsing/proofs                                  5s   1GB
Aug 31 15:16:39 Starting compiler/inference/proofs
Aug 31 15:16:45 Finished compiler/inference/proofs                                5s   1GB
Aug 31 15:16:46 Starting compiler/backend/semantics
Aug 31 15:20:03 Finished compiler/backend/semantics                            3m15s   3GB
Aug 31 15:20:04 Starting compiler/backend/reg_alloc/proofs
Aug 31 15:20:10 Finished compiler/backend/reg_alloc/proofs                        5s   1GB
Aug 31 15:20:11 Starting compiler/backend/proofs
Aug 31 15:21:02 Finished compiler/backend/proofs                                 49s   2GB
Aug 31 15:21:03 Starting compiler/backend/serialiser
Aug 31 15:21:09 Finished compiler/backend/serialiser                              5s   1GB
Aug 31 15:21:10 Starting compiler/encoders/x64/proofs
Aug 31 15:21:16 Finished compiler/encoders/x64/proofs                             5s   1GB
Aug 31 15:21:17 Starting compiler/encoders/arm7/proofs
Aug 31 15:33:38 Finished compiler/encoders/arm7/proofs                        12m19s   4GB
Aug 31 15:33:39 Starting compiler/encoders/arm8/proofs
Aug 31 15:41:55 Finished compiler/encoders/arm8/proofs                         8m15s   3GB
Aug 31 15:41:56 Starting compiler/encoders/arm8_asl/proofs
Aug 31 15:59:11 Finished compiler/encoders/arm8_asl/proofs                    17m14s   3GB
Aug 31 15:59:12 Starting compiler/encoders/mips/proofs
Aug 31 16:09:56 Finished compiler/encoders/mips/proofs                        10m42s   9GB
Aug 31 16:09:57 Starting compiler/encoders/riscv/proofs
Aug 31 16:19:36 Finished compiler/encoders/riscv/proofs                        9m38s   4GB
Aug 31 16:19:37 Starting compiler/encoders/ag32/proofs
Aug 31 16:22:48 Finished compiler/encoders/ag32/proofs                         3m10s   2GB
Aug 31 16:22:49 Starting compiler/backend/x64/proofs
Aug 31 16:22:55 Finished compiler/backend/x64/proofs                              5s   1GB
Aug 31 16:22:56 Starting compiler/backend/arm7/proofs
Aug 31 16:23:41 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 31 16:23:42 Starting compiler/backend/arm8/proofs
Aug 31 16:24:28 Finished compiler/backend/arm8/proofs                            45s   2GB
Aug 31 16:24:29 Starting compiler/backend/arm8_asl
Aug 31 16:25:10 Finished compiler/backend/arm8_asl                               40s   2GB
Aug 31 16:25:11 Starting compiler/backend/mips/proofs
Aug 31 16:25:57 Finished compiler/backend/mips/proofs                            44s   2GB
Aug 31 16:25:58 Starting compiler/backend/riscv/proofs
Aug 31 16:26:46 Finished compiler/backend/riscv/proofs                           47s   2GB
Aug 31 16:26:47 Starting compiler/backend/ag32/proofs
Aug 31 16:36:29 Finished compiler/backend/ag32/proofs                          9m41s   4GB
Aug 31 16:36:30 Starting compiler/backend/cv_compute
Aug 31 16:37:07 Finished compiler/backend/cv_compute                             36s   1GB
Aug 31 16:37:08 Starting cv_translator
Aug 31 16:42:41 Finished cv_translator                                         5m32s   3GB
Aug 31 16:42:42 Starting candle
Aug 31 16:42:48 Finished candle                                                   5s   1GB
Aug 31 16:42:49 Starting candle/set-theory
Aug 31 16:43:13 Finished candle/set-theory                                       22s   1GB
Aug 31 16:43:13 Starting candle/syntax-lib
Aug 31 16:43:20 Finished candle/syntax-lib                                        5s   1GB
Aug 31 16:43:21 Starting candle/standard
Aug 31 16:43:27 Finished candle/standard                                          5s   1GB
Aug 31 16:43:28 Starting candle/standard/syntax
Aug 31 16:43:49 Finished candle/standard/syntax                                  20s   1GB
Aug 31 16:43:50 Starting candle/standard/syntax/little_theories
Aug 31 16:45:12 Finished candle/standard/syntax/little_theories                1m21s   1GB
Aug 31 16:45:13 Starting candle/standard/semantics
Aug 31 16:45:19 Finished candle/standard/semantics                                5s   1GB
Aug 31 16:45:20 Starting candle/standard/monadic
Aug 31 16:45:26 Finished candle/standard/monadic                                  5s   1GB
Aug 31 16:45:27 Starting candle/standard/ml_kernel
Aug 31 16:47:50 Finished candle/standard/ml_kernel                             2m22s   5GB
Aug 31 16:47:51 Starting candle/overloading
Aug 31 16:47:58 Finished candle/overloading                                       5s   1GB
Aug 31 16:47:59 Starting candle/overloading/syntax
Aug 31 16:51:21 Finished candle/overloading/syntax                             3m21s   1GB
Aug 31 16:51:22 Starting candle/overloading/semantics
Aug 31 17:00:57 Finished candle/overloading/semantics                          9m34s   7GB
Aug 31 17:00:58 Starting candle/overloading/monadic
Aug 31 17:03:14 Finished candle/overloading/monadic                            2m14s   1GB
Aug 31 17:03:15 Starting candle/overloading/ml_kernel
Aug 31 17:10:36 Finished candle/overloading/ml_kernel                          7m20s   7GB
Aug 31 17:10:37 Starting candle/overloading/ml_checker
Aug 31 17:13:30 Finished candle/overloading/ml_checker                         2m51s   6GB
Aug 31 17:13:31 Starting candle/prover
Aug 31 17:13:37 Finished candle/prover                                            5s   1GB
Aug 31 17:13:38 Starting candle/prover/compute
Aug 31 17:13:44 Finished candle/prover/compute                                    5s   1GB
Aug 31 17:13:45 Starting pancake
Aug 31 17:13:52 Finished pancake                                                  5s   1GB
Aug 31 17:13:53 Starting pancake/semantics
Aug 31 17:17:13 Finished pancake/semantics                                     3m19s   2GB
Aug 31 17:17:14 Starting pancake/parser
Aug 31 17:18:01 Finished pancake/parser                                          46s   1GB
Aug 31 17:18:02 Starting pancake/static_checker
Aug 31 17:20:43 Finished pancake/static_checker                                2m39s   1GB
Aug 31 17:20:43 Starting pancake/proofs
Aug 31 17:37:34 Finished pancake/proofs                                       16m49s   6GB
Aug 31 17:37:35 Starting compiler/dafny
Aug 31 17:38:06 Finished compiler/dafny                                          30s   1GB
Aug 31 17:38:07 Starting compiler/dafny/translation
Aug 31 17:49:48 Finished compiler/dafny/translation                           11m40s   6GB
Aug 31 17:49:49 Starting compiler/dafny/compilation
Aug 31 17:52:10 Finished compiler/dafny/compilation                            2m19s   7GB
Aug 31 17:52:11 Starting compiler/dafny/semantics
Aug 31 17:52:56 Finished compiler/dafny/semantics                                44s   1GB
Aug 31 17:52:57 Starting compiler/dafny/proofs
Aug 31 17:54:43 Finished compiler/dafny/proofs                                 1m45s   1GB
Aug 31 17:54:44 Starting compiler/dafny/vcg
Aug 31 17:54:51 Finished compiler/dafny/vcg                                       6s   1GB
Aug 31 17:54:52 Starting compiler/dafny/vcg/examples
Aug 31 17:55:26 Finished compiler/dafny/vcg/examples                             33s   1GB
Aug 31 17:55:26 Starting compiler/scheme
Aug 31 17:55:59 Finished compiler/scheme                                         31s   1GB
Aug 31 17:56:00 Starting compiler/scheme/translation
Aug 31 18:02:52 Finished compiler/scheme/translation                           6m51s   6GB
Aug 31 18:02:53 Starting compiler/scheme/compilation
Aug 31 18:04:36 Finished compiler/scheme/compilation                           1m41s   5GB
Aug 31 18:04:36 Starting compiler/scheme/proofs
Aug 31 18:11:32 Finished compiler/scheme/proofs                                6m54s   3GB
Aug 31 18:11:33 Starting characteristic/examples
Aug 31 18:13:09 Finished characteristic/examples                               1m35s   4GB
Aug 31 18:13:10 Starting tutorial
Aug 31 18:13:16 Finished tutorial                                                 5s   1GB
Aug 31 18:13:17 Starting tutorial/solutions
Aug 31 18:16:14 Finished tutorial/solutions                                    2m56s   5GB
Aug 31 18:16:15 Starting translator/monadic/examples
Aug 31 18:19:25 Finished translator/monadic/examples                           3m09s   4GB
Aug 31 18:19:26 Starting examples
Aug 31 18:23:47 Finished examples                                              4m19s   3GB
Aug 31 18:23:47 Starting examples/compilation
Aug 31 18:23:55 Finished examples/compilation                                     6s   1GB
Aug 31 18:23:55 Starting examples/compilation/x64
Aug 31 18:33:10 Finished examples/compilation/x64                              9m14s   4GB
Aug 31 18:33:11 Starting examples/compilation/x64/proofs
Aug 31 18:37:05 Finished examples/compilation/x64/proofs                       3m52s   4GB
Aug 31 18:37:06 Starting examples/compilation/ag32
Aug 31 18:40:00 Finished examples/compilation/ag32                             2m53s   3GB
Aug 31 18:40:01 Starting examples/compilation/ag32/proofs
Aug 31 18:41:31 Finished examples/compilation/ag32/proofs                      1m29s   5GB
Aug 31 18:41:32 Starting examples/lpr_checker
Aug 31 18:42:17 Finished examples/lpr_checker                                    44s   1GB
Aug 31 18:42:18 Starting examples/lpr_checker/array
Aug 31 18:55:39 Finished examples/lpr_checker/array                           13m20s   6GB
Aug 31 18:55:40 Starting examples/lpr_checker/array/compilation
Aug 31 18:59:41 Finished examples/lpr_checker/array/compilation                3m59s   6GB
Aug 31 18:59:41 Starting examples/lpr_checker/array/compilation/proofs
Aug 31 19:01:27 Finished examples/lpr_checker/array/compilation/proofs         1m45s   5GB
Aug 31 19:01:28 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 31 19:03:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m49s   6GB
Aug 31 19:03:19 Starting .
Aug 31 19:03:29 Finished .                                                        5s   1GB
Aug 31 19:03:30 Starting examples/xlrup_checker
Aug 31 19:04:28 Finished examples/xlrup_checker                                  57s   1GB
Aug 31 19:04:29 Starting examples/xlrup_checker/array
Aug 31 19:14:11 Finished examples/xlrup_checker/array                          9m41s   3GB
Aug 31 19:14:12 Starting examples/xlrup_checker/array/compilation
Aug 31 19:15:56 Finished examples/xlrup_checker/array/compilation              1m43s   5GB
Aug 31 19:15:57 Starting examples/xlrup_checker/array/compilation/proofs
Aug 31 19:17:32 Finished examples/xlrup_checker/array/compilation/proofs       1m34s   5GB
Aug 31 19:17:33 Starting examples/cnf
Aug 31 19:18:07 Finished examples/cnf                                            33s   1GB
Aug 31 19:18:08 Starting examples/cnf/array
Aug 31 19:21:21 Finished examples/cnf/array                                    3m12s   2GB
Aug 31 19:21:22 Starting examples/cnf/dist
Aug 31 19:21:34 Finished examples/cnf/dist                                       10s   1GB
Aug 31 19:21:35 Starting examples/cnf/dist/array
Aug 31 19:26:10 Finished examples/cnf/dist/array                               4m34s   2GB
Aug 31 19:26:11 Starting examples/cnf/dist/array/compilation
Aug 31 19:27:16 Finished examples/cnf/dist/array/compilation                   1m04s   3GB
Aug 31 19:27:16 Starting examples/cnf/dist/array/compilation/proofs
Aug 31 19:28:43 Finished examples/cnf/dist/array/compilation/proofs            1m25s   4GB
Aug 31 19:28:44 Starting examples/cnf/lrup
Aug 31 19:28:59 Finished examples/cnf/lrup                                       14s   1GB
Aug 31 19:29:00 Starting examples/cnf/lrup/array
Aug 31 19:32:01 Finished examples/cnf/lrup/array                               2m59s   1GB
Aug 31 19:32:01 Starting examples/cnf/lrup/array/compilation
Aug 31 19:33:19 Finished examples/cnf/lrup/array/compilation                   1m16s   4GB
Aug 31 19:33:20 Starting examples/cnf/lrup/array/compilation/proofs
Aug 31 19:34:48 Finished examples/cnf/lrup/array/compilation/proofs            1m27s   4GB
Aug 31 19:34:49 Starting examples/scpog_checker
Aug 31 19:35:44 Finished examples/scpog_checker                                  54s   1GB
Aug 31 19:35:45 Starting examples/scpog_checker/array
Aug 31 19:41:38 Finished examples/scpog_checker/array                          5m51s   2GB
Aug 31 19:41:39 Starting examples/scpog_checker/array/compilation
Aug 31 19:44:25 Finished examples/scpog_checker/array/compilation              2m45s   8GB
Aug 31 19:44:26 Starting examples/scpog_checker/array/compilation/proofs
Aug 31 19:46:17 Finished examples/scpog_checker/array/compilation/proofs       1m50s   6GB
Aug 31 19:46:18 Starting examples/pseudo_bool
Aug 31 19:48:46 Finished examples/pseudo_bool                                  2m26s   1GB
Aug 31 19:48:47 Starting examples/pseudo_bool/cnf_encoding
Aug 31 19:49:29 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Aug 31 19:49:30 Starting examples/pseudo_bool/graph_encoding
Aug 31 19:50:23 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Aug 31 19:50:24 Starting examples/pseudo_bool/array
Aug 31 20:35:32 Finished examples/pseudo_bool/array                           45m06s  24GB
Aug 31 20:35:33 Starting examples/pseudo_bool/array/compilation
Aug 31 21:00:37 Finished examples/pseudo_bool/array/compilation               25m03s  22GB
Aug 31 21:00:38 Starting examples/pseudo_bool/array/compilation/proofs
Aug 31 21:08:47 Finished examples/pseudo_bool/array/compilation/proofs         8m08s   9GB
Aug 31 21:08:48 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 31 21:11:36 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m47s   9GB
Aug 31 21:11:37 Starting examples/pseudo_bool/cp_encoding
Aug 31 21:14:56 Finished examples/pseudo_bool/cp_encoding                      3m18s   1GB
Aug 31 21:14:56 Starting examples/pseudo_bool/cp_encoding/array
Aug 31 21:21:30 Finished examples/pseudo_bool/cp_encoding/array                6m32s   3GB
Aug 31 21:21:30 Starting examples/pseudo_bool/cp_encoding/array/compilation
Aug 31 21:40:08 Finished examples/pseudo_bool/cp_encoding/array/compilation    18m36s  40GB
Aug 31 21:40:09 Starting examples/pseudo_bool/cp_encoding/array/compilation/proofs
Aug 31 21:44:31 Finished examples/pseudo_bool/cp_encoding/array/compilation/proofs     4m21s  13GB
Aug 31 21:44:32 Starting examples/opentheory
Aug 31 21:51:52 Finished examples/opentheory                                   7m19s   3GB
Aug 31 21:51:53 Starting examples/opentheory/compilation
Aug 31 21:54:02 Finished examples/opentheory/compilation                       2m08s   5GB
Aug 31 21:54:03 Starting examples/opentheory/compilation/proofs
Aug 31 21:55:47 Finished examples/opentheory/compilation/proofs                1m43s   5GB
Aug 31 21:55:48 Starting examples/opentheory/compilation/ag32
Aug 31 21:58:02 Finished examples/opentheory/compilation/ag32                  2m13s   5GB
Aug 31 21:58:03 Starting examples/opentheory/compilation/ag32/proofs
Aug 31 22:00:10 Finished examples/opentheory/compilation/ag32/proofs           2m06s   7GB
Aug 31 22:00:11 Starting examples/sat_encodings
Aug 31 22:01:27 Finished examples/sat_encodings                                1m14s   1GB
Aug 31 22:01:28 Starting examples/sat_encodings/demo
Aug 31 22:01:35 Finished examples/sat_encodings/demo                              6s   1GB
Aug 31 22:01:36 Starting examples/sat_encodings/case_studies
Aug 31 22:03:30 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Aug 31 22:03:31 Starting examples/sat_encodings/translation
Aug 31 22:07:35 Finished examples/sat_encodings/translation                    4m03s   2GB
Aug 31 22:07:36 Starting examples/sat_encodings/translation/compilation
Aug 31 22:10:24 Finished examples/sat_encodings/translation/compilation        2m47s   5GB
Aug 31 22:10:25 Starting examples/deflate
Aug 31 22:10:54 Finished examples/deflate                                        27s   1GB
Aug 31 22:10:54 Starting examples/deflate/translation
Aug 31 22:12:04 Finished examples/deflate/translation                          1m08s   3GB
Aug 31 22:12:05 Starting examples/deflate/translation/compilation
Aug 31 22:13:23 Finished examples/deflate/translation/compilation              1m17s   4GB
Aug 31 22:13:24 Starting examples/vipr
Aug 31 22:16:18 Finished examples/vipr                                         2m53s   3GB
Aug 31 22:16:19 Starting examples/vipr/compilation
Aug 31 22:17:47 Finished examples/vipr/compilation                             1m26s   4GB
Aug 31 22:17:47 Starting examples/flover/Infra
Aug 31 22:18:30 Finished examples/flover/Infra                                   41s   1GB
Aug 31 22:18:31 Starting examples/flover/semantics
Aug 31 22:20:03 Finished examples/flover/semantics                             1m31s   1GB
Aug 31 22:20:04 Starting examples/flover
Aug 31 22:40:04 Finished examples/flover                                      19m59s   2GB
Aug 31 22:40:05 Starting examples/template
Aug 31 22:40:14 Finished examples/template                                        7s   1GB
Aug 31 22:40:15 Starting examples/template/translation
Aug 31 22:40:45 Finished examples/template/translation                           28s   1GB
Aug 31 22:40:45 Starting examples/template/compilation
Aug 31 22:42:09 Finished examples/template/compilation                         1m22s   4GB
Aug 31 22:42:10 Starting translator/okasaki-examples
Aug 31 22:45:39 Finished translator/okasaki-examples                           3m27s   3GB
Aug 31 22:45:40 Starting translator/other-examples
Aug 31 22:46:58 Finished translator/other-examples                             1m17s   3GB
Aug 31 22:46:58 Starting translator/other-examples/auxiliary
Aug 31 22:47:05 Finished translator/other-examples/auxiliary                      6s   1GB
Aug 31 22:47:06 Starting compiler/parsing/tests
Aug 31 22:47:58 Finished compiler/parsing/tests                                  51s   1GB
Aug 31 22:47:59 Starting compiler/inference/tests
Aug 31 22:48:54 Finished compiler/inference/tests                                54s   3GB
Aug 31 22:48:55 Starting compiler/printing/test
Aug 31 22:52:25 Finished compiler/printing/test                                3m28s  17GB
Aug 31 22:52:26 Starting compiler/repl
Aug 31 22:52:33 Finished compiler/repl                                            6s   1GB
Aug 31 22:52:34 Starting compiler/benchmarks
Aug 31 23:07:31 Finished compiler/benchmarks                                  14m56s   2GB
Aug 31 23:07:32 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Aug 31 23:07:39 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             6s   1GB
Aug 31 23:07:40 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Aug 31 23:07:46 Finished compiler/benchmarks/mlton_benchmarks/cakeml              5s   1GB
Aug 31 23:07:47 Starting compiler/bootstrap/translation
Sep 01 00:56:13 Finished compiler/bootstrap/translation                     1h48m23s  41GB
Sep 01 00:56:14 Starting compiler/bootstrap/compilation/x64/64
Sep 01 01:01:34 Finished compiler/bootstrap/compilation/x64/64                 5m18s  24GB
Sep 01 01:01:35 Starting compiler/bootstrap/compilation/x64/32
Sep 01 01:39:59 Finished compiler/bootstrap/compilation/x64/32                38m23s  64GB
Sep 01 01:40:00 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 01 01:49:21 Finished compiler/bootstrap/compilation/x64/32/proofs          9m19s  31GB
Sep 01 01:49:22 Starting compiler/bootstrap/compilation/arm8/64
Sep 01 02:48:51 Finished compiler/bootstrap/compilation/arm8/64               59m28s 103GB
Sep 01 02:48:52 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 01 02:59:43 Finished compiler/bootstrap/compilation/arm8/64/proofs        10m50s  42GB
Sep 01 02:59:44 Starting compiler/bootstrap/compilation/ag32/32
Sep 01 03:42:33 Finished compiler/bootstrap/compilation/ag32/32               42m47s  81GB
Sep 01 03:42:34 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 01 04:02:05 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
  HOLORIG=/scratch/cakeml/regression/cakeml-3490/compiler/bootstrap/compilation/ag32/32/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation/proofs
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanned 292 directories
Building 1 theory file
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                                   (0s)             OK
ag32BootstrapProofTheory                                   (18m)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** ag32BootstrapProofTheory (status 1)
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%30">>
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%41">>
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%30">>
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%41">>
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%30">>
 <<HOL message: Created theory "ag32BootstrapProof">>
 Proved triviality ___ "with_clos_conf_simp"
 Saved definition ____ "compiler_instance_def"
 Proved triviality ___ "compiler_instance_lemma"
 Saved theorem _______ "extcalls_ffi_names"
 Saved theorem _______ "target_state_rel_cake_start_asm_state"
 Saved theorem _______ "cake_compiled_thm"
 Saved theorem _______ "cake_installed"
 Saved theorem _______ "cake_machine_sem"
 Saved theorem _______ "get_stdin_stdin_fs"
 Saved theorem _______ "inFS_fname_fastForwardFD"
 Saved theorem _______ "not_inFS_fname_stdin_fs"
 Saved theorem _______ "ALOOKUP_stdin_fs_File_NONE"
 Saved theorem _______ "ALOOKUP_fastForwardFD_infds_neq"
 Saved theorem _______ "FST_ALOOKUP_fastForwardFD_infds"
 Saved theorem _______ "FST_ALOOKUP_add_stdo_infds"
 Saved theorem _______ "ALOOKUP_add_stdout_inode_tbl"
 Saved theorem _______ "ALOOKUP_add_stderr_inode_tbl"
 Saved theorem _______ "ALOOKUP_add_stdout_infds"
 Saved theorem _______ "ALOOKUP_add_stderr_infds"
 Proof of 
 
 wfcl cl 
 (let
    events = MAP get_output_io_event (cake_io_events cl (stdin_fs inp));
    out = extract_writes 1 events;
    err = extract_writes 2 events
  in
    if has_help_flag (TL cl) then out = explode help_string  err = ""
    else if has_version_flag (TL cl) then
      out = explode current_build_info_str  err = ""
    else if has_pancake_flag (TL cl) then
      (let
         (cout,cerr) = compile_pancake_32 (TL cl) inp
       in
         out = explode (concat (append cout))  err = explode cerr)
    else
      (let
         (cout,cerr) = compile_32 (TL cl) inp
       in
         out = explode (concat (append cout))  err = explode cerr))
 
 failed.
 Tactic failure proving "cake_extract_writes"; heap saved to ag32BootstrapProof.cake_extract_writes.dumpedheap.
 Resume with: bin/hol --holstate=ag32BootstrapProof.cake_extract_writes.dumpedheap
 Full log: /scratch/cakeml/regression/cakeml-3490/compiler/bootstrap/compilation/ag32/32/proofs/.hol/logs/ag32BootstrapProofTheory