Job 1811

CakeML:8d70115b666585aaa40b992c5d29ae2ac3d5919c
  Stop at errors and interrupts in repl_boot.cml [Feb 27 15:37:25]
#863 (repl)
Merging into:a94b08d68372d18b3de5703f212a08aa713df665
  Merge pull request #861 from mktnk3/pan-to-mc_updated [Feb 28 10:36:05]
HOL:056df98e1f9596a4b6565e74abc49207247cc49b
  More tweaks to DefnBase, and more test cases [Feb 28 00:06:07]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 01 06:41:39 Claimed job
Mar 01 06:41:43 Building HOL
Mar 01 06:51:07 Starting developers
Mar 01 06:51:10 Finished developers                                               2s  99MB
Mar 01 06:51:10 Starting developers/bin
Mar 01 06:52:11 Finished developers/bin                                        1m00s 675MB
Mar 01 06:52:11 Starting semantics/ffi
Mar 01 06:52:20 Finished semantics/ffi                                            9s 259MB
Mar 01 06:52:21 Starting semantics
Mar 01 06:54:36 Finished semantics                                             2m14s   1GB
Mar 01 06:54:36 Starting semantics/proofs
Mar 01 06:58:15 Finished semantics/proofs                                      3m38s   1GB
Mar 01 06:58:15 Starting semantics/alt_semantics
Mar 01 06:58:31 Finished semantics/alt_semantics                                 15s 532MB
Mar 01 06:58:31 Starting semantics/alt_semantics/proofs
Mar 01 07:00:52 Finished semantics/alt_semantics/proofs                        2m21s   1GB
Mar 01 07:00:53 Starting basis/pure
Mar 01 07:03:59 Finished basis/pure                                            3m05s   1GB
Mar 01 07:03:59 Starting translator
Mar 01 07:06:57 Finished translator                                            2m57s   2GB
Mar 01 07:06:57 Starting compiler/parsing
Mar 01 07:08:12 Finished compiler/parsing                                      1m15s   4GB
Mar 01 07:08:13 Starting characteristic
Mar 01 07:14:26 Finished characteristic                                        6m13s   2GB
Mar 01 07:14:26 Starting translator/monadic
Mar 01 07:16:26 Finished translator/monadic                                    2m00s   2GB
Mar 01 07:16:27 Starting basis
Mar 01 08:08:14 Finished basis                                                51m47s  27GB
Mar 01 08:08:14 Starting compiler/inference
Mar 01 08:09:40 Finished compiler/inference                                    1m25s   2GB
Mar 01 08:09:40 Starting compiler/backend/reg_alloc
Mar 01 08:11:21 Finished compiler/backend/reg_alloc                            1m40s   2GB
Mar 01 08:11:21 Starting compiler/backend/gc
Mar 01 08:15:50 Finished compiler/backend/gc                                   4m28s   2GB
Mar 01 08:15:50 Starting compiler/backend
Mar 01 08:21:49 Finished compiler/backend                                      5m59s   4GB
Mar 01 08:21:50 Starting compiler/encoders/asm
Mar 01 08:22:19 Finished compiler/encoders/asm                                   29s 997MB
Mar 01 08:22:19 Starting compiler/encoders/x64
Mar 01 08:23:29 Finished compiler/encoders/x64                                 1m09s   1GB
Mar 01 08:23:29 Starting compiler/encoders/arm7
Mar 01 08:25:41 Finished compiler/encoders/arm7                                2m11s   1GB
Mar 01 08:25:41 Starting compiler/encoders/arm8
Mar 01 08:26:26 Finished compiler/encoders/arm8                                  45s   1GB
Mar 01 08:26:26 Starting compiler/encoders/arm8_asl
Mar 01 10:36:15 Finished compiler/encoders/arm8_asl                         2h09m48s  36GB
Mar 01 10:36:15 Starting compiler/encoders/mips
Mar 01 10:37:46 Finished compiler/encoders/mips                                1m30s   1GB
Mar 01 10:37:46 Starting compiler/encoders/riscv
Mar 01 10:39:33 Finished compiler/encoders/riscv                               1m46s   1GB
Mar 01 10:39:33 Starting compiler/encoders/ag32
Mar 01 10:39:56 Finished compiler/encoders/ag32                                  22s   1GB
Mar 01 10:39:56 Starting compiler/backend/x64
Mar 01 10:40:18 Finished compiler/backend/x64                                    21s   1GB
Mar 01 10:40:18 Starting compiler/backend/arm7
Mar 01 10:40:41 Finished compiler/backend/arm7                                   22s   1GB
Mar 01 10:40:41 Starting compiler/backend/arm8
Mar 01 10:41:04 Finished compiler/backend/arm8                                   22s   1GB
Mar 01 10:41:05 Starting compiler/backend/mips
Mar 01 10:41:28 Finished compiler/backend/mips                                   23s   1GB
Mar 01 10:41:28 Starting compiler/backend/riscv
Mar 01 10:41:51 Finished compiler/backend/riscv                                  23s   1GB
Mar 01 10:41:51 Starting compiler/backend/ag32
Mar 01 10:43:14 Finished compiler/backend/ag32                                 1m22s   2GB
Mar 01 10:43:14 Starting compiler/parsing/proofs
Mar 01 10:45:52 Finished compiler/parsing/proofs                               2m37s   1GB
Mar 01 10:45:52 Starting compiler/inference/proofs
Mar 01 10:48:18 Finished compiler/inference/proofs                             2m25s   1GB
Mar 01 10:48:18 Starting compiler/backend/semantics
Mar 01 11:15:17 Finished compiler/backend/semantics                           26m58s   5GB
Mar 01 11:15:17 Starting compiler/backend/reg_alloc/proofs
Mar 01 11:18:36 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Mar 01 11:18:37 Starting compiler/backend/proofs
Mar 01 12:08:24 Finished compiler/backend/proofs                              49m47s  27GB
Mar 01 12:08:25 Starting compiler/backend/serialiser
Mar 01 12:09:57 Finished compiler/backend/serialiser                           1m32s   2GB
Mar 01 12:09:58 Starting compiler/encoders/x64/proofs
Mar 01 12:19:13 Finished compiler/encoders/x64/proofs                          9m15s   4GB
Mar 01 12:19:13 Starting compiler/encoders/arm7/proofs
Mar 01 12:31:54 Finished compiler/encoders/arm7/proofs                        12m40s   9GB
Mar 01 12:31:54 Starting compiler/encoders/arm8/proofs
Mar 01 12:38:23 Finished compiler/encoders/arm8/proofs                         6m29s   3GB
Mar 01 12:38:24 Starting compiler/encoders/arm8_asl/proofs
Mar 01 13:27:19 Finished compiler/encoders/arm8_asl/proofs                    48m54s   6GB
Mar 01 13:27:19 Starting compiler/encoders/mips/proofs
Mar 01 13:37:02 Finished compiler/encoders/mips/proofs                         9m42s   3GB
Mar 01 13:37:02 Starting compiler/encoders/riscv/proofs
Mar 01 13:45:19 Finished compiler/encoders/riscv/proofs                        8m16s   4GB
Mar 01 13:45:19 Starting compiler/encoders/ag32/proofs
Mar 01 13:47:40 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 01 13:47:41 Starting compiler/backend/x64/proofs
Mar 01 13:48:09 Finished compiler/backend/x64/proofs                             27s   2GB
Mar 01 13:48:09 Starting compiler/backend/arm7/proofs
Mar 01 13:48:38 Finished compiler/backend/arm7/proofs                            29s   2GB
Mar 01 13:48:38 Starting compiler/backend/arm8/proofs
Mar 01 13:49:06 Finished compiler/backend/arm8/proofs                            26s   1GB
Mar 01 13:49:06 Starting compiler/backend/arm8_asl
Mar 01 13:49:28 Finished compiler/backend/arm8_asl                               21s   2GB
Mar 01 13:49:28 Starting compiler/backend/mips/proofs
Mar 01 13:49:56 Finished compiler/backend/mips/proofs                            27s   1GB
Mar 01 13:49:56 Starting compiler/backend/riscv/proofs
Mar 01 13:50:25 Finished compiler/backend/riscv/proofs                           28s   2GB
Mar 01 13:50:25 Starting compiler/backend/ag32/proofs
Mar 01 14:02:22 Finished compiler/backend/ag32/proofs                         11m56s   4GB
Mar 01 14:02:22 Starting compiler/proofs
Mar 01 14:04:46 Finished compiler/proofs                                       2m23s   6GB
Mar 01 14:04:46 Starting candle/set-theory
Mar 01 14:05:22 Finished candle/set-theory                                       35s   1GB
Mar 01 14:05:22 Starting candle/syntax-lib
Mar 01 14:05:36 Finished candle/syntax-lib                                       13s 888MB
Mar 01 14:05:36 Starting candle/standard/syntax
Mar 01 14:07:40 Finished candle/standard/syntax                                2m04s   1GB
Mar 01 14:07:40 Starting candle/standard/semantics
Mar 01 14:09:31 Finished candle/standard/semantics                             1m50s   1GB
Mar 01 14:09:31 Starting candle/standard/monadic
Mar 01 14:11:22 Finished candle/standard/monadic                               1m51s   1GB
Mar 01 14:11:23 Starting candle/standard/ml_kernel
Mar 01 14:17:11 Finished candle/standard/ml_kernel                             5m48s   5GB
Mar 01 14:17:12 Starting candle/overloading/syntax
Mar 01 14:20:21 Finished candle/overloading/syntax                             3m08s   1GB
Mar 01 14:20:21 Starting candle/overloading/semantics
Mar 01 14:31:12 Finished candle/overloading/semantics                         10m50s   3GB
Mar 01 14:31:12 Starting candle/overloading/monadic
Mar 01 14:33:35 Finished candle/overloading/monadic                            2m23s   2GB
Mar 01 14:33:35 Starting candle/overloading/ml_kernel
Mar 01 14:40:18 Finished candle/overloading/ml_kernel                          6m42s   4GB
Mar 01 14:40:19 Starting candle/overloading/ml_checker
Mar 01 14:42:39 Finished candle/overloading/ml_checker                         2m19s   4GB
Mar 01 14:42:39 Starting candle/prover
Mar 01 14:50:08 Finished candle/prover                                         7m29s   4GB
Mar 01 14:50:09 Starting pancake
Mar 01 14:53:51 Finished pancake                                               3m41s   4GB
Mar 01 14:53:51 Starting pancake/ffi
Mar 01 14:53:51 Finished pancake/ffi                                              0s  35MB
Mar 01 14:53:51 Starting pancake/semantics
Mar 01 14:56:17 Finished pancake/semantics                                     2m25s   1GB
Mar 01 14:56:17 Starting pancake/proofs
Mar 01 15:07:41 Finished pancake/proofs                                       11m24s   7GB
Mar 01 15:07:42 Starting characteristic/examples
Mar 01 15:09:07 Finished characteristic/examples                               1m24s   4GB
Mar 01 15:09:07 Starting tutorial/solutions
Mar 01 15:25:40 Finished tutorial/solutions                                   16m32s  18GB
Mar 01 15:25:40 Starting translator/monadic/examples
Mar 01 15:29:42 Finished translator/monadic/examples                           4m01s   3GB
Mar 01 15:29:42 Starting examples
Mar 01 15:39:57 Finished examples                                             10m14s   5GB
Mar 01 15:39:57 Starting examples/compilation/x64
Mar 01 18:11:18 Finished examples/compilation/x64                           2h31m20s  25GB
Mar 01 18:11:18 Starting examples/compilation/x64/proofs
Mar 01 18:13:44 Finished examples/compilation/x64/proofs                       2m25s   4GB
Mar 01 18:13:44 Starting examples/compilation/ag32
Mar 01 18:48:53 Finished examples/compilation/ag32                            35m08s  15GB
Mar 01 18:48:53 Starting examples/compilation/ag32/proofs
Mar 01 18:49:54 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Mar 01 18:49:54 Starting examples/cost
Mar 01 19:46:31 Finished examples/cost                                        56m36s  13GB
Mar 01 19:46:31 Starting examples/lpr_checker
Mar 01 19:47:35 Finished examples/lpr_checker                                  1m03s   2GB
Mar 01 19:47:36 Starting examples/lpr_checker/array
Mar 01 20:15:07 Finished examples/lpr_checker/array                           27m31s  30GB
Mar 01 20:15:07 Starting examples/lpr_checker/array/compilation
Mar 01 21:44:15 Finished examples/lpr_checker/array/compilation             1h29m07s  57GB
Mar 01 21:44:15 Starting examples/lpr_checker/array/compilation/proofs
Mar 01 21:47:07 Finished examples/lpr_checker/array/compilation/proofs         2m51s   7GB
Mar 01 21:47:08 Starting examples/opentheory
Mar 01 22:04:33 Finished examples/opentheory                                  17m25s   7GB
Mar 01 22:04:33 Starting examples/opentheory
Mar 01 22:04:35 Finished examples/opentheory                                      1s 134MB
Mar 01 22:04:35 Starting examples/opentheory/compilation
Mar 01 22:45:26 Finished examples/opentheory/compilation                      40m50s  34GB
Mar 01 22:45:26 Starting examples/opentheory/compilation/proofs
Mar 01 22:46:24 Finished examples/opentheory/compilation/proofs                  58s   4GB
Mar 01 22:46:24 Starting examples/opentheory/compilation/ag32
Mar 01 23:25:23 Finished examples/opentheory/compilation/ag32                 38m58s  32GB
Mar 01 23:25:24 Starting examples/opentheory/compilation/ag32/proofs
Mar 01 23:27:08 Finished examples/opentheory/compilation/ag32/proofs           1m44s   7GB
Mar 01 23:27:08 Starting examples/sat_encodings
Mar 01 23:29:15 Finished examples/sat_encodings                                2m06s   1GB
Mar 01 23:29:15 Starting examples/sat_encodings/case_studies
Mar 01 23:30:59 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Mar 01 23:30:59 Starting examples/sat_encodings/translation
Mar 01 23:36:38 Finished examples/sat_encodings/translation                    5m38s   6GB
Mar 01 23:36:38 Starting examples/sat_encodings/translation/compilation
Mar 02 00:50:18 Finished examples/sat_encodings/translation/compilation     1h13m40s  20GB
Mar 02 00:50:19 Starting translator/okasaki-examples
Mar 02 00:59:12 Finished translator/okasaki-examples                           8m53s   3GB
Mar 02 00:59:12 Starting translator/other-examples
Mar 02 01:03:23 Finished translator/other-examples                             4m10s   1GB
Mar 02 01:03:23 Starting compiler/parsing/tests
Mar 02 01:04:20 Finished compiler/parsing/tests                                  56s 669MB
Mar 02 01:04:20 Starting compiler/inference/tests
Mar 02 01:17:55 Finished compiler/inference/tests                             13m34s   6GB
Mar 02 01:17:55 Starting compiler/printing/test
Mar 02 01:22:40 Finished compiler/printing/test                                4m45s   4GB
Mar 02 01:22:40 Starting compiler/repl
Mar 02 01:40:38 Finished compiler/repl                                        17m57s   8GB
Mar 02 01:40:38 Starting compiler/bootstrap/translation
Mar 02 02:35:17 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanned 88 directories
Starting work on precparserTheory
Starting work on monadic_encTheory
Starting work on caml_lexTheory
Starting work on README.md
README.md                                                                                                                                compiler/bootstrap/translation  (0s)     OK
Starting work on decProgTheory
precparserTheory                                                                                                                 examples/formal-languages/context-free  (1s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1]                                                                                                    (1.510s) 
monadic_encTheory                                                                                                                         compiler/encoders/monadic_enc (19s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                                                                                                                       compiler/encoders/monadic_enc (32s)     OK
monadic_enc32Theory                                                                                                                       compiler/encoders/monadic_enc (32s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]                                                                                                         (84.430s) 
decProgTheory                                                                                                                            compiler/bootstrap/translation(159s)     OK
Starting work on to_flatProgTheory
caml_lexTheory                                                                                                                                   compiler/parsing/ocaml(256s)     OK
Starting work on camlPEGTheory
camlPEGTheory                                                                                                                                    compiler/parsing/ocaml(109s)     OK
Starting work on camlPtreeConversionTheory
camlPtreeConversionTheory                                                                                                                        compiler/parsing/ocaml (45s)     OK
Starting work on caml_parserTheory
caml_parserTheory                                                                                                                                compiler/parsing/ocaml (13s)     OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4]                                                                                                               (425.530s) 
to_flatProgTheory                                                                                                                        compiler/bootstrap/translation(314s)     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                        compiler/bootstrap/translation(465s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                         compiler/bootstrap/translation(483s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                         compiler/bootstrap/translation(381s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                        compiler/bootstrap/translation(225s)     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                          compiler/bootstrap/translation(186s)     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                         compiler/bootstrap/translation(526s)     OK
Starting work on caml_lexProgTheory
caml_lexProgTheory                                                                                                                       compiler/bootstrap/translation(447s)     OK
Starting work on caml_parserProgTheory
caml_parserProgTheory                                                                                                                    compiler/bootstrap/translation (28s)FAIL<1>
 <<HOL warning: Theory.callhooks: Hook ThmSetData.onload.DefnBase.indn.parents failed on event TheoryLoaded(repl_decs_allowed) with problem 
 Exception raised at DefnBase.register_indn:
 Induction variable type of ivar P doesn't match that of constant generated_definition
 >>
 <<HOL warning: Theory.callhooks: Hook ThmSetData.onload.DefnBase.indn.parents failed on event TheoryLoaded(to_flatProg) with problem 
 Exception raised at DefnBase.register_indn:
 Induction variable type of ivar P doesn't match that of constant generated_definition
 >>
 Run out of store - interrupting threads
 Failed to recover - exiting