Job 1809

CakeML: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:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 28 09:02:41 Claimed job
Feb 28 09:02:49 Building HOL
Feb 28 09:12:28 Starting developers
Feb 28 09:12:33 Finished developers                                               4s 153MB
Feb 28 09:12:33 Starting developers/bin
Feb 28 09:12:37 Finished developers/bin                                           4s 674MB
Feb 28 09:12:37 Starting semantics/ffi
Feb 28 09:12:47 Finished semantics/ffi                                            9s 233MB
Feb 28 09:12:47 Starting semantics
Feb 28 09:15:01 Finished semantics                                             2m13s   1GB
Feb 28 09:15:01 Starting semantics/proofs
Feb 28 09:18:42 Finished semantics/proofs                                      3m40s   1GB
Feb 28 09:18:42 Starting semantics/alt_semantics
Feb 28 09:18:59 Finished semantics/alt_semantics                                 16s 525MB
Feb 28 09:18:59 Starting semantics/alt_semantics/proofs
Feb 28 09:21:26 Finished semantics/alt_semantics/proofs                        2m27s 925MB
Feb 28 09:21:27 Starting basis/pure
Feb 28 09:24:20 Finished basis/pure                                            2m53s 921MB
Feb 28 09:24:20 Starting translator
Feb 28 09:27:25 Finished translator                                            3m05s   1GB
Feb 28 09:27:26 Starting compiler/parsing
Feb 28 09:28:41 Finished compiler/parsing                                      1m15s   2GB
Feb 28 09:28:41 Starting characteristic
Feb 28 09:35:03 Finished characteristic                                        6m22s   1GB
Feb 28 09:35:03 Starting translator/monadic
Feb 28 09:36:58 Finished translator/monadic                                    1m55s   1GB
Feb 28 09:36:58 Starting basis
Feb 28 10:24:01 Finished basis                                                47m01s  18GB
Feb 28 10:24:01 Starting compiler/inference
Feb 28 10:25:30 Finished compiler/inference                                    1m28s   1GB
Feb 28 10:25:30 Starting compiler/backend/reg_alloc
Feb 28 10:27:14 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 28 10:27:14 Starting compiler/backend/gc
Feb 28 10:31:39 Finished compiler/backend/gc                                   4m25s   1GB
Feb 28 10:31:40 Starting compiler/backend
Feb 28 10:37:06 Finished compiler/backend                                      5m26s   2GB
Feb 28 10:37:06 Starting compiler/encoders/asm
Feb 28 10:37:36 Finished compiler/encoders/asm                                   29s 771MB
Feb 28 10:37:36 Starting compiler/encoders/x64
Feb 28 10:38:43 Finished compiler/encoders/x64                                 1m06s 778MB
Feb 28 10:38:43 Starting compiler/encoders/arm7
Feb 28 10:40:58 Finished compiler/encoders/arm7                                2m15s   1GB
Feb 28 10:40:58 Starting compiler/encoders/arm8
Feb 28 10:41:40 Finished compiler/encoders/arm8                                  41s   1GB
Feb 28 10:41:40 Starting compiler/encoders/arm8_asl
Feb 28 12:53:02 Finished compiler/encoders/arm8_asl                         2h11m21s  37GB
Feb 28 12:53:02 Starting compiler/encoders/mips
Feb 28 12:54:33 Finished compiler/encoders/mips                                1m31s   1GB
Feb 28 12:54:33 Starting compiler/encoders/riscv
Feb 28 12:56:22 Finished compiler/encoders/riscv                               1m49s   1GB
Feb 28 12:56:23 Starting compiler/encoders/ag32
Feb 28 12:56:44 Finished compiler/encoders/ag32                                  21s 688MB
Feb 28 12:56:45 Starting compiler/backend/x64
Feb 28 12:57:06 Finished compiler/backend/x64                                    21s   1GB
Feb 28 12:57:06 Starting compiler/backend/arm7
Feb 28 12:57:31 Finished compiler/backend/arm7                                   24s   1GB
Feb 28 12:57:31 Starting compiler/backend/arm8
Feb 28 12:57:53 Finished compiler/backend/arm8                                   21s   1GB
Feb 28 12:57:53 Starting compiler/backend/mips
Feb 28 12:58:15 Finished compiler/backend/mips                                   22s   1GB
Feb 28 12:58:15 Starting compiler/backend/riscv
Feb 28 12:58:38 Finished compiler/backend/riscv                                  23s   1GB
Feb 28 12:58:38 Starting compiler/backend/ag32
Feb 28 13:00:04 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 28 13:00:04 Starting compiler/parsing/proofs
Feb 28 13:03:51 Finished compiler/parsing/proofs                               3m47s   1GB
Feb 28 13:03:52 Starting compiler/inference/proofs
Feb 28 13:06:25 Finished compiler/inference/proofs                             2m33s   1GB
Feb 28 13:06:25 Starting compiler/backend/semantics
Feb 28 13:34:53 Finished compiler/backend/semantics                           28m28s   1GB
Feb 28 13:34:53 Starting compiler/backend/reg_alloc/proofs
Feb 28 13:38:22 Finished compiler/backend/reg_alloc/proofs                     3m28s   1GB
Feb 28 13:38:23 Starting compiler/backend/proofs
Feb 28 14:29:57 Finished compiler/backend/proofs                              51m33s  17GB
Feb 28 14:29:58 Starting compiler/backend/serialiser
Feb 28 14:31:34 Finished compiler/backend/serialiser                           1m36s   1GB
Feb 28 14:31:34 Starting compiler/encoders/x64/proofs
Feb 28 14:41:10 Finished compiler/encoders/x64/proofs                          9m35s   4GB
Feb 28 14:41:10 Starting compiler/encoders/arm7/proofs
Feb 28 14:54:19 Finished compiler/encoders/arm7/proofs                        13m08s   3GB
Feb 28 14:54:19 Starting compiler/encoders/arm8/proofs
Feb 28 15:01:05 Finished compiler/encoders/arm8/proofs                         6m45s   1GB
Feb 28 15:01:05 Starting compiler/encoders/arm8_asl/proofs
Feb 28 15:50:46 Finished compiler/encoders/arm8_asl/proofs                    49m37s   7GB
Feb 28 15:50:46 Starting compiler/encoders/mips/proofs
Feb 28 16:00:49 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Feb 28 16:00:49 Starting compiler/encoders/riscv/proofs
Feb 28 16:09:43 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Feb 28 16:09:43 Starting compiler/encoders/ag32/proofs
Feb 28 16:12:18 Finished compiler/encoders/ag32/proofs                         2m34s 639MB
Feb 28 16:12:18 Starting compiler/backend/x64/proofs
Feb 28 16:12:45 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 28 16:12:45 Starting compiler/backend/arm7/proofs
Feb 28 16:13:14 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 28 16:13:15 Starting compiler/backend/arm8/proofs
Feb 28 16:13:43 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 28 16:13:43 Starting compiler/backend/arm8_asl
Feb 28 16:14:11 Finished compiler/backend/arm8_asl                               27s   1GB
Feb 28 16:14:11 Starting compiler/backend/mips/proofs
Feb 28 16:14:40 Finished compiler/backend/mips/proofs                            28s   1GB
Feb 28 16:14:40 Starting compiler/backend/riscv/proofs
Feb 28 16:15:08 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 28 16:15:08 Starting compiler/backend/ag32/proofs
Feb 28 16:28:19 Finished compiler/backend/ag32/proofs                         13m10s   2GB
Feb 28 16:28:19 Starting compiler/proofs
Feb 28 16:30:43 Finished compiler/proofs                                       2m23s   3GB
Feb 28 16:30:43 Starting candle/set-theory
Feb 28 16:31:17 Finished candle/set-theory                                       33s 919MB
Feb 28 16:31:17 Starting candle/syntax-lib
Feb 28 16:31:30 Finished candle/syntax-lib                                       12s 776MB
Feb 28 16:31:30 Starting candle/standard/syntax
Feb 28 16:33:32 Finished candle/standard/syntax                                2m01s   1GB
Feb 28 16:33:32 Starting candle/standard/semantics
Feb 28 16:35:19 Finished candle/standard/semantics                             1m47s   1GB
Feb 28 16:35:19 Starting candle/standard/monadic
Feb 28 16:37:12 Finished candle/standard/monadic                               1m53s   1GB
Feb 28 16:37:12 Starting candle/standard/ml_kernel
Feb 28 16:43:20 Finished candle/standard/ml_kernel                             6m07s   4GB
Feb 28 16:43:20 Starting candle/overloading/syntax
Feb 28 16:46:30 Finished candle/overloading/syntax                             3m09s   1GB
Feb 28 16:46:30 Starting candle/overloading/semantics
Feb 28 16:58:33 Finished candle/overloading/semantics                         12m00s   2GB
Feb 28 16:58:34 Starting candle/overloading/monadic
Feb 28 17:01:05 Finished candle/overloading/monadic                            2m31s   1GB
Feb 28 17:01:05 Starting candle/overloading/ml_kernel
Feb 28 17:08:18 Finished candle/overloading/ml_kernel                          7m12s   3GB
Feb 28 17:08:18 Starting candle/overloading/ml_checker
Feb 28 17:10:43 Finished candle/overloading/ml_checker                         2m24s   3GB
Feb 28 17:10:43 Starting candle/prover
Feb 28 17:18:22 Finished candle/prover                                         7m39s   3GB
Feb 28 17:18:23 Starting pancake
Feb 28 17:21:07 Finished pancake                                               2m44s   2GB
Feb 28 17:21:07 Starting pancake/ffi
Feb 28 17:21:07 Finished pancake/ffi                                              0s  35MB
Feb 28 17:21:07 Starting pancake/semantics
Feb 28 17:23:38 Finished pancake/semantics                                     2m30s   1GB
Feb 28 17:23:38 Starting pancake/proofs
Feb 28 17:35:41 Finished pancake/proofs                                       12m03s   6GB
Feb 28 17:35:41 Starting characteristic/examples
Feb 28 17:37:02 Finished characteristic/examples                               1m21s   3GB
Feb 28 17:37:03 Starting tutorial/solutions
Feb 28 17:53:38 Finished tutorial/solutions                                   16m35s   9GB
Feb 28 17:53:38 Starting translator/monadic/examples
Feb 28 17:57:29 Finished translator/monadic/examples                           3m51s   2GB
Feb 28 17:57:29 Starting examples
Feb 28 18:06:57 Finished examples                                              9m26s   3GB
Feb 28 18:06:57 Starting examples/compilation/x64
Feb 28 20:36:58 Finished examples/compilation/x64                           2h29m58s  19GB
Feb 28 20:36:59 Starting examples/compilation/x64/proofs
Feb 28 20:39:25 Finished examples/compilation/x64/proofs                       2m25s   3GB
Feb 28 20:39:25 Starting examples/compilation/ag32
Feb 28 21:13:57 Finished examples/compilation/ag32                            34m32s   9GB
Feb 28 21:13:57 Starting examples/compilation/ag32/proofs
Feb 28 21:14:53 Finished examples/compilation/ag32/proofs                        55s   3GB
Feb 28 21:14:53 Starting examples/cost
Feb 28 22:10:09 Finished examples/cost                                        55m15s   7GB
Feb 28 22:10:09 Starting examples/lpr_checker
Feb 28 22:11:12 Finished examples/lpr_checker                                  1m02s   1GB
Feb 28 22:11:12 Starting examples/lpr_checker/array
Feb 28 22:39:32 Finished examples/lpr_checker/array                           28m20s   5GB
Feb 28 22:39:32 Starting examples/lpr_checker/array/compilation
Mar 01 00:03:06 Finished examples/lpr_checker/array/compilation             1h23m31s  53GB
Mar 01 00:03:06 Starting examples/lpr_checker/array/compilation/proofs
Mar 01 00:04:33 Finished examples/lpr_checker/array/compilation/proofs         1m27s   6GB
Mar 01 00:04:34 Starting examples/opentheory
Mar 01 00:14:26 Finished examples/opentheory                                   9m52s   6GB
Mar 01 00:14:26 Starting examples/opentheory
Mar 01 00:14:27 Finished examples/opentheory                                      1s 130MB
Mar 01 00:14:27 Starting examples/opentheory/compilation
Mar 01 00:53:43 Finished examples/opentheory/compilation                      39m16s  28GB
Mar 01 00:53:43 Starting examples/opentheory/compilation/proofs
Mar 01 00:54:48 Finished examples/opentheory/compilation/proofs                1m04s   2GB
Mar 01 00:54:48 Starting examples/opentheory/compilation/ag32
Mar 01 01:33:30 Finished examples/opentheory/compilation/ag32                 38m39s  31GB
Mar 01 01:33:31 Starting examples/opentheory/compilation/ag32/proofs
Mar 01 01:35:18 Finished examples/opentheory/compilation/ag32/proofs           1m47s   4GB
Mar 01 01:35:19 Starting examples/sat_encodings
Mar 01 01:37:20 Finished examples/sat_encodings                                2m01s 935MB
Mar 01 01:37:20 Starting examples/sat_encodings/case_studies
Mar 01 01:39:00 Finished examples/sat_encodings/case_studies                   1m40s 755MB
Mar 01 01:39:00 Starting examples/sat_encodings/translation
Mar 01 01:44:52 Finished examples/sat_encodings/translation                    5m51s   5GB
Mar 01 01:44:52 Starting examples/sat_encodings/translation/compilation
Mar 01 02:33:41 Finished examples/sat_encodings/translation/compilation       48m46s  21GB
Mar 01 02:33:41 Starting translator/okasaki-examples
Mar 01 02:38:32 Finished translator/okasaki-examples                           4m51s   1GB
Mar 01 02:38:32 Starting translator/other-examples
Mar 01 02:40:03 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  (4s)     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
teaTheory                                                                              examples/Crypto/TEA  (6s)     OK
Finished $(HOLDIR)/examples/Crypto/TEA [#theories: 1]                                                          (6.110s) 
Starting work on skiTheory
binomialTheory                                                                         examples/Crypto/RSA  (0s)     OK
Finished $(HOLDIR)/examples/Crypto/RSA [#theories: 3]                                                          (1.040s) 
Starting work on extra_boolTheory
skiTheory                                                                        examples/miller/ho_prover  (0s)     OK
Finished $(HOLDIR)/examples/miller/ho_prover [#theories: 1]                                                    (0.750s) 
Starting work on subtypeTheory
extra_boolTheory                                                                 examples/miller/formalize  (0s)     OK
Starting work on copying_gcTheory
RC6Theory                                                                              examples/Crypto/RC6  (7s)     OK
Finished $(HOLDIR)/examples/Crypto/RC6 [#theories: 1]                                                          (7.750s) 
Starting work on ninetyOneTheory
subtypeTheory                                                                     examples/miller/subtypes  (1s)     OK
Finished $(HOLDIR)/examples/miller/subtypes [#theories: 1]                                                     (1.550s) 
Starting work on extra_numTheory
MultTheory                                                                             examples/Crypto/AES  (9s)     OK
Starting work on RoundOpTheory
copying_gcTheory                                                       translator/other-examples/auxiliary  (1s)     OK
Starting work on regexpMatchTheory
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  (3s)     OK
Starting work on extra_realTheory
prob_canonTheory                                                                      examples/miller/prob  (6s)     OK
Starting work on orderTheory
extra_realTheory                                                                 examples/miller/formalize  (5s)     OK
Starting work on prob_algebraTheory
extra_arithTheory                                                                   examples/miller/groups  (9s)     OK
Starting work on groupTheory
orderTheory                                                                      examples/miller/formalize  (3s)     OK
Finished $(HOLDIR)/examples/miller/formalize [#theories: 7]                                                   (19.040s) 
Starting work on extra_binomialTheory
extra_binomialTheory                                                                examples/miller/groups  (2s)     OK
Finished $(CAKEMLDIR)/translator/other-examples/auxiliary [#theories: 4]                                      (12.410s) 
Starting work on README.md
README.md                                                                        translator/other-examples  (0s)     OK
Starting work on example_91Theory
groupTheory                                                                         examples/miller/groups  (7s)     OK
Starting work on finite_groupTheory
prob_algebraTheory                                                                    examples/miller/prob  (8s)     OK
Starting work on probTheory
finite_groupTheory                                                                  examples/miller/groups  (6s)     OK
Starting work on abelian_groupTheory
example_91Theory                                                                 translator/other-examples (12s)     OK
Starting work on num_polyTheory
abelian_groupTheory                                                                 examples/miller/groups  (4s)     OK
Starting work on example_balanced_bstTheory
RoundOpTheory                                                                          examples/Crypto/AES (38s)     OK
Starting work on aesTheory
probTheory                                                                            examples/miller/prob (13s)     OK
Starting work on prob_uniformTheory
num_polyTheory                                                                      examples/miller/groups  (6s)     OK
Starting work on mult_groupTheory
aesTheory                                                                              examples/Crypto/AES  (5s)     OK
Finished $(HOLDIR)/examples/Crypto/AES [#theories: 4]                                                         (58.190s) 
Starting work on example_copying_gcTheory
prob_uniformTheory                                                                    examples/miller/prob  (5s)     OK
Finished $(HOLDIR)/examples/miller/prob [#theories: 4]                                                        (33.630s) 
Starting work on example_parser_genTheory
example_balanced_bstTheory                                                       translator/other-examples (22s)     OK
Starting work on example_qsortTheory
mult_groupTheory                                                                    examples/miller/groups (20s)     OK
Finished $(HOLDIR)/examples/miller/groups [#theories: 7]                                                      (58.060s) 
Starting work on miller_rabinTheory
example_copying_gcTheory                                                         translator/other-examples (22s)     OK
Starting work on example_regexp_matcherTheory
example_qsortTheory                                                              translator/other-examples (14s)     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/cug/hk324/cml-regression/cakeml-1809/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/cug/hk324/cml-regression/cakeml-1809/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 = "??"}
miller_rabinTheory                                                                  examples/miller/miller (14s)MKILLED
example_regexp_matcherTheory                                                     translator/other-examples  (8s)MKILLED