Job 2072

CakeML:d37da9f29b19f03e870f9bce50d3380c60fbac4d
  Minor update to README of Dandelion [Dec 12 10:20:13]
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:0cdd3535ed2f647e048a3741f226dd1bdbb3fcbd
  Tidy itreeTau changes (remove Unicode; fix over-long lines; reduce pr [Dec 11 22:45:07]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Dec 12 10:25:30 Claimed job
Dec 12 10:25:36 Building HOL
Dec 12 10:37:00 Starting developers
Dec 12 10:37:05 Finished developers                                               5s 105MB
Dec 12 10:37:05 Starting developers/bin
Dec 12 10:37:11 Finished developers/bin                                           5s   1GB
Dec 12 10:37:11 Starting floatingPoint/tools/dandelion
Dec 12 10:47:21 Finished floatingPoint/tools/dandelion                        10m09s   1GB
Dec 12 10:47:22 Starting floatingPoint/icing/
Dec 12 13:27:56 Finished floatingPoint/icing/                               2h40m32s  16GB
Dec 12 13:27:56 Starting floatingPoint/icing/examples
Dec 12 13:29:34 Finished floatingPoint/icing/examples                          1m38s   6GB
Dec 12 13:29:34 Starting floatingPoint/libmGen/
Dec 12 14:12:18 Finished floatingPoint/libmGen/                               42m43s   6GB
Dec 12 14:12:18 Starting compiler/proofs
Dec 12 14:17:38 Finished compiler/proofs                                       5m19s   3GB
Dec 12 14:17:38 Starting compiler/bootstrap/translation
Dec 12 19:16:02 Finished compiler/bootstrap/translation                     4h58m22s  51GB
Dec 12 19:16:02 Starting semantics/ffi
Dec 12 19:16:06 Finished semantics/ffi                                            3s 219MB
Dec 12 19:16:06 Starting semantics
Dec 12 19:16:08 Finished semantics                                                1s  21MB
Dec 12 19:16:08 Starting semantics/proofs
Dec 12 19:16:39 Finished semantics/proofs                                        30s 757MB
Dec 12 19:16:39 Starting semantics/alt_semantics
Dec 12 19:17:06 Finished semantics/alt_semantics                                 27s 530MB
Dec 12 19:17:07 Starting semantics/alt_semantics/proofs
Dec 12 19:29:04 Finished semantics/alt_semantics/proofs                       11m57s   1GB
Dec 12 19:29:05 Starting basis/pure
Dec 12 19:29:06 Finished basis/pure                                               1s  17MB
Dec 12 19:29:06 Starting translator
Dec 12 19:30:56 Finished translator                                            1m49s   1GB
Dec 12 19:30:56 Starting compiler/parsing
Dec 12 19:30:58 Finished compiler/parsing                                         1s  19MB
Dec 12 19:30:58 Starting characteristic
Dec 12 19:31:00 Finished characteristic                                           1s  23MB
Dec 12 19:31:00 Starting translator/monadic
Dec 12 19:31:02 Finished translator/monadic                                       1s  26MB
Dec 12 19:31:02 Starting basis
Dec 12 19:34:27 Finished basis                                                 3m24s   2GB
Dec 12 19:34:27 Starting compiler/inference
Dec 12 19:34:29 Finished compiler/inference                                       1s  20MB
Dec 12 19:34:29 Starting compiler/backend/reg_alloc
Dec 12 19:34:30 Finished compiler/backend/reg_alloc                               1s  19MB
Dec 12 19:34:30 Starting compiler/backend/gc
Dec 12 19:34:33 Finished compiler/backend/gc                                      2s  26MB
Dec 12 19:34:33 Starting compiler/backend
Dec 12 19:34:43 Finished compiler/backend                                        10s 531MB
Dec 12 19:34:44 Starting compiler/encoders/asm
Dec 12 19:34:45 Finished compiler/encoders/asm                                    1s  25MB
Dec 12 19:34:45 Starting compiler/encoders/x64
Dec 12 19:34:47 Finished compiler/encoders/x64                                    1s  27MB
Dec 12 19:34:47 Starting compiler/encoders/arm7
Dec 12 19:34:49 Finished compiler/encoders/arm7                                   1s  24MB
Dec 12 19:34:49 Starting compiler/encoders/arm8
Dec 12 19:34:51 Finished compiler/encoders/arm8                                   1s  23MB
Dec 12 19:34:51 Starting compiler/encoders/arm8_asl
Dec 12 21:54:59 Finished compiler/encoders/arm8_asl                         2h20m06s  34GB
Dec 12 21:54:59 Starting compiler/encoders/mips
Dec 12 21:55:01 Finished compiler/encoders/mips                                   1s  24MB
Dec 12 21:55:01 Starting compiler/encoders/riscv
Dec 12 21:55:03 Finished compiler/encoders/riscv                                  1s  22MB
Dec 12 21:55:03 Starting compiler/encoders/ag32
Dec 12 21:55:05 Finished compiler/encoders/ag32                                   1s  24MB
Dec 12 21:55:05 Starting compiler/backend/x64
Dec 12 21:55:07 Finished compiler/backend/x64                                     2s  22MB
Dec 12 21:55:07 Starting compiler/backend/arm7
Dec 12 21:55:10 Finished compiler/backend/arm7                                    2s  31MB
Dec 12 21:55:10 Starting compiler/backend/arm8
Dec 12 21:55:12 Finished compiler/backend/arm8                                    2s  21MB
Dec 12 21:55:12 Starting compiler/backend/mips
Dec 12 21:55:15 Finished compiler/backend/mips                                    2s  26MB
Dec 12 21:55:15 Starting compiler/backend/riscv
Dec 12 21:55:17 Finished compiler/backend/riscv                                   2s  22MB
Dec 12 21:55:17 Starting compiler/backend/ag32
Dec 12 21:56:43 Finished compiler/backend/ag32                                 1m25s   1GB
Dec 12 21:56:43 Starting compiler/parsing/proofs
Dec 12 21:56:45 Finished compiler/parsing/proofs                                  1s  18MB
Dec 12 21:56:45 Starting compiler/inference/proofs
Dec 12 21:56:47 Finished compiler/inference/proofs                                1s  20MB
Dec 12 21:56:47 Starting compiler/backend/semantics
Dec 12 21:57:52 Finished compiler/backend/semantics                            1m04s   1GB
Dec 12 21:57:52 Starting compiler/backend/reg_alloc/proofs
Dec 12 21:57:54 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Dec 12 21:57:54 Starting compiler/backend/proofs
Dec 12 21:58:48 Finished compiler/backend/proofs                                 53s   2GB
Dec 12 21:58:48 Starting compiler/backend/serialiser
Dec 12 21:58:51 Finished compiler/backend/serialiser                              2s  32MB
Dec 12 21:58:51 Starting compiler/encoders/x64/proofs
Dec 12 22:08:43 Finished compiler/encoders/x64/proofs                          9m52s   6GB
Dec 12 22:08:43 Starting compiler/encoders/arm7/proofs
Dec 12 22:22:37 Finished compiler/encoders/arm7/proofs                        13m53s   4GB
Dec 12 22:22:37 Starting compiler/encoders/arm8/proofs
Dec 12 22:29:39 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Dec 12 22:29:39 Starting compiler/encoders/arm8_asl/proofs
Dec 12 23:22:22 Finished compiler/encoders/arm8_asl/proofs                    52m41s   9GB
Dec 12 23:22:23 Starting compiler/encoders/mips/proofs
Dec 12 23:32:54 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Dec 12 23:32:54 Starting compiler/encoders/riscv/proofs
Dec 12 23:41:59 Finished compiler/encoders/riscv/proofs                        9m04s   1GB
Dec 12 23:41:59 Starting compiler/encoders/ag32/proofs
Dec 12 23:44:40 Finished compiler/encoders/ag32/proofs                         2m41s 818MB
Dec 12 23:44:40 Starting compiler/backend/x64/proofs
Dec 12 23:45:05 Finished compiler/backend/x64/proofs                             24s   1GB
Dec 12 23:45:06 Starting compiler/backend/arm7/proofs
Dec 12 23:45:32 Finished compiler/backend/arm7/proofs                            26s   1GB
Dec 12 23:45:32 Starting compiler/backend/arm8/proofs
Dec 12 23:45:59 Finished compiler/backend/arm8/proofs                            26s   1GB
Dec 12 23:46:00 Starting compiler/backend/arm8_asl
Dec 12 23:46:20 Finished compiler/backend/arm8_asl                               20s   1GB
Dec 12 23:46:20 Starting compiler/backend/mips/proofs
Dec 12 23:46:46 Finished compiler/backend/mips/proofs                            25s   1GB
Dec 12 23:46:46 Starting compiler/backend/riscv/proofs
Dec 12 23:47:15 Finished compiler/backend/riscv/proofs                           28s   2GB
Dec 12 23:47:16 Starting compiler/backend/ag32/proofs
Dec 13 00:00:48 Finished compiler/backend/ag32/proofs                         13m31s   2GB
Dec 13 00:00:48 Starting candle/set-theory
Dec 13 00:01:24 Finished candle/set-theory                                       35s   1GB
Dec 13 00:01:24 Starting candle/syntax-lib
Dec 13 00:01:26 Finished candle/syntax-lib                                        1s  20MB
Dec 13 00:01:26 Starting candle/standard/syntax
Dec 13 00:01:34 Finished candle/standard/syntax                                   8s 582MB
Dec 13 00:01:35 Starting candle/standard/semantics
Dec 13 00:03:22 Finished candle/standard/semantics                             1m46s   1GB
Dec 13 00:03:22 Starting candle/standard/monadic
Dec 13 00:03:24 Finished candle/standard/monadic                                  1s  20MB
Dec 13 00:03:24 Starting candle/standard/ml_kernel
Dec 13 00:04:49 Finished candle/standard/ml_kernel                             1m24s   2GB
Dec 13 00:04:49 Starting candle/overloading/syntax
Dec 13 00:08:04 Finished candle/overloading/syntax                             3m14s   1GB
Dec 13 00:08:04 Starting candle/overloading/semantics
Dec 13 00:20:22 Finished candle/overloading/semantics                         12m17s   2GB
Dec 13 00:20:22 Starting candle/overloading/monadic
Dec 13 00:23:02 Finished candle/overloading/monadic                            2m39s   1GB
Dec 13 00:23:03 Starting candle/overloading/ml_kernel
Dec 13 00:30:26 Finished candle/overloading/ml_kernel                          7m23s   3GB
Dec 13 00:30:26 Starting candle/overloading/ml_checker
Dec 13 00:33:00 Finished candle/overloading/ml_checker                         2m33s   2GB
Dec 13 00:33:00 Starting candle/prover
Dec 13 00:42:52 Finished candle/prover                                         9m51s   3GB
Dec 13 00:42:52 Starting pancake
Dec 13 00:45:56 Finished pancake                                               3m04s   4GB
Dec 13 00:45:56 Starting pancake/ffi
Dec 13 00:45:57 Finished pancake/ffi                                              0s  13MB
Dec 13 00:45:57 Starting pancake/semantics
Dec 13 00:48:21 Finished pancake/semantics                                     2m23s   1GB
Dec 13 00:48:21 Starting pancake/proofs
Dec 13 00:51:25 Finished pancake/proofs                                        3m04s   1GB
Dec 13 00:51:26 Starting characteristic/examples
Dec 13 00:52:52 Finished characteristic/examples                               1m26s   3GB
Dec 13 00:52:52 Starting tutorial/solutions
Dec 13 01:07:58 Finished tutorial/solutions                                   15m05s   7GB
Dec 13 01:07:58 Starting translator/monadic/examples
Dec 13 01:11:44 Finished translator/monadic/examples                           3m45s   2GB
Dec 13 01:11:44 Starting examples
Dec 13 01:21:50 Finished examples                                             10m05s   3GB
Dec 13 01:21:50 Starting examples/compilation/x64
Dec 13 03:19:11 Finished examples/compilation/x64                           1h57m20s  18GB
Dec 13 03:19:11 Starting examples/compilation/x64/proofs
Dec 13 03:21:13 Finished examples/compilation/x64/proofs                       2m01s   3GB
Dec 13 03:21:13 Starting examples/compilation/ag32
Dec 13 03:51:01 Finished examples/compilation/ag32                            29m47s   8GB
Dec 13 03:51:01 Starting examples/compilation/ag32/proofs
Dec 13 03:51:52 Finished examples/compilation/ag32/proofs                        50s   3GB
Dec 13 03:51:52 Starting examples/compilation/to_word
Dec 13 03:55:04 Finished examples/compilation/to_word                          3m12s   5GB
Dec 13 03:55:04 Starting examples/lpr_checker
Dec 13 03:56:03 Finished examples/lpr_checker                                    58s 984MB
Dec 13 03:56:03 Starting examples/lpr_checker/array
Dec 13 04:30:42 Finished examples/lpr_checker/array                           34m38s   5GB
Dec 13 04:30:42 Starting examples/lpr_checker/array/compilation
Dec 13 05:09:08 Finished examples/lpr_checker/array/compilation               38m25s  23GB
Dec 13 05:09:08 Starting examples/lpr_checker/array/compilation/proofs
Dec 13 05:10:30 Finished examples/lpr_checker/array/compilation/proofs         1m21s   6GB
Dec 13 05:10:30 Starting examples/opentheory
Dec 13 05:21:00 Finished examples/opentheory                                  10m29s   4GB
Dec 13 05:21:00 Starting examples/opentheory
Dec 13 05:21:02 Finished examples/opentheory                                      1s  26MB
Dec 13 05:21:02 Starting examples/opentheory/compilation
Dec 13 05:57:02 Finished examples/opentheory/compilation                      35m59s  30GB
Dec 13 05:57:02 Starting examples/opentheory/compilation/proofs
Dec 13 05:57:51 Finished examples/opentheory/compilation/proofs                  48s   4GB
Dec 13 05:57:51 Starting examples/opentheory/compilation/ag32
Dec 13 06:31:30 Finished examples/opentheory/compilation/ag32                 33m38s  26GB
Dec 13 06:31:30 Starting examples/opentheory/compilation/ag32/proofs
Dec 13 06:33:17 Finished examples/opentheory/compilation/ag32/proofs           1m47s   6GB
Dec 13 06:33:18 Starting examples/sat_encodings
Dec 13 06:35:05 Finished examples/sat_encodings                                1m47s   1GB
Dec 13 06:35:05 Starting examples/sat_encodings/case_studies
Dec 13 06:36:41 Finished examples/sat_encodings/case_studies                   1m35s 984MB
Dec 13 06:36:41 Starting examples/sat_encodings/translation
Dec 13 06:42:28 Finished examples/sat_encodings/translation                    5m46s   3GB
Dec 13 06:42:28 Starting examples/sat_encodings/translation/compilation
Dec 13 07:30:09 Finished examples/sat_encodings/translation/compilation       47m39s  22GB
Dec 13 07:30:09 Starting examples/deflate
Dec 13 07:31:01 Finished examples/deflate                                        51s 858MB
Dec 13 07:31:01 Starting examples/deflate/translation
Dec 13 07:32:36 Finished examples/deflate/translation                          1m35s   3GB
Dec 13 07:32:37 Starting examples/deflate/translation/compilation
Dec 13 07:52:15 Finished examples/deflate/translation/compilation             19m38s  11GB
Dec 13 07:52:15 Starting translator/okasaki-examples
Dec 13 07:57:18 Finished translator/okasaki-examples                           5m02s   2GB
Dec 13 07:57:18 Starting translator/other-examples
Dec 13 07:59:40 Finished translator/other-examples                             2m21s   1GB
Dec 13 07:59:40 Starting compiler/parsing/tests
Dec 13 08:00:10 Finished compiler/parsing/tests                                  30s 703MB
Dec 13 08:00:10 Starting compiler/inference/tests
Dec 13 08:08:42 Finished compiler/inference/tests                              8m31s   5GB
Dec 13 08:08:42 Starting compiler/printing/test
Dec 13 08:12:19 Finished compiler/printing/test                                3m36s   3GB
Dec 13 08:12:19 Starting compiler/repl
Dec 13 08:20:42 Finished compiler/repl                                         8m22s   4GB
Dec 13 08:20:42 Starting unverified/sexpr-bootstrap/x64/64
Dec 13 08:33:21 Finished unverified/sexpr-bootstrap/x64/64                    12m36s  15GB
Dec 13 08:33:21 Starting unverified/sexpr-bootstrap/x64/32
Dec 13 08:43:33 Finished unverified/sexpr-bootstrap/x64/32                    10m11s  11GB
Dec 13 08:43:34 Starting compiler/benchmarks
Dec 13 08:43:38 Finished compiler/benchmarks                                      4s  32MB
Dec 13 08:43:38 Starting compiler/bootstrap/compilation/x64/64
Dec 13 19:39:09 Finished compiler/bootstrap/compilation/x64/64             10h55m29s  64GB
Dec 13 19:39:09 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 13 19:41:17 FAILED: compiler/bootstrap/compilation/x64/64/proofs
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/quotient/src[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$(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$(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/hol88[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/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/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/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[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)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64[0m
Scanned 100 directories
Starting work on README.md
Starting work on replProofTheory
README.md                                                                                                                                                                       (0s)     OK
replProofTheory                                                                                                                                                               (112s)FAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cug/hk324/cml-regression/cakeml-2072/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-2072/compiler/bootstrap/compilation/x64/64/proofs/replProofScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 F
 
 Failed to prove theorem no_closures_IMP_concrete_v.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}