CakeML Regression Test

Job 2242

CakeML:4ac0c7ccf30fd2e5c5505a039a348b2486659fcc
  fix ag32_basis_ffiProof [Nov 25 02:18:19]
#975 (byte)
Merging into:8ac36a22c960a9f4aaae14aa89dabaf177cd63fa
  Merge pull request #974 from CakeML/dominance [Nov 15 15:00:12]
HOL:8f74c6afc449d7002c926d75228bd4ecb539d82f
  Allow type vars in cv_typesLib functions [Nov 19 10:16:00]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Nov 28 09:01:24 Claimed job
Nov 28 09:01:30 Reusing HOL
Nov 28 09:02:12 Starting developers
Nov 28 09:02:17 Finished developers                                               5s 102MB
Nov 28 09:02:17 Starting developers/bin
Nov 28 09:02:23 Finished developers/bin                                           6s   1GB
Nov 28 09:02:23 Starting compiler/proofs
Nov 28 10:52:16 Finished compiler/proofs                                    1h49m51s  18GB
Nov 28 10:52:16 Starting compiler/bootstrap/translation
Nov 28 19:09:07 Finished compiler/bootstrap/translation                     8h16m50s  43GB
Nov 28 19:09:07 Starting semantics/ffi
Nov 28 19:09:13 Finished semantics/ffi                                            5s 208MB
Nov 28 19:09:13 Starting semantics
Nov 28 19:09:14 Finished semantics                                                1s  19MB
Nov 28 19:09:14 Starting semantics/proofs
Nov 28 19:09:47 Finished semantics/proofs                                        32s 717MB
Nov 28 19:09:48 Starting semantics/alt_semantics
Nov 28 19:10:20 Finished semantics/alt_semantics                                 31s 788MB
Nov 28 19:10:20 Starting semantics/alt_semantics/proofs
Nov 28 19:22:10 Finished semantics/alt_semantics/proofs                       11m49s   1GB
Nov 28 19:22:10 Starting basis/pure
Nov 28 19:22:12 Finished basis/pure                                               1s  22MB
Nov 28 19:22:12 Starting translator
Nov 28 19:24:02 Finished translator                                            1m49s   1GB
Nov 28 19:24:02 Starting compiler/parsing
Nov 28 19:24:03 Finished compiler/parsing                                         1s  18MB
Nov 28 19:24:04 Starting characteristic
Nov 28 19:24:06 Finished characteristic                                           1s  29MB
Nov 28 19:24:06 Starting translator/monadic
Nov 28 19:24:08 Finished translator/monadic                                       1s  18MB
Nov 28 19:24:08 Starting basis
Nov 28 19:27:52 Finished basis                                                 3m44s   3GB
Nov 28 19:27:52 Starting compiler/inference
Nov 28 19:27:54 Finished compiler/inference                                       1s  20MB
Nov 28 19:27:54 Starting compiler/backend/reg_alloc
Nov 28 19:27:55 Finished compiler/backend/reg_alloc                               1s  18MB
Nov 28 19:27:55 Starting compiler/backend/gc
Nov 28 19:27:58 Finished compiler/backend/gc                                      2s  23MB
Nov 28 19:27:58 Starting compiler/backend
Nov 28 19:28:10 Finished compiler/backend                                        12s 741MB
Nov 28 19:28:10 Starting compiler/encoders/asm
Nov 28 19:28:12 Finished compiler/encoders/asm                                    1s  21MB
Nov 28 19:28:12 Starting compiler/encoders/x64
Nov 28 19:28:14 Finished compiler/encoders/x64                                    1s  21MB
Nov 28 19:28:14 Starting compiler/encoders/arm7
Nov 28 19:28:16 Finished compiler/encoders/arm7                                   1s  24MB
Nov 28 19:28:16 Starting compiler/encoders/arm8
Nov 28 19:28:18 Finished compiler/encoders/arm8                                   1s  20MB
Nov 28 19:28:18 Starting compiler/encoders/arm8_asl
Nov 28 19:31:32 Finished compiler/encoders/arm8_asl                            3m13s   1GB
Nov 28 19:31:32 Starting compiler/encoders/mips
Nov 28 19:31:34 Finished compiler/encoders/mips                                   1s  19MB
Nov 28 19:31:34 Starting compiler/encoders/riscv
Nov 28 19:31:36 Finished compiler/encoders/riscv                                  1s  19MB
Nov 28 19:31:36 Starting compiler/encoders/ag32
Nov 28 19:31:37 Finished compiler/encoders/ag32                                   1s  23MB
Nov 28 19:31:37 Starting compiler/backend/x64
Nov 28 19:31:40 Finished compiler/backend/x64                                     2s  25MB
Nov 28 19:31:40 Starting compiler/backend/arm7
Nov 28 19:31:42 Finished compiler/backend/arm7                                    2s  29MB
Nov 28 19:31:42 Starting compiler/backend/arm8
Nov 28 19:31:44 Finished compiler/backend/arm8                                    2s  27MB
Nov 28 19:31:44 Starting compiler/backend/mips
Nov 28 19:31:47 Finished compiler/backend/mips                                    2s  28MB
Nov 28 19:31:47 Starting compiler/backend/riscv
Nov 28 19:31:49 Finished compiler/backend/riscv                                   2s  27MB
Nov 28 19:31:49 Starting compiler/backend/ag32
Nov 28 19:33:14 Finished compiler/backend/ag32                                 1m24s   1GB
Nov 28 19:33:14 Starting compiler/parsing/proofs
Nov 28 19:33:15 Finished compiler/parsing/proofs                                  1s  19MB
Nov 28 19:33:16 Starting compiler/inference/proofs
Nov 28 19:33:17 Finished compiler/inference/proofs                                1s  20MB
Nov 28 19:33:17 Starting compiler/backend/semantics
Nov 28 19:34:34 Finished compiler/backend/semantics                            1m16s   1GB
Nov 28 19:34:34 Starting compiler/backend/reg_alloc/proofs
Nov 28 19:34:36 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Nov 28 19:34:36 Starting compiler/backend/proofs
Nov 28 19:35:36 Finished compiler/backend/proofs                                 59s   3GB
Nov 28 19:35:36 Starting compiler/backend/serialiser
Nov 28 19:35:39 Finished compiler/backend/serialiser                              2s  31MB
Nov 28 19:35:39 Starting compiler/encoders/x64/proofs
Nov 28 19:45:25 Finished compiler/encoders/x64/proofs                          9m45s   5GB
Nov 28 19:45:25 Starting compiler/encoders/arm7/proofs
Nov 28 19:59:17 Finished compiler/encoders/arm7/proofs                        13m52s   4GB
Nov 28 19:59:17 Starting compiler/encoders/arm8/proofs
Nov 28 20:06:09 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
Nov 28 20:06:09 Starting compiler/encoders/arm8_asl/proofs
Nov 28 20:21:23 Finished compiler/encoders/arm8_asl/proofs                    15m13s   2GB
Nov 28 20:21:23 Starting compiler/encoders/mips/proofs
Nov 28 20:31:59 Finished compiler/encoders/mips/proofs                        10m35s   2GB
Nov 28 20:31:59 Starting compiler/encoders/riscv/proofs
Nov 28 20:41:03 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
Nov 28 20:41:03 Starting compiler/encoders/ag32/proofs
Nov 28 20:43:33 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Nov 28 20:43:33 Starting compiler/backend/x64/proofs
Nov 28 20:44:01 Finished compiler/backend/x64/proofs                             28s   1GB
Nov 28 20:44:02 Starting compiler/backend/arm7/proofs
Nov 28 20:44:34 Finished compiler/backend/arm7/proofs                            31s   1GB
Nov 28 20:44:34 Starting compiler/backend/arm8/proofs
Nov 28 20:45:04 Finished compiler/backend/arm8/proofs                            30s   1GB
Nov 28 20:45:04 Starting compiler/backend/arm8_asl
Nov 28 20:45:29 Finished compiler/backend/arm8_asl                               24s   1GB
Nov 28 20:45:29 Starting compiler/backend/mips/proofs
Nov 28 20:46:01 Finished compiler/backend/mips/proofs                            31s   2GB
Nov 28 20:46:01 Starting compiler/backend/riscv/proofs
Nov 28 20:46:34 Finished compiler/backend/riscv/proofs                           32s   1GB
Nov 28 20:46:34 Starting compiler/backend/ag32/proofs
Nov 28 21:00:17 Finished compiler/backend/ag32/proofs                         13m43s   3GB
Nov 28 21:00:17 Starting candle/set-theory
Nov 28 21:00:56 Finished candle/set-theory                                       38s   1GB
Nov 28 21:00:56 Starting candle/syntax-lib
Nov 28 21:00:57 Finished candle/syntax-lib                                        1s  20MB
Nov 28 21:00:57 Starting candle/standard/syntax
Nov 28 21:01:08 Finished candle/standard/syntax                                  10s 547MB
Nov 28 21:01:08 Starting candle/standard/semantics
Nov 28 21:03:09 Finished candle/standard/semantics                             2m01s   1GB
Nov 28 21:03:09 Starting candle/standard/monadic
Nov 28 21:03:11 Finished candle/standard/monadic                                  1s  29MB
Nov 28 21:03:11 Starting candle/standard/ml_kernel
Nov 28 21:04:51 Finished candle/standard/ml_kernel                             1m40s   3GB
Nov 28 21:04:51 Starting candle/overloading/syntax
Nov 28 21:08:16 Finished candle/overloading/syntax                             3m24s   1GB
Nov 28 21:08:16 Starting candle/overloading/semantics
Nov 28 21:20:49 Finished candle/overloading/semantics                         12m32s   2GB
Nov 28 21:20:49 Starting candle/overloading/monadic
Nov 28 21:23:36 Finished candle/overloading/monadic                            2m46s   2GB
Nov 28 21:23:36 Starting candle/overloading/ml_kernel
Nov 28 21:31:41 Finished candle/overloading/ml_kernel                          8m05s   3GB
Nov 28 21:31:41 Starting candle/overloading/ml_checker
Nov 28 21:34:20 Finished candle/overloading/ml_checker                         2m38s   3GB
Nov 28 21:34:20 Starting candle/prover
Nov 28 21:44:31 Finished candle/prover                                        10m11s   3GB
Nov 28 21:44:31 Starting pancake
Nov 28 21:45:14 Finished pancake                                                 42s 873MB
Nov 28 21:45:14 Starting pancake/ffi
Nov 28 21:45:14 Finished pancake/ffi                                              0s  13MB
Nov 28 21:45:14 Starting pancake/semantics
Nov 28 21:47:38 Finished pancake/semantics                                     2m23s   1GB
Nov 28 21:47:38 Starting pancake/parser
Nov 28 21:48:01 Finished pancake/parser                                          23s 613MB
Nov 28 21:48:02 Starting pancake/proofs
Nov 28 22:21:14 Finished pancake/proofs                                       33m11s   6GB
Nov 28 22:21:14 Starting characteristic/examples
Nov 28 22:22:48 Finished characteristic/examples                               1m34s   3GB
Nov 28 22:22:48 Starting tutorial/solutions
Nov 28 22:38:12 Finished tutorial/solutions                                   15m23s   9GB
Nov 28 22:38:12 Starting translator/monadic/examples
Nov 28 22:42:16 Finished translator/monadic/examples                           4m04s   3GB
Nov 28 22:42:17 Starting examples
Nov 28 22:58:13 Finished examples                                             15m56s   6GB
Nov 28 22:58:13 Starting examples/compilation/x64
Nov 29 00:57:39 Finished examples/compilation/x64                           1h59m25s  18GB
Nov 29 00:57:39 Starting examples/compilation/x64/proofs
Nov 29 01:00:14 Finished examples/compilation/x64/proofs                       2m35s   4GB
Nov 29 01:00:14 Starting examples/compilation/ag32
Nov 29 01:30:32 Finished examples/compilation/ag32                            30m17s   9GB
Nov 29 01:30:32 Starting examples/compilation/ag32/proofs
Nov 29 01:31:35 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Nov 29 01:31:35 Starting examples/compilation/to_word
Nov 29 01:34:58 Finished examples/compilation/to_word                          3m23s   7GB
Nov 29 01:34:59 Starting examples/lpr_checker
Nov 29 01:36:04 Finished examples/lpr_checker                                  1m04s   1GB
Nov 29 01:36:04 Starting examples/lpr_checker/array
Nov 29 02:07:15 Finished examples/lpr_checker/array                           31m11s   6GB
Nov 29 02:07:15 Starting examples/lpr_checker/array/compilation
Nov 29 02:59:35 Finished examples/lpr_checker/array/compilation               52m19s  31GB
Nov 29 02:59:35 Starting examples/lpr_checker/array/compilation/proofs
Nov 29 03:01:42 Finished examples/lpr_checker/array/compilation/proofs         2m06s   3GB
Nov 29 03:01:42 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 29 03:11:37 Finished examples/lpr_checker/array/compilation/proofsARM8     9m54s  24GB
Nov 29 03:11:37 Starting examples/pseudo_bool
Nov 29 03:13:25 Finished examples/pseudo_bool                                  1m48s   1GB
Nov 29 03:13:25 Starting examples/pseudo_bool/cnf_encoding
Nov 29 03:13:50 Finished examples/pseudo_bool/cnf_encoding                       25s 692MB
Nov 29 03:13:50 Starting examples/pseudo_bool/graph_encoding
Nov 29 03:14:33 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Nov 29 03:14:33 Starting examples/pseudo_bool/array
Nov 29 04:07:36 Finished examples/pseudo_bool/array                           53m02s   5GB
Nov 29 04:07:36 Starting examples/pseudo_bool/array/compilation
Nov 29 07:03:32 Finished examples/pseudo_bool/array/compilation             2h55m55s  30GB
Nov 29 07:03:32 Starting examples/pseudo_bool/array/compilation/proofs
Nov 29 07:06:23 Finished examples/pseudo_bool/array/compilation/proofs         2m51s   5GB
Nov 29 07:06:24 Starting examples/opentheory
Nov 29 07:17:29 Finished examples/opentheory                                  11m05s   3GB
Nov 29 07:17:29 Starting examples/opentheory
Nov 29 07:17:31 Finished examples/opentheory                                      1s  25MB
Nov 29 07:17:31 Starting examples/opentheory/compilation
Nov 29 07:54:31 Finished examples/opentheory/compilation                      37m00s  33GB
Nov 29 07:54:32 Starting examples/opentheory/compilation/proofs
Nov 29 07:55:35 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Nov 29 07:55:35 Starting examples/opentheory/compilation/ag32
Nov 29 08:30:19 Finished examples/opentheory/compilation/ag32                 34m44s  28GB
Nov 29 08:30:20 Starting examples/opentheory/compilation/ag32/proofs
Nov 29 08:32:16 Finished examples/opentheory/compilation/ag32/proofs           1m56s   8GB
Nov 29 08:32:16 Starting examples/sat_encodings
Nov 29 08:34:21 Finished examples/sat_encodings                                2m04s 953MB
Nov 29 08:34:21 Starting examples/sat_encodings/case_studies
Nov 29 08:36:06 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Nov 29 08:36:06 Starting examples/sat_encodings/translation
Nov 29 08:42:24 Finished examples/sat_encodings/translation                    6m18s   4GB
Nov 29 08:42:24 Starting examples/sat_encodings/translation/compilation
Nov 29 09:29:12 Finished examples/sat_encodings/translation/compilation       46m47s  27GB
Nov 29 09:29:12 Starting examples/deflate
Nov 29 09:30:11 Finished examples/deflate                                        59s 862MB
Nov 29 09:30:12 Starting examples/deflate/translation
Nov 29 09:31:55 Finished examples/deflate/translation                          1m42s   3GB
Nov 29 09:31:55 Starting examples/deflate/translation/compilation
Nov 29 09:52:08 Finished examples/deflate/translation/compilation             20m12s  13GB
Nov 29 09:52:08 Starting examples/vipr
Nov 29 09:56:11 Finished examples/vipr                                         4m02s   5GB
Nov 29 09:56:11 Starting examples/vipr/compilation
Nov 29 10:18:12 Finished examples/vipr/compilation                            22m01s  16GB
Nov 29 10:18:12 Starting translator/okasaki-examples
Nov 29 10:23:19 Finished translator/okasaki-examples                           5m06s   2GB
Nov 29 10:23:19 Starting translator/other-examples
Nov 29 10:26:04 Finished translator/other-examples                             2m44s   1GB
Nov 29 10:26:04 Starting compiler/parsing/tests
Nov 29 10:26:36 Finished compiler/parsing/tests                                  31s 752MB
Nov 29 10:26:36 Starting compiler/inference/tests
Nov 29 10:35:06 Finished compiler/inference/tests                              8m29s   6GB
Nov 29 10:35:06 Starting compiler/printing/test
Nov 29 10:38:48 Finished compiler/printing/test                                3m42s   4GB
Nov 29 10:38:49 Starting icing/flover
Nov 29 11:23:14 Finished icing/flover                                         44m25s   2GB
Nov 29 11:23:14 Starting icing/
Nov 29 12:17:34 Finished icing/                                               54m19s  11GB
Nov 29 12:17:34 Starting icing/examples
Nov 29 12:19:13 Finished icing/examples                                        1m38s   4GB
Nov 29 12:19:13 Starting compiler/repl
Nov 29 12:19:41 FAILED: compiler/repl
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/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/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/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/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/l3-machine-code/x64/model[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)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanned 86 directories
Starting work on README.md
Starting work on evaluate_skipTheory
README.md                                                                                                                                                                       (0s)     OK
evaluate_skipTheory                                                                                                                                                            (23s)FAIL<1>
                ref_rel (v_rel fr ft fe) (EL n s) (EL m s')
          else FLOOKUP fr n = NONE) 
     match_res_rel
       (env env'.
            LIST_REL ((n,v) (m,w). n = m  v_rel fr ft fe v w) env env') res
       res'
 
 failed.
 Failed to prove theorem pmatch_update.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 363)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}