Job 1807

CakeML:f99af5a3ce396207686cb57a9c71820469fbc64c
  fix the broken proofs [Feb 25 03:30:48]
#861 (pan-to-mc_updated)
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:oven3+4.19.67.1.amd64-smp+

Feb 27 21:31:04 Claimed job
Feb 27 21:31:06 Reusing+HOL
Feb 27 21:31:59 Starting+developers
Feb 27 21:32:07 Finished+developers++++++++++++++++++++++++++++++++++++++++8.15+148040
Feb 27 21:32:07 Starting+developers/bin
Feb 27 21:32:17 Finished+developers/bin++++++++++++++++++++++++++++++++++++9.79+683312
Feb 27 21:32:18 Starting+semantics/ffi
Feb 27 21:32:41 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++23.19+247396
Feb 27 21:32:41 Starting+semantics
Feb 27 21:36:53 Finished+semantics+++++++++++++++++++++++++++++++++++++++++250.94+1523280
Feb 27 21:36:53 Starting+semantics/proofs
Feb 27 21:44:55 Finished+semantics/proofs++++++++++++++++++++++++++++++++++482.39+1389084
Feb 27 21:44:56 Starting+semantics/alt_semantics
Feb 27 21:45:32 Finished+semantics/alt_semantics+++++++++++++++++++++++++++36.60+540944
Feb 27 21:45:33 Starting+semantics/alt_semantics/proofs
Feb 27 21:51:01 Finished+semantics/alt_semantics/proofs++++++++++++++++++++327.94+1389724
Feb 27 21:51:01 Starting+basis/pure
Feb 27 21:53:10 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++128.88+1222352
Feb 27 21:53:10 Starting+translator
Feb 27 21:59:29 Finished+translator++++++++++++++++++++++++++++++++++++++++379.04+1499648
Feb 27 21:59:29 Starting+compiler/parsing
Feb 27 22:02:15 Finished+compiler/parsing++++++++++++++++++++++++++++++++++165.21+3147804
Feb 27 22:02:15 Starting+characteristic
Feb 27 22:15:39 Finished+characteristic++++++++++++++++++++++++++++++++++++803.83+2261748
Feb 27 22:15:39 Starting+translator/monadic
Feb 27 22:19:48 Finished+translator/monadic++++++++++++++++++++++++++++++++248.37+1414916
Feb 27 22:19:48 Starting+basis
Feb 28 00:02:15 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6146.39+20659324
Feb 28 00:02:15 Starting+compiler/inference
Feb 28 00:05:03 Finished+compiler/inference++++++++++++++++++++++++++++++++167.57+1559664
Feb 28 00:05:03 Starting+compiler/backend/reg_alloc
Feb 28 00:08:14 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++190.70+1903512
Feb 28 00:08:14 Starting+compiler/backend/gc
Feb 28 00:16:30 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++495.58+2100040
Feb 28 00:16:30 Starting+compiler/backend
Feb 28 00:27:11 Finished+compiler/backend++++++++++++++++++++++++++++++++++641.16+2724056
Feb 28 00:27:11 Starting+compiler/encoders/asm
Feb 28 00:28:17 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++64.96+922128
Feb 28 00:28:17 Starting+compiler/encoders/x64
Feb 28 00:29:22 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++65.13+896576
Feb 28 00:29:22 Starting+compiler/encoders/arm7
Feb 28 00:32:18 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++175.65+741608
Feb 28 00:32:18 Starting+compiler/encoders/arm8
Feb 28 00:32:55 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++36.05+1087828
Feb 28 00:32:55 Starting+compiler/encoders/arm8_asl
Feb 28 00:40:01 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++426.02+1005180
Feb 28 00:40:01 Starting+compiler/encoders/mips
Feb 28 00:40:48 Finished+compiler/encoders/mips++++++++++++++++++++++++++++46.75+1093508
Feb 28 00:40:48 Starting+compiler/encoders/riscv
Feb 28 00:41:29 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++40.04+802596
Feb 28 00:41:29 Starting+compiler/encoders/ag32
Feb 28 00:42:16 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++46.88+747088
Feb 28 00:42:16 Starting+compiler/backend/x64
Feb 28 00:42:58 Finished+compiler/backend/x64++++++++++++++++++++++++++++++41.76+1228460
Feb 28 00:42:58 Starting+compiler/backend/arm7
Feb 28 00:43:50 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++51.82+1670708
Feb 28 00:43:50 Starting+compiler/backend/arm8
Feb 28 00:44:39 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++48.72+1444244
Feb 28 00:44:40 Starting+compiler/backend/mips
Feb 28 00:45:29 Finished+compiler/backend/mips+++++++++++++++++++++++++++++49.10+1457836
Feb 28 00:45:29 Starting+compiler/backend/riscv
Feb 28 00:46:17 Finished+compiler/backend/riscv++++++++++++++++++++++++++++47.71+1451288
Feb 28 00:46:17 Starting+compiler/backend/ag32
Feb 28 00:49:14 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++176.15+1598040
Feb 28 00:49:14 Starting+compiler/parsing/proofs
Feb 28 00:57:44 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++509.75+1215100
Feb 28 00:57:44 Starting+compiler/inference/proofs
Feb 28 01:03:13 Finished+compiler/inference/proofs+++++++++++++++++++++++++327.89+1038684
Feb 28 01:03:13 Starting+compiler/backend/semantics
Feb 28 02:05:51 Finished+compiler/backend/semantics++++++++++++++++++++++++3757.21+2973052
Feb 28 02:05:51 Starting+compiler/backend/reg_alloc/proofs
Feb 28 02:13:42 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++471.17+1405556
Feb 28 02:13:42 Starting+compiler/backend/proofs
Feb 28 03:57:09 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6206.62+13142584
Feb 28 03:57:10 Starting+compiler/backend/serialiser
Feb 28 04:00:31 Finished+compiler/backend/serialiser+++++++++++++++++++++++200.79+2010788
Feb 28 04:00:31 Starting+compiler/encoders/x64/proofs
Feb 28 04:22:01 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1290.26+4535708
Feb 28 04:22:02 Starting+compiler/encoders/arm7/proofs
Feb 28 04:51:19 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1757.48+3195676
Feb 28 04:51:20 Starting+compiler/encoders/arm8/proofs
Feb 28 05:06:36 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++915.67+1749856
Feb 28 05:06:36 Starting+compiler/encoders/arm8_asl/proofs
Feb 28 05:42:01 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++2124.96+2135152
Feb 28 05:42:01 Starting+compiler/encoders/mips/proofs
Feb 28 06:05:03 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1381.95+2263368
Feb 28 06:05:04 Starting+compiler/encoders/riscv/proofs
Feb 28 06:25:16 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1212.25+1316364
Feb 28 06:25:16 Starting+compiler/encoders/ag32/proofs
Feb 28 06:31:03 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++346.04+833024
Feb 28 06:31:03 Starting+compiler/backend/x64/proofs
Feb 28 06:32:02 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++59.52+1717280
Feb 28 06:32:03 Starting+compiler/backend/arm7/proofs
Feb 28 06:33:01 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++58.40+1152912
Feb 28 06:33:01 Starting+compiler/backend/arm8/proofs
Feb 28 06:34:01 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++58.89+1514332
Feb 28 06:34:01 Starting+compiler/backend/arm8_asl
Feb 28 06:34:49 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++48.48+1153308
Feb 28 06:34:50 Starting+compiler/backend/mips/proofs
Feb 28 06:35:51 Finished+compiler/backend/mips/proofs++++++++++++++++++++++60.97+1686348
Feb 28 06:35:51 Starting+compiler/backend/riscv/proofs
Feb 28 06:36:52 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++60.61+1744532
Feb 28 06:36:52 Starting+compiler/backend/ag32/proofs
Feb 28 07:05:12 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1699.75+2692632
Feb 28 07:05:12 Starting+compiler/proofs
Feb 28 07:09:40 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++267.11+3091156
Feb 28 07:09:40 Starting+candle/set-theory
Feb 28 07:10:49 Finished+candle/set-theory+++++++++++++++++++++++++++++++++68.86+950436
Feb 28 07:10:49 Starting+candle/syntax-lib
Feb 28 07:11:17 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++27.63+739372
Feb 28 07:11:17 Starting+candle/standard/syntax
Feb 28 07:15:41 Finished+candle/standard/syntax++++++++++++++++++++++++++++263.83+1294504
Feb 28 07:15:42 Starting+candle/standard/semantics
Feb 28 07:19:42 Finished+candle/standard/semantics+++++++++++++++++++++++++240.69+1380844
Feb 28 07:19:43 Starting+candle/standard/monadic
Feb 28 07:23:38 Finished+candle/standard/monadic+++++++++++++++++++++++++++235.34+1832380
Feb 28 07:23:38 Starting+candle/standard/ml_kernel
Feb 28 07:36:43 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++784.50+3949240
Feb 28 07:36:43 Starting+candle/overloading/syntax
Feb 28 07:43:35 Finished+candle/overloading/syntax+++++++++++++++++++++++++410.96+1352704
Feb 28 07:43:35 Starting+candle/overloading/semantics
Feb 28 08:09:37 Finished+candle/overloading/semantics++++++++++++++++++++++1561.74+2908276
Feb 28 08:09:37 Starting+candle/overloading/monadic
Feb 28 08:15:06 Finished+candle/overloading/monadic++++++++++++++++++++++++328.75+1905956
Feb 28 08:15:06 Starting+candle/overloading/ml_kernel
Feb 28 08:30:05 Finished+candle/overloading/ml_kernel++++++++++++++++++++++898.47+3198124
Feb 28 08:30:05 Starting+candle/overloading/ml_checker
Feb 28 08:35:28 Finished+candle/overloading/ml_checker+++++++++++++++++++++323.09+3568908
Feb 28 08:35:28 Starting+candle/prover
Feb 28 08:52:57 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1047.93+3682776
Feb 28 08:52:57 Starting+pancake
Feb 28 09:00:42 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++464.79+3085636
Feb 28 09:00:42 Starting+pancake/ffi
Feb 28 09:00:43 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.77+32072
Feb 28 09:00:43 Starting+pancake/semantics
Feb 28 09:06:03 Finished+pancake/semantics+++++++++++++++++++++++++++++++++319.61+1049176
Feb 28 09:06:03 Starting+pancake/proofs
Feb 28 09:32:44 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1600.34+6647104
Feb 28 09:32:44 Starting+characteristic/examples
Feb 28 09:35:36 Finished+characteristic/examples+++++++++++++++++++++++++++172.10+3098248
Feb 28 09:35:36 Starting+tutorial/solutions
Feb 28 10:11:10 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2133.37+9248420
Feb 28 10:11:10 Starting+translator/monadic/examples
Feb 28 10:18:04 Finished+translator/monadic/examples+++++++++++++++++++++++413.11+3409184
Feb 28 10:18:04 Starting+examples
Feb 28 10:36:30 Finished+examples++++++++++++++++++++++++++++++++++++++++++1105.90+3784104
Feb 28 10:36:30 Starting+examples/compilation/x64
Feb 28 16:07:12 Finished+examples/compilation/x64++++++++++++++++++++++++++19840.74+18286808
Feb 28 16:07:12 Starting+examples/compilation/x64/proofs
Feb 28 16:12:30 Finished+examples/compilation/x64/proofs+++++++++++++++++++317.74+3648364
Feb 28 16:12:30 Starting+examples/compilation/ag32
Feb 28 17:30:18 Finished+examples/compilation/ag32+++++++++++++++++++++++++4666.74+8108056
Feb 28 17:30:18 Starting+examples/compilation/ag32/proofs
Feb 28 17:32:15 Finished+examples/compilation/ag32/proofs++++++++++++++++++117.23+4360580
Feb 28 17:32:15 Starting+examples/cost
Feb 28 19:31:31 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7155.50+9154428
Feb 28 19:31:31 Starting+examples/lpr_checker
Feb 28 19:33:38 Finished+examples/lpr_checker++++++++++++++++++++++++++++++126.56+1695824
Feb 28 19:33:38 Starting+examples/lpr_checker/array
Feb 28 20:37:06 Finished+examples/lpr_checker/array++++++++++++++++++++++++3806.88+6466004
Feb 28 20:37:06 Starting+examples/lpr_checker/array/compilation
Feb 28 23:43:39 Finished+examples/lpr_checker/array/compilation++++++++++++11193.22+38095344
Feb 28 23:43:40 Starting+examples/lpr_checker/array/compilation/proofs
Feb 28 23:46:42 Finished+examples/lpr_checker/array/compilation/proofs+++++182.45+8004672
Feb 28 23:46:42 Starting+examples/opentheory
Mar 01 00:07:55 Finished+examples/opentheory+++++++++++++++++++++++++++++++1272.65+6549172
Mar 01 00:07:56 Starting+examples/opentheory
Mar 01 00:07:59 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.83+34464
Mar 01 00:07:59 Starting+examples/opentheory/compilation
Mar 01 01:40:06 Finished+examples/opentheory/compilation+++++++++++++++++++5526.09+43726808
Mar 01 01:40:06 Starting+examples/opentheory/compilation/proofs
Mar 01 01:42:04 Finished+examples/opentheory/compilation/proofs++++++++++++117.59+4716308
Mar 01 01:42:04 Starting+examples/opentheory/compilation/ag32
Mar 01 03:14:14 Finished+examples/opentheory/compilation/ag32++++++++++++++5529.89+46478900
Mar 01 03:14:14 Starting+examples/opentheory/compilation/ag32/proofs
Mar 01 03:18:05 Finished+examples/opentheory/compilation/ag32/proofs+++++++230.36+6972592
Mar 01 03:18:05 Starting+examples/sat_encodings
Mar 01 03:22:25 Finished+examples/sat_encodings++++++++++++++++++++++++++++259.77+1054360
Mar 01 03:22:25 Starting+examples/sat_encodings/case_studies
Mar 01 03:26:02 Finished+examples/sat_encodings/case_studies+++++++++++++++216.64+1260596
Mar 01 03:26:02 Starting+examples/sat_encodings/translation
Mar 01 03:38:02 Finished+examples/sat_encodings/translation++++++++++++++++719.90+3741604
Mar 01 03:38:03 Starting+examples/sat_encodings/translation/compilation
Mar 01 05:04:21 Finished+examples/sat_encodings/translation/compilation++++5178.02+25671700
Mar 01 05:04:21 Starting+translator/okasaki-examples
Mar 01 05:14:16 Finished+translator/okasaki-examples+++++++++++++++++++++++594.97+1865488
Mar 01 05:14:17 Starting+translator/other-examples
Mar 01 05:17:16 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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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  (9s)     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  (1s)     OK
Finished $(HOLDIR)/examples/Crypto/RSA [#theories: 3]                                                                                                                                                    (2.210s) 
Starting work on skiTheory
teaTheory                                                                                                                                                                        examples/Crypto/TEA (14s)     OK
Finished $(HOLDIR)/examples/Crypto/TEA [#theories: 1]                                                                                                                                                   (14.357s) 
Starting work on extra_boolTheory
skiTheory                                                                                                                                                                  examples/miller/ho_prover  (1s)     OK
Finished $(HOLDIR)/examples/miller/ho_prover [#theories: 1]                                                                                                                                              (1.404s) 
Starting work on subtypeTheory
extra_boolTheory                                                                                                                                                           examples/miller/formalize  (0s)     OK
Starting work on copying_gcTheory
RC6Theory                                                                                                                                                                        examples/Crypto/RC6 (17s)     OK
Finished $(HOLDIR)/examples/Crypto/RC6 [#theories: 1]                                                                                                                                                   (17.620s) 
Starting work on ninetyOneTheory
MultTheory                                                                                                                                                                       examples/Crypto/AES (18s)     OK
Starting work on RoundOpTheory
subtypeTheory                                                                                                                                                               examples/miller/subtypes  (3s)     OK
Finished $(HOLDIR)/examples/miller/subtypes [#theories: 1]                                                                                                                                               (3.571s) 
Starting work on extra_numTheory
copying_gcTheory                                                                                                                                                 translator/other-examples/auxiliary  (4s)     OK
Starting work on regexpMatchTheory
ninetyOneTheory                                                                                                                                                  translator/other-examples/auxiliary  (3s)     OK
Starting work on slr_parser_genTheory
extra_numTheory                                                                                                                                                            examples/miller/formalize  (3s)     OK
Starting work on extra_listTheory
extra_listTheory                                                                                                                                                           examples/miller/formalize  (3s)     OK
Starting work on extra_pred_setTheory
slr_parser_genTheory                                                                                                                                             translator/other-examples/auxiliary  (8s)     OK
Starting work on sequenceTheory
regexpMatchTheory                                                                                                                                                translator/other-examples/auxiliary (13s)     OK
Starting work on extra_arithTheory
extra_pred_setTheory                                                                                                                                                       examples/miller/formalize  (7s)     OK
Starting work on extra_realTheory
sequenceTheory                                                                                                                                                             examples/miller/formalize  (4s)     OK
Starting work on orderTheory
orderTheory                                                                                                                                                                examples/miller/formalize  (7s)     OK
Starting work on prob_canonTheory
extra_realTheory                                                                                                                                                           examples/miller/formalize (11s)     OK
Finished $(HOLDIR)/examples/miller/formalize [#theories: 7]                                                                                                                                             (37.653s) 
Finished $(CAKEMLDIR)/translator/other-examples/auxiliary [#theories: 4]                                                                                                                                (29.488s) 
Starting work on README.md
README.md                                                                                                                                                                  translator/other-examples  (0s)     OK
Starting work on example_91Theory
extra_arithTheory                                                                                                                                                             examples/miller/groups (18s)     OK
Starting work on groupTheory
prob_canonTheory                                                                                                                                                                examples/miller/prob (10s)     OK
Starting work on extra_binomialTheory
extra_binomialTheory                                                                                                                                                          examples/miller/groups  (6s)     OK
Starting work on prob_algebraTheory
example_91Theory                                                                                                                                                           translator/other-examples (23s)     OK
Starting work on example_balanced_bstTheory
groupTheory                                                                                                                                                                   examples/miller/groups (18s)     OK
Starting work on finite_groupTheory
prob_algebraTheory                                                                                                                                                              examples/miller/prob (18s)     OK
Starting work on probTheory
finite_groupTheory                                                                                                                                                            examples/miller/groups (12s)     OK
Starting work on abelian_groupTheory
RoundOpTheory                                                                                                                                                                    examples/Crypto/AES (69s)     OK
Starting work on aesTheory
abelian_groupTheory                                                                                                                                                           examples/miller/groups  (7s)     OK
Starting work on num_polyTheory
aesTheory                                                                                                                                                                        examples/Crypto/AES (10s)     OK
Finished $(HOLDIR)/examples/Crypto/AES [#theories: 4]                                                                                                                                                  (108.990s) 
Starting work on example_copying_gcTheory
probTheory                                                                                                                                                                      examples/miller/prob (23s)     OK
Starting work on prob_uniformTheory
num_polyTheory                                                                                                                                                                examples/miller/groups (11s)     OK
Starting work on mult_groupTheory
example_balanced_bstTheory                                                                                                                                                 translator/other-examples (39s)     OK
Starting work on example_parser_genTheory
prob_uniformTheory                                                                                                                                                              examples/miller/prob (12s)     OK
Finished $(HOLDIR)/examples/miller/prob [#theories: 4]                                                                                                                                                  (65.817s) 
Starting work on example_qsortTheory
example_copying_gcTheory                                                                                                                                                   translator/other-examples (41s)     OK
Starting work on example_regexp_matcherTheory
example_qsortTheory                                                                                                                                                        translator/other-examples (26s)     OK
mult_groupTheory                                                                                                                                                              examples/miller/groups (41s)     OK
Finished $(HOLDIR)/examples/miller/groups [#theories: 7]                                                                                                                                               (117.745s) 
Starting work on miller_rabinTheory
example_parser_genTheory                                                                                                                                                   translator/other-examples (52s)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"
 error in quse /root/regression/cakeml-1807/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 /root/regression/cakeml-1807/translator/other-examples/example_parser_genScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 Failed translation: getState
 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 (24s)MKILLED
miller_rabinTheory                                                                                                                                                            examples/miller/miller (19s)MKILLED