Job 2395

CakeML:30058919dee54ba63c352c10b14731a85ddb14a3
  Add arm8 bootstrap [Apr 30 10:13:13]
#991 (master)
Merging into:ba448b02f6dfebd0069315be9302ce9471b19ba4
  Fix for proofs broken by sublist in rich_listTheory [May 25 05:59:02]
HOL:19857c9570c4db45bb6410a1ced45b9ab7bb4cb7
  Fixed intLib to avoid noisy output; some cleanups in hurdUtils [May 22 11:23:37]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

May 26 11:09:31 Claimed job
May 26 11:09:33 Reusing HOL
May 26 11:10:16 Starting developers
May 26 11:10:21 Finished developers                                               5s 111MB
May 26 11:10:22 Starting developers/bin
May 26 11:10:28 Finished developers/bin                                           5s   1GB
May 26 11:10:28 Starting compiler/proofs
Jun 02 10:29:19 Resuming compiler/proofs
Jun 02 12:00:56 Finished compiler/proofs                                    1h31m36s  24GB
Jun 02 12:00:56 Starting compiler/bootstrap/translation
Jun 02 20:18:51 Finished compiler/bootstrap/translation                     8h17m54s  34GB
Jun 02 20:18:51 Starting semantics/ffi
Jun 02 20:18:58 Finished semantics/ffi                                            6s 224MB
Jun 02 20:18:58 Starting semantics
Jun 02 20:19:00 Finished semantics                                                1s  19MB
Jun 02 20:19:00 Starting semantics/proofs
Jun 02 20:19:36 Finished semantics/proofs                                        36s   1GB
Jun 02 20:19:37 Starting semantics/alt_semantics
Jun 02 20:20:10 Finished semantics/alt_semantics                                 33s 796MB
Jun 02 20:20:10 Starting semantics/alt_semantics/proofs
Jun 02 20:32:17 Finished semantics/alt_semantics/proofs                       12m06s   1GB
Jun 02 20:32:17 Starting basis/pure
Jun 02 20:32:18 Finished basis/pure                                               1s  21MB
Jun 02 20:32:19 Starting translator
Jun 02 20:34:11 Finished translator                                            1m52s   1GB
Jun 02 20:34:11 Starting compiler/parsing
Jun 02 20:34:13 Finished compiler/parsing                                         1s  23MB
Jun 02 20:34:13 Starting characteristic
Jun 02 20:34:15 Finished characteristic                                           1s  19MB
Jun 02 20:34:15 Starting translator/monadic
Jun 02 20:34:17 Finished translator/monadic                                       1s  19MB
Jun 02 20:34:17 Starting basis
Jun 02 20:37:58 Finished basis                                                 3m40s   3GB
Jun 02 20:37:58 Starting compiler/inference
Jun 02 20:38:00 Finished compiler/inference                                       1s  22MB
Jun 02 20:38:00 Starting compiler/backend/reg_alloc
Jun 02 20:38:01 Finished compiler/backend/reg_alloc                               1s  19MB
Jun 02 20:38:01 Starting compiler/backend/gc
Jun 02 20:38:04 Finished compiler/backend/gc                                      2s  23MB
Jun 02 20:38:04 Starting compiler/backend
Jun 02 20:38:18 Finished compiler/backend                                        13s 708MB
Jun 02 20:38:18 Starting compiler/encoders/asm
Jun 02 20:38:20 Finished compiler/encoders/asm                                    1s  27MB
Jun 02 20:38:20 Starting compiler/encoders/x64
Jun 02 20:38:22 Finished compiler/encoders/x64                                    1s  21MB
Jun 02 20:38:22 Starting compiler/encoders/arm7
Jun 02 20:38:24 Finished compiler/encoders/arm7                                   1s  29MB
Jun 02 20:38:24 Starting compiler/encoders/arm8
Jun 02 20:38:26 Finished compiler/encoders/arm8                                   1s  24MB
Jun 02 20:38:26 Starting compiler/encoders/arm8_asl
Jun 02 20:41:41 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Jun 02 20:41:41 Starting compiler/encoders/mips
Jun 02 20:41:43 Finished compiler/encoders/mips                                   1s  20MB
Jun 02 20:41:43 Starting compiler/encoders/riscv
Jun 02 20:41:45 Finished compiler/encoders/riscv                                  1s  20MB
Jun 02 20:41:45 Starting compiler/encoders/ag32
Jun 02 20:41:47 Finished compiler/encoders/ag32                                   1s  27MB
Jun 02 20:41:47 Starting compiler/backend/x64
Jun 02 20:41:49 Finished compiler/backend/x64                                     2s  26MB
Jun 02 20:41:49 Starting compiler/backend/arm7
Jun 02 20:41:51 Finished compiler/backend/arm7                                    2s  23MB
Jun 02 20:41:51 Starting compiler/backend/arm8
Jun 02 20:41:54 Finished compiler/backend/arm8                                    2s  22MB
Jun 02 20:41:54 Starting compiler/backend/mips
Jun 02 20:41:56 Finished compiler/backend/mips                                    2s  26MB
Jun 02 20:41:56 Starting compiler/backend/riscv
Jun 02 20:41:59 Finished compiler/backend/riscv                                   2s  25MB
Jun 02 20:41:59 Starting compiler/backend/ag32
Jun 02 20:43:25 Finished compiler/backend/ag32                                 1m26s   1GB
Jun 02 20:43:25 Starting compiler/parsing/proofs
Jun 02 20:43:27 Finished compiler/parsing/proofs                                  1s  19MB
Jun 02 20:43:27 Starting compiler/inference/proofs
Jun 02 20:43:29 Finished compiler/inference/proofs                                1s  25MB
Jun 02 20:43:29 Starting compiler/backend/semantics
Jun 02 20:47:23 Finished compiler/backend/semantics                            3m53s   1GB
Jun 02 20:47:23 Starting compiler/backend/reg_alloc/proofs
Jun 02 20:47:25 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Jun 02 20:47:25 Starting compiler/backend/proofs
Jun 02 20:48:25 Finished compiler/backend/proofs                               1m00s   2GB
Jun 02 20:48:25 Starting compiler/backend/serialiser
Jun 02 20:48:28 Finished compiler/backend/serialiser                              2s  45MB
Jun 02 20:48:28 Starting compiler/encoders/x64/proofs
Jun 02 20:58:27 Finished compiler/encoders/x64/proofs                          9m58s   4GB
Jun 02 20:58:27 Starting compiler/encoders/arm7/proofs
Jun 02 21:12:05 Finished compiler/encoders/arm7/proofs                        13m37s   4GB
Jun 02 21:12:05 Starting compiler/encoders/arm8/proofs
Jun 02 21:19:04 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Jun 02 21:19:04 Starting compiler/encoders/arm8_asl/proofs
Jun 02 21:35:01 Finished compiler/encoders/arm8_asl/proofs                    15m57s   1GB
Jun 02 21:35:02 Starting compiler/encoders/mips/proofs
Jun 02 21:45:26 Finished compiler/encoders/mips/proofs                        10m24s   3GB
Jun 02 21:45:26 Starting compiler/encoders/riscv/proofs
Jun 02 21:54:15 Finished compiler/encoders/riscv/proofs                        8m48s   2GB
Jun 02 21:54:15 Starting compiler/encoders/ag32/proofs
Jun 02 21:56:49 Finished compiler/encoders/ag32/proofs                         2m33s   1GB
Jun 02 21:56:49 Starting compiler/backend/x64/proofs
Jun 02 21:57:22 Finished compiler/backend/x64/proofs                             32s   1GB
Jun 02 21:57:22 Starting compiler/backend/arm7/proofs
Jun 02 21:57:56 Finished compiler/backend/arm7/proofs                            34s   1GB
Jun 02 21:57:56 Starting compiler/backend/arm8/proofs
Jun 02 21:58:29 Finished compiler/backend/arm8/proofs                            33s   1GB
Jun 02 21:58:29 Starting compiler/backend/arm8_asl
Jun 02 21:58:54 Finished compiler/backend/arm8_asl                               24s   2GB
Jun 02 21:58:54 Starting compiler/backend/mips/proofs
Jun 02 21:59:29 Finished compiler/backend/mips/proofs                            34s   2GB
Jun 02 21:59:29 Starting compiler/backend/riscv/proofs
Jun 02 22:00:06 Finished compiler/backend/riscv/proofs                           36s   2GB
Jun 02 22:00:06 Starting compiler/backend/ag32/proofs
Jun 02 22:14:43 Finished compiler/backend/ag32/proofs                         14m37s   3GB
Jun 02 22:14:43 Starting candle/set-theory
Jun 02 22:15:26 Finished candle/set-theory                                       42s   1GB
Jun 02 22:15:26 Starting candle/syntax-lib
Jun 02 22:15:28 Finished candle/syntax-lib                                        1s  20MB
Jun 02 22:15:28 Starting candle/standard/syntax
Jun 02 22:15:40 Finished candle/standard/syntax                                  12s 849MB
Jun 02 22:15:40 Starting candle/standard/semantics
Jun 02 22:17:54 Finished candle/standard/semantics                             2m13s   1GB
Jun 02 22:17:54 Starting candle/standard/monadic
Jun 02 22:17:56 Finished candle/standard/monadic                                  1s  26MB
Jun 02 22:17:56 Starting candle/standard/ml_kernel
Jun 02 22:19:43 Finished candle/standard/ml_kernel                             1m46s   3GB
Jun 02 22:19:43 Starting candle/overloading/syntax
Jun 02 22:23:17 Finished candle/overloading/syntax                             3m33s   1GB
Jun 02 22:23:17 Starting candle/overloading/semantics
Jun 02 22:35:48 Finished candle/overloading/semantics                         12m30s   2GB
Jun 02 22:35:48 Starting candle/overloading/monadic
Jun 02 22:38:37 Finished candle/overloading/monadic                            2m49s   1GB
Jun 02 22:38:37 Starting candle/overloading/ml_kernel
Jun 02 22:46:44 Finished candle/overloading/ml_kernel                          8m06s   4GB
Jun 02 22:46:45 Starting candle/overloading/ml_checker
Jun 02 22:49:24 Finished candle/overloading/ml_checker                         2m39s   3GB
Jun 02 22:49:24 Starting candle/prover
Jun 02 22:59:56 Finished candle/prover                                        10m31s   3GB
Jun 02 22:59:56 Starting pancake
Jun 02 23:00:45 Finished pancake                                                 48s 968MB
Jun 02 23:00:45 Starting pancake/ffi
Jun 02 23:00:45 Finished pancake/ffi                                              0s  13MB
Jun 02 23:00:46 Starting pancake/semantics
Jun 02 23:03:43 Finished pancake/semantics                                     2m57s   1GB
Jun 02 23:03:43 Starting pancake/parser
Jun 02 23:04:11 Finished pancake/parser                                          27s 736MB
Jun 02 23:04:11 Starting pancake/proofs
Jun 02 23:39:28 Finished pancake/proofs                                       35m16s   4GB
Jun 02 23:39:28 Starting characteristic/examples
Jun 02 23:41:03 Finished characteristic/examples                               1m34s   3GB
Jun 02 23:41:03 Starting tutorial/solutions
Jun 02 23:56:44 Finished tutorial/solutions                                   15m40s   9GB
Jun 02 23:56:44 Starting translator/monadic/examples
Jun 03 00:01:01 Finished translator/monadic/examples                           4m17s   3GB
Jun 03 00:01:01 Starting examples
Jun 03 00:16:50 Finished examples                                             15m48s   3GB
Jun 03 00:16:50 Starting examples/compilation/x64
Jun 03 02:18:28 Finished examples/compilation/x64                           2h01m38s  17GB
Jun 03 02:18:28 Starting examples/compilation/x64/proofs
Jun 03 02:21:15 Finished examples/compilation/x64/proofs                       2m46s   4GB
Jun 03 02:21:15 Starting examples/compilation/ag32
Jun 03 02:52:18 Finished examples/compilation/ag32                            31m03s   7GB
Jun 03 02:52:18 Starting examples/compilation/ag32/proofs
Jun 03 02:53:23 Finished examples/compilation/ag32/proofs                      1m04s   5GB
Jun 03 02:53:23 Starting examples/compilation/to_word
Jun 03 02:56:51 Finished examples/compilation/to_word                          3m27s   7GB
Jun 03 02:56:51 Starting examples/lpr_checker
Jun 03 02:58:01 Finished examples/lpr_checker                                  1m10s   1GB
Jun 03 02:58:01 Starting examples/lpr_checker/array
Jun 03 03:28:42 Finished examples/lpr_checker/array                           30m40s   8GB
Jun 03 03:28:42 Starting examples/lpr_checker/array/compilation
Jun 03 04:23:43 Finished examples/lpr_checker/array/compilation               55m01s  23GB
Jun 03 04:23:43 Starting examples/lpr_checker/array/compilation/proofs
Jun 03 04:25:37 Finished examples/lpr_checker/array/compilation/proofs         1m53s   3GB
Jun 03 04:25:37 Starting examples/lpr_checker/array/compilation/proofsARM8
Jun 03 04:33:12 Finished examples/lpr_checker/array/compilation/proofsARM8     7m35s  19GB
Jun 03 04:33:12 Starting examples/xlrup_checker
Jun 03 04:34:18 Finished examples/xlrup_checker                                1m05s   1GB
Jun 03 04:34:18 Starting examples/xlrup_checker/array
Jun 03 04:50:27 Finished examples/xlrup_checker/array                         16m08s   6GB
Jun 03 04:50:27 Starting examples/xlrup_checker/array/compilation
Jun 03 05:13:22 Finished examples/xlrup_checker/array/compilation             22m54s  20GB
Jun 03 05:13:22 Starting examples/xlrup_checker/array/compilation/proofs
Jun 03 05:14:25 Finished examples/xlrup_checker/array/compilation/proofs       1m03s   4GB
Jun 03 05:14:25 Starting examples/pseudo_bool
Jun 03 05:16:29 Finished examples/pseudo_bool                                  2m03s   1GB
Jun 03 05:16:29 Starting examples/pseudo_bool/cnf_encoding
Jun 03 05:16:59 Finished examples/pseudo_bool/cnf_encoding                       30s   1GB
Jun 03 05:16:59 Starting examples/pseudo_bool/graph_encoding
Jun 03 05:17:45 Finished examples/pseudo_bool/graph_encoding                     45s   1GB
Jun 03 05:17:45 Starting examples/pseudo_bool/array
Jun 03 06:28:46 Finished examples/pseudo_bool/array                         1h11m00s   8GB
Jun 03 06:28:46 Starting examples/pseudo_bool/array/compilation
Jun 03 14:26:13 Finished examples/pseudo_bool/array/compilation             7h57m26s  62GB
Jun 03 14:26:13 Starting examples/pseudo_bool/array/compilation/proofs
Jun 03 14:28:58 Finished examples/pseudo_bool/array/compilation/proofs         2m44s   6GB
Jun 03 14:28:58 Starting examples/opentheory
Jun 03 14:40:03 Finished examples/opentheory                                  11m05s   4GB
Jun 03 14:40:03 Starting examples/opentheory
Jun 03 14:40:05 Finished examples/opentheory                                      1s  31MB
Jun 03 14:40:05 Starting examples/opentheory/compilation
Jun 03 15:17:42 Finished examples/opentheory/compilation                      37m36s  32GB
Jun 03 15:17:42 Starting examples/opentheory/compilation/proofs
Jun 03 15:18:48 Finished examples/opentheory/compilation/proofs                1m05s   5GB
Jun 03 15:18:48 Starting examples/opentheory/compilation/ag32
Jun 03 15:53:09 Finished examples/opentheory/compilation/ag32                 34m20s  31GB
Jun 03 15:53:09 Starting examples/opentheory/compilation/ag32/proofs
Jun 03 15:55:09 Finished examples/opentheory/compilation/ag32/proofs           1m59s   4GB
Jun 03 15:55:09 Starting examples/sat_encodings
Jun 03 15:57:31 Finished examples/sat_encodings                                2m22s   1GB
Jun 03 15:57:31 Starting examples/sat_encodings/case_studies
Jun 03 15:59:25 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Jun 03 15:59:26 Starting examples/sat_encodings/translation
Jun 03 16:05:52 Finished examples/sat_encodings/translation                    6m26s   5GB
Jun 03 16:05:52 Starting examples/sat_encodings/translation/compilation
Jun 03 16:52:49 Finished examples/sat_encodings/translation/compilation       46m56s  22GB
Jun 03 16:52:49 Starting examples/deflate
Jun 03 16:53:58 Finished examples/deflate                                      1m08s 856MB
Jun 03 16:53:58 Starting examples/deflate/translation
Jun 03 16:55:47 Finished examples/deflate/translation                          1m48s   3GB
Jun 03 16:55:47 Starting examples/deflate/translation/compilation
Jun 03 17:16:16 Finished examples/deflate/translation/compilation             20m29s  13GB
Jun 03 17:16:17 Starting examples/vipr
Jun 03 17:20:27 Finished examples/vipr                                         4m10s   4GB
Jun 03 17:20:28 Starting examples/vipr/compilation
Jun 03 17:41:37 Finished examples/vipr/compilation                            21m09s  21GB
Jun 03 17:41:37 Starting translator/okasaki-examples
Jun 03 17:47:01 Finished translator/okasaki-examples                           5m24s   2GB
Jun 03 17:47:01 Starting translator/other-examples
Jun 03 17:50:54 Finished translator/other-examples                             3m53s   2GB
Jun 03 17:50:54 Starting compiler/parsing/tests
Jun 03 17:51:28 Finished compiler/parsing/tests                                  33s   1GB
Jun 03 17:51:28 Starting compiler/inference/tests
Jun 03 18:00:09 Finished compiler/inference/tests                              8m41s   7GB
Jun 03 18:00:10 Starting compiler/printing/test
Jun 03 18:04:12 Finished compiler/printing/test                                4m02s   3GB
Jun 03 18:04:12 Starting icing/flover
Jun 03 18:49:28 Finished icing/flover                                         45m15s   2GB
Jun 03 18:49:28 Starting icing/
Jun 03 19:43:17 Finished icing/                                               53m48s   5GB
Jun 03 19:43:17 Starting icing/examples
Jun 03 19:44:58 Finished icing/examples                                        1m40s   3GB
Jun 03 19:44:58 Starting compiler/repl
Jun 03 19:53:47 Finished compiler/repl                                         8m49s   6GB
Jun 03 19:53:47 Starting unverified/sexpr-bootstrap/x64/64
Jun 03 20:07:34 Finished unverified/sexpr-bootstrap/x64/64                    13m46s  17GB
Jun 03 20:07:34 Starting unverified/sexpr-bootstrap/x64/32
Jun 03 20:18:37 Finished unverified/sexpr-bootstrap/x64/32                    11m03s  14GB
Jun 03 20:18:37 Starting compiler/benchmarks
Jun 03 20:34:32 Finished compiler/benchmarks                                  15m54s   2GB
Jun 03 20:34:32 Starting compiler/bootstrap/compilation/x64/64
Jun 04 09:09:45 Finished compiler/bootstrap/compilation/x64/64             12h35m12s  63GB
Jun 04 09:09:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 04 09:30:55 Finished compiler/bootstrap/compilation/x64/64/proofs         21m10s  21GB
Jun 04 09:30:56 Starting compiler/bootstrap/compilation/x64/32
Jun 04 16:54:39 Finished compiler/bootstrap/compilation/x64/32              7h23m43s  63GB
Jun 04 16:54:39 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 04 16:57:58 Finished compiler/bootstrap/compilation/x64/32/proofs          3m18s  20GB
Jun 04 16:57:58 Starting compiler/bootstrap/compilation/arm8/64
Jun 05 06:26:44 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$(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/inference/proofs[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/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanned 98 directories
Starting work on README.md
Starting work on to_dataBootstrapTheory
Starting work on cake-sexpr-64
README.md                                                                                                   (0s)     OK
cake-sexpr-64                                                                                             (149s)     OK
to_dataBootstrapTheory                                                                                    (112m)     OK
Starting work on to_lab_arm8BootstrapTheory
to_lab_arm8BootstrapTheory                                                                                (665m)     OK
Starting work on arm8BootstrapTheory
arm8BootstrapTheory                                                                                       (245m)     OK
Starting work on arm8_config_encTheory
arm8_config_encTheory                                                                                     (136m)     OK
Don't know how to build necessary target(s): /home/cug/hk324/cml-regression/cakeml-2395/compiler/bootstrap/compilation/arm8/64/sexprBootstrap32Script.sml