Job 1548

CakeML:76ed0b05089a77059dee72d197fc56c3dae661e8
  Merge pull request #829 from CakeML/help [Jun 18 08:39:57]
HOL:b7716bd92d1115f6a85cbf82d4dd47e1bb88828a
  Remove unnecessary dependencies in examples/polynomial/polynomial [Jun 09 01:52:42]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jun 18 08:40:02 Claimed job
Jun 18 08:40:04 Reusing HOL
Jun 18 08:40:50 Starting developers
Jun 18 08:40:55 Finished developers                                               4s 155MB
Jun 18 08:40:55 Starting developers/bin
Jun 18 08:41:01 Finished developers/bin                                           6s   1GB
Jun 18 08:41:01 Starting semantics/ffi
Jun 18 08:41:13 Finished semantics/ffi                                           11s 240MB
Jun 18 08:41:13 Starting semantics
Jun 18 08:42:36 Finished semantics                                             1m22s   1GB
Jun 18 08:42:36 Starting semantics/proofs
Jun 18 08:46:05 Finished semantics/proofs                                      3m28s   1GB
Jun 18 08:46:05 Starting semantics/alt_semantics
Jun 18 08:46:14 Finished semantics/alt_semantics                                  9s 324MB
Jun 18 08:46:14 Starting semantics/alt_semantics/proofs
Jun 18 08:48:28 Finished semantics/alt_semantics/proofs                        2m13s 806MB
Jun 18 08:48:28 Starting basis/pure
Jun 18 08:49:19 Finished basis/pure                                              50s 847MB
Jun 18 08:49:19 Starting translator
Jun 18 08:52:35 Finished translator                                            3m15s   1GB
Jun 18 08:52:35 Starting compiler/parsing
Jun 18 08:53:44 Finished compiler/parsing                                      1m09s   3GB
Jun 18 08:53:45 Starting characteristic
Jun 18 08:59:31 Finished characteristic                                        5m46s   1GB
Jun 18 08:59:31 Starting translator/monadic
Jun 18 09:01:13 Finished translator/monadic                                    1m41s   2GB
Jun 18 09:01:13 Starting basis
Jun 18 09:44:33 Finished basis                                                43m19s  20GB
Jun 18 09:44:34 Starting compiler/inference
Jun 18 09:45:41 Finished compiler/inference                                    1m07s   1GB
Jun 18 09:45:41 Starting compiler/backend/reg_alloc
Jun 18 09:46:49 Finished compiler/backend/reg_alloc                            1m07s   1GB
Jun 18 09:46:49 Starting compiler/backend/gc
Jun 18 09:50:10 Finished compiler/backend/gc                                   3m20s   2GB
Jun 18 09:50:10 Starting compiler/backend
Jun 18 09:55:01 Finished compiler/backend                                      4m50s   3GB
Jun 18 09:55:01 Starting compiler/encoders/asm
Jun 18 09:55:23 Finished compiler/encoders/asm                                   22s 739MB
Jun 18 09:55:23 Starting compiler/encoders/x64
Jun 18 09:55:49 Finished compiler/encoders/x64                                   25s   1GB
Jun 18 09:55:49 Starting compiler/encoders/arm7
Jun 18 09:56:40 Finished compiler/encoders/arm7                                  50s 826MB
Jun 18 09:56:40 Starting compiler/encoders/arm8
Jun 18 09:56:53 Finished compiler/encoders/arm8                                  12s 971MB
Jun 18 09:56:53 Starting compiler/encoders/mips
Jun 18 09:57:11 Finished compiler/encoders/mips                                  17s   1GB
Jun 18 09:57:11 Starting compiler/encoders/riscv
Jun 18 09:57:27 Finished compiler/encoders/riscv                                 15s 904MB
Jun 18 09:57:27 Starting compiler/encoders/ag32
Jun 18 09:57:45 Finished compiler/encoders/ag32                                  17s 571MB
Jun 18 09:57:45 Starting compiler/backend/x64
Jun 18 09:58:04 Finished compiler/backend/x64                                    18s   1GB
Jun 18 09:58:05 Starting compiler/backend/arm7
Jun 18 09:58:26 Finished compiler/backend/arm7                                   21s   1GB
Jun 18 09:58:26 Starting compiler/backend/arm8
Jun 18 09:58:44 Finished compiler/backend/arm8                                   17s   1GB
Jun 18 09:58:44 Starting compiler/backend/mips
Jun 18 09:59:04 Finished compiler/backend/mips                                   19s   1GB
Jun 18 09:59:04 Starting compiler/backend/riscv
Jun 18 09:59:24 Finished compiler/backend/riscv                                  19s   1GB
Jun 18 09:59:24 Starting compiler/backend/ag32
Jun 18 10:00:32 Finished compiler/backend/ag32                                 1m08s   1GB
Jun 18 10:00:33 Starting compiler/parsing/proofs
Jun 18 10:06:33 Finished compiler/parsing/proofs                               5m59s   1GB
Jun 18 10:06:33 Starting compiler/inference/proofs
Jun 18 10:09:01 Finished compiler/inference/proofs                             2m28s   1GB
Jun 18 10:09:01 Starting compiler/backend/semantics
Jun 18 10:37:13 Finished compiler/backend/semantics                           28m11s   2GB
Jun 18 10:37:13 Starting compiler/backend/reg_alloc/proofs
Jun 18 10:40:37 Finished compiler/backend/reg_alloc/proofs                     3m23s   1GB
Jun 18 10:40:37 Starting compiler/backend/proofs
Jun 18 11:31:57 Finished compiler/backend/proofs                              51m19s  22GB
Jun 18 11:31:57 Starting compiler/encoders/x64/proofs
Jun 18 11:41:37 Finished compiler/encoders/x64/proofs                          9m40s   4GB
Jun 18 11:41:38 Starting compiler/encoders/arm7/proofs
Jun 18 11:54:45 Finished compiler/encoders/arm7/proofs                        13m06s   3GB
Jun 18 11:54:45 Starting compiler/encoders/arm8/proofs
Jun 18 12:01:29 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
Jun 18 12:01:29 Starting compiler/encoders/mips/proofs
Jun 18 12:11:27 Finished compiler/encoders/mips/proofs                         9m57s   3GB
Jun 18 12:11:27 Starting compiler/encoders/riscv/proofs
Jun 18 12:20:11 Finished compiler/encoders/riscv/proofs                        8m44s   1GB
Jun 18 12:20:12 Starting compiler/encoders/ag32/proofs
Jun 18 12:22:46 Finished compiler/encoders/ag32/proofs                         2m34s 672MB
Jun 18 12:22:46 Starting compiler/backend/x64/proofs
Jun 18 12:23:09 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 18 12:23:09 Starting compiler/backend/arm7/proofs
Jun 18 12:23:31 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 18 12:23:31 Starting compiler/backend/arm8/proofs
Jun 18 12:23:54 Finished compiler/backend/arm8/proofs                            22s   1GB
Jun 18 12:23:54 Starting compiler/backend/mips/proofs
Jun 18 12:24:16 Finished compiler/backend/mips/proofs                            21s   1GB
Jun 18 12:24:16 Starting compiler/backend/riscv/proofs
Jun 18 12:24:38 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 18 12:24:38 Starting compiler/backend/ag32/proofs
Jun 18 12:37:02 Finished compiler/backend/ag32/proofs                         12m23s   4GB
Jun 18 12:37:02 Starting compiler/proofs
Jun 18 12:38:45 Finished compiler/proofs                                       1m42s   3GB
Jun 18 12:38:45 Starting candle/set-theory
Jun 18 12:39:14 Finished candle/set-theory                                       29s 872MB
Jun 18 12:39:14 Starting candle/syntax-lib
Jun 18 12:39:25 Finished candle/syntax-lib                                       10s 742MB
Jun 18 12:39:25 Starting candle/standard/syntax
Jun 18 12:41:16 Finished candle/standard/syntax                                1m51s   1GB
Jun 18 12:41:16 Starting candle/standard/semantics
Jun 18 12:43:00 Finished candle/standard/semantics                             1m43s   1GB
Jun 18 12:43:00 Starting candle/standard/monadic
Jun 18 12:44:43 Finished candle/standard/monadic                               1m41s   1GB
Jun 18 12:44:43 Starting candle/standard/ml_kernel
Jun 18 12:50:20 Finished candle/standard/ml_kernel                             5m37s   6GB
Jun 18 12:50:20 Starting candle/overloading/syntax
Jun 18 12:53:27 Finished candle/overloading/syntax                             3m06s   1GB
Jun 18 12:53:27 Starting candle/overloading/semantics
Jun 18 13:05:27 Finished candle/overloading/semantics                         12m00s   4GB
Jun 18 13:05:27 Starting characteristic/examples
Jun 18 13:06:47 Finished characteristic/examples                               1m19s   2GB
Jun 18 13:06:47 Starting tutorial/solutions
Jun 18 13:22:22 Finished tutorial/solutions                                   15m34s  14GB
Jun 18 13:22:22 Starting translator/monadic/examples
Jun 18 13:25:30 Finished translator/monadic/examples                           3m07s   2GB
Jun 18 13:25:30 Starting examples
Jun 18 13:33:52 Finished examples                                              8m22s   3GB
Jun 18 13:33:52 Starting examples/compilation/x64
Jun 18 15:58:24 Finished examples/compilation/x64                           2h24m32s  15GB
Jun 18 15:58:24 Starting examples/compilation/x64/proofs
Jun 18 16:00:18 Finished examples/compilation/x64/proofs                       1m53s   3GB
Jun 18 16:00:18 Starting examples/compilation/ag32
Jun 18 16:35:28 Finished examples/compilation/ag32                            35m10s   7GB
Jun 18 16:35:28 Starting examples/compilation/ag32/proofs
Jun 18 16:36:15 Finished examples/compilation/ag32/proofs                        46s   2GB
Jun 18 16:36:15 Starting examples/cost
Jun 18 17:29:56 Finished examples/cost                                        53m40s   7GB
Jun 18 17:29:56 Starting examples/lpr_checker
Jun 18 17:33:56 Finished examples/lpr_checker                                  4m00s   2GB
Jun 18 17:33:56 Starting examples/lpr_checker/compilation
Jun 18 17:51:49 Finished examples/lpr_checker/compilation                     17m52s  10GB
Jun 18 17:51:49 Starting examples/lpr_checker/compilation/proofs
Jun 18 17:52:32 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Jun 18 17:52:32 Starting examples/lpr_checker/array
Jun 18 18:06:47 Finished examples/lpr_checker/array                           14m15s   3GB
Jun 18 18:06:48 Starting examples/lpr_checker/array/compilation
Jun 18 18:26:35 Finished examples/lpr_checker/array/compilation               19m47s  13GB
Jun 18 18:26:35 Starting examples/lpr_checker/array/compilation/proofs
Jun 18 18:27:48 Finished examples/lpr_checker/array/compilation/proofs         1m12s   3GB
Jun 18 18:27:48 Starting examples/opentheory
Jun 18 18:37:25 Finished examples/opentheory                                   9m37s   6GB
Jun 18 18:37:25 Starting examples/opentheory
Jun 18 18:37:26 Finished examples/opentheory                                      1s  31MB
Jun 18 18:37:26 Starting examples/opentheory/compilation
Jun 18 19:09:34 Finished examples/opentheory/compilation                      32m08s  18GB
Jun 18 19:09:35 Starting examples/opentheory/compilation/proofs
Jun 18 19:10:15 Finished examples/opentheory/compilation/proofs                  40s   3GB
Jun 18 19:10:16 Starting examples/opentheory/compilation/ag32
Jun 18 19:43:57 Finished examples/opentheory/compilation/ag32                 33m41s  19GB
Jun 18 19:43:57 Starting examples/opentheory/compilation/ag32/proofs
Jun 18 19:45:32 Finished examples/opentheory/compilation/ag32/proofs           1m34s   5GB
Jun 18 19:45:32 Starting examples/sat_encodings
Jun 18 19:47:19 Finished examples/sat_encodings                                1m46s 786MB
Jun 18 19:47:19 Starting examples/sat_encodings/case_studies
Jun 18 19:48:50 Finished examples/sat_encodings/case_studies                   1m30s   1GB
Jun 18 19:48:50 Starting examples/sat_encodings/translation
Jun 18 19:54:37 Finished examples/sat_encodings/translation                    5m46s   3GB
Jun 18 19:54:37 Starting examples/sat_encodings/translation/compilation
Jun 18 20:34:59 Finished examples/sat_encodings/translation/compilation       40m22s  14GB
Jun 18 20:34:59 Starting translator/okasaki-examples
Jun 18 20:39:23 Finished translator/okasaki-examples                           4m23s   1GB
Jun 18 20:39:23 Starting translator/other-examples
Jun 18 20:41:26 Finished translator/other-examples                             2m03s   1GB
Jun 18 20:41:26 Starting compiler/parsing/tests
Jun 18 20:41:52 Finished compiler/parsing/tests                                  25s 582MB
Jun 18 20:41:52 Starting compiler/inference/tests
Jun 18 20:49:46 Finished compiler/inference/tests                              7m54s   3GB
Jun 18 20:49:46 Starting compiler/bootstrap/translation
Jun 18 23:17:49 Finished compiler/bootstrap/translation                     2h28m01s  24GB
Jun 18 23:17:49 Starting unverified/sexpr-bootstrap/x64/64
Jun 18 23:30:01 Finished unverified/sexpr-bootstrap/x64/64                    12m11s   8GB
Jun 18 23:30:01 Starting unverified/sexpr-bootstrap/x64/32
Jun 18 23:40:45 Finished unverified/sexpr-bootstrap/x64/32                    10m43s   8GB
Jun 18 23:40:46 Starting compiler/benchmarks
Jun 18 23:40:47 Finished compiler/benchmarks                                      1s  40MB
Jun 18 23:40:48 Starting compiler/bootstrap/compilation/x64/64
Jun 19 12:43:23 Finished compiler/bootstrap/compilation/x64/64             13h02m34s  64GB
Jun 19 12:43:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 19 12:43:27 FAILED: compiler/bootstrap/compilation/x64/64/proofs
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/model
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/model
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/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Starting work on README.md
Starting work on x64BootstrapProofTheory
README.md                                                                                                                                                   real:    0s  user:    0s     OK
x64BootstrapProofTheory                                                                                                                                     real:    0s  user:    0sFAIL<1>
 WARNING: /home/cug/hk324/cakeml/.holpath overrides value for CAKEMLDIR from /home/cug/hk324/cml-regression/cakeml-1548/.holpath
 Cannot find file /home/cug/hk324/cakeml/compiler/backend/proofs/backendProofTheory.ui
 error in load $(CAKEMLDIR)/compiler/backend/proofs/backendProofTheory : Fail "Cannot find file /home/cug/hk324/cakeml/compiler/backend/proofs/backendProofTheory.ui"
 error in load /home/cug/hk324/cml-regression/cakeml-1548/compiler/bootstrap/compilation/x64/64/proofs/x64BootstrapProofScript : Fail "Cannot find file /home/cug/hk324/cakeml/compiler/backend/proofs/backendProofTheory.ui"
 Uncaught exception: Fail "Cannot find file /home/cug/hk324/cakeml/compiler/backend/proofs/backendProofTheory.ui"
2021-06-21T00:11:31Z Resuming compiler/bootstrap/compilation/x64/64/proofs
2021-06-21T00:11:35Z FAILED: compiler/bootstrap/compilation/x64/64/proofs
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/model
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/model
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/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Starting work on x64BootstrapProofTheory
x64BootstrapProofTheory                                                                                                                                     real:    2s  user:    1sFAIL<1>
 error in load $(CAKEMLDIR)/basis/pure/mlstringTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load $(CAKEMLDIR)/compiler/backend/closLangTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load $(CAKEMLDIR)/compiler/backend/bviTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load $(CAKEMLDIR)/compiler/backend/bvi_to_dataTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load $(CAKEMLDIR)/compiler/backend/proofs/bvi_to_dataProofTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load $(CAKEMLDIR)/compiler/backend/proofs/backendProofTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 error in load /home/cug/hk324/cml-regression/cakeml-1548/compiler/bootstrap/compilation/x64/64/proofs/x64BootstrapProofScript : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"
 <<HOL message: link_parents: the following parents of "byte"
   should already be in the theory graph (but aren't): ("words",1621956107,641615)>>
 Uncaught exception: TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}"