Job 2071

CakeML:00c06dba1f90b2a7168b1b8cabbd6ae58d4607d2
  Reenable Sollya build [Dec 10 13:11:45]
#911 (libm_gen)
Merging into:68d5c7577d631f58bb40f40e1ebfe49873f26a38
  Merge pull request #915 from CakeML/translator-fix [Dec 03 06:09:07]
HOL:7a7ef58e684a9ee1a7fef81e009c2b3da204add1
  Get examples/dev/inlineCompile to compile again [Dec 08 04:15:59]
Machine:oven3

Dec 10 13:12:10 Claimed job
Dec 10 13:12:12 Reusing HOL
Dec 10 13:13:04 Starting developers
Dec 10 13:13:13 Finished developers                                               8s 120MB
Dec 10 13:13:13 Starting developers/bin
Dec 10 13:13:26 Finished developers/bin                                          12s   1GB
Dec 10 13:13:26 Starting floatingPoint/tools/dandelion
Dec 10 13:34:15 Finished floatingPoint/tools/dandelion                        20m48s   1GB
Dec 10 13:34:15 Starting floatingPoint/icing/
Dec 10 18:39:07 Finished floatingPoint/icing/                               5h04m51s  21GB
Dec 10 18:39:07 Starting floatingPoint/icing/examples
Dec 10 18:42:19 Finished floatingPoint/icing/examples                          3m12s   5GB
Dec 10 18:42:19 Starting floatingPoint/libmGen/
Dec 10 20:12:02 Finished floatingPoint/libmGen/                             1h29m42s   6GB
Dec 10 20:12:02 Starting compiler/proofs
Dec 10 20:23:28 Finished compiler/proofs                                      11m25s   3GB
Dec 10 20:23:28 Starting compiler/bootstrap/translation
Dec 11 06:49:48 Finished compiler/bootstrap/translation                    10h26m19s  44GB
Dec 11 06:49:48 Starting semantics/ffi
Dec 11 06:49:56 Finished semantics/ffi                                            7s 214MB
Dec 11 06:49:57 Starting semantics
Dec 11 06:49:59 Finished semantics                                                2s  33MB
Dec 11 06:49:59 Starting semantics/proofs
Dec 11 06:51:13 Finished semantics/proofs                                      1m13s 927MB
Dec 11 06:51:14 Starting semantics/alt_semantics
Dec 11 06:52:12 Finished semantics/alt_semantics                                 58s 546MB
Dec 11 06:52:12 Starting semantics/alt_semantics/proofs
Dec 11 07:18:43 Finished semantics/alt_semantics/proofs                       26m30s   2GB
Dec 11 07:18:43 Starting basis/pure
Dec 11 07:18:46 Finished basis/pure                                               2s  30MB
Dec 11 07:18:46 Starting translator
Dec 11 07:22:25 Finished translator                                            3m38s   1GB
Dec 11 07:22:25 Starting compiler/parsing
Dec 11 07:22:28 Finished compiler/parsing                                         2s  21MB
Dec 11 07:22:28 Starting characteristic
Dec 11 07:22:31 Finished characteristic                                           3s  42MB
Dec 11 07:22:31 Starting translator/monadic
Dec 11 07:22:35 Finished translator/monadic                                       2s  27MB
Dec 11 07:22:35 Starting basis
Dec 11 07:30:17 Finished basis                                                 7m42s   3GB
Dec 11 07:30:18 Starting compiler/inference
Dec 11 07:30:20 Finished compiler/inference                                       2s  31MB
Dec 11 07:30:21 Starting compiler/backend/reg_alloc
Dec 11 07:30:23 Finished compiler/backend/reg_alloc                               2s  16MB
Dec 11 07:30:23 Starting compiler/backend/gc
Dec 11 07:30:27 Finished compiler/backend/gc                                      3s  33MB
Dec 11 07:30:27 Starting compiler/backend
Dec 11 07:30:52 Finished compiler/backend                                        24s 679MB
Dec 11 07:30:52 Starting compiler/encoders/asm
Dec 11 07:30:55 Finished compiler/encoders/asm                                    2s  26MB
Dec 11 07:30:56 Starting compiler/encoders/x64
Dec 11 07:30:58 Finished compiler/encoders/x64                                    2s  34MB
Dec 11 07:30:59 Starting compiler/encoders/arm7
Dec 11 07:31:02 Finished compiler/encoders/arm7                                   2s  22MB
Dec 11 07:31:02 Starting compiler/encoders/arm8
Dec 11 07:31:04 Finished compiler/encoders/arm8                                   2s  33MB
Dec 11 07:31:05 Starting compiler/encoders/arm8_asl
Dec 11 11:58:38 Finished compiler/encoders/arm8_asl                         4h27m33s  45GB
Dec 11 11:58:39 Starting compiler/encoders/mips
Dec 11 11:58:42 Finished compiler/encoders/mips                                   2s  22MB
Dec 11 11:58:42 Starting compiler/encoders/riscv
Dec 11 11:58:45 Finished compiler/encoders/riscv                                  2s  25MB
Dec 11 11:58:45 Starting compiler/encoders/ag32
Dec 11 11:58:48 Finished compiler/encoders/ag32                                   2s  26MB
Dec 11 11:58:48 Starting compiler/backend/x64
Dec 11 11:58:52 Finished compiler/backend/x64                                     3s  33MB
Dec 11 11:58:52 Starting compiler/backend/arm7
Dec 11 11:58:56 Finished compiler/backend/arm7                                    3s  33MB
Dec 11 11:58:56 Starting compiler/backend/arm8
Dec 11 11:59:00 Finished compiler/backend/arm8                                    3s  33MB
Dec 11 11:59:00 Starting compiler/backend/mips
Dec 11 11:59:04 Finished compiler/backend/mips                                    3s  34MB
Dec 11 11:59:04 Starting compiler/backend/riscv
Dec 11 11:59:07 Finished compiler/backend/riscv                                   3s  33MB
Dec 11 11:59:08 Starting compiler/backend/ag32
Dec 11 12:02:11 Finished compiler/backend/ag32                                 3m03s   1GB
Dec 11 12:02:11 Starting compiler/parsing/proofs
Dec 11 12:02:14 Finished compiler/parsing/proofs                                  2s  26MB
Dec 11 12:02:14 Starting compiler/inference/proofs
Dec 11 12:02:17 Finished compiler/inference/proofs                                2s  30MB
Dec 11 12:02:18 Starting compiler/backend/semantics
Dec 11 12:04:41 Finished compiler/backend/semantics                            2m23s   1GB
Dec 11 12:04:41 Starting compiler/backend/reg_alloc/proofs
Dec 11 12:04:44 Finished compiler/backend/reg_alloc/proofs                        2s  35MB
Dec 11 12:04:44 Starting compiler/backend/proofs
Dec 11 12:06:45 Finished compiler/backend/proofs                               2m00s   2GB
Dec 11 12:06:45 Starting compiler/backend/serialiser
Dec 11 12:06:51 Finished compiler/backend/serialiser                              5s  48MB
Dec 11 12:06:51 Starting compiler/encoders/x64/proofs
Dec 11 12:29:08 Finished compiler/encoders/x64/proofs                         22m16s   5GB
Dec 11 12:29:08 Starting compiler/encoders/arm7/proofs
Dec 11 12:59:58 Finished compiler/encoders/arm7/proofs                        30m49s   4GB
Dec 11 12:59:58 Starting compiler/encoders/arm8/proofs
Dec 11 13:16:02 Finished compiler/encoders/arm8/proofs                        16m04s   1GB
Dec 11 13:16:03 Starting compiler/encoders/arm8_asl/proofs
Dec 11 15:13:35 Finished compiler/encoders/arm8_asl/proofs                  1h57m32s   7GB
Dec 11 15:13:35 Starting compiler/encoders/mips/proofs
Dec 11 15:37:34 Finished compiler/encoders/mips/proofs                        23m58s   2GB
Dec 11 15:37:35 Starting compiler/encoders/riscv/proofs
Dec 11 15:57:54 Finished compiler/encoders/riscv/proofs                       20m19s   1GB
Dec 11 15:57:54 Starting compiler/encoders/ag32/proofs
Dec 11 16:03:52 Finished compiler/encoders/ag32/proofs                         5m57s   1GB
Dec 11 16:03:52 Starting compiler/backend/x64/proofs
Dec 11 16:04:47 Finished compiler/backend/x64/proofs                             55s   1GB
Dec 11 16:04:48 Starting compiler/backend/arm7/proofs
Dec 11 16:05:45 Finished compiler/backend/arm7/proofs                            57s   1GB
Dec 11 16:05:46 Starting compiler/backend/arm8/proofs
Dec 11 16:06:42 Finished compiler/backend/arm8/proofs                            56s   1GB
Dec 11 16:06:42 Starting compiler/backend/arm8_asl
Dec 11 16:07:26 Finished compiler/backend/arm8_asl                               43s   1GB
Dec 11 16:07:26 Starting compiler/backend/mips/proofs
Dec 11 16:08:19 Finished compiler/backend/mips/proofs                            52s   1GB
Dec 11 16:08:19 Starting compiler/backend/riscv/proofs
Dec 11 16:09:14 Finished compiler/backend/riscv/proofs                           54s   1GB
Dec 11 16:09:14 Starting compiler/backend/ag32/proofs
Dec 11 16:39:51 Finished compiler/backend/ag32/proofs                         30m36s   2GB
Dec 11 16:39:51 Starting candle/set-theory
Dec 11 16:40:59 Finished candle/set-theory                                     1m07s   1GB
Dec 11 16:40:59 Starting candle/syntax-lib
Dec 11 16:41:01 Finished candle/syntax-lib                                        2s  17MB
Dec 11 16:41:02 Starting candle/standard/syntax
Dec 11 16:41:20 Finished candle/standard/syntax                                  18s 545MB
Dec 11 16:41:21 Starting candle/standard/semantics
Dec 11 16:45:11 Finished candle/standard/semantics                             3m49s   1GB
Dec 11 16:45:11 Starting candle/standard/monadic
Dec 11 16:45:14 Finished candle/standard/monadic                                  3s  32MB
Dec 11 16:45:14 Starting candle/standard/ml_kernel
Dec 11 16:48:34 Finished candle/standard/ml_kernel                             3m19s   3GB
Dec 11 16:48:34 Starting candle/overloading/syntax
Dec 11 16:55:24 Finished candle/overloading/syntax                             6m49s   1GB
Dec 11 16:55:24 Starting candle/overloading/semantics
Dec 11 17:21:55 Finished candle/overloading/semantics                         26m30s   2GB
Dec 11 17:21:55 Starting candle/overloading/monadic
Dec 11 17:27:31 Finished candle/overloading/monadic                            5m35s   1GB
Dec 11 17:27:31 Starting candle/overloading/ml_kernel
Dec 11 17:42:56 Finished candle/overloading/ml_kernel                         15m25s   3GB
Dec 11 17:42:57 Starting candle/overloading/ml_checker
Dec 11 17:48:20 Finished candle/overloading/ml_checker                         5m23s   2GB
Dec 11 17:48:21 Starting candle/prover
Dec 11 18:09:57 Finished candle/prover                                        21m36s   3GB
Dec 11 18:09:58 Starting pancake
Dec 11 18:16:20 Finished pancake                                               6m22s   4GB
Dec 11 18:16:21 Starting pancake/ffi
Dec 11 18:16:21 Finished pancake/ffi                                              0s  16MB
Dec 11 18:16:21 Starting pancake/semantics
Dec 11 18:21:33 Finished pancake/semantics                                     5m11s   1GB
Dec 11 18:21:34 Starting pancake/proofs
Dec 11 18:27:45 Finished pancake/proofs                                        6m11s   1GB
Dec 11 18:27:46 Starting characteristic/examples
Dec 11 18:30:47 Finished characteristic/examples                               3m01s   3GB
Dec 11 18:30:47 Starting tutorial/solutions
Dec 11 19:04:21 Finished tutorial/solutions                                   33m33s   7GB
Dec 11 19:04:21 Starting translator/monadic/examples
Dec 11 19:10:58 Finished translator/monadic/examples                           6m37s   2GB
Dec 11 19:10:59 Starting examples
Dec 11 19:30:23 Finished examples                                             19m24s   3GB
Dec 11 19:30:23 Starting examples/compilation/x64
Dec 11 23:48:44 Finished examples/compilation/x64                           4h18m20s  21GB
Dec 11 23:48:44 Starting examples/compilation/x64/proofs
Dec 11 23:52:56 Finished examples/compilation/x64/proofs                       4m11s   3GB
Dec 11 23:52:56 Starting examples/compilation/ag32
Dec 12 01:00:21 Finished examples/compilation/ag32                          1h07m24s  10GB
Dec 12 01:00:21 Starting examples/compilation/ag32/proofs
Dec 12 01:02:02 Finished examples/compilation/ag32/proofs                      1m40s   3GB
Dec 12 01:02:03 Starting examples/compilation/to_word
Dec 12 01:08:44 Finished examples/compilation/to_word                          6m41s   5GB
Dec 12 01:08:45 Starting examples/lpr_checker
Dec 12 01:10:40 Finished examples/lpr_checker                                  1m55s   1GB
Dec 12 01:10:41 Starting examples/lpr_checker/array
Dec 12 02:30:21 Finished examples/lpr_checker/array                         1h19m39s   7GB
Dec 12 02:30:21 Starting examples/lpr_checker/array/compilation
Dec 12 03:50:08 Finished examples/lpr_checker/array/compilation             1h19m46s  37GB
Dec 12 03:50:08 Starting examples/lpr_checker/array/compilation/proofs
Dec 12 03:52:46 Finished examples/lpr_checker/array/compilation/proofs         2m38s   5GB
Dec 12 03:52:46 Starting examples/opentheory
Dec 12 04:15:01 Finished examples/opentheory                                  22m13s   3GB
Dec 12 04:15:01 Starting examples/opentheory
Dec 12 04:15:04 Finished examples/opentheory                                      3s  31MB
Dec 12 04:15:05 Starting examples/opentheory/compilation
Dec 12 05:39:45 Finished examples/opentheory/compilation                    1h24m40s  42GB
Dec 12 05:39:45 Starting examples/opentheory/compilation/proofs
Dec 12 05:41:27 Finished examples/opentheory/compilation/proofs                1m41s   4GB
Dec 12 05:41:28 Starting examples/opentheory/compilation/ag32
Dec 12 06:57:24 Finished examples/opentheory/compilation/ag32               1h15m56s  40GB
Dec 12 06:57:25 Starting examples/opentheory/compilation/ag32/proofs
Dec 12 07:01:05 Finished examples/opentheory/compilation/ag32/proofs           3m40s   6GB
Dec 12 07:01:05 Starting examples/sat_encodings
Dec 12 07:04:48 Finished examples/sat_encodings                                3m42s 907MB
Dec 12 07:04:48 Starting examples/sat_encodings/case_studies
Dec 12 07:08:34 Finished examples/sat_encodings/case_studies                   3m45s   1GB
Dec 12 07:08:34 Starting examples/sat_encodings/translation
Dec 12 07:20:15 Finished examples/sat_encodings/translation                   11m41s   3GB
Dec 12 07:20:15 Starting examples/sat_encodings/translation/compilation
Dec 12 08:40:14 Finished examples/sat_encodings/translation/compilation     1h19m58s  21GB
Dec 12 08:40:15 Starting examples/deflate
Dec 12 08:41:58 Finished examples/deflate                                      1m43s 681MB
Dec 12 08:41:59 Starting examples/deflate/translation
Dec 12 08:44:53 Finished examples/deflate/translation                          2m54s   3GB
Dec 12 08:44:53 Starting examples/deflate/translation/compilation
Dec 12 09:22:16 Finished examples/deflate/translation/compilation             37m22s  16GB
Dec 12 09:22:16 Starting translator/okasaki-examples
Dec 12 09:32:20 Finished translator/okasaki-examples                          10m03s   2GB
Dec 12 09:32:20 Starting translator/other-examples
Dec 12 09:37:14 Finished translator/other-examples                             4m54s   1GB
Dec 12 09:37:15 Starting compiler/parsing/tests
Dec 12 09:38:23 Finished compiler/parsing/tests                                1m07s 587MB
Dec 12 09:38:23 Starting compiler/inference/tests
Dec 12 09:55:24 Finished compiler/inference/tests                             17m00s   4GB
Dec 12 09:55:24 Starting compiler/printing/test
Dec 12 10:02:22 Finished compiler/printing/test                                6m57s   3GB
Dec 12 10:02:22 Starting compiler/repl
Dec 12 10:20:39 Finished compiler/repl                                        18m17s   4GB
Dec 12 10:20:40 Starting unverified/sexpr-bootstrap/x64/64
Dec 12 10:43:42 Finished unverified/sexpr-bootstrap/x64/64                    23m02s  15GB
Dec 12 10:43:42 Starting unverified/sexpr-bootstrap/x64/32
Dec 12 11:02:19 Finished unverified/sexpr-bootstrap/x64/32                    18m36s  11GB
Dec 12 11:02:19 Starting compiler/benchmarks
Dec 12 11:02:24 Finished compiler/benchmarks                                      4s  33MB
Dec 12 11:02:24 Starting compiler/bootstrap/compilation/x64/64
Dec 13 11:47:26 Finished compiler/bootstrap/compilation/x64/64             24h45m00s  97GB
Dec 13 11:47:26 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 13 11:51:44 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                                                   (226s)FAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /local/regression_new/cakeml-2071/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /local/regression_new/cakeml-2071/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"}