Job 2438

CakeML:4d60801be46c6f5175cbb29119e7fe3ffd4b901b
  Add arm8 bootstrap [Jun 17 22:48:38]
#991 (master)
Merging into:c03b0f4110b1846ada0d2ba523e9c1e363817906
  fix a broken proof in data_to_word_memoryProof [Jul 03 14:07:01]
HOL:a0047680ef60f5bf44fe05190b5dcf8756ab4a73
  Get help/src-sml to build again after 7c55b699b9714 [Jul 02 04:04:45]
Machine:lammmington

Jul 03 22:43:32 Claimed job
Jul 03 22:43:38 Building HOL
Jul 03 22:57:56 Starting developers
Jul 03 22:58:00 Finished developers                                               2s 200MB
Jul 03 22:58:01 Starting developers/bin
Jul 03 22:58:13 Finished developers/bin                                          11s   1GB
Jul 03 22:58:14 Starting compiler/proofs
Jul 10 12:56:10 Resuming compiler/proofs
Jul 10 12:56:15 Finished compiler/proofs                                          4s 253MB
Jul 10 12:56:16 Starting compiler/bootstrap/translation
Jul 10 21:19:03 Finished compiler/bootstrap/translation                     8h22m45s  77GB
Jul 10 21:19:04 Starting semantics/ffi
Jul 10 21:19:13 Finished semantics/ffi                                            8s 651MB
Jul 10 21:19:14 Starting semantics
Jul 10 21:19:15 Finished semantics                                                0s  68MB
Jul 10 21:19:16 Starting semantics/proofs
Jul 10 21:19:53 Finished semantics/proofs                                        36s   2GB
Jul 10 21:19:54 Starting semantics/alt_semantics
Jul 10 21:20:36 Finished semantics/alt_semantics                                 41s   1GB
Jul 10 21:20:37 Starting semantics/alt_semantics/proofs
Jul 10 21:31:45 Finished semantics/alt_semantics/proofs                       11m07s   4GB
Jul 10 21:31:46 Starting basis/pure
Jul 10 21:31:48 Finished basis/pure                                               0s  70MB
Jul 10 21:31:48 Starting translator
Jul 10 21:33:33 Finished translator                                            1m43s   3GB
Jul 10 21:33:33 Starting compiler/parsing
Jul 10 21:33:35 Finished compiler/parsing                                         0s  75MB
Jul 10 21:33:36 Starting characteristic
Jul 10 21:33:37 Finished characteristic                                           0s  96MB
Jul 10 21:33:38 Starting translator/monadic
Jul 10 21:33:39 Finished translator/monadic                                       0s  94MB
Jul 10 21:33:40 Starting basis
Jul 10 21:37:15 Finished basis                                                 3m34s   5GB
Jul 10 21:37:16 Starting compiler/inference
Jul 10 21:37:18 Finished compiler/inference                                       0s  99MB
Jul 10 21:37:19 Starting compiler/backend/reg_alloc
Jul 10 21:37:20 Finished compiler/backend/reg_alloc                               0s  68MB
Jul 10 21:37:21 Starting compiler/backend/gc
Jul 10 21:37:22 Finished compiler/backend/gc                                      0s 137MB
Jul 10 21:37:23 Starting compiler/backend
Jul 10 21:37:43 Finished compiler/backend                                        18s   1GB
Jul 10 21:37:43 Starting compiler/encoders/asm
Jul 10 21:37:45 Finished compiler/encoders/asm                                    0s  89MB
Jul 10 21:37:46 Starting compiler/encoders/x64
Jul 10 21:37:47 Finished compiler/encoders/x64                                    0s 102MB
Jul 10 21:37:48 Starting compiler/encoders/arm7
Jul 10 21:37:50 Finished compiler/encoders/arm7                                   0s 101MB
Jul 10 21:37:50 Starting compiler/encoders/arm8
Jul 10 21:37:52 Finished compiler/encoders/arm8                                   0s 101MB
Jul 10 21:37:53 Starting compiler/encoders/arm8_asl
Jul 10 23:49:34 Finished compiler/encoders/arm8_asl                         2h11m40s  44GB
Jul 10 23:49:35 Starting compiler/encoders/mips
Jul 10 23:49:37 Finished compiler/encoders/mips                                   0s 100MB
Jul 10 23:49:38 Starting compiler/encoders/riscv
Jul 10 23:49:39 Finished compiler/encoders/riscv                                  0s 101MB
Jul 10 23:49:40 Starting compiler/encoders/ag32
Jul 10 23:49:41 Finished compiler/encoders/ag32                                   0s  99MB
Jul 10 23:49:42 Starting compiler/backend/x64
Jul 10 23:49:44 Finished compiler/backend/x64                                     0s 136MB
Jul 10 23:49:45 Starting compiler/backend/arm7
Jul 10 23:49:47 Finished compiler/backend/arm7                                    0s 136MB
Jul 10 23:49:48 Starting compiler/backend/arm8
Jul 10 23:49:49 Finished compiler/backend/arm8                                    0s 135MB
Jul 10 23:49:50 Starting compiler/backend/mips
Jul 10 23:49:52 Finished compiler/backend/mips                                    0s 136MB
Jul 10 23:49:53 Starting compiler/backend/riscv
Jul 10 23:49:55 Finished compiler/backend/riscv                                   0s 136MB
Jul 10 23:49:56 Starting compiler/backend/ag32
Jul 10 23:51:16 Finished compiler/backend/ag32                                 1m19s   2GB
Jul 10 23:51:17 Starting compiler/parsing/proofs
Jul 10 23:51:18 Finished compiler/parsing/proofs                                  0s  76MB
Jul 10 23:51:19 Starting compiler/inference/proofs
Jul 10 23:51:20 Finished compiler/inference/proofs                                0s  92MB
Jul 10 23:51:21 Starting compiler/backend/semantics
Jul 10 23:55:09 Finished compiler/backend/semantics                            3m46s   3GB
Jul 10 23:55:10 Starting compiler/backend/reg_alloc/proofs
Jul 10 23:55:12 Finished compiler/backend/reg_alloc/proofs                        0s  96MB
Jul 10 23:55:12 Starting compiler/backend/proofs
Jul 10 23:56:17 Finished compiler/backend/proofs                               1m03s   3GB
Jul 10 23:56:18 Starting compiler/backend/serialiser
Jul 10 23:56:20 Finished compiler/backend/serialiser                              0s 144MB
Jul 10 23:56:21 Starting compiler/encoders/x64/proofs
Jul 11 00:05:49 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Jul 11 00:05:49 Starting compiler/encoders/arm7/proofs
Jul 11 00:18:43 Finished compiler/encoders/arm7/proofs                        12m52s  11GB
Jul 11 00:18:44 Starting compiler/encoders/arm8/proofs
Jul 11 00:25:13 Finished compiler/encoders/arm8/proofs                         6m28s   3GB
Jul 11 00:25:14 Starting compiler/encoders/arm8_asl/proofs
Jul 11 01:12:55 Finished compiler/encoders/arm8_asl/proofs                    47m39s  12GB
Jul 11 01:12:55 Starting compiler/encoders/mips/proofs
Jul 11 01:22:53 Finished compiler/encoders/mips/proofs                         9m56s   7GB
Jul 11 01:22:54 Starting compiler/encoders/riscv/proofs
Jul 11 01:31:10 Finished compiler/encoders/riscv/proofs                        8m14s   5GB
Jul 11 01:31:11 Starting compiler/encoders/ag32/proofs
Jul 11 01:33:34 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Jul 11 01:33:35 Starting compiler/backend/x64/proofs
Jul 11 01:34:18 Finished compiler/backend/x64/proofs                             42s   3GB
Jul 11 01:34:19 Starting compiler/backend/arm7/proofs
Jul 11 01:35:06 Finished compiler/backend/arm7/proofs                            45s   2GB
Jul 11 01:35:07 Starting compiler/backend/arm8/proofs
Jul 11 01:35:49 Finished compiler/backend/arm8/proofs                            40s   3GB
Jul 11 01:35:50 Starting compiler/backend/arm8_asl
Jul 11 01:36:20 Finished compiler/backend/arm8_asl                               29s   2GB
Jul 11 01:36:20 Starting compiler/backend/mips/proofs
Jul 11 01:37:08 Finished compiler/backend/mips/proofs                            46s   3GB
Jul 11 01:37:09 Starting compiler/backend/riscv/proofs
Jul 11 01:38:01 Finished compiler/backend/riscv/proofs                           51s   4GB
Jul 11 01:38:02 Starting compiler/backend/ag32/proofs
Jul 11 01:52:08 Finished compiler/backend/ag32/proofs                         14m05s   6GB
Jul 11 01:52:09 Starting compiler/backend/cv_compute
Jul 11 01:53:55 Finished compiler/backend/cv_compute                           1m44s   3GB
Jul 11 01:53:56 Starting cv_translator
Jul 11 02:13:25 Finished cv_translator                                        19m27s  14GB
Jul 11 02:13:26 Starting candle/set-theory
Jul 11 02:14:13 Finished candle/set-theory                                       46s   1GB
Jul 11 02:14:14 Starting candle/syntax-lib
Jul 11 02:14:15 Finished candle/syntax-lib                                        0s  72MB
Jul 11 02:14:16 Starting candle/standard/syntax
Jul 11 02:14:35 Finished candle/standard/syntax                                  18s   1GB
Jul 11 02:14:36 Starting candle/standard/semantics
Jul 11 02:17:11 Finished candle/standard/semantics                             2m34s   3GB
Jul 11 02:17:12 Starting candle/standard/monadic
Jul 11 02:17:14 Finished candle/standard/monadic                                  0s 106MB
Jul 11 02:17:15 Starting candle/standard/ml_kernel
Jul 11 02:19:13 Finished candle/standard/ml_kernel                             1m57s   6GB
Jul 11 02:19:14 Starting candle/overloading/syntax
Jul 11 02:22:51 Finished candle/overloading/syntax                             3m36s   3GB
Jul 11 02:22:52 Starting candle/overloading/semantics
Jul 11 02:34:31 Finished candle/overloading/semantics                         11m37s   5GB
Jul 11 02:34:31 Starting candle/overloading/monadic
Jul 11 02:37:08 Finished candle/overloading/monadic                            2m35s   3GB
Jul 11 02:37:09 Starting candle/overloading/ml_kernel
Jul 11 02:44:46 Finished candle/overloading/ml_kernel                          7m36s   7GB
Jul 11 02:44:47 Starting candle/overloading/ml_checker
Jul 11 02:47:21 Finished candle/overloading/ml_checker                         2m33s   7GB
Jul 11 02:47:22 Starting candle/prover
Jul 11 02:57:26 Finished candle/prover                                        10m03s   5GB
Jul 11 02:57:27 Starting pancake
Jul 11 02:58:36 Finished pancake                                               1m08s   1GB
Jul 11 02:58:37 Starting pancake/ffi
Jul 11 02:58:38 Finished pancake/ffi                                              0s  24MB
Jul 11 02:58:39 Starting pancake/semantics
Jul 11 03:01:21 Finished pancake/semantics                                     2m41s   3GB
Jul 11 03:01:22 Starting pancake/parser
Jul 11 03:01:56 Finished pancake/parser                                          33s   2GB
Jul 11 03:01:57 Starting pancake/proofs
Jul 11 03:32:59 Finished pancake/proofs                                       31m01s   8GB
Jul 11 03:33:00 Starting characteristic/examples
Jul 11 03:34:39 Finished characteristic/examples                               1m38s   6GB
Jul 11 03:34:40 Starting tutorial/solutions
Jul 11 03:37:13 Finished tutorial/solutions                                    2m31s   4GB
Jul 11 03:37:13 Starting translator/monadic/examples
Jul 11 03:41:12 Finished translator/monadic/examples                           3m57s   5GB
Jul 11 03:41:13 Starting examples
Jul 11 03:55:46 Finished examples                                             14m32s   8GB
Jul 11 03:55:47 Starting examples/compilation/x64
Jul 11 04:04:53 Finished examples/compilation/x64                              9m05s   7GB
Jul 11 04:04:54 Starting examples/compilation/x64/proofs
Jul 11 04:09:28 Finished examples/compilation/x64/proofs                       4m32s   8GB
Jul 11 04:09:28 Starting examples/compilation/ag32
Jul 11 04:12:03 Finished examples/compilation/ag32                             2m33s   5GB
Jul 11 04:12:04 Starting examples/compilation/ag32/proofs
Jul 11 04:13:59 Finished examples/compilation/ag32/proofs                      1m54s  10GB
Jul 11 04:14:00 Starting examples/compilation/to_word
Jul 11 04:18:14 Finished examples/compilation/to_word                          4m13s  13GB
Jul 11 04:18:15 Starting examples/lpr_checker
Jul 11 04:19:39 Finished examples/lpr_checker                                  1m23s   2GB
Jul 11 04:19:40 Starting examples/lpr_checker/array
Jul 11 04:48:52 Finished examples/lpr_checker/array                           29m11s  21GB
Jul 11 04:48:53 Starting examples/lpr_checker/array/compilation
Jul 11 04:51:23 Finished examples/lpr_checker/array/compilation                2m29s   9GB
Jul 11 04:51:24 Starting examples/lpr_checker/array/compilation/proofs
Jul 11 04:53:29 Finished examples/lpr_checker/array/compilation/proofs         2m04s  10GB
Jul 11 04:53:30 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 11 04:55:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m47s   9GB
Jul 11 04:55:18 Starting examples/xlrup_checker
Jul 11 04:56:32 Finished examples/xlrup_checker                                1m13s   1GB
Jul 11 04:56:33 Starting examples/xlrup_checker/array
Jul 11 05:11:43 Finished examples/xlrup_checker/array                         15m08s   8GB
Jul 11 05:11:43 Starting examples/xlrup_checker/array/compilation
Jul 11 05:13:08 Finished examples/xlrup_checker/array/compilation              1m24s   6GB
Jul 11 05:13:09 Starting examples/xlrup_checker/array/compilation/proofs
Jul 11 05:14:58 Finished examples/xlrup_checker/array/compilation/proofs       1m47s   8GB
Jul 11 05:14:59 Starting examples/pseudo_bool
Jul 11 05:17:10 Finished examples/pseudo_bool                                  2m10s   2GB
Jul 11 05:17:11 Starting examples/pseudo_bool/cnf_encoding
Jul 11 05:17:51 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Jul 11 05:17:52 Starting examples/pseudo_bool/graph_encoding
Jul 11 05:18:45 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Jul 11 05:18:46 Starting examples/pseudo_bool/array
Jul 11 06:25:48 Finished examples/pseudo_bool/array                         1h07m01s  44GB
Jul 11 06:25:49 Starting examples/pseudo_bool/array/compilation
Jul 11 06:38:49 Finished examples/pseudo_bool/array/compilation               12m58s  28GB
Jul 11 06:38:50 Starting examples/pseudo_bool/array/compilation/proofs
Jul 11 06:42:45 Finished examples/pseudo_bool/array/compilation/proofs         3m54s   9GB
Jul 11 06:42:46 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jul 11 06:44:30 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m43s  10GB
Jul 11 06:44:31 Starting examples/opentheory
Jul 11 06:55:12 Finished examples/opentheory                                  10m40s   8GB
Jul 11 06:55:13 Starting examples/opentheory
Jul 11 06:55:15 Finished examples/opentheory                                      0s 130MB
Jul 11 06:55:16 Starting examples/opentheory/compilation
Jul 11 06:57:26 Finished examples/opentheory/compilation                       2m08s   8GB
Jul 11 06:57:27 Starting examples/opentheory/compilation/proofs
Jul 11 06:59:08 Finished examples/opentheory/compilation/proofs                1m40s   8GB
Jul 11 06:59:09 Starting examples/opentheory/compilation/ag32
Jul 11 07:01:14 Finished examples/opentheory/compilation/ag32                  2m04s   9GB
Jul 11 07:01:15 Starting examples/opentheory/compilation/ag32/proofs
Jul 11 07:03:37 Finished examples/opentheory/compilation/ag32/proofs           2m21s  14GB
Jul 11 07:03:38 Starting examples/sat_encodings
Jul 11 07:06:32 Finished examples/sat_encodings                                2m53s   1GB
Jul 11 07:06:33 Starting examples/sat_encodings/case_studies
Jul 11 07:08:41 Finished examples/sat_encodings/case_studies                   2m06s   2GB
Jul 11 07:08:41 Starting examples/sat_encodings/translation
Jul 11 07:15:05 Finished examples/sat_encodings/translation                    6m22s   7GB
Jul 11 07:15:06 Starting examples/sat_encodings/translation/compilation
Jul 11 07:17:28 Finished examples/sat_encodings/translation/compilation        2m20s   6GB
Jul 11 07:17:28 Starting examples/deflate
Jul 11 07:18:50 Finished examples/deflate                                      1m20s   2GB
Jul 11 07:18:51 Starting examples/deflate/translation
Jul 11 07:20:32 Finished examples/deflate/translation                          1m40s   7GB
Jul 11 07:20:33 Starting examples/deflate/translation/compilation
Jul 11 07:21:36 Finished examples/deflate/translation/compilation              1m02s   5GB
Jul 11 07:21:37 Starting examples/vipr
Jul 11 07:25:53 Finished examples/vipr                                         4m15s   8GB
Jul 11 07:25:54 Starting examples/vipr/compilation
Jul 11 07:27:11 Finished examples/vipr/compilation                             1m16s   5GB
Jul 11 07:27:12 Starting translator/okasaki-examples
Jul 11 07:32:23 Finished translator/okasaki-examples                           5m09s   4GB
Jul 11 07:32:24 Starting translator/other-examples
Jul 11 07:37:09 Finished translator/other-examples                             4m44s   3GB
Jul 11 07:37:10 Starting compiler/parsing/tests
Jul 11 07:37:45 Finished compiler/parsing/tests                                  34s   1GB
Jul 11 07:37:46 Starting compiler/inference/tests
Jul 11 07:38:27 Finished compiler/inference/tests                                40s   3GB
Jul 11 07:38:28 Starting compiler/printing/test
Jul 11 07:40:01 Finished compiler/printing/test                                1m32s   6GB
Jul 11 07:40:02 Starting icing/flover
Jul 11 08:17:35 Finished icing/flover                                         37m32s   4GB
Jul 11 08:17:36 Starting icing/
Jul 11 08:45:46 Finished icing/                                               28m08s   9GB
Jul 11 08:45:47 Starting icing/examples
Jul 11 08:47:35 Finished icing/examples                                        1m47s   9GB
Jul 11 08:47:36 Starting compiler/repl
Jul 11 08:56:50 Finished compiler/repl                                         9m12s   9GB
Jul 11 08:56:51 Starting unverified/sexpr-bootstrap/x64/64
Jul 11 09:08:47 Finished unverified/sexpr-bootstrap/x64/64                    11m55s  18GB
Jul 11 09:08:48 Starting unverified/sexpr-bootstrap/x64/32
Jul 11 09:18:08 Finished unverified/sexpr-bootstrap/x64/32                     9m19s  15GB
Jul 11 09:18:09 Starting compiler/benchmarks
Jul 11 09:18:53 Finished compiler/benchmarks                                     43s 713MB
Jul 11 09:18:54 Starting compiler/bootstrap/compilation/x64/64
Jul 11 10:17:00 Finished compiler/bootstrap/compilation/x64/64                58m04s 131GB
Jul 11 10:17:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 11 10:39:05 Finished compiler/bootstrap/compilation/x64/64/proofs         22m03s  51GB
Jul 11 10:39:06 Starting compiler/bootstrap/compilation/x64/32
Jul 11 11:16:09 Finished compiler/bootstrap/compilation/x64/32                37m01s  88GB
Jul 11 11:16:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 11 11:20:41 Finished compiler/bootstrap/compilation/x64/32/proofs          4m29s  23GB
Jul 11 11:20:42 Starting compiler/bootstrap/compilation/arm8/64
Jul 12 00:56:29 FAILED: compiler/bootstrap/compilation/arm8/64
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/algebra/base[0m
Scanning [1m$(HOLDIR)/src/algebra/construction[0m
Scanning [1m$(HOLDIR)/src/algebra[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover/compute[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 99 directories
Starting work on README.md
Starting work on to_dataBootstrapTheory
Starting work on cake-sexpr-64
README.md                                                           (0s)     OK
cake-sexpr-64                                                     (171s)     OK
to_dataBootstrapTheory                                            (109m)     OK
Starting work on to_lab_arm8BootstrapTheory
to_lab_arm8BootstrapTheory                                        (638m)     OK
Starting work on arm8BootstrapTheory
arm8BootstrapTheory                                               (266m)FAIL<1>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "arm8Bootstrap">>
           lab_to_target eval: runtime: 4h18m56s,    gctime: 15m08s,     systime: 18m52s.
           lab_to_target real: 4h37m42s
           lab_to_target size: 75157206
                       export: runtime: 32.1s,    gctime: 13.1s,     systime: 3.9s.
 error in quse /scratch/cakeml/regression2/cakeml-2438/compiler/bootstrap/compilation/arm8/64/arm8BootstrapScript.sml : HOL_ERR {message = "", origin_function = "dest_SmartAppend", origin_structure = "miscSyntax"}
 error in load /scratch/cakeml/regression2/cakeml-2438/compiler/bootstrap/compilation/arm8/64/arm8BootstrapScript : HOL_ERR {message = "", origin_function = "dest_SmartAppend", origin_structure = "miscSyntax"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "dest_SmartAppend", origin_structure = "miscSyntax"}