CakeML Regression Test

Job 924

CakeML:55bcf9b13e7e80741070b122b1d8599effddd232
  Change definition of cause_type_error [Jun 28 15:58:04]
#661 (divord)
Merging into:71e11ac160b9119014d5860128750b891c1061a4
  Adjust a proof that broke due to change in HOL [Jun 29 12:04:52]
HOL:27b999029af7e69c3496b29a745728c30561192b
  Fix regular-play/selftest.sml given testutils changes [Jun 26 01:16:59]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 29 12:05:08 Claimed job
Jun 29 12:05:10 Reusing HOL
Jun 29 12:05:15 Starting developers
Jun 29 12:05:15 Finished developers                                               0s  20MB
Jun 29 12:05:16 Starting developers/bin
Jun 29 12:05:19 Finished developers/bin                                           2s 144MB
Jun 29 12:05:19 Starting semantics/ffi
Jun 29 12:05:27 Finished semantics/ffi                                            7s 212MB
Jun 29 12:05:27 Starting semantics
Jun 29 12:06:43 Finished semantics                                             1m15s   1GB
Jun 29 12:06:43 Starting semantics/proofs
Jun 29 12:09:41 Finished semantics/proofs                                      2m57s   1GB
Jun 29 12:09:42 Starting semantics/alt_semantics
Jun 29 12:09:48 Finished semantics/alt_semantics                                  5s 287MB
Jun 29 12:09:48 Starting semantics/alt_semantics/proofs
Jun 29 12:11:33 Finished semantics/alt_semantics/proofs                        1m45s 726MB
Jun 29 12:11:34 Starting basis/pure
Jun 29 12:12:17 Finished basis/pure                                              42s 710MB
Jun 29 12:12:17 Starting translator
Jun 29 12:13:55 Finished translator                                            1m37s   1GB
Jun 29 12:13:55 Starting compiler/parsing
Jun 29 12:14:52 Finished compiler/parsing                                        56s   3GB
Jun 29 12:14:52 Starting characteristic
Jun 29 12:19:58 Finished characteristic                                        5m06s   1GB
Jun 29 12:19:59 Starting translator/monadic
Jun 29 12:21:25 Finished translator/monadic                                    1m25s   1GB
Jun 29 12:21:25 Starting basis
Jun 29 12:38:04 Finished basis                                                16m38s   2GB
Jun 29 12:38:04 Starting compiler/inference
Jun 29 12:39:39 Finished compiler/inference                                    1m34s   1GB
Jun 29 12:39:39 Starting compiler/backend/reg_alloc
Jun 29 12:40:37 Finished compiler/backend/reg_alloc                              57s   1GB
Jun 29 12:40:37 Starting compiler/backend/gc
Jun 29 12:48:32 Finished compiler/backend/gc                                   7m54s   1GB
Jun 29 12:48:32 Starting compiler/backend
Jun 29 12:48:33 Finished compiler/backend                                         0s  42MB
Jun 29 12:48:34 Starting compiler/encoders/asm
Jun 29 12:48:34 Finished compiler/encoders/asm                                    0s  37MB
Jun 29 12:48:34 Starting compiler/encoders/x64
Jun 29 12:48:57 Finished compiler/encoders/x64                                   22s 946MB
Jun 29 12:48:57 Starting compiler/encoders/arm7
Jun 29 12:49:42 Finished compiler/encoders/arm7                                  44s 732MB
Jun 29 12:49:42 Starting compiler/encoders/arm8
Jun 29 12:49:53 Finished compiler/encoders/arm8                                  11s 888MB
Jun 29 12:49:54 Starting compiler/encoders/mips
Jun 29 12:50:09 Finished compiler/encoders/mips                                  14s 748MB
Jun 29 12:50:09 Starting compiler/encoders/riscv
Jun 29 12:50:22 Finished compiler/encoders/riscv                                 12s 761MB
Jun 29 12:50:22 Starting compiler/encoders/ag32
Jun 29 12:50:37 Finished compiler/encoders/ag32                                  14s 690MB
Jun 29 12:50:37 Starting compiler/backend/x64
Jun 29 12:50:52 Finished compiler/backend/x64                                    14s 959MB
Jun 29 12:50:52 Starting compiler/backend/arm7
Jun 29 12:51:10 Finished compiler/backend/arm7                                   17s   1GB
Jun 29 12:51:11 Starting compiler/backend/arm8
Jun 29 12:51:26 Finished compiler/backend/arm8                                   15s   1GB
Jun 29 12:51:27 Starting compiler/backend/mips
Jun 29 12:51:43 Finished compiler/backend/mips                                   16s   1GB
Jun 29 12:51:43 Starting compiler/backend/riscv
Jun 29 12:52:00 Finished compiler/backend/riscv                                  16s   1GB
Jun 29 12:52:01 Starting compiler/backend/ag32
Jun 29 12:53:06 Finished compiler/backend/ag32                                 1m05s   1GB
Jun 29 12:53:06 Starting compiler/parsing/proofs
Jun 29 12:58:40 Finished compiler/parsing/proofs                               5m33s   1GB
Jun 29 12:58:40 Starting compiler/inference/proofs
Jun 29 13:01:21 Finished compiler/inference/proofs                             2m41s   1GB
Jun 29 13:01:22 Starting compiler/backend/semantics
Jun 29 13:08:28 Finished compiler/backend/semantics                            7m05s   1GB
Jun 29 13:08:28 Starting compiler/backend/reg_alloc/proofs
Jun 29 13:11:43 Finished compiler/backend/reg_alloc/proofs                     3m14s 676MB
Jun 29 13:11:43 Starting compiler/backend/proofs
Jun 29 13:50:07 Finished compiler/backend/proofs                              38m24s   3GB
Jun 29 13:50:08 Starting compiler/encoders/x64/proofs
Jun 29 13:59:17 Finished compiler/encoders/x64/proofs                          9m07s   5GB
Jun 29 13:59:17 Starting compiler/encoders/arm7/proofs
Jun 29 14:11:53 Finished compiler/encoders/arm7/proofs                        12m35s   3GB
Jun 29 14:11:53 Starting compiler/encoders/arm8/proofs
Jun 29 14:18:26 Finished compiler/encoders/arm8/proofs                         6m32s   1GB
Jun 29 14:18:26 Starting compiler/encoders/mips/proofs
Jun 29 14:27:54 Finished compiler/encoders/mips/proofs                         9m27s   2GB
Jun 29 14:27:54 Starting compiler/encoders/riscv/proofs
Jun 29 14:36:25 Finished compiler/encoders/riscv/proofs                        8m31s   1GB
Jun 29 14:36:26 Starting compiler/encoders/ag32/proofs
Jun 29 14:38:54 Finished compiler/encoders/ag32/proofs                         2m28s 677MB
Jun 29 14:38:54 Starting compiler/backend/x64/proofs
Jun 29 14:39:11 Finished compiler/backend/x64/proofs                             15s 983MB
Jun 29 14:39:11 Starting compiler/backend/arm7/proofs
Jun 29 14:39:28 Finished compiler/backend/arm7/proofs                            17s   1GB
Jun 29 14:39:29 Starting compiler/backend/arm8/proofs
Jun 29 14:39:45 Finished compiler/backend/arm8/proofs                            15s 745MB
Jun 29 14:39:45 Starting compiler/backend/mips/proofs
Jun 29 14:40:02 Finished compiler/backend/mips/proofs                            16s   1GB
Jun 29 14:40:02 Starting compiler/backend/riscv/proofs
Jun 29 14:40:19 Finished compiler/backend/riscv/proofs                           16s   1GB
Jun 29 14:40:19 Starting compiler/backend/ag32/proofs
Jun 29 14:49:18 Finished compiler/backend/ag32/proofs                          8m58s   2GB
Jun 29 14:49:19 Starting compiler/proofs
Jun 29 14:50:31 Finished compiler/proofs                                       1m12s   3GB
Jun 29 14:50:32 Starting candle/set-theory
Jun 29 14:50:56 Finished candle/set-theory                                       24s 790MB
Jun 29 14:50:57 Starting candle/syntax-lib
Jun 29 14:51:06 Finished candle/syntax-lib                                        8s 513MB
Jun 29 14:51:06 Starting candle/standard/syntax
Jun 29 14:52:46 Finished candle/standard/syntax                                1m39s 959MB
Jun 29 14:52:46 Starting candle/standard/semantics
Jun 29 14:54:19 Finished candle/standard/semantics                             1m32s   1GB
Jun 29 14:54:19 Starting candle/standard/monadic
Jun 29 14:55:51 Finished candle/standard/monadic                               1m31s   1GB
Jun 29 14:55:52 Starting candle/standard/ml_kernel
Jun 29 14:59:37 Finished candle/standard/ml_kernel                             3m45s   3GB
Jun 29 14:59:38 Starting candle/standard/opentheory
Jun 29 15:07:51 Finished candle/standard/opentheory                            8m12s   4GB
Jun 29 15:07:51 Starting candle/standard/opentheory/compilation
Jun 29 15:37:16 Finished candle/standard/opentheory/compilation               29m24s  15GB
Jun 29 15:37:17 Starting candle/standard/opentheory/compilation/proofs
Jun 29 15:37:57 Finished candle/standard/opentheory/compilation/proofs           39s   2GB
Jun 29 15:37:57 Starting characteristic/examples
Jun 29 15:39:20 Finished characteristic/examples                               1m23s   2GB
Jun 29 15:39:21 Starting tutorial/solutions
Jun 29 15:52:14 Finished tutorial/solutions                                   12m52s   7GB
Jun 29 15:52:14 Starting translator/monadic/examples
Jun 29 15:55:00 Finished translator/monadic/examples                           2m46s   2GB
Jun 29 15:55:01 Starting examples
Jun 29 16:03:41 Finished examples                                              8m39s   3GB
Jun 29 16:03:41 Starting examples/compilation/x64
Jun 29 18:05:11 Finished examples/compilation/x64                           2h01m29s  14GB
Jun 29 18:05:11 Starting examples/compilation/x64/proofs
Jun 29 18:06:36 Finished examples/compilation/x64/proofs                       1m24s   2GB
Jun 29 18:06:36 Starting examples/compilation/ag32
Jun 29 18:35:05 Finished examples/compilation/ag32                            28m28s   5GB
Jun 29 18:35:05 Starting examples/compilation/ag32/proofs
Jun 29 18:35:50 Finished examples/compilation/ag32/proofs                        44s   2GB
Jun 29 18:35:50 Starting translator/okasaki-examples
Jun 29 18:39:51 Finished translator/okasaki-examples                           4m01s   1GB
Jun 29 18:39:52 Starting translator/other-examples
Jun 29 18:42:32 FAILED: translator/other-examples
Starting work on MultTheory
Starting work on tablesTheory
tablesTheory                                                                                                                                                                      OK
MultTheory                                                                                                                                                                        OK
Starting work on RoundOpTheory
RoundOpTheory                                                                                                                                                                     OK
Starting work on aesTheory
aesTheory                                                                                                                                                                         OK
]0;Holmake: .]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/Crypto/RC6]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/Crypto/RC6[1mWorking in $(HOLDIR)/examples/Crypto/RC6[0m
Starting work on RC6Theory
RC6Theory                                                                                                                                                                         OK
]0;Holmake: .]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/Crypto/TEA]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/Crypto/TEA[1mWorking in $(HOLDIR)/examples/Crypto/TEA[0m
Starting work on teaTheory
teaTheory                                                                                                                                                                         OK
Starting work on lazy_teaTheory
lazy_teaTheory                                                                                                                                                                    OK
]0;Holmake: .]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/RSA]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/RSA[1mWorking in $(HOLDIR)/examples/RSA[0m
Starting work on powerTheory
Starting work on summationTheory
powerTheory                                                                                                                                                                       OK
summationTheory                                                                                                                                                                   OK
Starting work on binomialTheory
Starting work on congruentTheory
binomialTheory                                                                                                                                                                    OK
congruentTheory                                                                                                                                                                   OK
Starting work on fermatTheory
fermatTheory                                                                                                                                                                      OK
Starting work on rsaTheory
rsaTheory                                                                                                                                                                         OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/formalize]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/ho_prover]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/useful]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/useful[1mWorking in $(HOLDIR)/examples/miller/useful[0m
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/ho_prover]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/ho_prover[1mWorking in $(HOLDIR)/examples/miller/ho_prover[0m
Starting work on skiTheory
skiTheory                                                                                                                                                                         OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/formalize]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/subtypes]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/subtypes[1mWorking in $(HOLDIR)/examples/miller/subtypes[0m
Starting work on subtypeTheory
subtypeTheory                                                                                                                                                                     OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/formalize]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/formalize[1mWorking in $(HOLDIR)/examples/miller/formalize[0m
Starting work on extra_boolTheory
extra_boolTheory                                                                                                                                                                  OK
Starting work on extra_numTheory
extra_numTheory                                                                                                                                                                   OK
Starting work on extra_listTheory
Starting work on sequenceTheory
sequenceTheory                                                                                                                                                                    OK
extra_listTheory                                                                                                                                                                  OK
Starting work on extra_pred_setTheory
extra_pred_setTheory                                                                                                                                                              OK
Starting work on extra_realTheory
Starting work on orderTheory
orderTheory                                                                                                                                                                       OK
extra_realTheory                                                                                                                                                                  OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/groups]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/groups[1mWorking in $(HOLDIR)/examples/miller/groups[0m
Starting work on extra_arithTheory
extra_arithTheory                                                                                                                                                                 OK
Starting work on groupTheory
Starting work on extra_binomialTheory
Starting work on ftaTheory
extra_binomialTheory                                                                                                                                                              OK
ftaTheory                                                                                                                                                                         OK
groupTheory                                                                                                                                                                       OK
Starting work on finite_groupTheory
finite_groupTheory                                                                                                                                                                OK
Starting work on abelian_groupTheory
Starting work on num_polyTheory
abelian_groupTheory                                                                                                                                                               OK
num_polyTheory                                                                                                                                                                    OK
Starting work on mult_groupTheory
mult_groupTheory                                                                                                                                                                  OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/prob]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/prob[1mWorking in $(HOLDIR)/examples/miller/prob[0m
Starting work on prob_canonTheory
Starting work on prob_pseudoTheory
prob_pseudoTheory                                                                                                                                                                 OK
prob_canonTheory                                                                                                                                                                  OK
Starting work on prob_algebraTheory
prob_algebraTheory                                                                                                                                                                OK
Starting work on probTheory
probTheory                                                                                                                                                                        OK
Starting work on prob_uniformTheory
Starting work on prob_bernoulliTheory
Starting work on prob_binomialTheory
Starting work on prob_diceTheory
prob_binomialTheory                                                                                                                                                               OK
Starting work on prob_geometricTheory
prob_uniformTheory                                                                                                                                                                OK
Starting work on prob_trichotomyTheory
prob_bernoulliTheory                                                                                                                                                              OK
Starting work on prob_walkTheory
prob_diceTheory                                                                                                                                                                   OK
prob_geometricTheory                                                                                                                                                              OK
prob_trichotomyTheory                                                                                                                                                             OK
prob_walkTheory                                                                                                                                                                   OK
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/miller/miller[1mWorking in $(HOLDIR)/examples/miller/miller[0m
Starting work on miller_rabinTheory
miller_rabinTheory                                                                                                                                                                OK
Starting work on miller_rabin_mlTheory
miller_rabin_mlTheory                                                                                                                                                             OK
]0;Holmake: .]0;Holmake: ~/regression/cakeml-924/basis]0;Holmake: ~/regression/cakeml-924/basis/pure]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/balanced_bst]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-924/basis/pure]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-924/basis/pure]0;Holmake: ~/regression/cakeml-924/misc]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-924/misc]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-27b999029af7e69c3496b29a745728c30561192b/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-924/misc]0;Holmake: ~/regression/cakeml-924/developers]0;Holmake: ~/regression/cakeml-924/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-924/misc]0;Holmake: ~/regression/cakeml-924/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-924/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-924/misc]0;Holmake: ~/regression/cakeml-924/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-924/basis/pure]0;Holmake: ~/regression/cakeml-924/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-924/basis]0;Holmake: ~/regression/cakeml-924/characteristic]0;Holmake: ~/regression/cakeml-924/compiler/parsing]0;Holmake: ~/regression/cakeml-924/semantics]0;Holmake: ~/regression/cakeml-924/semantics/ffi]0;Holmake: ~/regression/cakeml-924/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-924/semantics]0;Holmake: ~/regression/cakeml-924/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-924/compiler/parsing]0;Holmake: ~/regression/cakeml-924/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-924/characteristic]0;Holmake: ~/regression/cakeml-924/semantics/proofs]0;Holmake: ~/regression/cakeml-924/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-924/characteristic]0;Holmake: ~/regression/cakeml-924/translator]0;Holmake: ~/regression/cakeml-924/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-924/characteristic]0;Holmake: ~/regression/cakeml-924/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-924/basis]0;Holmake: ~/regression/cakeml-924/translator/monadic]0;Holmake: ~/regression/cakeml-924/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-924/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-924/translator/monadic]0;Holmake: ~/regression/cakeml-924/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-924/basis]0;Holmake: ~/regression/cakeml-924/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: auxiliary]0;Holmake: auxiliary[1mWorking in $(CAKEMLDIR)/translator/other-examples/auxiliary[0m
Starting work on copying_gcTheory
Starting work on ninetyOneTheory
Starting work on regexpMatchTheory
Starting work on slr_parser_genTheory
regexpMatchTheory                                                                                                                                                        FAILED! <1>
 Saved theorem _____ "regexp_case_cong"
 Saved theorem _____ "regexp_case_eq"
 <<HOL message: Defined type: "regexp">>
 
 Exception raised at Defn.multi_dest_eq:
 on line 96, characters 4-43:
 Expected an equality
 error in quse /home/myreen/regression/cakeml-924/translator/other-examples/auxiliary/regexpMatchScript.sml : HOL_ERR {message = "on line 96, characters 4-43:\nExpected an equality", origin_function = "multi_dest_eq", origin_structure = "Defn"}
 error in load regexpMatchScript : HOL_ERR {message = "on line 96, characters 4-43:\nExpected an equality", origin_function = "multi_dest_eq", origin_structure = "Defn"}
 Uncaught exception: HOL_ERR {message = "on line 96, characters 4-43:\nExpected an equality", origin_function = "multi_dest_eq", origin_structure = "Defn"}
copying_gcTheory                                                                                                                                                            M-KILLED
ninetyOneTheory                                                                                                                                                             M-KILLED
slr_parser_genTheory                                                                                                                                                        M-KILLED
]0;Holmake: .