Job 1172

CakeML:ea9c31be21392fff4368718527b96960080722c7
  Fix bootstrap translation of dataLang explorer [Feb 04 13:59:15]
#723 (explorer-data)
Merging into:742e79a817066a6099785ab5150013848c9d0441
  Merge pull request #721 from CakeML/exit_stderr [Feb 02 19:14:20]
HOL:2ab28aee333f79a324fa8db4805e5882e4b841e2
  Use polyscripter more in Core Theories section of DESCRIPTION [Feb 01 05:37:03]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Feb 04 14:02:39 Claimed job
Feb 04 14:02:44 Building HOL
Feb 04 14:13:25 Starting developers
Feb 04 14:13:29 Finished developers                                               4s  59MB
Feb 04 14:13:29 Starting developers/bin
Feb 04 14:13:36 Finished developers/bin                                           7s   1GB
Feb 04 14:13:36 Starting semantics/ffi
Feb 04 14:13:46 Finished semantics/ffi                                            9s 250MB
Feb 04 14:13:46 Starting semantics
Feb 04 14:18:26 Finished semantics                                             4m40s   1GB
Feb 04 14:18:26 Starting semantics/proofs
Feb 04 14:33:54 Finished semantics/proofs                                     15m27s   1GB
Feb 04 14:33:54 Starting semantics/alt_semantics
Feb 04 14:34:02 Finished semantics/alt_semantics                                  7s 299MB
Feb 04 14:34:02 Starting semantics/alt_semantics/proofs
Feb 04 14:40:56 Finished semantics/alt_semantics/proofs                        6m54s 836MB
Feb 04 14:40:56 Starting basis/pure
Feb 04 14:43:47 Finished basis/pure                                            2m51s 891MB
Feb 04 14:43:48 Starting translator
Feb 04 14:55:56 Finished translator                                           12m08s   1GB
Feb 04 14:55:56 Starting compiler/parsing
Feb 04 14:58:31 Finished compiler/parsing                                      2m35s   1GB
Feb 04 14:58:31 Starting characteristic
Feb 04 15:16:20 Finished characteristic                                       17m48s   2GB
Feb 04 15:16:20 Starting translator/monadic
Feb 04 15:18:21 Finished translator/monadic                                    2m00s   1GB
Feb 04 15:18:21 Starting basis
Feb 04 15:51:15 Finished basis                                                32m54s  11GB
Feb 04 15:51:15 Starting compiler/inference
Feb 04 15:54:48 Finished compiler/inference                                    3m32s   2GB
Feb 04 15:54:48 Starting compiler/backend/reg_alloc
Feb 04 15:55:48 Finished compiler/backend/reg_alloc                            1m00s   1GB
Feb 04 15:55:48 Starting compiler/backend/gc
Feb 04 15:59:50 Finished compiler/backend/gc                                   4m02s   2GB
Feb 04 15:59:50 Starting compiler/backend
Feb 04 16:06:22 Finished compiler/backend                                      6m31s   4GB
Feb 04 16:06:22 Starting compiler/encoders/asm
Feb 04 16:06:43 Finished compiler/encoders/asm                                   20s 806MB
Feb 04 16:06:43 Starting compiler/encoders/x64
Feb 04 16:07:55 Finished compiler/encoders/x64                                 1m12s   1GB
Feb 04 16:07:55 Starting compiler/encoders/arm7
Feb 04 16:09:43 Finished compiler/encoders/arm7                                1m47s   1GB
Feb 04 16:09:43 Starting compiler/encoders/arm8
Feb 04 16:10:16 Finished compiler/encoders/arm8                                  33s 624MB
Feb 04 16:10:16 Starting compiler/encoders/mips
Feb 04 16:11:44 Finished compiler/encoders/mips                                1m27s   1GB
Feb 04 16:11:44 Starting compiler/encoders/riscv
Feb 04 16:13:07 Finished compiler/encoders/riscv                               1m23s   1GB
Feb 04 16:13:07 Starting compiler/encoders/ag32
Feb 04 16:13:24 Finished compiler/encoders/ag32                                  16s 871MB
Feb 04 16:13:24 Starting compiler/backend/x64
Feb 04 16:13:42 Finished compiler/backend/x64                                    17s   1GB
Feb 04 16:13:42 Starting compiler/backend/arm7
Feb 04 16:14:02 Finished compiler/backend/arm7                                   20s   1GB
Feb 04 16:14:02 Starting compiler/backend/arm8
Feb 04 16:14:19 Finished compiler/backend/arm8                                   17s 994MB
Feb 04 16:14:19 Starting compiler/backend/mips
Feb 04 16:14:37 Finished compiler/backend/mips                                   17s   1GB
Feb 04 16:14:37 Starting compiler/backend/riscv
Feb 04 16:14:56 Finished compiler/backend/riscv                                  18s   1GB
Feb 04 16:14:56 Starting compiler/backend/ag32
Feb 04 16:16:11 Finished compiler/backend/ag32                                 1m15s   1GB
Feb 04 16:16:11 Starting compiler/parsing/proofs
Feb 04 16:21:56 Finished compiler/parsing/proofs                               5m44s   1GB
Feb 04 16:21:56 Starting compiler/inference/proofs
Feb 04 16:25:40 Finished compiler/inference/proofs                             3m43s   1GB
Feb 04 16:25:40 Starting compiler/backend/semantics
Feb 04 18:02:24 Finished compiler/backend/semantics                         1h36m44s   2GB
Feb 04 18:02:25 Starting compiler/backend/reg_alloc/proofs
Feb 04 18:06:04 Finished compiler/backend/reg_alloc/proofs                     3m38s 925MB
Feb 04 18:06:04 Starting compiler/backend/proofs
Feb 05 04:11:29 Finished compiler/backend/proofs                           10h05m25s  20GB
Feb 05 04:11:29 Starting compiler/encoders/x64/proofs
Feb 05 04:23:07 Finished compiler/encoders/x64/proofs                         11m37s   2GB
Feb 05 04:23:07 Starting compiler/encoders/arm7/proofs
Feb 05 04:36:49 Finished compiler/encoders/arm7/proofs                        13m41s   4GB
Feb 05 04:36:49 Starting compiler/encoders/arm8/proofs
Feb 05 04:43:48 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
Feb 05 04:43:48 Starting compiler/encoders/mips/proofs
Feb 05 04:54:05 Finished compiler/encoders/mips/proofs                        10m17s   3GB
Feb 05 04:54:05 Starting compiler/encoders/riscv/proofs
Feb 05 05:03:47 Finished compiler/encoders/riscv/proofs                        9m41s   1GB
Feb 05 05:03:47 Starting compiler/encoders/ag32/proofs
Feb 05 05:06:21 Finished compiler/encoders/ag32/proofs                         2m34s 878MB
Feb 05 05:06:21 Starting compiler/backend/x64/proofs
Feb 05 05:06:41 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 05 05:06:41 Starting compiler/backend/arm7/proofs
Feb 05 05:07:03 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 05 05:07:03 Starting compiler/backend/arm8/proofs
Feb 05 05:07:23 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 05 05:07:23 Starting compiler/backend/mips/proofs
Feb 05 05:07:43 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 05 05:07:43 Starting compiler/backend/riscv/proofs
Feb 05 05:08:03 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 05 05:08:03 Starting compiler/backend/ag32/proofs
Feb 05 05:22:30 Finished compiler/backend/ag32/proofs                         14m23s   4GB
Feb 05 05:22:30 Starting compiler/proofs
Feb 05 05:24:15 Finished compiler/proofs                                       1m44s   3GB
Feb 05 05:24:15 Starting candle/set-theory
Feb 05 05:24:43 Finished candle/set-theory                                       27s 792MB
Feb 05 05:24:43 Starting candle/syntax-lib
Feb 05 05:24:52 Finished candle/syntax-lib                                        9s 690MB
Feb 05 05:24:53 Starting candle/standard/syntax
Feb 05 05:26:36 Finished candle/standard/syntax                                1m43s 939MB
Feb 05 05:26:36 Starting candle/standard/semantics
Feb 05 05:28:14 Finished candle/standard/semantics                             1m37s   1GB
Feb 05 05:28:14 Starting candle/standard/monadic
Feb 05 05:30:43 Finished candle/standard/monadic                               2m29s   1GB
Feb 05 05:30:43 Starting candle/standard/ml_kernel
Feb 05 05:45:33 Finished candle/standard/ml_kernel                            14m50s   4GB
Feb 05 05:45:33 Starting candle/standard/opentheory
Feb 05 05:57:03 Finished candle/standard/opentheory                           11m30s   4GB
Feb 05 05:57:03 Starting candle/standard/opentheory/compilation
Feb 05 06:29:45 Finished candle/standard/opentheory/compilation               32m42s  12GB
Feb 05 06:29:46 Starting candle/standard/opentheory/compilation/proofs
Feb 05 06:30:26 Finished candle/standard/opentheory/compilation/proofs           40s   3GB
Feb 05 06:30:26 Starting characteristic/examples
Feb 05 06:31:59 Finished characteristic/examples                               1m33s   2GB
Feb 05 06:31:59 Starting tutorial/solutions
Feb 05 06:47:02 Finished tutorial/solutions                                   15m02s   7GB
Feb 05 06:47:02 Starting translator/monadic/examples
Feb 05 06:50:11 Finished translator/monadic/examples                           3m09s   2GB
Feb 05 06:50:11 Starting examples
Feb 05 06:58:52 Finished examples                                              8m40s   4GB
Feb 05 06:58:52 Starting examples/compilation/x64
Feb 05 09:21:23 Finished examples/compilation/x64                           2h22m30s  12GB
Feb 05 09:21:23 Starting examples/compilation/x64/proofs
Feb 05 09:22:57 Finished examples/compilation/x64/proofs                       1m34s   3GB
Feb 05 09:22:57 Starting examples/compilation/ag32
Feb 05 09:55:31 Finished examples/compilation/ag32                            32m33s   7GB
Feb 05 09:55:31 Starting examples/compilation/ag32/proofs
Feb 05 09:56:47 Finished examples/compilation/ag32/proofs                      1m16s   3GB
Feb 05 09:56:47 Starting examples/cost
Feb 05 10:38:06 Finished examples/cost                                        41m18s   6GB
Feb 05 10:38:07 Starting examples/lpr_checker
Feb 05 10:41:55 Finished examples/lpr_checker                                  3m47s   2GB
Feb 05 10:41:55 Starting examples/lpr_checker/compilation
Feb 05 10:59:28 Finished examples/lpr_checker/compilation                     17m33s   8GB
Feb 05 10:59:28 Starting examples/lpr_checker/compilation/proofs
Feb 05 11:00:05 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Feb 05 11:00:05 Starting examples/lpr_checker/array
Feb 05 11:10:20 Finished examples/lpr_checker/array                           10m14s   3GB
Feb 05 11:10:20 Starting examples/lpr_checker/array/compilation
Feb 05 11:26:38 Finished examples/lpr_checker/array/compilation               16m18s   9GB
Feb 05 11:26:38 Starting examples/lpr_checker/array/compilation/proofs
Feb 05 11:28:58 Finished examples/lpr_checker/array/compilation/proofs         2m19s   4GB
Feb 05 11:28:58 Starting translator/okasaki-examples
Feb 05 11:35:19 Finished translator/okasaki-examples                           6m20s   1GB
Feb 05 11:35:19 Starting translator/other-examples
Feb 05 11:36:57 FAILED: translator/other-examples
Scanning [1m$(HOLDIR)/examples/Crypto/RC6[0m
Scanning [1m$(HOLDIR)/examples/Crypto/TEA[0m
Scanning [1m$(HOLDIR)/examples/RSA[0m
Scanning [1m$(HOLDIR)/examples/miller/ho_prover[0m
Scanning [1m$(HOLDIR)/examples/miller/subtypes[0m
Scanning [1m$(HOLDIR)/examples/miller/formalize[0m
Scanning [1m$(HOLDIR)/examples/miller/groups[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/lem_lib_stub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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
Starting work on MultTheory
Starting work on tablesTheory
Starting work on RC6Theory
Starting work on teaTheory
teaTheory                                       real:    5s  user:    5s     OK
Starting work on powerTheory
RC6Theory                                       real:    6s  user:    5s     OK
Starting work on summationTheory
powerTheory                                     real:    0s  user:    0s     OK
Starting work on skiTheory
summationTheory                                 real:    0s  user:    0s     OK
Starting work on binomialTheory
binomialTheory                                  real:    0s  user:    0s     OK
Starting work on extra_boolTheory
skiTheory                                       real:    1s  user:    0s     OK
Starting work on subtypeTheory
extra_boolTheory                                real:    0s  user:    0s     OK
Starting work on copying_gcTheory
MultTheory                                      real:    9s  user:    8s     OK
Starting work on ninetyOneTheory
tablesTheory                                    real:    9s  user:    8s     OK
Starting work on RoundOpTheory
subtypeTheory                                   real:    2s  user:    1s     OK
Starting work on extra_numTheory
copying_gcTheory                                real:    1s  user:    1s     OK
Starting work on regexpMatchTheory
ninetyOneTheory                                 real:    2s  user:    1s     OK
Starting work on slr_parser_genTheory
extra_numTheory                                 real:    2s  user:    1s     OK
Starting work on extra_listTheory
slr_parser_genTheory                            real:    2s  user:    1s     OK
Starting work on sequenceTheory
regexpMatchTheory                               real:    5s  user:    4s     OK
Starting work on extra_arithTheory
extra_listTheory                                real:    4s  user:    3s     OK
Starting work on extra_pred_setTheory
sequenceTheory                                  real:    2s  user:    1s     OK
Starting work on prob_canonTheory
prob_canonTheory                                real:    4s  user:    3s     OK
Starting work on README.md
README.md                                       real:    0s  user:    0s     OK
Starting work on example_91Theory
extra_pred_setTheory                            real:    5s  user:    4s     OK
Starting work on extra_realTheory
extra_arithTheory                               real:   10s  user:    9s     OK
Starting work on orderTheory
orderTheory                                     real:    3s  user:    3s     OK
Starting work on groupTheory
example_91Theory                                real:   10s  user:    9s     OK
Starting work on extra_binomialTheory
extra_binomialTheory                            real:    3s  user:    3s     OK
Starting work on example_balanced_bstTheory
groupTheory                                     real:    8s  user:    7s     OK
Starting work on finite_groupTheory
extra_realTheory                                real:   22s  user:   21s     OK
Starting work on prob_algebraTheory
finite_groupTheory                              real:    7s  user:    7s     OK
Starting work on abelian_groupTheory
abelian_groupTheory                             real:    5s  user:    4s     OK
Starting work on num_polyTheory
prob_algebraTheory                              real:    7s  user:    6s     OK
Starting work on probTheory
example_balanced_bstTheory                      real:   20s  user:   18s     OK
Starting work on example_copying_gcTheory
num_polyTheory                                  real:    7s  user:    6s     OK
Starting work on mult_groupTheory
RoundOpTheory                                   real:   47s  user:   46s     OK
Starting work on aesTheory
aesTheory                                       real:    4s  user:    3s     OK
Starting work on example_parser_genTheory
probTheory                                      real:   11s  user:   10s     OK
Starting work on prob_uniformTheory
prob_uniformTheory                              real:    5s  user:    4s     OK
Starting work on example_qsortTheory
example_copying_gcTheory                        real:   19s  user:   18s     OK
Starting work on example_regexp_matcherTheory
mult_groupTheory                                real:   20s  user:   20s     OK
Starting work on miller_rabinTheory
example_qsortTheory                             real:   12s  user:   11s     OK
example_regexp_matcherTheory                    real:   12s  user:   11s     OK
miller_rabinTheory                              real:   12s  user:   12s     OK
Starting work on example_primality_testTheory
example_parser_genTheory                        real:   32s  user:   31s     OK
example_primality_testTheory                    real:    5s  user:    4sFAIL<1>
 error in load $(CAKEMLDIR)/characteristic/cfNormaliseTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/characteristic/cfAppTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/characteristic/cfTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/characteristic/cfTacticsTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/characteristic/cfDivTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/basis/RuntimeProgTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/basis/OptionProgTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load $(CAKEMLDIR)/basis/ListProgTheory : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 error in load /home/cur/sao/cakeml/regression/cakeml-1172/translator/other-examples/example_primality_testScript : GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"
 Uncaught exception: GrammarError "Attempt to have differently associated infixes (RIGHT and NONASSOC) at same level(470)"