Job 3294

CakeML:003b1a2a9bc10dade699478b159a7599df2da249
  import astSyntax before astToSexprLib [Mar 29 10:36:09]
#1357 (noparse)
Merging into:4e312c0f7e18b9c5789c8ac4e0af257bff895cf5
  Define a C function for customFFI [Mar 25 03:52:57]
HOL:63f2eb9c146352dfd0bab8c5604a096d1e554d03
  minor fixes to examples and updated internal docs [Mar 17 21:01:43]
Machine:lammmington

Mar 29 11:23:15 Claimed job
Mar 29 11:23:19 Reusing HOL
Mar 29 11:23:30 Starting developers
Mar 29 11:23:35 Finished developers                                               4s 107MB
Mar 29 11:23:36 Starting developers/bin
Mar 29 11:23:41 Finished developers/bin                                           3s  89MB
Mar 29 11:23:41 Starting misc
Mar 29 11:24:26 Finished misc                                                    43s   1GB
Mar 29 11:24:26 Starting compiler/proofs
Mar 29 12:24:27 Finished compiler/proofs                                      59m59s   9GB
Mar 29 12:24:28 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 29 18:25:20 Finished compiler/bootstrap/compilation/x64/64/proofs       6h00m50s 110GB
Mar 29 18:25:21 Starting semantics/ffi
Mar 29 18:25:32 Finished semantics/ffi                                           10s 551MB
Mar 29 18:25:33 Starting semantics
Mar 29 18:25:35 Finished semantics                                                1s  95MB
Mar 29 18:25:36 Starting semantics/proofs
Mar 29 18:25:57 Finished semantics/proofs                                        20s 751MB
Mar 29 18:25:58 Starting semantics/alt_semantics
Mar 29 18:26:15 Finished semantics/alt_semantics                                 16s 600MB
Mar 29 18:26:16 Starting semantics/alt_semantics/proofs
Mar 29 18:29:36 Finished semantics/alt_semantics/proofs                        3m19s   3GB
Mar 29 18:29:37 Starting basis/pure
Mar 29 18:29:39 Finished basis/pure                                               0s  90MB
Mar 29 18:29:39 Starting translator
Mar 29 18:30:43 Finished translator                                            1m02s   3GB
Mar 29 18:30:44 Starting compiler/parsing
Mar 29 18:30:46 Finished compiler/parsing                                         1s 103MB
Mar 29 18:30:47 Starting characteristic
Mar 29 18:30:49 Finished characteristic                                           1s 126MB
Mar 29 18:30:50 Starting translator/monadic
Mar 29 18:30:52 Finished translator/monadic                                       1s 124MB
Mar 29 18:30:53 Starting translator/monadic/monad_base
Mar 29 18:30:55 Finished translator/monadic/monad_base                            0s  87MB
Mar 29 18:30:55 Starting profiler
Mar 29 18:31:26 Finished profiler                                                29s   1GB
Mar 29 18:31:27 Starting basis
Mar 29 18:32:56 Finished basis                                                 1m27s   4GB
Mar 29 18:32:56 Starting compiler
Mar 29 18:33:00 Finished compiler                                                 2s 225MB
Mar 29 18:33:01 Starting compiler/inference
Mar 29 18:33:03 Finished compiler/inference                                       1s 108MB
Mar 29 18:33:04 Starting compiler/backend/reg_alloc
Mar 29 18:33:05 Finished compiler/backend/reg_alloc                               1s  88MB
Mar 29 18:33:06 Starting compiler/backend/gc
Mar 29 18:33:09 Finished compiler/backend/gc                                      1s 147MB
Mar 29 18:33:10 Starting compiler/backend
Mar 29 18:33:15 Finished compiler/backend                                         4s 240MB
Mar 29 18:33:16 Starting compiler/encoders/asm
Mar 29 18:33:18 Finished compiler/encoders/asm                                    1s 100MB
Mar 29 18:33:19 Starting compiler/encoders/x64
Mar 29 18:33:21 Finished compiler/encoders/x64                                    1s 106MB
Mar 29 18:33:22 Starting compiler/encoders/arm7
Mar 29 18:33:24 Finished compiler/encoders/arm7                                   1s 109MB
Mar 29 18:33:25 Starting compiler/encoders/arm8
Mar 29 18:33:27 Finished compiler/encoders/arm8                                   1s 107MB
Mar 29 18:33:28 Starting compiler/encoders/arm8_asl
Mar 29 18:34:27 Finished compiler/encoders/arm8_asl                              58s  20GB
Mar 29 18:34:28 Starting compiler/encoders/mips
Mar 29 18:34:30 Finished compiler/encoders/mips                                   1s 104MB
Mar 29 18:34:30 Starting compiler/encoders/riscv
Mar 29 18:34:32 Finished compiler/encoders/riscv                                  1s 105MB
Mar 29 18:34:33 Starting compiler/encoders/ag32
Mar 29 18:34:35 Finished compiler/encoders/ag32                                   1s 108MB
Mar 29 18:34:36 Starting compiler/encoders/tests
Mar 29 18:34:38 Finished compiler/encoders/tests                                  1s 131MB
Mar 29 18:34:39 Starting compiler/encoders/monadic_enc
Mar 29 18:35:00 Finished compiler/encoders/monadic_enc                           20s   1GB
Mar 29 18:35:01 Starting compiler/backend/x64
Mar 29 18:35:04 Finished compiler/backend/x64                                     1s 146MB
Mar 29 18:35:04 Starting compiler/backend/arm7
Mar 29 18:35:07 Finished compiler/backend/arm7                                    1s 147MB
Mar 29 18:35:08 Starting compiler/backend/arm8
Mar 29 18:35:10 Finished compiler/backend/arm8                                    1s 145MB
Mar 29 18:35:11 Starting compiler/backend/mips
Mar 29 18:35:13 Finished compiler/backend/mips                                    1s 147MB
Mar 29 18:35:14 Starting compiler/backend/riscv
Mar 29 18:35:17 Finished compiler/backend/riscv                                   1s 147MB
Mar 29 18:35:17 Starting compiler/backend/ag32
Mar 29 18:36:16 Finished compiler/backend/ag32                                   57s   3GB
Mar 29 18:36:17 Starting compiler/backend/pattern_matching
Mar 29 18:36:18 Finished compiler/backend/pattern_matching                        0s  91MB
Mar 29 18:36:19 Starting compiler/parsing/ocaml
Mar 29 18:38:04 Finished compiler/parsing/ocaml                                1m44s   1GB
Mar 29 18:38:05 Starting compiler/printing
Mar 29 18:38:59 Finished compiler/printing                                       53s   1GB
Mar 29 18:39:00 Starting compiler/parsing/proofs
Mar 29 18:39:02 Finished compiler/parsing/proofs                                  1s 101MB
Mar 29 18:39:03 Starting compiler/inference/proofs
Mar 29 18:39:05 Finished compiler/inference/proofs                                1s 120MB
Mar 29 18:39:06 Starting compiler/backend/semantics
Mar 29 18:41:46 Finished compiler/backend/semantics                            2m39s   3GB
Mar 29 18:41:47 Starting compiler/backend/reg_alloc/proofs
Mar 29 18:41:50 Finished compiler/backend/reg_alloc/proofs                        1s 122MB
Mar 29 18:41:50 Starting compiler/backend/proofs
Mar 29 18:42:31 Finished compiler/backend/proofs                                 39s   2GB
Mar 29 18:42:32 Starting compiler/backend/serialiser
Mar 29 18:42:34 Finished compiler/backend/serialiser                              1s 156MB
Mar 29 18:42:35 Starting compiler/encoders/x64/proofs
Mar 29 18:42:37 Finished compiler/encoders/x64/proofs                             1s 105MB
Mar 29 18:42:38 Starting compiler/encoders/arm7/proofs
Mar 29 18:53:20 Finished compiler/encoders/arm7/proofs                        10m41s  11GB
Mar 29 18:53:21 Starting compiler/encoders/arm8/proofs
Mar 29 18:59:50 Finished compiler/encoders/arm8/proofs                         6m27s   6GB
Mar 29 18:59:51 Starting compiler/encoders/arm8_asl/proofs
Mar 29 19:15:18 Finished compiler/encoders/arm8_asl/proofs                    15m26s   4GB
Mar 29 19:15:18 Starting compiler/encoders/mips/proofs
Mar 29 19:24:28 Finished compiler/encoders/mips/proofs                         9m08s  14GB
Mar 29 19:24:29 Starting compiler/encoders/riscv/proofs
Mar 29 19:32:07 Finished compiler/encoders/riscv/proofs                        7m36s   4GB
Mar 29 19:32:08 Starting compiler/encoders/ag32/proofs
Mar 29 19:34:39 Finished compiler/encoders/ag32/proofs                         2m30s   2GB
Mar 29 19:34:40 Starting compiler/backend/x64/proofs
Mar 29 19:34:43 Finished compiler/backend/x64/proofs                              2s 210MB
Mar 29 19:34:44 Starting compiler/backend/arm7/proofs
Mar 29 19:35:18 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 29 19:35:19 Starting compiler/backend/arm8/proofs
Mar 29 19:35:51 Finished compiler/backend/arm8/proofs                            31s   1GB
Mar 29 19:35:52 Starting compiler/backend/arm8_asl
Mar 29 19:36:18 Finished compiler/backend/arm8_asl                               24s   2GB
Mar 29 19:36:18 Starting compiler/backend/mips/proofs
Mar 29 19:36:54 Finished compiler/backend/mips/proofs                            34s   2GB
Mar 29 19:36:55 Starting compiler/backend/riscv/proofs
Mar 29 19:37:33 Finished compiler/backend/riscv/proofs                           37s   2GB
Mar 29 19:37:34 Starting compiler/backend/ag32/proofs
Mar 29 19:45:10 Finished compiler/backend/ag32/proofs                          7m34s   4GB
Mar 29 19:45:11 Starting compiler/backend/cv_compute
Mar 29 19:45:37 Finished compiler/backend/cv_compute                             25s   1GB
Mar 29 19:45:38 Starting cv_translator
Mar 29 19:50:15 Finished cv_translator                                         4m36s   6GB
Mar 29 19:50:16 Starting candle
Mar 29 19:50:17 Finished candle                                                   0s  15MB
Mar 29 19:50:18 Starting candle/set-theory
Mar 29 19:50:47 Finished candle/set-theory                                       28s 952MB
Mar 29 19:50:48 Starting candle/syntax-lib
Mar 29 19:50:49 Finished candle/syntax-lib                                        0s  83MB
Mar 29 19:50:50 Starting candle/standard
Mar 29 19:50:51 Finished candle/standard                                          0s  16MB
Mar 29 19:50:52 Starting candle/standard/syntax
Mar 29 19:51:07 Finished candle/standard/syntax                                  14s 761MB
Mar 29 19:51:08 Starting candle/standard/semantics
Mar 29 19:53:14 Finished candle/standard/semantics                             2m05s   2GB
Mar 29 19:53:15 Starting candle/standard/monadic
Mar 29 19:53:17 Finished candle/standard/monadic                                  1s 128MB
Mar 29 19:53:18 Starting candle/standard/ml_kernel
Mar 29 19:55:13 Finished candle/standard/ml_kernel                             1m54s   4GB
Mar 29 19:55:14 Starting candle/overloading
Mar 29 19:55:15 Finished candle/overloading                                       0s  17MB
Mar 29 19:55:16 Starting candle/overloading/syntax
Mar 29 19:58:13 Finished candle/overloading/syntax                             2m56s   2GB
Mar 29 19:58:14 Starting candle/overloading/semantics
Mar 29 20:06:45 Finished candle/overloading/semantics                          8m30s   7GB
Mar 29 20:06:46 Starting candle/overloading/monadic
Mar 29 20:08:38 Finished candle/overloading/monadic                            1m51s   2GB
Mar 29 20:08:39 Starting candle/overloading/ml_kernel
Mar 29 20:14:45 Finished candle/overloading/ml_kernel                          6m04s   6GB
Mar 29 20:14:45 Starting candle/overloading/ml_checker
Mar 29 20:17:08 Finished candle/overloading/ml_checker                         2m22s   6GB
Mar 29 20:17:09 Starting candle/prover
Mar 29 20:17:12 Finished candle/prover                                            2s 186MB
Mar 29 20:17:13 Starting candle/prover/compute
Mar 29 20:17:16 Finished candle/prover/compute                                    1s 169MB
Mar 29 20:17:17 Starting pancake
Mar 29 20:17:19 Finished pancake                                                  1s 143MB
Mar 29 20:17:20 Starting pancake/semantics
Mar 29 20:20:06 Finished pancake/semantics                                     2m44s   2GB
Mar 29 20:20:07 Starting pancake/parser
Mar 29 20:20:37 Finished pancake/parser                                          29s 474MB
Mar 29 20:20:38 Starting pancake/static_checker
Mar 29 20:21:44 Finished pancake/static_checker                                1m05s   1GB
Mar 29 20:21:45 Starting pancake/proofs
Mar 29 20:37:14 Finished pancake/proofs                                       15m28s   5GB
Mar 29 20:37:15 Starting compiler/dafny
Mar 29 20:37:39 Finished compiler/dafny                                          23s 730MB
Mar 29 20:37:40 Starting compiler/dafny/translation
Mar 29 20:46:42 Finished compiler/dafny/translation                            9m00s   6GB
Mar 29 20:46:43 Starting compiler/dafny/compilation
Mar 29 20:48:30 Finished compiler/dafny/compilation                            1m46s   6GB
Mar 29 20:48:31 Starting compiler/dafny/semantics
Mar 29 20:49:09 Finished compiler/dafny/semantics                                36s 553MB
Mar 29 20:49:10 Starting compiler/dafny/proofs
Mar 29 20:50:38 Finished compiler/dafny/proofs                                 1m27s   1GB
Mar 29 20:50:39 Starting compiler/dafny/vcg
Mar 29 20:50:41 Finished compiler/dafny/vcg                                       1s 108MB
Mar 29 20:50:42 Starting compiler/dafny/vcg/examples
Mar 29 20:51:07 Finished compiler/dafny/vcg/examples                             24s   1GB
Mar 29 20:51:08 Starting compiler/scheme
Mar 29 20:51:34 Finished compiler/scheme                                         25s   1GB
Mar 29 20:51:35 Starting compiler/scheme/translation
Mar 29 20:57:26 Finished compiler/scheme/translation                           5m49s   6GB
Mar 29 20:57:27 Starting compiler/scheme/compilation
Mar 29 20:58:47 Finished compiler/scheme/compilation                           1m18s   4GB
Mar 29 20:58:47 Starting compiler/scheme/proofs
Mar 29 21:04:25 Finished compiler/scheme/proofs                                5m36s   3GB
Mar 29 21:04:26 Starting characteristic/examples
Mar 29 21:05:52 Finished characteristic/examples                               1m25s   5GB
Mar 29 21:05:53 Starting tutorial/solutions
Mar 29 21:08:26 Finished tutorial/solutions                                    2m32s   3GB
Mar 29 21:08:27 Starting translator/monadic/examples
Mar 29 21:11:23 Finished translator/monadic/examples                           2m54s   4GB
Mar 29 21:11:24 Starting examples
Mar 29 21:15:45 Finished examples                                              4m19s   5GB
Mar 29 21:15:45 Starting examples/compilation
Mar 29 21:15:46 Finished examples/compilation                                     0s  14MB
Mar 29 21:15:47 Starting examples/compilation/x64
Mar 29 21:23:08 Finished examples/compilation/x64                              7m19s   4GB
Mar 29 21:23:09 Starting examples/compilation/x64/proofs
Mar 29 21:25:56 Finished examples/compilation/x64/proofs                       2m46s   4GB
Mar 29 21:25:57 Starting examples/compilation/ag32
Mar 29 21:28:10 Finished examples/compilation/ag32                             2m11s   3GB
Mar 29 21:28:11 Starting examples/compilation/ag32/proofs
Mar 29 21:29:14 Finished examples/compilation/ag32/proofs                      1m02s   4GB
Mar 29 21:29:15 Starting examples/lpr_checker
Mar 29 21:29:52 Finished examples/lpr_checker                                    35s   1GB
Mar 29 21:29:52 Starting examples/lpr_checker/array
Mar 29 21:41:15 Finished examples/lpr_checker/array                           11m21s  10GB
Mar 29 21:41:16 Starting examples/lpr_checker/array/compilation
Mar 29 21:44:55 Finished examples/lpr_checker/array/compilation                3m37s   6GB
Mar 29 21:44:55 Starting examples/lpr_checker/array/compilation/proofs
Mar 29 21:46:16 Finished examples/lpr_checker/array/compilation/proofs         1m19s   5GB
Mar 29 21:46:17 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 29 21:47:33 Finished examples/lpr_checker/array/compilation/proofsARM8     1m15s   4GB
Mar 29 21:47:34 Starting .
Mar 29 21:47:39 Finished .                                                        3s 353MB
Mar 29 21:47:39 Starting examples/xlrup_checker
Mar 29 21:48:32 Finished examples/xlrup_checker                                  51s   1GB
Mar 29 21:48:33 Starting examples/xlrup_checker/array
Mar 29 21:56:51 Finished examples/xlrup_checker/array                          8m17s   5GB
Mar 29 21:56:52 Starting examples/xlrup_checker/array/compilation
Mar 29 21:58:11 Finished examples/xlrup_checker/array/compilation              1m18s   5GB
Mar 29 21:58:12 Starting examples/xlrup_checker/array/compilation/proofs
Mar 29 21:59:19 Finished examples/xlrup_checker/array/compilation/proofs       1m05s   4GB
Mar 29 21:59:20 Starting examples/scpog_checker
Mar 29 22:00:05 Finished examples/scpog_checker                                  44s   2GB
Mar 29 22:00:06 Starting examples/scpog_checker/array
Mar 29 22:05:19 Finished examples/scpog_checker/array                          5m12s   4GB
Mar 29 22:05:20 Starting examples/scpog_checker/array/compilation
Mar 29 22:07:24 Finished examples/scpog_checker/array/compilation              2m02s   8GB
Mar 29 22:07:25 Starting examples/scpog_checker/array/compilation/proofs
Mar 29 22:08:39 Finished examples/scpog_checker/array/compilation/proofs       1m13s   6GB
Mar 29 22:08:40 Starting examples/pseudo_bool
Mar 29 22:10:49 Finished examples/pseudo_bool                                  2m07s   2GB
Mar 29 22:10:50 Starting examples/pseudo_bool/cnf_encoding
Mar 29 22:11:22 Finished examples/pseudo_bool/cnf_encoding                       30s   1GB
Mar 29 22:11:24 Starting examples/pseudo_bool/graph_encoding
Mar 29 22:12:11 Finished examples/pseudo_bool/graph_encoding                     44s   1GB
Mar 29 22:12:11 Starting examples/pseudo_bool/array
Mar 29 22:51:21 Finished examples/pseudo_bool/array                           39m06s  24GB
Mar 29 22:51:21 Starting examples/pseudo_bool/array/compilation
Mar 29 23:09:26 Finished examples/pseudo_bool/array/compilation               18m03s  21GB
Mar 29 23:09:27 Starting examples/pseudo_bool/array/compilation/proofs
Mar 29 23:13:50 Finished examples/pseudo_bool/array/compilation/proofs         4m21s   7GB
Mar 29 23:13:50 Starting examples/pseudo_bool/array/compilation/proofsARM8
Mar 29 23:15:16 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m24s   6GB
Mar 29 23:15:17 Starting examples/opentheory
Mar 29 23:22:03 Finished examples/opentheory                                   6m45s   5GB
Mar 29 23:22:04 Starting examples/opentheory/compilation
Mar 29 23:23:41 Finished examples/opentheory/compilation                       1m36s   6GB
Mar 29 23:23:42 Starting examples/opentheory/compilation/proofs
Mar 29 23:24:54 Finished examples/opentheory/compilation/proofs                1m10s   4GB
Mar 29 23:24:55 Starting examples/opentheory/compilation/ag32
Mar 29 23:26:41 Finished examples/opentheory/compilation/ag32                  1m45s   6GB
Mar 29 23:26:42 Starting examples/opentheory/compilation/ag32/proofs
Mar 29 23:28:04 Finished examples/opentheory/compilation/ag32/proofs           1m21s   7GB
Mar 29 23:28:05 Starting examples/sat_encodings
Mar 29 23:29:10 Finished examples/sat_encodings                                1m04s 801MB
Mar 29 23:29:11 Starting examples/sat_encodings/demo
Mar 29 23:29:12 Finished examples/sat_encodings/demo                              0s  15MB
Mar 29 23:29:12 Starting examples/sat_encodings/case_studies
Mar 29 23:30:53 Finished examples/sat_encodings/case_studies                   1m38s   1GB
Mar 29 23:30:54 Starting examples/sat_encodings/translation
Mar 29 23:34:12 Finished examples/sat_encodings/translation                    3m16s   4GB
Mar 29 23:34:13 Starting examples/sat_encodings/translation/compilation
Mar 29 23:36:18 Finished examples/sat_encodings/translation/compilation        2m04s   5GB
Mar 29 23:36:19 Starting examples/deflate
Mar 29 23:36:41 Finished examples/deflate                                        21s 450MB
Mar 29 23:36:42 Starting examples/deflate/translation
Mar 29 23:37:36 Finished examples/deflate/translation                            53s   3GB
Mar 29 23:37:37 Starting examples/deflate/translation/compilation
Mar 29 23:38:38 Finished examples/deflate/translation/compilation                59s   4GB
Mar 29 23:38:38 Starting examples/vipr
Mar 29 23:41:42 Finished examples/vipr                                         3m03s   5GB
Mar 29 23:41:43 Starting examples/vipr/compilation
Mar 29 23:42:47 Finished examples/vipr/compilation                             1m02s   4GB
Mar 29 23:42:48 Starting examples/template
Mar 29 23:42:51 Finished examples/template                                        2s 162MB
Mar 29 23:42:52 Starting examples/template/translation
Mar 29 23:43:12 Finished examples/template/translation                           19s 878MB
Mar 29 23:43:13 Starting examples/template/compilation
Mar 29 23:44:20 Finished examples/template/compilation                         1m05s   4GB
Mar 29 23:44:21 Starting translator/okasaki-examples
Mar 29 23:47:26 Finished translator/okasaki-examples                           3m04s   3GB
Mar 29 23:47:27 Starting translator/other-examples
Mar 29 23:48:20 Finished translator/other-examples                               52s   2GB
Mar 29 23:48:21 Starting translator/other-examples/auxiliary
Mar 29 23:48:22 Finished translator/other-examples/auxiliary                      0s  20MB
Mar 29 23:48:23 Starting compiler/parsing/tests
Mar 29 23:49:01 Finished compiler/parsing/tests                                  36s   1GB
Mar 29 23:49:02 Starting compiler/inference/tests
Mar 29 23:49:45 Finished compiler/inference/tests                                42s   3GB
Mar 29 23:49:46 Starting compiler/printing/test
Mar 29 23:52:46 Finished compiler/printing/test                                2m58s  17GB
Mar 29 23:52:46 Starting compiler/repl
Mar 29 23:52:50 Finished compiler/repl                                            2s 252MB
Mar 29 23:52:51 Starting compiler/benchmarks
Mar 29 23:53:45 Finished compiler/benchmarks                                     53s 747MB
Mar 29 23:53:46 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Mar 29 23:53:50 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 261MB
Mar 29 23:53:50 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Mar 29 23:53:54 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 281MB
Mar 29 23:53:55 Starting compiler/bootstrap/translation
Mar 30 01:47:58 Finished compiler/bootstrap/translation                     1h54m00s  63GB
Mar 30 01:47:59 Starting compiler/bootstrap/compilation/x64/64
Mar 30 01:51:15 Finished compiler/bootstrap/compilation/x64/64                 3m15s  18GB
Mar 30 01:51:16 Starting compiler/bootstrap/compilation/x64/32
Mar 30 02:17:57 Finished compiler/bootstrap/compilation/x64/32                26m38s  51GB
Mar 30 02:17:58 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 30 02:23:04 Finished compiler/bootstrap/compilation/x64/32/proofs          5m05s  26GB
Mar 30 02:23:05 Starting compiler/bootstrap/compilation/arm8/64
Mar 30 03:07:30 Finished compiler/bootstrap/compilation/arm8/64               44m23s 102GB
Mar 30 03:07:31 Starting compiler/bootstrap/compilation/arm8/64/proofs
Mar 30 03:16:15 Finished compiler/bootstrap/compilation/arm8/64/proofs         8m42s  32GB
Mar 30 03:16:16 Starting compiler/bootstrap/compilation/ag32/32
Mar 30 03:46:10 Finished compiler/bootstrap/compilation/ag32/32               29m52s  81GB
Mar 30 03:46:11 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 30 03:51:26 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m13s  30GB
Mar 30 03:51:26 Starting unverified/sexpr-bootstrap/x64/64
Mar 30 03:54:38 FAILED: unverified/sexpr-bootstrap/x64/64
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/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
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/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
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/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanned 99 directories
Starting work on cake.S
Starting work on README.md
Starting work on cake-sexpr-x64-64
README.md                        unverified/sexpr-bootstrap/x64/64  (0s)     OK
cake.S                                              developers/bin  (0s)     OK
cake-sexpr-x64-64                unverified/sexpr-bootstrap/x64/64(156s)FAIL<1>
 <<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 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 warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%41">>
 <<HOL warning: Type.mk_vartype: non-standard syntax: "%%gen_tyvar%%30">>
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:59: error: Structure (astSyntax) has not been declared Found near astSyntax.IntLit_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:60: error: Structure (astSyntax) has not been declared Found near astSyntax.Char_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:61: error: Structure (astSyntax) has not been declared Found near astSyntax.Word8_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:62: error: Structure (astSyntax) has not been declared Found near astSyntax.Word64_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:77: error: Structure (astSyntax) has not been declared Found near astSyntax.Shift_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:81: error: Structure (astSyntax) has not been declared Found near astSyntax.FFI_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:85: error: Structure (astSyntax) has not been declared
 Found near mk_comb (WordT_tm, astSyntax.W8)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:86: error: Structure (astSyntax) has not been declared
 Found near mk_comb (WordT_tm, astSyntax.W64)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:88: error: Structure (astSyntax) has not been declared
 Found near mk_comb (Compare_tm, astSyntax.Lt)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:89: error: Structure (astSyntax) has not been declared
 Found near mk_comb (Compare_tm, astSyntax.Leq)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:90: error: Structure (astSyntax) has not been declared
 Found near mk_comb (Compare_tm, astSyntax.Gt)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:91: error: Structure (astSyntax) has not been declared
 Found near mk_comb (Compare_tm, astSyntax.Geq)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:92: error: Structure (astSyntax) has not been declared
 Found near mk_comb (AltCompare_tm, astSyntax.Lt)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:93: error: Structure (astSyntax) has not been declared
 Found near mk_comb (AltCompare_tm, astSyntax.Leq)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:94: error: Structure (astSyntax) has not been declared
 Found near mk_comb (AltCompare_tm, astSyntax.Gt)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:95: error: Structure (astSyntax) has not been declared
 Found near mk_comb (AltCompare_tm, astSyntax.Geq)
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:150: error: Structure (astSyntax) has not been declared Found near astSyntax.Pvar_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:151: error: Structure (astSyntax) has not been declared Found near astSyntax.Pany
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:154: error: Structure (astSyntax) has not been declared Found near astSyntax.App_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:155: error: Structure (astSyntax) has not been declared Found near astSyntax.Lit_tm
 /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml:156: error: Structure (astSyntax) has not been declared Found near astSyntax.Plit_tm
 error in quse /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/astToSexprLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/unverified/sexpr-bootstrap/astToSexprLib : Fail "Static Errors"
 error in load /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/x64/64/x64SexprScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression3/cakeml-3294/unverified/sexpr-bootstrap/x64/64/.hol/logs/cake-sexpr-x64-64