Job 2468

CakeML:4d60801be46c6f5175cbb29119e7fe3ffd4b901b
  Add arm8 bootstrap [Jun 17 22:48:38]
#991 (master)
Merging into:6cdeb10d4b89bd7583574cdfb1d7a3c11bf8f52d
  Adjust translations of toSortedAList [Jul 19 09:41:46]
HOL:c37de731916a5fe5fdc6218d4b2e19234435e4ce
  Add lots of regexp matching regression tests for DBSearchParser [Jul 15 06:13:45]
Machine:lammmington

Jul 19 10:16:20 Claimed job
Jul 19 10:16:24 Reusing HOL
Jul 19 10:16:34 Starting developers
Jul 19 10:16:38 Finished developers                                               2s 224MB
Jul 19 10:16:39 Starting developers/bin
Jul 19 10:16:49 Finished developers/bin                                           9s   1GB
Jul 19 10:16:50 Starting compiler/proofs
Jul 19 12:08:36 Finished compiler/proofs                                    1h51m44s  34GB
Jul 19 12:08:37 Starting compiler/bootstrap/translation
Jul 19 20:31:02 Finished compiler/bootstrap/translation                     8h22m24s  80GB
Jul 19 20:31:03 Starting semantics/ffi
Jul 19 20:31:12 Finished semantics/ffi                                            7s 636MB
Jul 19 20:31:13 Starting semantics
Jul 19 20:31:14 Finished semantics                                                0s  69MB
Jul 19 20:31:15 Starting semantics/proofs
Jul 19 20:31:53 Finished semantics/proofs                                        37s   1GB
Jul 19 20:31:54 Starting semantics/alt_semantics
Jul 19 20:32:35 Finished semantics/alt_semantics                                 40s   1GB
Jul 19 20:32:36 Starting semantics/alt_semantics/proofs
Jul 19 20:43:42 Finished semantics/alt_semantics/proofs                       11m05s   2GB
Jul 19 20:43:43 Starting basis/pure
Jul 19 20:43:44 Finished basis/pure                                               0s  70MB
Jul 19 20:43:45 Starting translator
Jul 19 20:45:31 Finished translator                                            1m44s   3GB
Jul 19 20:45:31 Starting compiler/parsing
Jul 19 20:45:33 Finished compiler/parsing                                         0s  75MB
Jul 19 20:45:34 Starting characteristic
Jul 19 20:45:35 Finished characteristic                                           0s  96MB
Jul 19 20:45:36 Starting translator/monadic
Jul 19 20:45:38 Finished translator/monadic                                       0s  96MB
Jul 19 20:45:38 Starting basis
Jul 19 20:49:16 Finished basis                                                 3m36s   5GB
Jul 19 20:49:17 Starting compiler/inference
Jul 19 20:49:18 Finished compiler/inference                                       0s  99MB
Jul 19 20:49:19 Starting compiler/backend/reg_alloc
Jul 19 20:49:20 Finished compiler/backend/reg_alloc                               0s  69MB
Jul 19 20:49:21 Starting compiler/backend/gc
Jul 19 20:49:23 Finished compiler/backend/gc                                      0s 144MB
Jul 19 20:49:24 Starting compiler/backend
Jul 19 20:49:45 Finished compiler/backend                                        19s   1GB
Jul 19 20:49:45 Starting compiler/encoders/asm
Jul 19 20:49:47 Finished compiler/encoders/asm                                    0s  94MB
Jul 19 20:49:48 Starting compiler/encoders/x64
Jul 19 20:49:49 Finished compiler/encoders/x64                                    0s 100MB
Jul 19 20:49:50 Starting compiler/encoders/arm7
Jul 19 20:49:52 Finished compiler/encoders/arm7                                   0s 101MB
Jul 19 20:49:52 Starting compiler/encoders/arm8
Jul 19 20:49:54 Finished compiler/encoders/arm8                                   0s 101MB
Jul 19 20:49:55 Starting compiler/encoders/arm8_asl
Jul 19 20:52:10 Finished compiler/encoders/arm8_asl                            2m13s   1GB
Jul 19 20:52:10 Starting compiler/encoders/mips
Jul 19 20:52:12 Finished compiler/encoders/mips                                   0s 100MB
Jul 19 20:52:13 Starting compiler/encoders/riscv
Jul 19 20:52:14 Finished compiler/encoders/riscv                                  0s 100MB
Jul 19 20:52:15 Starting compiler/encoders/ag32
Jul 19 20:52:17 Finished compiler/encoders/ag32                                   0s 100MB
Jul 19 20:52:17 Starting compiler/backend/x64
Jul 19 20:52:19 Finished compiler/backend/x64                                     0s 134MB
Jul 19 20:52:20 Starting compiler/backend/arm7
Jul 19 20:52:22 Finished compiler/backend/arm7                                    0s 134MB
Jul 19 20:52:23 Starting compiler/backend/arm8
Jul 19 20:52:25 Finished compiler/backend/arm8                                    0s 134MB
Jul 19 20:52:25 Starting compiler/backend/mips
Jul 19 20:52:27 Finished compiler/backend/mips                                    0s 134MB
Jul 19 20:52:28 Starting compiler/backend/riscv
Jul 19 20:52:30 Finished compiler/backend/riscv                                   0s 134MB
Jul 19 20:52:31 Starting compiler/backend/ag32
Jul 19 20:53:51 Finished compiler/backend/ag32                                 1m19s   2GB
Jul 19 20:53:52 Starting compiler/parsing/proofs
Jul 19 20:53:53 Finished compiler/parsing/proofs                                  0s  77MB
Jul 19 20:53:54 Starting compiler/inference/proofs
Jul 19 20:53:56 Finished compiler/inference/proofs                                0s  93MB
Jul 19 20:53:57 Starting compiler/backend/semantics
Jul 19 20:57:43 Finished compiler/backend/semantics                            3m45s   3GB
Jul 19 20:57:44 Starting compiler/backend/reg_alloc/proofs
Jul 19 20:57:46 Finished compiler/backend/reg_alloc/proofs                        0s  96MB
Jul 19 20:57:47 Starting compiler/backend/proofs
Jul 19 20:58:52 Finished compiler/backend/proofs                               1m04s   3GB
Jul 19 20:58:53 Starting compiler/backend/serialiser
Jul 19 20:58:54 Finished compiler/backend/serialiser                              0s 150MB
Jul 19 20:58:55 Starting compiler/encoders/x64/proofs
Jul 19 21:08:25 Finished compiler/encoders/x64/proofs                          9m29s   5GB
Jul 19 21:08:26 Starting compiler/encoders/arm7/proofs
Jul 19 21:21:19 Finished compiler/encoders/arm7/proofs                        12m51s  10GB
Jul 19 21:21:20 Starting compiler/encoders/arm8/proofs
Jul 19 21:27:56 Finished compiler/encoders/arm8/proofs                         6m35s   5GB
Jul 19 21:27:57 Starting compiler/encoders/arm8_asl/proofs
Jul 19 21:41:50 Finished compiler/encoders/arm8_asl/proofs                    13m52s   4GB
Jul 19 21:41:51 Starting compiler/encoders/mips/proofs
Jul 19 21:52:04 Finished compiler/encoders/mips/proofs                        10m11s   7GB
Jul 19 21:52:05 Starting compiler/encoders/riscv/proofs
Jul 19 22:00:27 Finished compiler/encoders/riscv/proofs                        8m20s   4GB
Jul 19 22:00:28 Starting compiler/encoders/ag32/proofs
Jul 19 22:02:48 Finished compiler/encoders/ag32/proofs                         2m19s   2GB
Jul 19 22:02:49 Starting compiler/backend/x64/proofs
Jul 19 22:03:34 Finished compiler/backend/x64/proofs                             43s   3GB
Jul 19 22:03:35 Starting compiler/backend/arm7/proofs
Jul 19 22:04:20 Finished compiler/backend/arm7/proofs                            44s   2GB
Jul 19 22:04:21 Starting compiler/backend/arm8/proofs
Jul 19 22:05:03 Finished compiler/backend/arm8/proofs                            41s   3GB
Jul 19 22:05:03 Starting compiler/backend/arm8_asl
Jul 19 22:05:33 Finished compiler/backend/arm8_asl                               28s   2GB
Jul 19 22:05:33 Starting compiler/backend/mips/proofs
Jul 19 22:06:19 Finished compiler/backend/mips/proofs                            44s   3GB
Jul 19 22:06:20 Starting compiler/backend/riscv/proofs
Jul 19 22:07:10 Finished compiler/backend/riscv/proofs                           48s   3GB
Jul 19 22:07:11 Starting compiler/backend/ag32/proofs
Jul 19 22:22:29 Finished compiler/backend/ag32/proofs                         15m17s   4GB
Jul 19 22:22:30 Starting compiler/backend/cv_compute
Jul 19 22:24:15 Finished compiler/backend/cv_compute                           1m44s   3GB
Jul 19 22:24:15 Starting cv_translator
Jul 19 22:43:30 Finished cv_translator                                        19m13s  13GB
Jul 19 22:43:31 Starting candle/set-theory
Jul 19 22:44:22 Finished candle/set-theory                                       50s   1GB
Jul 19 22:44:23 Starting candle/syntax-lib
Jul 19 22:44:24 Finished candle/syntax-lib                                        0s  75MB
Jul 19 22:44:25 Starting candle/standard/syntax
Jul 19 22:44:44 Finished candle/standard/syntax                                  17s   1GB
Jul 19 22:44:45 Starting candle/standard/semantics
Jul 19 22:47:25 Finished candle/standard/semantics                             2m39s   4GB
Jul 19 22:47:26 Starting candle/standard/monadic
Jul 19 22:47:27 Finished candle/standard/monadic                                  0s 106MB
Jul 19 22:47:28 Starting candle/standard/ml_kernel
Jul 19 22:49:22 Finished candle/standard/ml_kernel                             1m53s   7GB
Jul 19 22:49:23 Starting candle/overloading/syntax
Jul 19 22:52:56 Finished candle/overloading/syntax                             3m32s   3GB
Jul 19 22:52:57 Starting candle/overloading/semantics
Jul 19 23:04:33 Finished candle/overloading/semantics                         11m34s   9GB
Jul 19 23:04:34 Starting candle/overloading/monadic
Jul 19 23:07:11 Finished candle/overloading/monadic                            2m36s   2GB
Jul 19 23:07:12 Starting candle/overloading/ml_kernel
Jul 19 23:14:53 Finished candle/overloading/ml_kernel                          7m40s   7GB
Jul 19 23:14:54 Starting candle/overloading/ml_checker
Jul 19 23:17:28 Finished candle/overloading/ml_checker                         2m32s   7GB
Jul 19 23:17:29 Starting candle/prover
Jul 19 23:27:38 Finished candle/prover                                        10m08s   5GB
Jul 19 23:27:38 Starting pancake
Jul 19 23:28:43 Finished pancake                                               1m03s   1GB
Jul 19 23:28:44 Starting pancake/ffi
Jul 19 23:28:45 Finished pancake/ffi                                              0s  24MB
Jul 19 23:28:46 Starting pancake/semantics
Jul 19 23:31:29 Finished pancake/semantics                                     2m42s   2GB
Jul 19 23:31:30 Starting pancake/parser
Jul 19 23:32:06 Finished pancake/parser                                          35s   2GB
Jul 19 23:32:07 Starting pancake/proofs
Jul 20 00:03:11 Finished pancake/proofs                                       31m03s   9GB
Jul 20 00:03:12 Starting characteristic/examples
Jul 20 00:04:49 Finished characteristic/examples                               1m35s   6GB
Jul 20 00:04:50 Starting tutorial/solutions
Jul 20 00:07:23 Finished tutorial/solutions                                    2m32s   4GB
Jul 20 00:07:24 Starting translator/monadic/examples
Jul 20 00:11:21 Finished translator/monadic/examples                           3m55s   5GB
Jul 20 00:11:22 Starting examples
Jul 20 00:25:48 Finished examples                                             14m25s   8GB
Jul 20 00:25:48 Starting examples/compilation/x64
Jul 20 00:34:55 Finished examples/compilation/x64                              9m05s   7GB
Jul 20 00:34:56 Starting examples/compilation/x64/proofs
Jul 20 00:39:42 Finished examples/compilation/x64/proofs                       4m45s   9GB
Jul 20 00:39:43 Starting examples/compilation/ag32
Jul 20 00:42:19 Finished examples/compilation/ag32                             2m35s   4GB
Jul 20 00:42:20 Starting examples/compilation/ag32/proofs
Jul 20 00:44:09 Finished examples/compilation/ag32/proofs                      1m48s   8GB
Jul 20 00:44:10 Starting examples/compilation/to_word
Jul 20 00:48:09 Finished examples/compilation/to_word                          3m57s  12GB
Jul 20 00:48:10 Starting examples/lpr_checker
Jul 20 00:49:31 Finished examples/lpr_checker                                  1m20s   2GB
Jul 20 00:49:32 Starting examples/lpr_checker/array
Jul 20 01:18:09 Finished examples/lpr_checker/array                           28m36s  20GB
Jul 20 01:18:10 Starting examples/lpr_checker/array/compilation
Jul 20 01:20:37 Finished examples/lpr_checker/array/compilation                2m25s   9GB
Jul 20 01:20:38 Starting examples/lpr_checker/array/compilation/proofs
Jul 20 01:22:35 Finished examples/lpr_checker/array/compilation/proofs         1m56s   7GB
Jul 20 01:22:36 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 20 01:24:22 Finished examples/lpr_checker/array/compilation/proofsARM8     1m44s   8GB
Jul 20 01:24:23 Starting examples/xlrup_checker
Jul 20 01:25:36 Finished examples/xlrup_checker                                1m12s   1GB
Jul 20 01:25:37 Starting examples/xlrup_checker/array
Jul 20 01:40:36 Finished examples/xlrup_checker/array                         14m58s   8GB
Jul 20 01:40:37 Starting examples/xlrup_checker/array/compilation
Jul 20 01:42:02 Finished examples/xlrup_checker/array/compilation              1m23s   6GB
Jul 20 01:42:03 Starting examples/xlrup_checker/array/compilation/proofs
Jul 20 01:43:38 Finished examples/xlrup_checker/array/compilation/proofs       1m34s   7GB
Jul 20 01:43:39 Starting examples/pseudo_bool
Jul 20 01:45:52 Finished examples/pseudo_bool                                  2m12s   2GB
Jul 20 01:45:53 Starting examples/pseudo_bool/cnf_encoding
Jul 20 01:46:33 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Jul 20 01:46:34 Starting examples/pseudo_bool/graph_encoding
Jul 20 01:47:28 Finished examples/pseudo_bool/graph_encoding                     52s   2GB
Jul 20 01:47:29 Starting examples/pseudo_bool/array
Jul 20 02:53:37 Finished examples/pseudo_bool/array                         1h06m07s  41GB
Jul 20 02:53:38 Starting examples/pseudo_bool/array/compilation
Jul 20 03:06:28 Finished examples/pseudo_bool/array/compilation               12m49s  29GB
Jul 20 03:06:29 Starting examples/pseudo_bool/array/compilation/proofs
Jul 20 03:10:20 Finished examples/pseudo_bool/array/compilation/proofs         3m49s  10GB
Jul 20 03:10:21 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jul 20 03:12:08 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m46s  11GB
Jul 20 03:12:09 Starting examples/opentheory
Jul 20 03:22:58 Finished examples/opentheory                                  10m48s   8GB
Jul 20 03:22:59 Starting examples/opentheory
Jul 20 03:23:01 Finished examples/opentheory                                      0s 130MB
Jul 20 03:23:02 Starting examples/opentheory/compilation
Jul 20 03:25:02 Finished examples/opentheory/compilation                       1m58s   9GB
Jul 20 03:25:03 Starting examples/opentheory/compilation/proofs
Jul 20 03:26:43 Finished examples/opentheory/compilation/proofs                1m39s   7GB
Jul 20 03:26:44 Starting examples/opentheory/compilation/ag32
Jul 20 03:28:49 Finished examples/opentheory/compilation/ag32                  2m03s   9GB
Jul 20 03:28:49 Starting examples/opentheory/compilation/ag32/proofs
Jul 20 03:31:09 Finished examples/opentheory/compilation/ag32/proofs           2m18s  12GB
Jul 20 03:31:10 Starting examples/sat_encodings
Jul 20 03:34:03 Finished examples/sat_encodings                                2m52s   1GB
Jul 20 03:34:04 Starting examples/sat_encodings/case_studies
Jul 20 03:36:13 Finished examples/sat_encodings/case_studies                   2m08s   2GB
Jul 20 03:36:14 Starting examples/sat_encodings/translation
Jul 20 03:42:37 Finished examples/sat_encodings/translation                    6m21s   7GB
Jul 20 03:42:37 Starting examples/sat_encodings/translation/compilation
Jul 20 03:44:56 Finished examples/sat_encodings/translation/compilation        2m17s   6GB
Jul 20 03:44:57 Starting examples/deflate
Jul 20 03:46:19 Finished examples/deflate                                      1m20s   2GB
Jul 20 03:46:20 Starting examples/deflate/translation
Jul 20 03:47:59 Finished examples/deflate/translation                          1m38s   8GB
Jul 20 03:48:00 Starting examples/deflate/translation/compilation
Jul 20 03:49:03 Finished examples/deflate/translation/compilation              1m02s   5GB
Jul 20 03:49:04 Starting examples/vipr
Jul 20 03:53:12 Finished examples/vipr                                         4m07s   8GB
Jul 20 03:53:13 Starting examples/vipr/compilation
Jul 20 03:54:28 Finished examples/vipr/compilation                             1m14s   5GB
Jul 20 03:54:29 Starting translator/okasaki-examples
Jul 20 03:59:35 Finished translator/okasaki-examples                           5m05s   4GB
Jul 20 03:59:36 Starting translator/other-examples
Jul 20 04:04:26 Finished translator/other-examples                             4m49s   3GB
Jul 20 04:04:27 Starting compiler/parsing/tests
Jul 20 04:05:01 Finished compiler/parsing/tests                                  33s   1GB
Jul 20 04:05:02 Starting compiler/inference/tests
Jul 20 04:05:42 Finished compiler/inference/tests                                38s   3GB
Jul 20 04:05:43 Starting compiler/printing/test
Jul 20 04:07:17 Finished compiler/printing/test                                1m33s   6GB
Jul 20 04:07:18 Starting icing/flover
Jul 20 04:44:54 Finished icing/flover                                         37m35s   4GB
Jul 20 04:44:55 Starting icing/
Jul 20 05:13:12 Finished icing/                                               28m15s  10GB
Jul 20 05:13:12 Starting icing/examples
Jul 20 05:14:58 Finished icing/examples                                        1m44s   8GB
Jul 20 05:14:58 Starting compiler/repl
Jul 20 05:23:47 Finished compiler/repl                                         8m47s   9GB
Jul 20 05:23:48 Starting unverified/sexpr-bootstrap/x64/64
Jul 20 05:35:28 Finished unverified/sexpr-bootstrap/x64/64                    11m38s  16GB
Jul 20 05:35:29 Starting unverified/sexpr-bootstrap/x64/32
Jul 20 05:45:04 Finished unverified/sexpr-bootstrap/x64/32                     9m34s  14GB
Jul 20 05:45:05 Starting compiler/benchmarks
Jul 20 05:45:49 Finished compiler/benchmarks                                     43s 713MB
Jul 20 05:45:50 Starting compiler/bootstrap/compilation/x64/64
Jul 20 06:40:00 Finished compiler/bootstrap/compilation/x64/64                54m08s 112GB
Jul 20 06:40:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 20 07:02:31 Finished compiler/bootstrap/compilation/x64/64/proofs         22m29s  48GB
Jul 20 07:02:32 Starting compiler/bootstrap/compilation/x64/32
Jul 20 07:39:08 Finished compiler/bootstrap/compilation/x64/32                36m35s  92GB
Jul 20 07:39:09 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 20 07:44:04 Finished compiler/bootstrap/compilation/x64/32/proofs          4m53s  23GB
Jul 20 07:44:04 Starting compiler/bootstrap/compilation/arm8/64
Jul 20 21:14:00 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                                                     (173s)     OK
to_dataBootstrapTheory                                            (108m)     OK
Starting work on to_lab_arm8BootstrapTheory
to_lab_arm8BootstrapTheory                                        (652m)     OK
Starting work on arm8BootstrapTheory
arm8BootstrapTheory                                               (270m)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: 4h24m07s,    gctime: 18m43s,     systime: 20m27s.
           lab_to_target real: 4h44m28s
           lab_to_target size: 75597898
                       export: runtime: 7.7s,    gctime: 0.00000s,     systime: 2.0s.
 error in quse /scratch/cakeml/regression2/cakeml-2468/compiler/bootstrap/compilation/arm8/64/arm8BootstrapScript.sml : HOL_ERR {message = "", origin_function = "dest_SmartAppend", origin_structure = "miscSyntax"}
 error in load /scratch/cakeml/regression2/cakeml-2468/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"}