Job 1952

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jul 04 23:40:04 Claimed job
Jul 04 23:40:06 Reusing HOL
Jul 04 23:40:44 Starting developers
Jul 04 23:40:50 Finished developers                                               5s  88MB
Jul 04 23:40:50 Starting developers/bin
Jul 04 23:42:25 Finished developers/bin                                        1m35s   1GB
Jul 04 23:42:25 Starting semantics/ffi
Jul 04 23:42:36 Finished semantics/ffi                                           10s 198MB
Jul 04 23:42:37 Starting semantics
Jul 04 23:45:19 Finished semantics                                             2m41s   1GB
Jul 04 23:45:19 Starting semantics/proofs
Jul 04 23:52:58 Finished semantics/proofs                                      7m38s   1GB
Jul 04 23:52:58 Starting semantics/alt_semantics
Jul 04 23:53:29 Finished semantics/alt_semantics                                 30s 504MB
Jul 04 23:53:29 Starting semantics/alt_semantics/proofs
Jul 05 00:06:13 Finished semantics/alt_semantics/proofs                       12m43s   2GB
Jul 05 00:06:13 Starting basis/pure
Jul 05 00:07:23 Finished basis/pure                                            1m09s 826MB
Jul 05 00:07:23 Starting translator
Jul 05 00:11:25 Finished translator                                            4m01s   1GB
Jul 05 00:11:25 Starting compiler/parsing
Jul 05 00:12:57 Finished compiler/parsing                                      1m31s   5GB
Jul 05 00:12:57 Starting characteristic
Jul 05 00:20:21 Finished characteristic                                        7m23s   2GB
Jul 05 00:20:21 Starting translator/monadic
Jul 05 00:22:28 Finished translator/monadic                                    2m06s   1GB
Jul 05 00:22:28 Starting basis
Jul 05 01:18:14 Finished basis                                                55m45s  14GB
Jul 05 01:18:15 Starting compiler/inference
Jul 05 01:20:00 Finished compiler/inference                                    1m45s   1GB
Jul 05 01:20:00 Starting compiler/backend/reg_alloc
Jul 05 01:21:50 Finished compiler/backend/reg_alloc                            1m49s   1GB
Jul 05 01:21:50 Starting compiler/backend/gc
Jul 05 01:26:48 Finished compiler/backend/gc                                   4m57s   2GB
Jul 05 01:26:49 Starting compiler/backend
Jul 05 01:33:37 Finished compiler/backend                                      6m47s   3GB
Jul 05 01:33:37 Starting compiler/encoders/asm
Jul 05 01:34:10 Finished compiler/encoders/asm                                   32s 748MB
Jul 05 01:34:10 Starting compiler/encoders/x64
Jul 05 01:35:24 Finished compiler/encoders/x64                                 1m13s 779MB
Jul 05 01:35:25 Starting compiler/encoders/arm7
Jul 05 01:37:48 Finished compiler/encoders/arm7                                2m23s   1GB
Jul 05 01:37:48 Starting compiler/encoders/arm8
Jul 05 01:38:34 Finished compiler/encoders/arm8                                  45s 748MB
Jul 05 01:38:34 Starting compiler/encoders/arm8_asl
Jul 05 04:08:22 Finished compiler/encoders/arm8_asl                         2h29m47s  39GB
Jul 05 04:08:22 Starting compiler/encoders/mips
Jul 05 04:10:06 Finished compiler/encoders/mips                                1m43s   1GB
Jul 05 04:10:06 Starting compiler/encoders/riscv
Jul 05 04:12:06 Finished compiler/encoders/riscv                               2m00s 966MB
Jul 05 04:12:06 Starting compiler/encoders/ag32
Jul 05 04:12:30 Finished compiler/encoders/ag32                                  23s 651MB
Jul 05 04:12:31 Starting compiler/backend/x64
Jul 05 04:12:55 Finished compiler/backend/x64                                    23s   1GB
Jul 05 04:12:55 Starting compiler/backend/arm7
Jul 05 04:13:21 Finished compiler/backend/arm7                                   25s   1GB
Jul 05 04:13:21 Starting compiler/backend/arm8
Jul 05 04:13:46 Finished compiler/backend/arm8                                   23s   1GB
Jul 05 04:13:46 Starting compiler/backend/mips
Jul 05 04:14:10 Finished compiler/backend/mips                                   24s   1GB
Jul 05 04:14:11 Starting compiler/backend/riscv
Jul 05 04:14:35 Finished compiler/backend/riscv                                  24s   1GB
Jul 05 04:14:36 Starting compiler/backend/ag32
Jul 05 04:16:11 Finished compiler/backend/ag32                                 1m35s   1GB
Jul 05 04:16:12 Starting compiler/parsing/proofs
Jul 05 04:20:22 Finished compiler/parsing/proofs                               4m09s 994MB
Jul 05 04:20:22 Starting compiler/inference/proofs
Jul 05 04:23:21 Finished compiler/inference/proofs                             2m59s   1GB
Jul 05 04:23:21 Starting compiler/backend/semantics
Jul 05 04:53:40 Finished compiler/backend/semantics                           30m18s   3GB
Jul 05 04:53:41 Starting compiler/backend/reg_alloc/proofs
Jul 05 04:57:47 Finished compiler/backend/reg_alloc/proofs                     4m05s   1GB
Jul 05 04:57:47 Starting compiler/backend/proofs
Jul 05 06:00:43 Finished compiler/backend/proofs                            1h02m55s  16GB
Jul 05 06:00:43 Starting compiler/backend/serialiser
Jul 05 06:02:33 Finished compiler/backend/serialiser                           1m49s   2GB
Jul 05 06:02:33 Starting compiler/encoders/x64/proofs
Jul 05 06:12:59 Finished compiler/encoders/x64/proofs                         10m25s   7GB
Jul 05 06:12:59 Starting compiler/encoders/arm7/proofs
Jul 05 06:27:41 Finished compiler/encoders/arm7/proofs                        14m41s   3GB
Jul 05 06:27:41 Starting compiler/encoders/arm8/proofs
Jul 05 06:35:11 Finished compiler/encoders/arm8/proofs                         7m29s   1GB
Jul 05 06:35:11 Starting compiler/encoders/arm8_asl/proofs
Jul 05 07:29:22 Finished compiler/encoders/arm8_asl/proofs                    54m10s   5GB
Jul 05 07:29:22 Starting compiler/encoders/mips/proofs
Jul 05 07:40:47 Finished compiler/encoders/mips/proofs                        11m25s   2GB
Jul 05 07:40:47 Starting compiler/encoders/riscv/proofs
Jul 05 07:50:26 Finished compiler/encoders/riscv/proofs                        9m38s   1GB
Jul 05 07:50:26 Starting compiler/encoders/ag32/proofs
Jul 05 07:53:19 Finished compiler/encoders/ag32/proofs                         2m52s 818MB
Jul 05 07:53:20 Starting compiler/backend/x64/proofs
Jul 05 07:53:50 Finished compiler/backend/x64/proofs                             30s   1GB
Jul 05 07:53:51 Starting compiler/backend/arm7/proofs
Jul 05 07:54:23 Finished compiler/backend/arm7/proofs                            31s   1GB
Jul 05 07:54:23 Starting compiler/backend/arm8/proofs
Jul 05 07:54:54 Finished compiler/backend/arm8/proofs                            30s   1GB
Jul 05 07:54:54 Starting compiler/backend/arm8_asl
Jul 05 07:55:19 Finished compiler/backend/arm8_asl                               25s   1GB
Jul 05 07:55:20 Starting compiler/backend/mips/proofs
Jul 05 07:55:51 Finished compiler/backend/mips/proofs                            30s   1GB
Jul 05 07:55:51 Starting compiler/backend/riscv/proofs
Jul 05 07:56:22 Finished compiler/backend/riscv/proofs                           30s   1GB
Jul 05 07:56:22 Starting compiler/backend/ag32/proofs
Jul 05 08:11:19 Finished compiler/backend/ag32/proofs                         14m56s   2GB
Jul 05 08:11:19 Starting compiler/proofs
Jul 05 08:13:56 Finished compiler/proofs                                       2m36s   3GB
Jul 05 08:13:56 Starting candle/set-theory
Jul 05 08:14:33 Finished candle/set-theory                                       36s   1GB
Jul 05 08:14:33 Starting candle/syntax-lib
Jul 05 08:14:47 Finished candle/syntax-lib                                       13s 656MB
Jul 05 08:14:47 Starting candle/standard/syntax
Jul 05 08:16:59 Finished candle/standard/syntax                                2m11s   1GB
Jul 05 08:17:00 Starting candle/standard/semantics
Jul 05 08:18:55 Finished candle/standard/semantics                             1m55s   1GB
Jul 05 08:18:56 Starting candle/standard/monadic
Jul 05 08:21:03 Finished candle/standard/monadic                               2m06s   1GB
Jul 05 08:21:03 Starting candle/standard/ml_kernel
Jul 05 08:28:12 Finished candle/standard/ml_kernel                             7m08s   3GB
Jul 05 08:28:12 Starting candle/overloading/syntax
Jul 05 08:31:42 Finished candle/overloading/syntax                             3m29s   1GB
Jul 05 08:31:42 Starting candle/overloading/semantics
Jul 05 08:44:40 Finished candle/overloading/semantics                         12m57s   2GB
Jul 05 08:44:40 Starting candle/overloading/monadic
Jul 05 08:47:31 Finished candle/overloading/monadic                            2m50s   1GB
Jul 05 08:47:32 Starting candle/overloading/ml_kernel
Jul 05 08:55:32 Finished candle/overloading/ml_kernel                          8m00s   3GB
Jul 05 08:55:33 Starting candle/overloading/ml_checker
Jul 05 08:58:01 Finished candle/overloading/ml_checker                         2m28s   3GB
Jul 05 08:58:01 Starting candle/prover
Jul 05 09:09:36 Finished candle/prover                                        11m34s   3GB
Jul 05 09:09:37 Starting pancake
Jul 05 09:13:45 Finished pancake                                               4m08s   4GB
Jul 05 09:13:45 Starting pancake/ffi
Jul 05 09:13:46 Finished pancake/ffi                                              0s  17MB
Jul 05 09:13:46 Starting pancake/semantics
Jul 05 09:16:43 Finished pancake/semantics                                     2m56s   1GB
Jul 05 09:16:43 Starting pancake/proofs
Jul 05 09:30:27 Finished pancake/proofs                                       13m44s   6GB
Jul 05 09:30:28 Starting characteristic/examples
Jul 05 09:32:00 Finished characteristic/examples                               1m30s   2GB
Jul 05 09:32:00 Starting tutorial/solutions
Jul 05 09:48:44 Finished tutorial/solutions                                   16m43s   9GB
Jul 05 09:48:44 Starting translator/monadic/examples
Jul 05 09:52:58 Finished translator/monadic/examples                           4m13s   2GB
Jul 05 09:52:58 Starting examples
Jul 05 10:04:16 Finished examples                                             11m18s   3GB
Jul 05 10:04:17 Starting examples/compilation/x64
Jul 05 12:13:43 Finished examples/compilation/x64                           2h09m25s  13GB
Jul 05 12:13:43 Starting examples/compilation/x64/proofs
Jul 05 12:16:25 Finished examples/compilation/x64/proofs                       2m41s   2GB
Jul 05 12:16:25 Starting examples/compilation/ag32
Jul 05 12:51:18 Finished examples/compilation/ag32                            34m51s   7GB
Jul 05 12:51:18 Starting examples/compilation/ag32/proofs
Jul 05 12:52:17 Finished examples/compilation/ag32/proofs                        58s   2GB
Jul 05 12:52:17 Starting examples/lpr_checker
Jul 05 12:53:23 Finished examples/lpr_checker                                  1m05s 895MB
Jul 05 12:53:23 Starting examples/lpr_checker/array
Jul 05 13:30:19 Finished examples/lpr_checker/array                           36m55s   6GB
Jul 05 13:30:19 Starting examples/lpr_checker/array/compilation
Jul 05 14:11:54 Finished examples/lpr_checker/array/compilation               41m35s  22GB
Jul 05 14:11:55 Starting examples/lpr_checker/array/compilation/proofs
Jul 05 14:13:23 Finished examples/lpr_checker/array/compilation/proofs         1m28s   6GB
Jul 05 14:13:23 Starting examples/opentheory
Jul 05 14:24:43 Finished examples/opentheory                                  11m19s   5GB
Jul 05 14:24:44 Starting examples/opentheory
Jul 05 14:24:45 Finished examples/opentheory                                      1s  29MB
Jul 05 14:24:45 Starting examples/opentheory/compilation
Jul 05 15:04:30 Finished examples/opentheory/compilation                      39m44s  19GB
Jul 05 15:04:30 Starting examples/opentheory/compilation/proofs
Jul 05 15:05:45 Finished examples/opentheory/compilation/proofs                1m14s   3GB
Jul 05 15:05:45 Starting examples/opentheory/compilation/ag32
Jul 05 15:41:26 Finished examples/opentheory/compilation/ag32                 35m40s  21GB
Jul 05 15:41:26 Starting examples/opentheory/compilation/ag32/proofs
Jul 05 15:43:20 Finished examples/opentheory/compilation/ag32/proofs           1m53s   6GB
Jul 05 15:43:20 Starting examples/sat_encodings
Jul 05 15:45:28 Finished examples/sat_encodings                                2m07s 988MB
Jul 05 15:45:28 Starting examples/sat_encodings/case_studies
Jul 05 15:47:21 Finished examples/sat_encodings/case_studies                   1m52s   1GB
Jul 05 15:47:21 Starting examples/sat_encodings/translation
Jul 05 15:53:35 Finished examples/sat_encodings/translation                    6m14s   3GB
Jul 05 15:53:36 Starting examples/sat_encodings/translation/compilation
Jul 05 16:45:56 Finished examples/sat_encodings/translation/compilation       52m20s  22GB
Jul 05 16:45:57 Starting examples/deflate
Jul 05 16:46:59 Finished examples/deflate                                      1m01s 859MB
Jul 05 16:46:59 Starting examples/deflate/translation
Jul 05 16:48:41 Finished examples/deflate/translation                          1m41s   2GB
Jul 05 16:48:41 Starting examples/deflate/translation/compilation
Jul 05 17:12:04 Finished examples/deflate/translation/compilation             23m22s  15GB
Jul 05 17:12:05 Starting translator/okasaki-examples
Jul 05 17:17:31 Finished translator/okasaki-examples                           5m26s   1GB
Jul 05 17:17:31 Starting translator/other-examples
Jul 05 17:20:11 Finished translator/other-examples                             2m39s   1GB
Jul 05 17:20:11 Starting compiler/parsing/tests
Jul 05 17:20:43 Finished compiler/parsing/tests                                  31s 689MB
Jul 05 17:20:44 Starting compiler/inference/tests
Jul 05 17:29:28 Finished compiler/inference/tests                              8m44s   6GB
Jul 05 17:29:28 Starting compiler/printing/test
Jul 05 17:33:21 Finished compiler/printing/test                                3m52s   3GB
Jul 05 17:33:21 Starting icing/flover
Jul 05 18:25:29 Finished icing/flover                                         52m05s   1GB
Jul 05 18:25:29 Starting icing/
Jul 05 19:42:54 Finished icing/                                             1h17m25s   6GB
Jul 05 19:42:55 Starting icing/examples
Jul 05 19:44:41 Finished icing/examples                                        1m46s   5GB
Jul 05 19:44:41 Starting compiler/repl
Jul 05 19:58:47 Finished compiler/repl                                        14m05s   7GB
Jul 05 19:58:47 Starting compiler/bootstrap/translation
Jul 05 22:49:24 FAILED: compiler/bootstrap/translation
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
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/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
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/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
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.178s) 
monadic_encTheory                    compiler/encoders/monadic_enc (14s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                  compiler/encoders/monadic_enc (21s)     OK
monadic_enc64Theory                  compiler/encoders/monadic_enc (22s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (58.227s) 
decProgTheory                       compiler/bootstrap/translation(179s)     OK
Starting work on to_flatProgTheory
caml_lexTheory                              compiler/parsing/ocaml(239s)     OK
Starting work on camlPEGTheory
camlPEGTheory                               compiler/parsing/ocaml(116s)     OK
Starting work on camlPtreeConversionTheory
camlPtreeConversionTheory                   compiler/parsing/ocaml (61s)     OK
Starting work on caml_parserTheory
caml_parserTheory                           compiler/parsing/ocaml (13s)     OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4]          (431.506s) 
to_flatProgTheory                   compiler/bootstrap/translation(368s)     OK
Starting work on to_closProgTheory
to_closProgTheory                   compiler/bootstrap/translation(667s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                    compiler/bootstrap/translation(573s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                    compiler/bootstrap/translation(475s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                   compiler/bootstrap/translation(272s)     OK
Starting work on lexerProgTheory
lexerProgTheory                     compiler/bootstrap/translation(198s)     OK
Starting work on parserProgTheory
parserProgTheory                    compiler/bootstrap/translation(588s)     OK
Starting work on caml_lexProgTheory
caml_lexProgTheory                  compiler/bootstrap/translation(518s)     OK
Starting work on caml_parserProgTheory
caml_parserProgTheory               compiler/bootstrap/translation (17m)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                 compiler/bootstrap/translation (18m)     OK
Starting work on inferProgTheory
inferProgTheory                     compiler/bootstrap/translation (40m)     OK
Starting work on explorerProgTheory
explorerProgTheory                  compiler/bootstrap/translation (17m)     OK
Starting work on decodeProgTheory
decodeProgTheory                    compiler/bootstrap/translation(313s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory               compiler/bootstrap/translation(211s)FAIL<1>
 No matching sub-term found
 error in quse /home/cake/oven/regression/cakeml-1952/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/cake/oven/regression/cakeml-1952/compiler/bootstrap/translation/sexp_parserProgScript : HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 Proof of 
 
 print_sexp s = print_sexp_alt s
 
 failed.
 Failed to prove theorem print_sexp_alt_thm.
 Uncaught exception: HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}