Job 1953

CakeML:4cba31259526004a87507ef2f43cc46a0ef0272d
  Merge remote-tracking branch 'origin/master' into gh859 [Jul 04 21:00:13]
#862 (gh859)
Merging into:cbf165f01258b1e3d4f325d1e849520e87d4ee71
  Fix a couple of proofs broken by recent HOL changes [Jul 04 23:33:18]
HOL:36b541e828806d911b2fee3e1cb1e3298068dfd9
  Tidy up some simpleSexp proofs [Jul 01 07:00:10]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jul 05 06:23:11 Claimed job
Jul 05 06:23:13 Reusing HOL
Jul 05 06:23:26 Starting developers
Jul 05 06:23:30 Finished developers                                               4s 135MB
Jul 05 06:23:31 Starting developers/bin
Jul 05 06:23:37 Finished developers/bin                                           6s   1GB
Jul 05 06:23:37 Starting semantics/ffi
Jul 05 06:23:47 Finished semantics/ffi                                            9s 258MB
Jul 05 06:23:47 Starting semantics
Jul 05 06:26:16 Finished semantics                                             2m28s   1GB
Jul 05 06:26:16 Starting semantics/proofs
Jul 05 06:33:18 Finished semantics/proofs                                      7m02s   1GB
Jul 05 06:33:18 Starting semantics/alt_semantics
Jul 05 06:33:46 Finished semantics/alt_semantics                                 27s 553MB
Jul 05 06:33:46 Starting semantics/alt_semantics/proofs
Jul 05 06:45:22 Finished semantics/alt_semantics/proofs                       11m35s   2GB
Jul 05 06:45:22 Starting basis/pure
Jul 05 06:46:29 Finished basis/pure                                            1m07s 933MB
Jul 05 06:46:29 Starting translator
Jul 05 06:50:14 Finished translator                                            3m45s   2GB
Jul 05 06:50:15 Starting compiler/parsing
Jul 05 06:51:39 Finished compiler/parsing                                      1m23s   5GB
Jul 05 06:51:39 Starting characteristic
Jul 05 06:58:43 Finished characteristic                                        7m03s   2GB
Jul 05 06:58:43 Starting translator/monadic
Jul 05 07:00:43 Finished translator/monadic                                    2m00s   1GB
Jul 05 07:00:44 Starting basis
Jul 05 07:53:34 Finished basis                                                52m49s  20GB
Jul 05 07:53:34 Starting compiler/inference
Jul 05 07:55:14 Finished compiler/inference                                    1m39s   1GB
Jul 05 07:55:14 Starting compiler/backend/reg_alloc
Jul 05 07:56:59 Finished compiler/backend/reg_alloc                            1m45s   1GB
Jul 05 07:56:59 Starting compiler/backend/gc
Jul 05 08:01:32 Finished compiler/backend/gc                                   4m32s   2GB
Jul 05 08:01:32 Starting compiler/backend
Jul 05 08:07:49 Finished compiler/backend                                      6m16s   3GB
Jul 05 08:07:49 Starting compiler/encoders/asm
Jul 05 08:08:20 Finished compiler/encoders/asm                                   30s 753MB
Jul 05 08:08:20 Starting compiler/encoders/x64
Jul 05 08:09:28 Finished compiler/encoders/x64                                 1m07s 872MB
Jul 05 08:09:28 Starting compiler/encoders/arm7
Jul 05 08:11:39 Finished compiler/encoders/arm7                                2m10s   1GB
Jul 05 08:11:39 Starting compiler/encoders/arm8
Jul 05 08:12:22 Finished compiler/encoders/arm8                                  42s 835MB
Jul 05 08:12:22 Starting compiler/encoders/arm8_asl
Jul 05 10:30:34 Finished compiler/encoders/arm8_asl                         2h18m10s  31GB
Jul 05 10:30:35 Starting compiler/encoders/mips
Jul 05 10:32:08 Finished compiler/encoders/mips                                1m33s   1GB
Jul 05 10:32:08 Starting compiler/encoders/riscv
Jul 05 10:33:56 Finished compiler/encoders/riscv                               1m47s   1GB
Jul 05 10:33:56 Starting compiler/encoders/ag32
Jul 05 10:34:18 Finished compiler/encoders/ag32                                  22s 696MB
Jul 05 10:34:18 Starting compiler/backend/x64
Jul 05 10:34:42 Finished compiler/backend/x64                                    23s   1GB
Jul 05 10:34:42 Starting compiler/backend/arm7
Jul 05 10:35:07 Finished compiler/backend/arm7                                   24s   1GB
Jul 05 10:35:07 Starting compiler/backend/arm8
Jul 05 10:35:30 Finished compiler/backend/arm8                                   23s   1GB
Jul 05 10:35:31 Starting compiler/backend/mips
Jul 05 10:35:54 Finished compiler/backend/mips                                   23s   1GB
Jul 05 10:35:54 Starting compiler/backend/riscv
Jul 05 10:36:18 Finished compiler/backend/riscv                                  23s   1GB
Jul 05 10:36:18 Starting compiler/backend/ag32
Jul 05 10:37:46 Finished compiler/backend/ag32                                 1m28s   1GB
Jul 05 10:37:46 Starting compiler/parsing/proofs
Jul 05 10:41:32 Finished compiler/parsing/proofs                               3m45s   1GB
Jul 05 10:41:32 Starting compiler/inference/proofs
Jul 05 10:44:20 Finished compiler/inference/proofs                             2m47s   1GB
Jul 05 10:44:20 Starting compiler/backend/semantics
Jul 05 11:10:26 Finished compiler/backend/semantics                           26m05s   2GB
Jul 05 11:10:26 Starting compiler/backend/reg_alloc/proofs
Jul 05 11:14:08 Finished compiler/backend/reg_alloc/proofs                     3m42s 873MB
Jul 05 11:14:08 Starting compiler/backend/proofs
Jul 05 12:09:14 Finished compiler/backend/proofs                              55m03s  12GB
Jul 05 12:09:15 Starting compiler/backend/serialiser
Jul 05 12:10:58 Finished compiler/backend/serialiser                           1m43s   2GB
Jul 05 12:10:58 Starting compiler/encoders/x64/proofs
Jul 05 12:20:43 Finished compiler/encoders/x64/proofs                          9m44s   6GB
Jul 05 12:20:44 Starting compiler/encoders/arm7/proofs
Jul 05 12:34:21 Finished compiler/encoders/arm7/proofs                        13m36s   3GB
Jul 05 12:34:21 Starting compiler/encoders/arm8/proofs
Jul 05 12:41:14 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
Jul 05 12:41:14 Starting compiler/encoders/arm8_asl/proofs
Jul 05 13:32:58 Finished compiler/encoders/arm8_asl/proofs                    51m42s  12GB
Jul 05 13:32:58 Starting compiler/encoders/mips/proofs
Jul 05 13:43:34 Finished compiler/encoders/mips/proofs                        10m35s   2GB
Jul 05 13:43:34 Starting compiler/encoders/riscv/proofs
Jul 05 13:52:35 Finished compiler/encoders/riscv/proofs                        9m00s   1GB
Jul 05 13:52:35 Starting compiler/encoders/ag32/proofs
Jul 05 13:55:15 Finished compiler/encoders/ag32/proofs                         2m39s 776MB
Jul 05 13:55:15 Starting compiler/backend/x64/proofs
Jul 05 13:55:44 Finished compiler/backend/x64/proofs                             29s   1GB
Jul 05 13:55:45 Starting compiler/backend/arm7/proofs
Jul 05 13:56:14 Finished compiler/backend/arm7/proofs                            29s   1GB
Jul 05 13:56:14 Starting compiler/backend/arm8/proofs
Jul 05 13:56:44 Finished compiler/backend/arm8/proofs                            29s   1GB
Jul 05 13:56:44 Starting compiler/backend/arm8_asl
Jul 05 13:57:08 Finished compiler/backend/arm8_asl                               23s   1GB
Jul 05 13:57:08 Starting compiler/backend/mips/proofs
Jul 05 13:57:36 Finished compiler/backend/mips/proofs                            28s   1GB
Jul 05 13:57:36 Starting compiler/backend/riscv/proofs
Jul 05 13:58:06 Finished compiler/backend/riscv/proofs                           29s   1GB
Jul 05 13:58:06 Starting compiler/backend/ag32/proofs
Jul 05 14:12:09 Finished compiler/backend/ag32/proofs                         14m02s   2GB
Jul 05 14:12:09 Starting compiler/proofs
Jul 05 14:14:39 Finished compiler/proofs                                       2m30s   3GB
Jul 05 14:14:40 Starting candle/set-theory
Jul 05 14:15:15 Finished candle/set-theory                                       35s   1GB
Jul 05 14:15:15 Starting candle/syntax-lib
Jul 05 14:15:29 Finished candle/syntax-lib                                       13s 673MB
Jul 05 14:15:29 Starting candle/standard/syntax
Jul 05 14:17:35 Finished candle/standard/syntax                                2m06s   1GB
Jul 05 14:17:35 Starting candle/standard/semantics
Jul 05 14:19:26 Finished candle/standard/semantics                             1m50s   1GB
Jul 05 14:19:26 Starting candle/standard/monadic
Jul 05 14:21:22 Finished candle/standard/monadic                               1m55s   1GB
Jul 05 14:21:22 Starting candle/standard/ml_kernel
Jul 05 14:27:54 Finished candle/standard/ml_kernel                             6m31s   3GB
Jul 05 14:27:54 Starting candle/overloading/syntax
Jul 05 14:31:13 Finished candle/overloading/syntax                             3m18s 996MB
Jul 05 14:31:13 Starting candle/overloading/semantics
Jul 05 14:43:19 Finished candle/overloading/semantics                         12m05s   2GB
Jul 05 14:43:19 Starting candle/overloading/monadic
Jul 05 14:45:57 Finished candle/overloading/monadic                            2m38s   1GB
Jul 05 14:45:57 Starting candle/overloading/ml_kernel
Jul 05 14:53:27 Finished candle/overloading/ml_kernel                          7m29s   3GB
Jul 05 14:53:27 Starting candle/overloading/ml_checker
Jul 05 14:55:55 Finished candle/overloading/ml_checker                         2m27s   3GB
Jul 05 14:55:55 Starting candle/prover
Jul 05 15:06:41 Finished candle/prover                                        10m45s   2GB
Jul 05 15:06:41 Starting pancake
Jul 05 15:10:36 Finished pancake                                               3m55s   3GB
Jul 05 15:10:36 Starting pancake/ffi
Jul 05 15:10:37 Finished pancake/ffi                                              0s  35MB
Jul 05 15:10:37 Starting pancake/semantics
Jul 05 15:13:16 Finished pancake/semantics                                     2m39s   1GB
Jul 05 15:13:16 Starting pancake/proofs
Jul 05 15:25:44 Finished pancake/proofs                                       12m27s   6GB
Jul 05 15:25:44 Starting characteristic/examples
Jul 05 15:27:10 Finished characteristic/examples                               1m25s   2GB
Jul 05 15:27:10 Starting tutorial/solutions
Jul 05 15:43:02 Finished tutorial/solutions                                   15m52s   8GB
Jul 05 15:43:03 Starting translator/monadic/examples
Jul 05 15:47:04 Finished translator/monadic/examples                           3m58s   2GB
Jul 05 15:47:05 Starting examples
Jul 05 15:57:09 Finished examples                                             10m04s   3GB
Jul 05 15:57:09 Starting examples/compilation/x64
Jul 05 18:01:50 Finished examples/compilation/x64                           2h04m40s  18GB
Jul 05 18:01:50 Starting examples/compilation/x64/proofs
Jul 05 18:04:25 Finished examples/compilation/x64/proofs                       2m34s   3GB
Jul 05 18:04:25 Starting examples/compilation/ag32
Jul 05 18:37:30 Finished examples/compilation/ag32                            33m05s   8GB
Jul 05 18:37:30 Starting examples/compilation/ag32/proofs
Jul 05 18:38:26 Finished examples/compilation/ag32/proofs                        55s   3GB
Jul 05 18:38:26 Starting examples/lpr_checker
Jul 05 18:39:30 Finished examples/lpr_checker                                  1m03s   1GB
Jul 05 18:39:30 Starting examples/lpr_checker/array
Jul 05 19:13:05 Finished examples/lpr_checker/array                           33m34s   9GB
Jul 05 19:13:05 Starting examples/lpr_checker/array/compilation
Jul 05 19:51:31 Finished examples/lpr_checker/array/compilation               38m25s  23GB
Jul 05 19:51:31 Starting examples/lpr_checker/array/compilation/proofs
Jul 05 19:52:56 Finished examples/lpr_checker/array/compilation/proofs         1m25s   6GB
Jul 05 19:52:56 Starting examples/opentheory
Jul 05 20:03:39 Finished examples/opentheory                                  10m42s   4GB
Jul 05 20:03:39 Starting examples/opentheory
Jul 05 20:03:40 Finished examples/opentheory                                      1s 145MB
Jul 05 20:03:40 Starting examples/opentheory/compilation
Jul 05 20:41:54 Finished examples/opentheory/compilation                      38m12s  28GB
Jul 05 20:41:54 Starting examples/opentheory/compilation/proofs
Jul 05 20:42:47 Finished examples/opentheory/compilation/proofs                  53s   4GB
Jul 05 20:42:48 Starting examples/opentheory/compilation/ag32
Jul 05 21:15:59 Finished examples/opentheory/compilation/ag32                 33m11s  25GB
Jul 05 21:15:59 Starting examples/opentheory/compilation/ag32/proofs
Jul 05 21:17:45 Finished examples/opentheory/compilation/ag32/proofs           1m45s   3GB
Jul 05 21:17:45 Starting examples/sat_encodings
Jul 05 21:19:48 Finished examples/sat_encodings                                2m03s 745MB
Jul 05 21:19:48 Starting examples/sat_encodings/case_studies
Jul 05 21:21:34 Finished examples/sat_encodings/case_studies                   1m45s 811MB
Jul 05 21:21:34 Starting examples/sat_encodings/translation
Jul 05 21:27:23 Finished examples/sat_encodings/translation                    5m48s   5GB
Jul 05 21:27:23 Starting examples/sat_encodings/translation/compilation
Jul 05 22:14:04 Finished examples/sat_encodings/translation/compilation       46m40s  19GB
Jul 05 22:14:04 Starting examples/deflate
Jul 05 22:15:04 Finished examples/deflate                                        59s 853MB
Jul 05 22:15:04 Starting examples/deflate/translation
Jul 05 22:16:39 Finished examples/deflate/translation                          1m35s   3GB
Jul 05 22:16:39 Starting examples/deflate/translation/compilation
Jul 05 22:37:36 Finished examples/deflate/translation/compilation             20m56s  12GB
Jul 05 22:37:36 Starting translator/okasaki-examples
Jul 05 22:42:45 Finished translator/okasaki-examples                           5m08s   1GB
Jul 05 22:42:45 Starting translator/other-examples
Jul 05 22:45:12 Finished translator/other-examples                             2m26s   1GB
Jul 05 22:45:12 Starting compiler/parsing/tests
Jul 05 22:45:44 Finished compiler/parsing/tests                                  31s 582MB
Jul 05 22:45:44 Starting compiler/inference/tests
Jul 05 22:54:20 Finished compiler/inference/tests                              8m36s   5GB
Jul 05 22:54:21 Starting compiler/printing/test
Jul 05 22:58:04 Finished compiler/printing/test                                3m43s   3GB
Jul 05 22:58:04 Starting icing/flover
Jul 05 23:42:43 Finished icing/flover                                         44m36s   1GB
Jul 05 23:42:43 Starting icing/
Jul 06 00:42:03 Finished icing/                                               59m20s   7GB
Jul 06 00:42:03 Starting icing/examples
Jul 06 00:43:47 Finished icing/examples                                        1m43s   5GB
Jul 06 00:43:48 Starting compiler/repl
Jul 06 00:57:15 Finished compiler/repl                                        13m27s   8GB
Jul 06 00:57:15 Starting compiler/bootstrap/translation
Jul 06 03:33:48 FAILED: compiler/bootstrap/translation
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/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$(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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[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)/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[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanned 88 directories
Starting work on precparserTheory
Starting work on monadic_encTheory
Starting work on caml_lexTheory
Starting work on README.md
README.md                                                                   compiler/bootstrap/translation  (0s)     OK
Starting work on decProgTheory
precparserTheory                                                    examples/formal-languages/context-free  (1s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1]                                       (1.070s) 
monadic_encTheory                                                            compiler/encoders/monadic_enc (14s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                          compiler/encoders/monadic_enc (19s)     OK
monadic_enc64Theory                                                          compiler/encoders/monadic_enc (19s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]                                            (53.900s) 
decProgTheory                                                               compiler/bootstrap/translation(165s)     OK
Starting work on to_flatProgTheory
caml_lexTheory                                                                      compiler/parsing/ocaml(230s)     OK
Starting work on camlPEGTheory
camlPEGTheory                                                                       compiler/parsing/ocaml(108s)     OK
Starting work on camlPtreeConversionTheory
camlPtreeConversionTheory                                                           compiler/parsing/ocaml (58s)     OK
Starting work on caml_parserTheory
caml_parserTheory                                                                   compiler/parsing/ocaml (12s)     OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4]                                                  (410.380s) 
to_flatProgTheory                                                           compiler/bootstrap/translation(322s)     OK
Starting work on to_closProgTheory
to_closProgTheory                                                           compiler/bootstrap/translation(602s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                            compiler/bootstrap/translation(539s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                            compiler/bootstrap/translation(455s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                           compiler/bootstrap/translation(257s)     OK
Starting work on lexerProgTheory
lexerProgTheory                                                             compiler/bootstrap/translation(188s)     OK
Starting work on parserProgTheory
parserProgTheory                                                            compiler/bootstrap/translation(551s)     OK
Starting work on caml_lexProgTheory
caml_lexProgTheory                                                          compiler/bootstrap/translation(480s)     OK
Starting work on caml_parserProgTheory
caml_parserProgTheory                                                       compiler/bootstrap/translation (16m)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                         compiler/bootstrap/translation(996s)     OK
Starting work on inferProgTheory
inferProgTheory                                                             compiler/bootstrap/translation (38m)     OK
Starting work on explorerProgTheory
explorerProgTheory                                                          compiler/bootstrap/translation(918s)     OK
Starting work on decodeProgTheory
decodeProgTheory                                                            compiler/bootstrap/translation(275s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                       compiler/bootstrap/translation(205s)FAIL<1>
 print_sexp s = print_sexp_alt s
 
 failed.
 Failed to prove theorem print_sexp_alt_thm.
 
 Exception raised at Q.MATCH_GOALSUB_ABBREV_TAC:
 No matching sub-term found
 error in quse /home/cug/hk324/cml-regression/cakeml-1953/compiler/bootstrap/translation/sexp_parserProgScript.sml : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 error in load /home/cug/hk324/cml-regression/cakeml-1953/compiler/bootstrap/translation/sexp_parserProgScript : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 Uncaught exception: HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}