Job 1955

CakeML:4745ef909252018e77ad25adbb175c21a8f78185
  Fix/simplify proof broken by recent HOL change [Jul 05 23:59:42]
HOL:8b0248d705162f895cc7228fd638fe1c7d74b600
  Fix Unicode violation from 5184a58dae1 [Jul 04 06:34:10]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jul 06 00:20:04 Claimed job
Jul 06 00:20:07 Building HOL
Jul 06 00:32:22 Starting developers
Jul 06 00:32:27 Finished developers                                               5s  97MB
Jul 06 00:32:27 Starting developers/bin
Jul 06 00:33:57 Finished developers/bin                                        1m29s   1GB
Jul 06 00:33:57 Starting semantics/ffi
Jul 06 00:34:09 Finished semantics/ffi                                           11s 182MB
Jul 06 00:34:09 Starting semantics
Jul 06 00:37:02 Finished semantics                                             2m52s   1GB
Jul 06 00:37:02 Starting semantics/proofs
Jul 06 00:44:54 Finished semantics/proofs                                      7m52s   1GB
Jul 06 00:44:55 Starting semantics/alt_semantics
Jul 06 00:45:25 Finished semantics/alt_semantics                                 29s 583MB
Jul 06 00:45:25 Starting semantics/alt_semantics/proofs
Jul 06 00:58:19 Finished semantics/alt_semantics/proofs                       12m53s   1GB
Jul 06 00:58:19 Starting basis/pure
Jul 06 01:02:18 Finished basis/pure                                            3m57s 860MB
Jul 06 01:02:18 Starting translator
Jul 06 01:06:17 Finished translator                                            3m58s   1GB
Jul 06 01:06:17 Starting compiler/parsing
Jul 06 01:07:55 Finished compiler/parsing                                      1m37s   4GB
Jul 06 01:07:55 Starting characteristic
Jul 06 01:15:14 Finished characteristic                                        7m18s   2GB
Jul 06 01:15:14 Starting translator/monadic
Jul 06 01:17:23 Finished translator/monadic                                    2m08s   1GB
Jul 06 01:17:23 Starting basis
Jul 06 02:14:05 Finished basis                                                56m40s  12GB
Jul 06 02:14:05 Starting compiler/inference
Jul 06 02:15:50 Finished compiler/inference                                    1m44s   1GB
Jul 06 02:15:50 Starting compiler/backend/reg_alloc
Jul 06 02:17:41 Finished compiler/backend/reg_alloc                            1m50s   1GB
Jul 06 02:17:41 Starting compiler/backend/gc
Jul 06 02:22:40 Finished compiler/backend/gc                                   4m58s   2GB
Jul 06 02:22:40 Starting compiler/backend
Jul 06 02:29:24 Finished compiler/backend                                      6m43s   2GB
Jul 06 02:29:24 Starting compiler/encoders/asm
Jul 06 02:29:58 Finished compiler/encoders/asm                                   33s 949MB
Jul 06 02:29:58 Starting compiler/encoders/x64
Jul 06 02:31:12 Finished compiler/encoders/x64                                 1m13s   1GB
Jul 06 02:31:12 Starting compiler/encoders/arm7
Jul 06 02:33:39 Finished compiler/encoders/arm7                                2m26s   1GB
Jul 06 02:33:39 Starting compiler/encoders/arm8
Jul 06 02:34:25 Finished compiler/encoders/arm8                                  46s   1GB
Jul 06 02:34:25 Starting compiler/encoders/arm8_asl
Jul 06 05:05:32 Finished compiler/encoders/arm8_asl                         2h31m05s  34GB
Jul 06 05:05:32 Starting compiler/encoders/mips
Jul 06 05:07:17 Finished compiler/encoders/mips                                1m44s   1GB
Jul 06 05:07:17 Starting compiler/encoders/riscv
Jul 06 05:09:18 Finished compiler/encoders/riscv                               2m00s   1GB
Jul 06 05:09:18 Starting compiler/encoders/ag32
Jul 06 05:09:42 Finished compiler/encoders/ag32                                  23s 597MB
Jul 06 05:09:42 Starting compiler/backend/x64
Jul 06 05:10:06 Finished compiler/backend/x64                                    24s   1GB
Jul 06 05:10:06 Starting compiler/backend/arm7
Jul 06 05:10:33 Finished compiler/backend/arm7                                   25s   1GB
Jul 06 05:10:33 Starting compiler/backend/arm8
Jul 06 05:10:56 Finished compiler/backend/arm8                                   23s   1GB
Jul 06 05:10:57 Starting compiler/backend/mips
Jul 06 05:11:21 Finished compiler/backend/mips                                   24s   1GB
Jul 06 05:11:21 Starting compiler/backend/riscv
Jul 06 05:11:46 Finished compiler/backend/riscv                                  24s   1GB
Jul 06 05:11:46 Starting compiler/backend/ag32
Jul 06 05:13:21 Finished compiler/backend/ag32                                 1m34s   1GB
Jul 06 05:13:21 Starting compiler/parsing/proofs
Jul 06 05:17:31 Finished compiler/parsing/proofs                               4m10s   1GB
Jul 06 05:17:32 Starting compiler/inference/proofs
Jul 06 05:20:32 Finished compiler/inference/proofs                             2m59s   1GB
Jul 06 05:20:32 Starting compiler/backend/semantics
Jul 06 05:51:40 Finished compiler/backend/semantics                           31m08s   3GB
Jul 06 05:51:41 Starting compiler/backend/reg_alloc/proofs
Jul 06 05:55:48 Finished compiler/backend/reg_alloc/proofs                     4m06s 791MB
Jul 06 05:55:48 Starting compiler/backend/proofs
Jul 06 06:59:27 Finished compiler/backend/proofs                            1h03m38s  20GB
Jul 06 06:59:27 Starting compiler/backend/serialiser
Jul 06 07:01:17 Finished compiler/backend/serialiser                           1m49s   2GB
Jul 06 07:01:17 Starting compiler/encoders/x64/proofs
Jul 06 07:11:47 Finished compiler/encoders/x64/proofs                         10m29s   6GB
Jul 06 07:11:47 Starting compiler/encoders/arm7/proofs
Jul 06 07:26:29 Finished compiler/encoders/arm7/proofs                        14m41s   6GB
Jul 06 07:26:29 Starting compiler/encoders/arm8/proofs
Jul 06 07:34:02 Finished compiler/encoders/arm8/proofs                         7m32s   1GB
Jul 06 07:34:02 Starting compiler/encoders/arm8_asl/proofs
Jul 06 08:29:28 Finished compiler/encoders/arm8_asl/proofs                    55m25s   5GB
Jul 06 08:29:28 Starting compiler/encoders/mips/proofs
Jul 06 08:40:57 Finished compiler/encoders/mips/proofs                        11m28s   2GB
Jul 06 08:40:57 Starting compiler/encoders/riscv/proofs
Jul 06 08:50:40 Finished compiler/encoders/riscv/proofs                        9m42s 950MB
Jul 06 08:50:40 Starting compiler/encoders/ag32/proofs
Jul 06 08:53:35 Finished compiler/encoders/ag32/proofs                         2m54s 675MB
Jul 06 08:53:35 Starting compiler/backend/x64/proofs
Jul 06 08:54:06 Finished compiler/backend/x64/proofs                             30s   1GB
Jul 06 08:54:06 Starting compiler/backend/arm7/proofs
Jul 06 08:54:39 Finished compiler/backend/arm7/proofs                            32s   1GB
Jul 06 08:54:39 Starting compiler/backend/arm8/proofs
Jul 06 08:55:09 Finished compiler/backend/arm8/proofs                            30s   1GB
Jul 06 08:55:10 Starting compiler/backend/arm8_asl
Jul 06 08:55:44 Finished compiler/backend/arm8_asl                               34s   1GB
Jul 06 08:55:44 Starting compiler/backend/mips/proofs
Jul 06 08:56:14 Finished compiler/backend/mips/proofs                            29s   1GB
Jul 06 08:56:14 Starting compiler/backend/riscv/proofs
Jul 06 08:56:45 Finished compiler/backend/riscv/proofs                           30s   1GB
Jul 06 08:56:45 Starting compiler/backend/ag32/proofs
Jul 06 09:11:33 Finished compiler/backend/ag32/proofs                         14m47s   2GB
Jul 06 09:11:33 Starting compiler/proofs
Jul 06 09:14:17 Finished compiler/proofs                                       2m43s   5GB
Jul 06 09:14:18 Starting candle/set-theory
Jul 06 09:14:54 Finished candle/set-theory                                       36s 905MB
Jul 06 09:14:54 Starting candle/syntax-lib
Jul 06 09:15:09 Finished candle/syntax-lib                                       14s 586MB
Jul 06 09:15:09 Starting candle/standard/syntax
Jul 06 09:17:22 Finished candle/standard/syntax                                2m12s 959MB
Jul 06 09:17:22 Starting candle/standard/semantics
Jul 06 09:19:20 Finished candle/standard/semantics                             1m57s   1GB
Jul 06 09:19:20 Starting candle/standard/monadic
Jul 06 09:21:25 Finished candle/standard/monadic                               2m04s   1GB
Jul 06 09:21:25 Starting candle/standard/ml_kernel
Jul 06 09:28:34 Finished candle/standard/ml_kernel                             7m08s   2GB
Jul 06 09:28:35 Starting candle/overloading/syntax
Jul 06 09:32:05 Finished candle/overloading/syntax                             3m30s   1GB
Jul 06 09:32:05 Starting candle/overloading/semantics
Jul 06 09:44:49 Finished candle/overloading/semantics                         12m43s   2GB
Jul 06 09:44:50 Starting candle/overloading/monadic
Jul 06 09:47:42 Finished candle/overloading/monadic                            2m51s   1GB
Jul 06 09:47:42 Starting candle/overloading/ml_kernel
Jul 06 09:55:47 Finished candle/overloading/ml_kernel                          8m04s   4GB
Jul 06 09:55:47 Starting candle/overloading/ml_checker
Jul 06 09:58:21 Finished candle/overloading/ml_checker                         2m33s   2GB
Jul 06 09:58:21 Starting candle/prover
Jul 06 10:09:55 Finished candle/prover                                        11m33s   2GB
Jul 06 10:09:55 Starting pancake
Jul 06 10:14:07 Finished pancake                                               4m11s   4GB
Jul 06 10:14:07 Starting pancake/ffi
Jul 06 10:14:08 Finished pancake/ffi                                              0s  17MB
Jul 06 10:14:08 Starting pancake/semantics
Jul 06 10:16:58 Finished pancake/semantics                                     2m49s   1GB
Jul 06 10:16:58 Starting pancake/proofs
Jul 06 10:30:45 Finished pancake/proofs                                       13m46s   7GB
Jul 06 10:30:46 Starting characteristic/examples
Jul 06 10:32:16 Finished characteristic/examples                               1m29s   3GB
Jul 06 10:32:17 Starting tutorial/solutions
Jul 06 10:48:51 Finished tutorial/solutions                                   16m34s   9GB
Jul 06 10:48:52 Starting translator/monadic/examples
Jul 06 10:53:03 Finished translator/monadic/examples                           4m10s   3GB
Jul 06 10:53:03 Starting examples
Jul 06 11:04:27 Finished examples                                             11m23s   3GB
Jul 06 11:04:27 Starting examples/compilation/x64
Jul 06 13:13:10 Finished examples/compilation/x64                           2h08m42s  14GB
Jul 06 13:13:10 Starting examples/compilation/x64/proofs
Jul 06 13:15:49 Finished examples/compilation/x64/proofs                       2m38s   3GB
Jul 06 13:15:49 Starting examples/compilation/ag32
Jul 06 13:51:04 Finished examples/compilation/ag32                            35m14s   7GB
Jul 06 13:51:04 Starting examples/compilation/ag32/proofs
Jul 06 13:52:02 Finished examples/compilation/ag32/proofs                        58s   2GB
Jul 06 13:52:03 Starting examples/lpr_checker
Jul 06 13:53:08 Finished examples/lpr_checker                                  1m05s   1GB
Jul 06 13:53:09 Starting examples/lpr_checker/array
Jul 06 14:30:25 Finished examples/lpr_checker/array                           37m14s   4GB
Jul 06 14:30:26 Starting examples/lpr_checker/array/compilation
Jul 06 15:12:01 Finished examples/lpr_checker/array/compilation               41m35s  24GB
Jul 06 15:12:01 Starting examples/lpr_checker/array/compilation/proofs
Jul 06 15:13:30 Finished examples/lpr_checker/array/compilation/proofs         1m28s   5GB
Jul 06 15:13:30 Starting examples/opentheory
Jul 06 15:24:44 Finished examples/opentheory                                  11m13s   5GB
Jul 06 15:24:44 Starting examples/opentheory
Jul 06 15:24:46 Finished examples/opentheory                                      1s  23MB
Jul 06 15:24:46 Starting examples/opentheory/compilation
Jul 06 16:04:37 Finished examples/opentheory/compilation                      39m49s  19GB
Jul 06 16:04:37 Starting examples/opentheory/compilation/proofs
Jul 06 16:05:32 Finished examples/opentheory/compilation/proofs                  53s   3GB
Jul 06 16:05:32 Starting examples/opentheory/compilation/ag32
Jul 06 16:40:37 Finished examples/opentheory/compilation/ag32                 35m04s  26GB
Jul 06 16:40:37 Starting examples/opentheory/compilation/ag32/proofs
Jul 06 16:42:31 Finished examples/opentheory/compilation/ag32/proofs           1m54s   6GB
Jul 06 16:42:32 Starting examples/sat_encodings
Jul 06 16:44:40 Finished examples/sat_encodings                                2m08s 908MB
Jul 06 16:44:40 Starting examples/sat_encodings/case_studies
Jul 06 16:46:33 Finished examples/sat_encodings/case_studies                   1m51s 830MB
Jul 06 16:46:33 Starting examples/sat_encodings/translation
Jul 06 16:52:49 Finished examples/sat_encodings/translation                    6m15s   3GB
Jul 06 16:52:49 Starting examples/sat_encodings/translation/compilation
Jul 06 17:45:36 Finished examples/sat_encodings/translation/compilation       52m44s  20GB
Jul 06 17:45:36 Starting examples/deflate
Jul 06 17:46:39 Finished examples/deflate                                      1m02s 756MB
Jul 06 17:46:39 Starting examples/deflate/translation
Jul 06 17:48:22 Finished examples/deflate/translation                          1m42s   3GB
Jul 06 17:48:22 Starting examples/deflate/translation/compilation
Jul 06 18:11:55 Finished examples/deflate/translation/compilation             23m32s  17GB
Jul 06 18:11:56 Starting translator/okasaki-examples
Jul 06 18:17:23 Finished translator/okasaki-examples                           5m26s   2GB
Jul 06 18:17:23 Starting translator/other-examples
Jul 06 18:20:04 Finished translator/other-examples                             2m41s   1GB
Jul 06 18:20:05 Starting compiler/parsing/tests
Jul 06 18:20:36 Finished compiler/parsing/tests                                  31s 600MB
Jul 06 18:20:36 Starting compiler/inference/tests
Jul 06 18:29:26 Finished compiler/inference/tests                              8m48s   3GB
Jul 06 18:29:26 Starting compiler/printing/test
Jul 06 18:33:19 Finished compiler/printing/test                                3m53s   2GB
Jul 06 18:33:20 Starting icing/flover
Jul 06 19:25:04 Finished icing/flover                                         51m43s   1GB
Jul 06 19:25:04 Starting icing/
Jul 06 20:43:00 Finished icing/                                             1h17m54s   6GB
Jul 06 20:43:00 Starting icing/examples
Jul 06 20:44:44 Finished icing/examples                                        1m43s   6GB
Jul 06 20:44:44 Starting compiler/repl
Jul 06 20:58:29 Finished compiler/repl                                        13m45s   7GB
Jul 06 20:58:30 Starting compiler/bootstrap/translation
Jul 06 23:48:59 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 (13s)     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 (21s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (57.378s) 
decProgTheory                       compiler/bootstrap/translation(185s)     OK
Starting work on to_flatProgTheory
caml_lexTheory                              compiler/parsing/ocaml(237s)     OK
Starting work on camlPEGTheory
camlPEGTheory                               compiler/parsing/ocaml(117s)     OK
Starting work on camlPtreeConversionTheory
camlPtreeConversionTheory                   compiler/parsing/ocaml (60s)     OK
Starting work on caml_parserTheory
caml_parserTheory                           compiler/parsing/ocaml (13s)     OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4]          (428.717s) 
to_flatProgTheory                   compiler/bootstrap/translation(356s)     OK
Starting work on to_closProgTheory
to_closProgTheory                   compiler/bootstrap/translation(655s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                    compiler/bootstrap/translation(565s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                    compiler/bootstrap/translation(469s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                   compiler/bootstrap/translation(275s)     OK
Starting work on lexerProgTheory
lexerProgTheory                     compiler/bootstrap/translation(209s)     OK
Starting work on parserProgTheory
parserProgTheory                    compiler/bootstrap/translation(619s)     OK
Starting work on caml_lexProgTheory
caml_lexProgTheory                  compiler/bootstrap/translation(499s)     OK
Starting work on caml_parserProgTheory
caml_parserProgTheory               compiler/bootstrap/translation (18m)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                 compiler/bootstrap/translation (19m)     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(293s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory               compiler/bootstrap/translation(210s)FAIL<1>
 No matching sub-term found
 error in quse /home/cake/oven/regression/cakeml-1955/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-1955/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"}