Job 1808

CakeML:8d70115b666585aaa40b992c5d29ae2ac3d5919c
  Stop at errors and interrupts in repl_boot.cml [Feb 27 15:37:25]
#863 (repl)
Merging into:d372405eb3f523c7e398bf05e90efc3e21e4e75c
  Get around a problem with DefnBase.one_line_ify [Feb 27 21:16:50]
HOL:707434f48dcd4d8f5d06ccae4cdc957b3fc7b4bd
  Tweak one_line_ify for case structures not quite aligning with eqns [Feb 26 00:33:01]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 28 07:18:56 Claimed job
Feb 28 07:19:12 Reusing HOL
Feb 28 07:19:21 Starting developers
Feb 28 07:19:24 Finished developers                                               2s 113MB
Feb 28 07:19:25 Starting developers/bin
Feb 28 07:20:27 Finished developers/bin                                        1m02s 675MB
Feb 28 07:20:27 Starting semantics/ffi
Feb 28 07:20:37 Finished semantics/ffi                                            9s 251MB
Feb 28 07:20:37 Starting semantics
Feb 28 07:22:40 Finished semantics                                             2m02s   1GB
Feb 28 07:22:40 Starting semantics/proofs
Feb 28 07:26:15 Finished semantics/proofs                                      3m35s   1GB
Feb 28 07:26:16 Starting semantics/alt_semantics
Feb 28 07:26:31 Finished semantics/alt_semantics                                 15s 501MB
Feb 28 07:26:32 Starting semantics/alt_semantics/proofs
Feb 28 07:28:53 Finished semantics/alt_semantics/proofs                        2m21s   1GB
Feb 28 07:28:53 Starting basis/pure
Feb 28 07:30:03 Finished basis/pure                                            1m10s   1GB
Feb 28 07:30:03 Starting translator
Feb 28 07:33:02 Finished translator                                            2m58s   2GB
Feb 28 07:33:03 Starting compiler/parsing
Feb 28 07:34:18 Finished compiler/parsing                                      1m15s   3GB
Feb 28 07:34:18 Starting characteristic
Feb 28 07:40:33 Finished characteristic                                        6m14s   2GB
Feb 28 07:40:33 Starting translator/monadic
Feb 28 07:42:36 Finished translator/monadic                                    2m02s   3GB
Feb 28 07:42:36 Starting basis
Feb 28 08:29:38 Finished basis                                                47m00s  29GB
Feb 28 08:29:38 Starting compiler/inference
Feb 28 08:30:59 Finished compiler/inference                                    1m20s   1GB
Feb 28 08:31:00 Starting compiler/backend/reg_alloc
Feb 28 08:32:40 Finished compiler/backend/reg_alloc                            1m40s   2GB
Feb 28 08:32:40 Starting compiler/backend/gc
Feb 28 08:37:00 Finished compiler/backend/gc                                   4m19s   3GB
Feb 28 08:37:00 Starting compiler/backend
Feb 28 08:42:53 Finished compiler/backend                                      5m53s   3GB
Feb 28 08:42:54 Starting compiler/encoders/asm
Feb 28 08:43:24 Finished compiler/encoders/asm                                   30s   1GB
Feb 28 08:43:25 Starting compiler/encoders/x64
Feb 28 08:43:56 Finished compiler/encoders/x64                                   30s   1GB
Feb 28 08:43:56 Starting compiler/encoders/arm7
Feb 28 08:44:50 Finished compiler/encoders/arm7                                  54s   1GB
Feb 28 08:44:51 Starting compiler/encoders/arm8
Feb 28 08:45:08 Finished compiler/encoders/arm8                                  17s   1GB
Feb 28 08:45:08 Starting compiler/encoders/arm8_asl
Feb 28 08:47:44 Finished compiler/encoders/arm8_asl                            2m35s   1GB
Feb 28 08:47:44 Starting compiler/encoders/mips
Feb 28 08:48:05 Finished compiler/encoders/mips                                  20s   1GB
Feb 28 08:48:06 Starting compiler/encoders/riscv
Feb 28 08:48:26 Finished compiler/encoders/riscv                                 19s   1GB
Feb 28 08:48:26 Starting compiler/encoders/ag32
Feb 28 08:48:49 Finished compiler/encoders/ag32                                  23s   1GB
Feb 28 08:48:50 Starting compiler/backend/x64
Feb 28 08:49:12 Finished compiler/backend/x64                                    22s   1GB
Feb 28 08:49:12 Starting compiler/backend/arm7
Feb 28 08:49:35 Finished compiler/backend/arm7                                   22s   1GB
Feb 28 08:49:35 Starting compiler/backend/arm8
Feb 28 08:49:58 Finished compiler/backend/arm8                                   22s   1GB
Feb 28 08:49:58 Starting compiler/backend/mips
Feb 28 08:50:21 Finished compiler/backend/mips                                   22s   1GB
Feb 28 08:50:21 Starting compiler/backend/riscv
Feb 28 08:50:45 Finished compiler/backend/riscv                                  24s   1GB
Feb 28 08:50:46 Starting compiler/backend/ag32
Feb 28 08:52:08 Finished compiler/backend/ag32                                 1m22s   2GB
Feb 28 08:52:08 Starting compiler/parsing/proofs
Feb 28 08:54:48 Finished compiler/parsing/proofs                               2m39s   1GB
Feb 28 08:54:48 Starting compiler/inference/proofs
Feb 28 08:57:15 Finished compiler/inference/proofs                             2m26s   1GB
Feb 28 08:57:15 Starting compiler/backend/semantics
Feb 28 09:24:57 Finished compiler/backend/semantics                           27m41s   3GB
Feb 28 09:24:57 Starting compiler/backend/reg_alloc/proofs
Feb 28 09:28:16 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Feb 28 09:28:16 Starting compiler/backend/proofs
Feb 28 10:23:35 Finished compiler/backend/proofs                              55m18s  19GB
Feb 28 10:23:35 Starting compiler/backend/serialiser
Feb 28 10:25:20 Finished compiler/backend/serialiser                           1m44s   2GB
Feb 28 10:25:21 Starting compiler/encoders/x64/proofs
Feb 28 10:35:45 Finished compiler/encoders/x64/proofs                         10m24s   4GB
Feb 28 10:35:45 Starting compiler/encoders/arm7/proofs
Feb 28 10:49:43 Finished compiler/encoders/arm7/proofs                        13m57s   6GB
Feb 28 10:49:43 Starting compiler/encoders/arm8/proofs
Feb 28 10:56:58 Finished compiler/encoders/arm8/proofs                         7m14s   3GB
Feb 28 10:56:58 Starting compiler/encoders/arm8_asl/proofs
Feb 28 11:12:15 Finished compiler/encoders/arm8_asl/proofs                    15m17s   3GB
Feb 28 11:12:15 Starting compiler/encoders/mips/proofs
Feb 28 11:22:25 Finished compiler/encoders/mips/proofs                        10m09s   3GB
Feb 28 11:22:25 Starting compiler/encoders/riscv/proofs
Feb 28 11:31:25 Finished compiler/encoders/riscv/proofs                        8m59s   4GB
Feb 28 11:31:25 Starting compiler/encoders/ag32/proofs
Feb 28 11:34:13 Finished compiler/encoders/ag32/proofs                         2m47s   2GB
Feb 28 11:34:13 Starting compiler/backend/x64/proofs
Feb 28 11:34:42 Finished compiler/backend/x64/proofs                             29s   1GB
Feb 28 11:34:42 Starting compiler/backend/arm7/proofs
Feb 28 11:35:12 Finished compiler/backend/arm7/proofs                            29s   1GB
Feb 28 11:35:12 Starting compiler/backend/arm8/proofs
Feb 28 11:35:39 Finished compiler/backend/arm8/proofs                            26s   1GB
Feb 28 11:35:39 Starting compiler/backend/arm8_asl
Feb 28 11:36:02 Finished compiler/backend/arm8_asl                               22s   2GB
Feb 28 11:36:02 Starting compiler/backend/mips/proofs
Feb 28 11:36:31 Finished compiler/backend/mips/proofs                            28s   1GB
Feb 28 11:36:31 Starting compiler/backend/riscv/proofs
Feb 28 11:37:02 Finished compiler/backend/riscv/proofs                           30s   2GB
Feb 28 11:37:02 Starting compiler/backend/ag32/proofs
Feb 28 11:49:42 Finished compiler/backend/ag32/proofs                         12m37s   3GB
Feb 28 11:49:42 Starting compiler/proofs
Feb 28 11:51:50 Finished compiler/proofs                                       2m07s   6GB
Feb 28 11:51:50 Starting candle/set-theory
Feb 28 11:52:26 Finished candle/set-theory                                       35s   1GB
Feb 28 11:52:26 Starting candle/syntax-lib
Feb 28 11:52:40 Finished candle/syntax-lib                                       13s 859MB
Feb 28 11:52:40 Starting candle/standard/syntax
Feb 28 11:54:46 Finished candle/standard/syntax                                2m04s   1GB
Feb 28 11:54:46 Starting candle/standard/semantics
Feb 28 11:56:34 Finished candle/standard/semantics                             1m48s   1GB
Feb 28 11:56:34 Starting candle/standard/monadic
Feb 28 11:58:25 Finished candle/standard/monadic                               1m50s   2GB
Feb 28 11:58:25 Starting candle/standard/ml_kernel
Feb 28 12:04:16 Finished candle/standard/ml_kernel                             5m50s   5GB
Feb 28 12:04:16 Starting candle/overloading/syntax
Feb 28 12:07:25 Finished candle/overloading/syntax                             3m08s   1GB
Feb 28 12:07:25 Starting candle/overloading/semantics
Feb 28 12:18:10 Finished candle/overloading/semantics                         10m44s   4GB
Feb 28 12:18:10 Starting candle/overloading/monadic
Feb 28 12:20:32 Finished candle/overloading/monadic                            2m21s   2GB
Feb 28 12:20:32 Starting candle/overloading/ml_kernel
Feb 28 12:27:23 Finished candle/overloading/ml_kernel                          6m50s   7GB
Feb 28 12:27:23 Starting candle/overloading/ml_checker
Feb 28 12:29:49 Finished candle/overloading/ml_checker                         2m25s   5GB
Feb 28 12:29:49 Starting candle/prover
Feb 28 12:37:31 Finished candle/prover                                         7m42s   4GB
Feb 28 12:37:32 Starting pancake
Feb 28 12:40:22 Finished pancake                                               2m49s   3GB
Feb 28 12:40:22 Starting pancake/ffi
Feb 28 12:40:22 Finished pancake/ffi                                              0s  35MB
Feb 28 12:40:22 Starting pancake/semantics
Feb 28 12:43:15 Finished pancake/semantics                                     2m52s   1GB
Feb 28 12:43:16 Starting pancake/proofs
Feb 28 12:54:39 Finished pancake/proofs                                       11m23s   9GB
Feb 28 12:54:39 Starting characteristic/examples
Feb 28 12:56:04 Finished characteristic/examples                               1m24s   4GB
Feb 28 12:56:04 Starting tutorial/solutions
Feb 28 13:13:30 Finished tutorial/solutions                                   17m25s  12GB
Feb 28 13:13:30 Starting translator/monadic/examples
Feb 28 13:17:33 Finished translator/monadic/examples                           4m02s   4GB
Feb 28 13:17:33 Starting examples
Feb 28 13:27:51 Finished examples                                             10m18s   5GB
Feb 28 13:27:52 Starting examples/compilation/x64
Feb 28 16:00:37 Finished examples/compilation/x64                           2h32m44s  27GB
Feb 28 16:00:37 Starting examples/compilation/x64/proofs
Feb 28 16:03:03 Finished examples/compilation/x64/proofs                       2m25s   4GB
Feb 28 16:03:03 Starting examples/compilation/ag32
Feb 28 16:38:22 Finished examples/compilation/ag32                            35m18s  15GB
Feb 28 16:38:22 Starting examples/compilation/ag32/proofs
Feb 28 16:39:20 Finished examples/compilation/ag32/proofs                        57s   5GB
Feb 28 16:39:20 Starting examples/cost
Feb 28 17:36:39 Finished examples/cost                                        57m18s  12GB
Feb 28 17:36:40 Starting examples/lpr_checker
Feb 28 17:37:43 Finished examples/lpr_checker                                  1m03s   2GB
Feb 28 17:37:43 Starting examples/lpr_checker/array
Feb 28 18:04:58 Finished examples/lpr_checker/array                           27m14s  15GB
Feb 28 18:04:58 Starting examples/lpr_checker/array/compilation
Feb 28 19:32:57 Finished examples/lpr_checker/array/compilation             1h27m56s  50GB
Feb 28 19:32:57 Starting examples/lpr_checker/array/compilation/proofs
Feb 28 19:34:22 Finished examples/lpr_checker/array/compilation/proofs         1m24s   7GB
Feb 28 19:34:22 Starting examples/opentheory
Feb 28 19:43:55 Finished examples/opentheory                                   9m33s   7GB
Feb 28 19:43:56 Starting examples/opentheory
Feb 28 19:43:57 Finished examples/opentheory                                      1s 134MB
Feb 28 19:43:57 Starting examples/opentheory/compilation
Feb 28 20:24:34 Finished examples/opentheory/compilation                      40m37s  43GB
Feb 28 20:24:34 Starting examples/opentheory/compilation/proofs
Feb 28 20:25:32 Finished examples/opentheory/compilation/proofs                  57s   4GB
Feb 28 20:25:32 Starting examples/opentheory/compilation/ag32
Feb 28 21:03:55 Finished examples/opentheory/compilation/ag32                 38m22s  31GB
Feb 28 21:03:55 Starting examples/opentheory/compilation/ag32/proofs
Feb 28 21:05:40 Finished examples/opentheory/compilation/ag32/proofs           1m44s   7GB
Feb 28 21:05:40 Starting examples/sat_encodings
Feb 28 21:07:44 Finished examples/sat_encodings                                2m04s   1GB
Feb 28 21:07:45 Starting examples/sat_encodings/case_studies
Feb 28 21:09:29 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Feb 28 21:09:29 Starting examples/sat_encodings/translation
Feb 28 21:15:12 Finished examples/sat_encodings/translation                    5m42s   6GB
Feb 28 21:15:13 Starting examples/sat_encodings/translation/compilation
Feb 28 22:30:40 Finished examples/sat_encodings/translation/compilation     1h15m25s  31GB
Feb 28 22:30:41 Starting translator/okasaki-examples
Feb 28 22:35:19 Finished translator/okasaki-examples                           4m37s   3GB
Feb 28 22:35:19 Starting translator/other-examples
Feb 28 22:36:55 FAILED: translator/other-examples
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/examples/Crypto/AES[0m
Scanning [1m$(HOLDIR)/examples/Crypto/RC6[0m
Scanning [1m$(HOLDIR)/src/TeX[0m
Scanning [1m$(HOLDIR)/src/bag[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)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/emit[0m
Scanning [1m$(HOLDIR)/examples/Crypto/TEA[0m
Scanning [1m$(HOLDIR)/examples/Crypto/RSA[0m
Scanning [1m$(HOLDIR)/examples/miller/ho_prover[0m
Scanning [1m$(HOLDIR)/examples/miller/subtypes[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/examples/miller/formalize[0m
Scanning [1m$(HOLDIR)/examples/miller/groups[0m
Scanning [1m$(HOLDIR)/src/probability[0m
Scanning [1m$(HOLDIR)/examples/miller/prob[0m
Scanning [1m$(HOLDIR)/examples/miller/miller[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)/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)/translator/other-examples/auxiliary[0m
Scanned 48 directories
Starting work on MultTheory
Starting work on tablesTheory
Starting work on RC6Theory
Starting work on teaTheory
tablesTheory                                                                                                                                        examples/Crypto/AES  (5s)     OK
Starting work on powerTheory
powerTheory                                                                                                                                         examples/Crypto/RSA  (0s)     OK
Starting work on summationTheory
summationTheory                                                                                                                                     examples/Crypto/RSA  (0s)     OK
Starting work on binomialTheory
binomialTheory                                                                                                                                      examples/Crypto/RSA  (0s)     OK
Finished $(HOLDIR)/examples/Crypto/RSA [#theories: 3]                                                                                                                       (1.130s) 
Starting work on skiTheory
teaTheory                                                                                                                                           examples/Crypto/TEA  (6s)     OK
Finished $(HOLDIR)/examples/Crypto/TEA [#theories: 1]                                                                                                                       (6.960s) 
Starting work on extra_boolTheory
extra_boolTheory                                                                                                                              examples/miller/formalize  (0s)     OK
Starting work on copying_gcTheory
skiTheory                                                                                                                                     examples/miller/ho_prover  (0s)     OK
Finished $(HOLDIR)/examples/miller/ho_prover [#theories: 1]                                                                                                                 (0.850s) 
Starting work on subtypeTheory
RC6Theory                                                                                                                                           examples/Crypto/RC6  (8s)     OK
Finished $(HOLDIR)/examples/Crypto/RC6 [#theories: 1]                                                                                                                       (8.970s) 
Starting work on ninetyOneTheory
subtypeTheory                                                                                                                                  examples/miller/subtypes  (1s)     OK
Finished $(HOLDIR)/examples/miller/subtypes [#theories: 1]                                                                                                                  (1.850s) 
Starting work on extra_numTheory
copying_gcTheory                                                                                                                    translator/other-examples/auxiliary  (2s)     OK
Starting work on regexpMatchTheory
MultTheory                                                                                                                                          examples/Crypto/AES (10s)     OK
Starting work on RoundOpTheory
ninetyOneTheory                                                                                                                     translator/other-examples/auxiliary  (1s)     OK
Starting work on slr_parser_genTheory
extra_numTheory                                                                                                                               examples/miller/formalize  (1s)     OK
Starting work on extra_listTheory
extra_listTheory                                                                                                                              examples/miller/formalize  (1s)     OK
Starting work on extra_pred_setTheory
slr_parser_genTheory                                                                                                                translator/other-examples/auxiliary  (3s)     OK
Starting work on sequenceTheory
regexpMatchTheory                                                                                                                   translator/other-examples/auxiliary  (5s)     OK
Starting work on extra_arithTheory
sequenceTheory                                                                                                                                examples/miller/formalize  (1s)     OK
Starting work on prob_canonTheory
extra_pred_setTheory                                                                                                                          examples/miller/formalize  (4s)     OK
Starting work on extra_realTheory
prob_canonTheory                                                                                                                                   examples/miller/prob  (7s)     OK
Starting work on orderTheory
extra_realTheory                                                                                                                              examples/miller/formalize  (6s)     OK
Starting work on prob_algebraTheory
extra_arithTheory                                                                                                                                examples/miller/groups  (8s)     OK
Starting work on groupTheory
orderTheory                                                                                                                                   examples/miller/formalize  (3s)     OK
Finished $(HOLDIR)/examples/miller/formalize [#theories: 7]                                                                                                                (20.600s) 
Starting work on extra_binomialTheory
extra_binomialTheory                                                                                                                             examples/miller/groups  (3s)     OK
Finished $(CAKEMLDIR)/translator/other-examples/auxiliary [#theories: 4]                                                                                                   (13.300s) 
Starting work on README.md
README.md                                                                                                                                     translator/other-examples  (0s)     OK
Starting work on example_91Theory
groupTheory                                                                                                                                      examples/miller/groups  (8s)     OK
Starting work on finite_groupTheory
prob_algebraTheory                                                                                                                                 examples/miller/prob (11s)     OK
Starting work on probTheory
finite_groupTheory                                                                                                                               examples/miller/groups  (7s)     OK
Starting work on abelian_groupTheory
abelian_groupTheory                                                                                                                              examples/miller/groups  (4s)     OK
Starting work on num_polyTheory
example_91Theory                                                                                                                              translator/other-examples (15s)     OK
Starting work on example_balanced_bstTheory
RoundOpTheory                                                                                                                                       examples/Crypto/AES (40s)     OK
Starting work on aesTheory
num_polyTheory                                                                                                                                   examples/miller/groups  (6s)     OK
Starting work on mult_groupTheory
probTheory                                                                                                                                         examples/miller/prob (16s)     OK
Starting work on prob_uniformTheory
aesTheory                                                                                                                                           examples/Crypto/AES  (6s)     OK
Finished $(HOLDIR)/examples/Crypto/AES [#theories: 4]                                                                                                                      (61.880s) 
Starting work on example_copying_gcTheory
prob_uniformTheory                                                                                                                                 examples/miller/prob  (7s)     OK
Finished $(HOLDIR)/examples/miller/prob [#theories: 4]                                                                                                                     (42.220s) 
Starting work on example_parser_genTheory
mult_groupTheory                                                                                                                                 examples/miller/groups (19s)     OK
Finished $(HOLDIR)/examples/miller/groups [#theories: 7]                                                                                                                   (58.560s) 
Starting work on miller_rabinTheory
example_balanced_bstTheory                                                                                                                    translator/other-examples (23s)     OK
Starting work on example_qsortTheory
example_copying_gcTheory                                                                                                                      translator/other-examples (24s)     OK
Starting work on example_regexp_matcherTheory
miller_rabinTheory                                                                                                                               examples/miller/miller (16s)     OK
Finished $(HOLDIR)/examples/miller/miller [#theories: 1]                                                                                                                   (16.600s) 
Starting work on example_primality_testTheory
example_qsortTheory                                                                                                                           translator/other-examples (16s)     OK
example_parser_genTheory                                                                                                                      translator/other-examples (29s)FAIL<1>
   invalidated by NewBinding(SLR_PARSER_GEN_ACTION_TYPE_def)>>
 Saved theorem _______ "SLR_PARSER_GEN_ACTION_TYPE_def"
 Attempting proof of: EqualityType SLR_PARSER_GEN_ACTION_TYPE
 .. done EqualityType proof.
 Adding type :action.
 Saved theorem _______ "nsLookup_example_parser_gen_env_18_pfun_eqs"
 Failed translation: getState
 error in quse /home/myreen/regression/cakeml-1808/translator/other-examples/example_parser_genScript.sml : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 error in load /home/myreen/regression/cakeml-1808/translator/other-examples/example_parser_genScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
example_regexp_matcherTheory                                                                                                                  translator/other-examples (10s)MKILLED
example_primality_testTheory                                                                                                                  translator/other-examples  (2s)MKILLED