Job 3485

CakeML:262da39ab2e96213cee09875afeb5bba1ec3ffb9
  Fix whole_prog proof and remove news-printing option [Aug 27 12:25:10]
#1470 (pan_news)
Merging into:dcc03f2866f05b1db18b9f45c731ce45c3a3133e
  Merge pull request #1472 from CakeML/release-notes [Aug 26 06:32:27]
HOL:a390cbabd3a4521bab4ee20281e3e42933a8a3ae
  Holmake: resolve a foreign HOLHEAP in its own Holmakefile's directory [Aug 20 06:42:59]
Machine:lammmington

Aug 27 12:41:33 Claimed job
Aug 27 12:41:42 Reusing HOL
Aug 27 12:41:50 Starting developers
Aug 27 12:42:43 Finished developers                                              52s   1GB
Aug 27 12:42:44 Starting developers/bin
Aug 27 12:42:53 Finished developers/bin                                           8s   1GB
Aug 27 12:42:54 Starting misc
Aug 27 12:43:45 Finished misc                                                    50s   1GB
Aug 27 12:43:46 Starting compiler/proofs
Aug 27 14:04:03 Finished compiler/proofs                                    1h20m15s  13GB
Aug 27 14:04:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 27 20:52:26 Finished compiler/bootstrap/compilation/x64/64/proofs       6h48m21s  97GB
Aug 27 20:52:27 Starting semantics/ffi
Aug 27 20:52:51 Finished semantics/ffi                                           22s   1GB
Aug 27 20:52:51 Starting semantics
Aug 27 20:52:58 Finished semantics                                                5s   1GB
Aug 27 20:52:59 Starting semantics/proofs
Aug 27 20:53:28 Finished semantics/proofs                                        28s   1GB
Aug 27 20:53:29 Starting semantics/alt_semantics
Aug 27 20:53:52 Finished semantics/alt_semantics                                 22s   1GB
Aug 27 20:53:53 Starting semantics/alt_semantics/proofs
Aug 27 20:57:54 Finished semantics/alt_semantics/proofs                        4m00s   2GB
Aug 27 20:57:55 Starting basis/pure
Aug 27 20:58:02 Finished basis/pure                                               6s   1GB
Aug 27 20:58:03 Starting translator
Aug 27 20:59:21 Finished translator                                            1m17s   2GB
Aug 27 20:59:22 Starting compiler/parsing
Aug 27 21:00:14 Finished compiler/parsing                                        51s   2GB
Aug 27 21:00:15 Starting characteristic
Aug 27 21:00:22 Finished characteristic                                           5s   1GB
Aug 27 21:00:22 Starting translator/monadic
Aug 27 21:00:29 Finished translator/monadic                                       5s   1GB
Aug 27 21:00:30 Starting translator/monadic/monad_base
Aug 27 21:00:36 Finished translator/monadic/monad_base                            5s   1GB
Aug 27 21:00:37 Starting profiler
Aug 27 21:01:14 Finished profiler                                                36s   1GB
Aug 27 21:01:15 Starting basis
Aug 27 21:03:06 Finished basis                                                 1m50s   4GB
Aug 27 21:03:07 Starting compiler
Aug 27 21:03:13 Finished compiler                                                 5s   1GB
Aug 27 21:03:14 Starting compiler/inference
Aug 27 21:03:21 Finished compiler/inference                                       5s   1GB
Aug 27 21:03:22 Starting compiler/backend/reg_alloc
Aug 27 21:03:28 Finished compiler/backend/reg_alloc                               5s   1GB
Aug 27 21:03:29 Starting compiler/backend/gc
Aug 27 21:03:35 Finished compiler/backend/gc                                      5s   1GB
Aug 27 21:03:36 Starting compiler/backend
Aug 27 21:03:42 Finished compiler/backend                                         5s   1GB
Aug 27 21:03:43 Starting compiler/encoders/asm
Aug 27 21:03:50 Finished compiler/encoders/asm                                    5s   1GB
Aug 27 21:03:51 Starting compiler/encoders/x64
Aug 27 21:03:57 Finished compiler/encoders/x64                                    5s   1GB
Aug 27 21:03:58 Starting compiler/encoders/arm7
Aug 27 21:04:04 Finished compiler/encoders/arm7                                   5s   1GB
Aug 27 21:04:05 Starting compiler/encoders/arm8
Aug 27 21:04:11 Finished compiler/encoders/arm8                                   5s   1GB
Aug 27 21:04:12 Starting compiler/encoders/arm8_asl
Aug 27 21:04:39 Finished compiler/encoders/arm8_asl                              25s   1GB
Aug 27 21:04:39 Starting compiler/encoders/mips
Aug 27 21:04:46 Finished compiler/encoders/mips                                   5s   1GB
Aug 27 21:04:47 Starting compiler/encoders/riscv
Aug 27 21:04:53 Finished compiler/encoders/riscv                                  5s   1GB
Aug 27 21:04:54 Starting compiler/encoders/ag32
Aug 27 21:05:01 Finished compiler/encoders/ag32                                   5s   1GB
Aug 27 21:05:01 Starting compiler/encoders/tests
Aug 27 21:05:08 Finished compiler/encoders/tests                                  5s   1GB
Aug 27 21:05:09 Starting compiler/encoders/monadic_enc
Aug 27 21:05:36 Finished compiler/encoders/monadic_enc                           26s   1GB
Aug 27 21:05:37 Starting compiler/backend/x64
Aug 27 21:05:43 Finished compiler/backend/x64                                     5s   1GB
Aug 27 21:05:44 Starting compiler/backend/arm7
Aug 27 21:05:50 Finished compiler/backend/arm7                                    5s   1GB
Aug 27 21:05:51 Starting compiler/backend/arm8
Aug 27 21:05:58 Finished compiler/backend/arm8                                    5s   1GB
Aug 27 21:05:58 Starting compiler/backend/mips
Aug 27 21:06:05 Finished compiler/backend/mips                                    5s   1GB
Aug 27 21:06:06 Starting compiler/backend/riscv
Aug 27 21:06:12 Finished compiler/backend/riscv                                   5s   1GB
Aug 27 21:06:13 Starting compiler/backend/ag32
Aug 27 21:07:22 Finished compiler/backend/ag32                                 1m08s   1GB
Aug 27 21:07:23 Starting compiler/backend/pattern_matching
Aug 27 21:07:44 Finished compiler/backend/pattern_matching                       20s   1GB
Aug 27 21:07:45 Starting compiler/parsing/ocaml
Aug 27 21:10:11 Finished compiler/parsing/ocaml                                2m25s   1GB
Aug 27 21:10:12 Starting compiler/printing
Aug 27 21:11:15 Finished compiler/printing                                     1m02s   1GB
Aug 27 21:11:16 Starting compiler/parsing/proofs
Aug 27 21:11:22 Finished compiler/parsing/proofs                                  5s   1GB
Aug 27 21:11:23 Starting compiler/inference/proofs
Aug 27 21:11:30 Finished compiler/inference/proofs                                5s   1GB
Aug 27 21:11:30 Starting compiler/backend/semantics
Aug 27 21:14:47 Finished compiler/backend/semantics                            3m15s   2GB
Aug 27 21:14:48 Starting compiler/backend/reg_alloc/proofs
Aug 27 21:14:54 Finished compiler/backend/reg_alloc/proofs                        5s   1GB
Aug 27 21:14:55 Starting compiler/backend/proofs
Aug 27 21:15:47 Finished compiler/backend/proofs                                 50s   2GB
Aug 27 21:15:47 Starting compiler/backend/serialiser
Aug 27 21:15:54 Finished compiler/backend/serialiser                              5s   1GB
Aug 27 21:15:55 Starting compiler/encoders/x64/proofs
Aug 27 21:16:01 Finished compiler/encoders/x64/proofs                             5s   1GB
Aug 27 21:16:02 Starting compiler/encoders/arm7/proofs
Aug 27 21:28:36 Finished compiler/encoders/arm7/proofs                        12m32s   4GB
Aug 27 21:28:37 Starting compiler/encoders/arm8/proofs
Aug 27 21:36:37 Finished compiler/encoders/arm8/proofs                         7m59s   4GB
Aug 27 21:36:38 Starting compiler/encoders/arm8_asl/proofs
Aug 27 21:53:42 Finished compiler/encoders/arm8_asl/proofs                    17m03s   3GB
Aug 27 21:53:43 Starting compiler/encoders/mips/proofs
Aug 27 22:04:40 Finished compiler/encoders/mips/proofs                        10m55s  10GB
Aug 27 22:04:41 Starting compiler/encoders/riscv/proofs
Aug 27 22:14:10 Finished compiler/encoders/riscv/proofs                        9m28s   3GB
Aug 27 22:14:11 Starting compiler/encoders/ag32/proofs
Aug 27 22:17:26 Finished compiler/encoders/ag32/proofs                         3m13s   1GB
Aug 27 22:17:27 Starting compiler/backend/x64/proofs
Aug 27 22:17:33 Finished compiler/backend/x64/proofs                              5s   1GB
Aug 27 22:17:34 Starting compiler/backend/arm7/proofs
Aug 27 22:18:19 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 27 22:18:20 Starting compiler/backend/arm8/proofs
Aug 27 22:19:05 Finished compiler/backend/arm8/proofs                            44s   2GB
Aug 27 22:19:06 Starting compiler/backend/arm8_asl
Aug 27 22:19:43 Finished compiler/backend/arm8_asl                               35s   1GB
Aug 27 22:19:44 Starting compiler/backend/mips/proofs
Aug 27 22:20:30 Finished compiler/backend/mips/proofs                            45s   2GB
Aug 27 22:20:31 Starting compiler/backend/riscv/proofs
Aug 27 22:21:21 Finished compiler/backend/riscv/proofs                           48s   2GB
Aug 27 22:21:22 Starting compiler/backend/ag32/proofs
Aug 27 22:31:22 Finished compiler/backend/ag32/proofs                          9m59s   5GB
Aug 27 22:31:23 Starting compiler/backend/cv_compute
Aug 27 22:31:59 Finished compiler/backend/cv_compute                             35s   1GB
Aug 27 22:32:00 Starting cv_translator
Aug 27 22:37:38 Finished cv_translator                                         5m36s   3GB
Aug 27 22:37:39 Starting candle
Aug 27 22:37:45 Finished candle                                                   5s   1GB
Aug 27 22:37:46 Starting candle/set-theory
Aug 27 22:38:09 Finished candle/set-theory                                       22s   1GB
Aug 27 22:38:10 Starting candle/syntax-lib
Aug 27 22:38:16 Finished candle/syntax-lib                                        5s   1GB
Aug 27 22:38:17 Starting candle/standard
Aug 27 22:38:23 Finished candle/standard                                          5s   1GB
Aug 27 22:38:24 Starting candle/standard/syntax
Aug 27 22:38:44 Finished candle/standard/syntax                                  19s   1GB
Aug 27 22:38:45 Starting candle/standard/syntax/little_theories
Aug 27 22:40:10 Finished candle/standard/syntax/little_theories                1m24s   1GB
Aug 27 22:40:11 Starting candle/standard/semantics
Aug 27 22:40:18 Finished candle/standard/semantics                                5s   1GB
Aug 27 22:40:19 Starting candle/standard/monadic
Aug 27 22:40:25 Finished candle/standard/monadic                                  5s   1GB
Aug 27 22:40:26 Starting candle/standard/ml_kernel
Aug 27 22:42:45 Finished candle/standard/ml_kernel                             2m18s   4GB
Aug 27 22:42:46 Starting candle/overloading
Aug 27 22:42:53 Finished candle/overloading                                       5s   1GB
Aug 27 22:42:54 Starting candle/overloading/syntax
Aug 27 22:46:22 Finished candle/overloading/syntax                             3m27s   2GB
Aug 27 22:46:22 Starting candle/overloading/semantics
Aug 27 22:56:15 Finished candle/overloading/semantics                          9m51s   5GB
Aug 27 22:56:16 Starting candle/overloading/monadic
Aug 27 22:58:27 Finished candle/overloading/monadic                            2m10s   1GB
Aug 27 22:58:28 Starting candle/overloading/ml_kernel
Aug 27 23:06:11 Finished candle/overloading/ml_kernel                          7m42s   7GB
Aug 27 23:06:12 Starting candle/overloading/ml_checker
Aug 27 23:09:09 Finished candle/overloading/ml_checker                         2m55s   6GB
Aug 27 23:09:10 Starting candle/prover
Aug 27 23:09:16 Finished candle/prover                                            5s   1GB
Aug 27 23:09:17 Starting candle/prover/compute
Aug 27 23:09:24 Finished candle/prover/compute                                    5s   1GB
Aug 27 23:09:25 Starting pancake
Aug 27 23:09:31 Finished pancake                                                  5s   1GB
Aug 27 23:09:32 Starting pancake/semantics
Aug 27 23:12:53 Finished pancake/semantics                                     3m20s   2GB
Aug 27 23:12:54 Starting pancake/parser
Aug 27 23:13:42 Finished pancake/parser                                          47s   1GB
Aug 27 23:13:43 Starting pancake/static_checker
Aug 27 23:16:25 Finished pancake/static_checker                                2m40s   1GB
Aug 27 23:16:26 Starting pancake/proofs
Aug 27 23:32:51 Finished pancake/proofs                                       16m24s   5GB
Aug 27 23:32:52 Starting compiler/dafny
Aug 27 23:33:23 Finished compiler/dafny                                          29s   1GB
Aug 27 23:33:24 Starting compiler/dafny/translation
Aug 27 23:44:47 Finished compiler/dafny/translation                           11m23s   6GB
Aug 27 23:44:48 Starting compiler/dafny/compilation
Aug 27 23:47:08 Finished compiler/dafny/compilation                            2m18s   6GB
Aug 27 23:47:09 Starting compiler/dafny/semantics
Aug 27 23:47:54 Finished compiler/dafny/semantics                                44s   1GB
Aug 27 23:47:55 Starting compiler/dafny/proofs
Aug 27 23:49:43 Finished compiler/dafny/proofs                                 1m47s   1GB
Aug 27 23:49:44 Starting compiler/dafny/vcg
Aug 27 23:49:51 Finished compiler/dafny/vcg                                       5s   1GB
Aug 27 23:49:52 Starting compiler/dafny/vcg/examples
Aug 27 23:50:26 Finished compiler/dafny/vcg/examples                             33s   1GB
Aug 27 23:50:27 Starting compiler/scheme
Aug 27 23:50:59 Finished compiler/scheme                                         31s   1GB
Aug 27 23:51:00 Starting compiler/scheme/translation
Aug 27 23:58:09 Finished compiler/scheme/translation                           7m08s   5GB
Aug 27 23:58:10 Starting compiler/scheme/compilation
Aug 27 23:59:59 Finished compiler/scheme/compilation                           1m48s   5GB
Aug 28 00:00:00 Starting compiler/scheme/proofs
Aug 28 00:06:53 Finished compiler/scheme/proofs                                6m51s   2GB
Aug 28 00:06:54 Starting characteristic/examples
Aug 28 00:08:37 Finished characteristic/examples                               1m42s   4GB
Aug 28 00:08:38 Starting tutorial
Aug 28 00:08:44 Finished tutorial                                                 5s   1GB
Aug 28 00:08:45 Starting tutorial/solutions
Aug 28 00:11:45 Finished tutorial/solutions                                    2m58s   5GB
Aug 28 00:11:46 Starting translator/monadic/examples
Aug 28 00:15:00 Finished translator/monadic/examples                           3m13s   4GB
Aug 28 00:15:01 Starting examples
Aug 28 00:19:18 Finished examples                                              4m15s   3GB
Aug 28 00:19:19 Starting examples/compilation
Aug 28 00:19:26 Finished examples/compilation                                     6s   1GB
Aug 28 00:19:27 Starting examples/compilation/x64
Aug 28 00:28:52 Finished examples/compilation/x64                              9m23s   4GB
Aug 28 00:28:53 Starting examples/compilation/x64/proofs
Aug 28 00:32:40 Finished examples/compilation/x64/proofs                       3m46s   4GB
Aug 28 00:32:41 Starting examples/compilation/ag32
Aug 28 00:35:36 Finished examples/compilation/ag32                             2m54s   3GB
Aug 28 00:35:37 Starting examples/compilation/ag32/proofs
Aug 28 00:37:07 Finished examples/compilation/ag32/proofs                      1m28s   5GB
Aug 28 00:37:07 Starting examples/lpr_checker
Aug 28 00:37:52 Finished examples/lpr_checker                                    43s   1GB
Aug 28 00:37:53 Starting examples/lpr_checker/array
Aug 28 00:51:27 Finished examples/lpr_checker/array                           13m32s   6GB
Aug 28 00:51:28 Starting examples/lpr_checker/array/compilation
Aug 28 00:55:24 Finished examples/lpr_checker/array/compilation                3m55s   6GB
Aug 28 00:55:24 Starting examples/lpr_checker/array/compilation/proofs
Aug 28 00:57:11 Finished examples/lpr_checker/array/compilation/proofs         1m45s   6GB
Aug 28 00:57:12 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 28 00:59:08 Finished examples/lpr_checker/array/compilation/proofsARM8     1m54s   6GB
Aug 28 00:59:08 Starting .
Aug 28 00:59:15 Finished .                                                        5s   1GB
Aug 28 00:59:16 Starting examples/xlrup_checker
Aug 28 01:00:15 Finished examples/xlrup_checker                                  58s   1GB
Aug 28 01:00:16 Starting examples/xlrup_checker/array
Aug 28 01:10:34 Finished examples/xlrup_checker/array                         10m16s   3GB
Aug 28 01:10:34 Starting examples/xlrup_checker/array/compilation
Aug 28 01:12:22 Finished examples/xlrup_checker/array/compilation              1m46s   5GB
Aug 28 01:12:23 Starting examples/xlrup_checker/array/compilation/proofs
Aug 28 01:14:02 Finished examples/xlrup_checker/array/compilation/proofs       1m37s   5GB
Aug 28 01:14:02 Starting examples/cnf
Aug 28 01:14:31 Finished examples/cnf                                            27s   1GB
Aug 28 01:14:32 Starting examples/cnf/array
Aug 28 01:17:14 Finished examples/cnf/array                                    2m40s   2GB
Aug 28 01:17:15 Starting examples/cnf/dist
Aug 28 01:17:26 Finished examples/cnf/dist                                       10s   1GB
Aug 28 01:17:27 Starting examples/cnf/dist/array
Aug 28 01:24:46 Finished examples/cnf/dist/array                               7m19s   6GB
Aug 28 01:24:47 Starting examples/cnf/dist/array/compilation
Aug 28 01:25:51 Finished examples/cnf/dist/array/compilation                   1m03s   3GB
Aug 28 01:25:52 Starting examples/cnf/dist/array/compilation/proofs
Aug 28 01:27:17 Finished examples/cnf/dist/array/compilation/proofs            1m23s   4GB
Aug 28 01:27:17 Starting examples/scpog_checker
Aug 28 01:28:14 Finished examples/scpog_checker                                  55s   1GB
Aug 28 01:28:15 Starting examples/scpog_checker/array
Aug 28 01:34:38 Finished examples/scpog_checker/array                          6m22s   2GB
Aug 28 01:34:39 Starting examples/scpog_checker/array/compilation
Aug 28 01:37:26 Finished examples/scpog_checker/array/compilation              2m44s   8GB
Aug 28 01:37:26 Starting examples/scpog_checker/array/compilation/proofs
Aug 28 01:39:19 Finished examples/scpog_checker/array/compilation/proofs       1m51s   6GB
Aug 28 01:39:20 Starting examples/pseudo_bool
Aug 28 01:41:51 Finished examples/pseudo_bool                                  2m29s   1GB
Aug 28 01:41:52 Starting examples/pseudo_bool/cnf_encoding
Aug 28 01:42:32 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Aug 28 01:42:32 Starting examples/pseudo_bool/graph_encoding
Aug 28 01:43:26 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Aug 28 01:43:27 Starting examples/pseudo_bool/array
Aug 28 02:29:47 Finished examples/pseudo_bool/array                           46m18s  18GB
Aug 28 02:29:47 Starting examples/pseudo_bool/array/compilation
Aug 28 02:54:25 Finished examples/pseudo_bool/array/compilation               24m36s  22GB
Aug 28 02:54:26 Starting examples/pseudo_bool/array/compilation/proofs
Aug 28 03:02:33 Finished examples/pseudo_bool/array/compilation/proofs         8m06s   9GB
Aug 28 03:02:34 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 28 03:05:28 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m53s   8GB
Aug 28 03:05:29 Starting examples/pseudo_bool/cp_encoding
Aug 28 03:08:55 Finished examples/pseudo_bool/cp_encoding                      3m25s   2GB
Aug 28 03:08:56 Starting examples/pseudo_bool/cp_encoding/array
Aug 28 03:15:40 Finished examples/pseudo_bool/cp_encoding/array                6m43s   4GB
Aug 28 03:15:41 Starting examples/pseudo_bool/cp_encoding/array/compilation
Aug 28 03:34:23 Finished examples/pseudo_bool/cp_encoding/array/compilation    18m40s  37GB
Aug 28 03:34:24 Starting examples/pseudo_bool/cp_encoding/array/compilation/proofs
Aug 28 03:38:45 Finished examples/pseudo_bool/cp_encoding/array/compilation/proofs     4m19s  13GB
Aug 28 03:38:45 Starting examples/opentheory
Aug 28 03:46:16 Finished examples/opentheory                                   7m29s   4GB
Aug 28 03:46:17 Starting examples/opentheory/compilation
Aug 28 03:48:29 Finished examples/opentheory/compilation                       2m10s   5GB
Aug 28 03:48:29 Starting examples/opentheory/compilation/proofs
Aug 28 03:50:11 Finished examples/opentheory/compilation/proofs                1m40s   5GB
Aug 28 03:50:11 Starting examples/opentheory/compilation/ag32
Aug 28 03:52:34 Finished examples/opentheory/compilation/ag32                  2m21s   7GB
Aug 28 03:52:35 Starting examples/opentheory/compilation/ag32/proofs
Aug 28 03:54:38 Finished examples/opentheory/compilation/ag32/proofs           2m02s   7GB
Aug 28 03:54:39 Starting examples/sat_encodings
Aug 28 03:55:55 Finished examples/sat_encodings                                1m15s   1GB
Aug 28 03:55:56 Starting examples/sat_encodings/demo
Aug 28 03:56:04 Finished examples/sat_encodings/demo                              6s   1GB
Aug 28 03:56:04 Starting examples/sat_encodings/case_studies
Aug 28 03:57:57 Finished examples/sat_encodings/case_studies                   1m51s   1GB
Aug 28 03:57:58 Starting examples/sat_encodings/translation
Aug 28 04:02:12 Finished examples/sat_encodings/translation                    4m12s   3GB
Aug 28 04:02:13 Starting examples/sat_encodings/translation/compilation
Aug 28 04:05:03 Finished examples/sat_encodings/translation/compilation        2m49s   5GB
Aug 28 04:05:04 Starting examples/deflate
Aug 28 04:05:32 Finished examples/deflate                                        27s   1GB
Aug 28 04:05:33 Starting examples/deflate/translation
Aug 28 04:06:42 Finished examples/deflate/translation                          1m08s   2GB
Aug 28 04:06:43 Starting examples/deflate/translation/compilation
Aug 28 04:08:01 Finished examples/deflate/translation/compilation              1m16s   4GB
Aug 28 04:08:02 Starting examples/vipr
Aug 28 04:10:47 Finished examples/vipr                                         2m44s   3GB
Aug 28 04:10:48 Starting examples/vipr/compilation
Aug 28 04:12:20 Finished examples/vipr/compilation                             1m31s   4GB
Aug 28 04:12:21 Starting examples/flover/Infra
Aug 28 04:13:05 Finished examples/flover/Infra                                   42s   1GB
Aug 28 04:13:06 Starting examples/flover/semantics
Aug 28 04:14:41 Finished examples/flover/semantics                             1m34s   1GB
Aug 28 04:14:42 Starting examples/flover
Aug 28 04:34:51 Finished examples/flover                                      20m07s   2GB
Aug 28 04:34:52 Starting examples/template
Aug 28 04:35:00 Finished examples/template                                        7s   1GB
Aug 28 04:35:01 Starting examples/template/translation
Aug 28 04:35:31 Finished examples/template/translation                           29s   1GB
Aug 28 04:35:32 Starting examples/template/compilation
Aug 28 04:36:57 Finished examples/template/compilation                         1m24s   4GB
Aug 28 04:36:58 Starting translator/okasaki-examples
Aug 28 04:40:18 Finished translator/okasaki-examples                           3m18s   3GB
Aug 28 04:40:19 Starting translator/other-examples
Aug 28 04:41:36 Finished translator/other-examples                             1m16s   3GB
Aug 28 04:41:37 Starting translator/other-examples/auxiliary
Aug 28 04:41:44 Finished translator/other-examples/auxiliary                      6s   1GB
Aug 28 04:41:45 Starting compiler/parsing/tests
Aug 28 04:42:37 Finished compiler/parsing/tests                                  50s   1GB
Aug 28 04:42:38 Starting compiler/inference/tests
Aug 28 04:43:33 Finished compiler/inference/tests                                54s   3GB
Aug 28 04:43:34 Starting compiler/printing/test
Aug 28 04:47:02 Finished compiler/printing/test                                3m27s  16GB
Aug 28 04:47:03 Starting compiler/repl
Aug 28 04:47:10 Finished compiler/repl                                            5s   1GB
Aug 28 04:47:11 Starting compiler/benchmarks
Aug 28 05:02:04 Finished compiler/benchmarks                                  14m52s   2GB
Aug 28 05:02:05 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Aug 28 05:02:11 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             5s   1GB
Aug 28 05:02:12 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Aug 28 05:02:19 Finished compiler/benchmarks/mlton_benchmarks/cakeml              5s   1GB
Aug 28 05:02:20 Starting compiler/bootstrap/translation
Aug 28 06:59:17 FAILED: compiler/bootstrap/translation
  HOLORIG=/scratch/cakeml/regression3/cakeml-3485/compiler/bootstrap/translation [ -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/cnf
Scanning $(CAKEMLDIR)/examples/cnf/array
Scanning $(CAKEMLDIR)/examples/cnf/dist
Scanning $(CAKEMLDIR)/examples/cnf/dist/array
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation/proofs
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 $(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 288 directories
Building 6 theory files
Starting work on README.md
Starting work on to_word32ProgTheory
README.md                                                   (0s)             OK
to_word32ProgTheory                                        (26m)   [1/6]     OK
Starting work on to_target32ProgTheory
to_target32ProgTheory                                     (927s)   [2/6]     OK
Starting work on from_pancake32ProgTheory
from_pancake32ProgTheory                                   (19m)   [3/6]     OK
Starting work on arm7ProgTheory
arm7ProgTheory                                            (618s)   [4/6]     OK
Starting work on ag32ProgTheory
ag32ProgTheory                                            (483s)   [5/6]     OK
Starting work on compiler32ProgTheory
compiler32ProgTheory                                       (29m)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** compiler32ProgTheory (status 1)
 Adding nsLookup representation thms for 4 consts [compiler32Prog_env_258, compiler32Prog_env_257, ..., compiler32Prog_env_255]
 Saved theorem _______ "nsLookup_compiler32Prog_env_259_pfun_eqs"
 Saved theorem _______ "compiler_parse_pancake_feature_v_thm"
 Translating compiler_print_bool
 Saved theorem _______ "nsLookup_compiler32Prog_env_260_pfun_eqs"
 Saved theorem _______ "compiler_print_bool_v_thm"
 Saved definition ____ "nonzero_exit_code_for_error_msg_def"
 Translating compiler_is_error_msg
 Adding nsLookup representation thms for [compiler32Prog_env_260, compiler32Prog_env_259]
 Saved theorem _______ "nsLookup_compiler32Prog_env_261_pfun_eqs"
 Saved theorem _______ "compiler_is_error_msg_v_thm"
 Translating compiler32prog_nonzero_exit_code_for_error_msg
 Adding nsLookup representation thms for [compiler32Prog_env_261]
 Saved theorem _______ "nsLookup_compiler32Prog_env_262_pfun_eqs"
 Saved theorem _______ "compiler32prog_nonzero_exit_code_for_error_msg_v_thm"
 Translating compiler_compile_pancake
 Adding nsLookup representation thms for [compiler32Prog_env_262]
 Saved theorem _______ "nsLookup_compiler32Prog_env_263_pfun_eqs"
 Saved theorem _______ "compiler_compile_pancake_v_thm"
 Translating compiler_pancake_backend_conf
 Adding nsLookup representation thms for [compiler32Prog_env_263]
 Saved theorem _______ "nsLookup_compiler32Prog_env_264_pfun_eqs"
 Saved theorem _______ "compiler_pancake_backend_conf_v_thm"
 Translating compiler_compile_pancake_32
 Adding nsLookup representation thms for [compiler32Prog_env_264]
 Saved theorem _______ "nsLookup_compiler32Prog_env_265_pfun_eqs"
 Saved theorem _______ "compiler_compile_pancake_32_v_thm"
 Translating compiler_has_pancake_flag
 Adding nsLookup representation thms for [compiler32Prog_env_265]
 Saved theorem _______ "nsLookup_compiler32Prog_env_266_pfun_eqs"
 Saved theorem _______ "compiler_has_pancake_flag_v_thm"
 Saved theorem _______ "nsLookup_compiler32Prog_env_267_pfun_eqs"
 Post condition: POSTv uv. &UNIT_TYPE () uv * (STDIO fs * COMMANDLINE cl)
 Adding nsLookup representation thms for [compiler32Prog_env_266]
 Using CF specification CommandLine_arguments_spec from theory CommandLineProof
 Post condition: POSTv argv. COMMANDLINE cl * STDIO fs * &LIST_TYPE STRING_TYPE (TL cl) argv
 Using translator specification compiler_has_help_flag_v_thm from theory compiler32Prog
 Post condition: POSTv bv. COMMANDLINE cl * STDIO fs * &BOOL (has_help_flag (TL cl)) bv
 Using CF specification print_spec from theory TextIOProof
 Proof of 
 
 IS_SOME (stdin_content fs) 
 app p main_v [Conv NONE []] (STDIO fs * COMMANDLINE cl)
   (POSTv uv.
      &UNIT_TYPE () uv * STDIO (full_compile_32 (TL cl) (get_stdin fs) fs) *
      COMMANDLINE cl)
 
 failed.
 Tactic failure proving "main_spec"; heap saved to compiler32Prog.main_spec.dumpedheap.
 Resume with: bin/hol --holstate=compiler32Prog.main_spec.dumpedheap
 Full log: /scratch/cakeml/regression3/cakeml-3485/compiler/bootstrap/translation/.hol/logs/compiler32ProgTheory