Job 1173

CakeML:294f486b84cc652213e7bc903d33ef82c8dee18f
  Add a python script that parses sexps [Feb 05 16:28:55]
#724 (constrain_op_case)
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 05 21:57:06 Claimed job
Feb 05 21:57:10 Reusing HOL
Feb 05 21:58:01 Starting developers
Feb 05 21:58:05 Finished developers                                               3s  97MB
Feb 05 21:58:05 Starting developers/bin
Feb 05 21:58:12 Finished developers/bin                                           6s   1GB
Feb 05 21:58:12 Starting semantics/ffi
Feb 05 21:58:22 Finished semantics/ffi                                            9s 245MB
Feb 05 21:58:22 Starting semantics
Feb 05 22:02:49 Finished semantics                                             4m27s 914MB
Feb 05 22:02:49 Starting semantics/proofs
Feb 05 22:18:08 Finished semantics/proofs                                     15m18s   1GB
Feb 05 22:18:08 Starting semantics/alt_semantics
Feb 05 22:18:16 Finished semantics/alt_semantics                                  7s 294MB
Feb 05 22:18:16 Starting semantics/alt_semantics/proofs
Feb 05 22:25:11 Finished semantics/alt_semantics/proofs                        6m55s 803MB
Feb 05 22:25:11 Starting basis/pure
Feb 05 22:26:03 Finished basis/pure                                              51s 712MB
Feb 05 22:26:03 Starting translator
Feb 05 22:38:32 Finished translator                                           12m29s   1GB
Feb 05 22:38:33 Starting compiler/parsing
Feb 05 22:41:01 Finished compiler/parsing                                      2m28s   2GB
Feb 05 22:41:01 Starting characteristic
Feb 05 22:59:20 Finished characteristic                                       18m17s   1GB
Feb 05 22:59:21 Starting translator/monadic
Feb 05 23:01:19 Finished translator/monadic                                    1m57s   1GB
Feb 05 23:01:19 Starting basis
Feb 05 23:34:09 Finished basis                                                32m50s  12GB
Feb 05 23:34:09 Starting compiler/inference
Feb 05 23:35:07 Finished compiler/inference                                      57s   1GB
Feb 05 23:35:07 Starting compiler/backend/reg_alloc
Feb 05 23:36:06 Finished compiler/backend/reg_alloc                              59s   1GB
Feb 05 23:36:06 Starting compiler/backend/gc
Feb 05 23:40:06 Finished compiler/backend/gc                                   3m58s   2GB
Feb 05 23:40:06 Starting compiler/backend
Feb 05 23:46:38 Finished compiler/backend                                      6m32s   4GB
Feb 05 23:46:38 Starting compiler/encoders/asm
Feb 05 23:46:59 Finished compiler/encoders/asm                                   20s 851MB
Feb 05 23:46:59 Starting compiler/encoders/x64
Feb 05 23:47:24 Finished compiler/encoders/x64                                   24s   1GB
Feb 05 23:47:24 Starting compiler/encoders/arm7
Feb 05 23:48:10 Finished compiler/encoders/arm7                                  46s 720MB
Feb 05 23:48:10 Starting compiler/encoders/arm8
Feb 05 23:48:23 Finished compiler/encoders/arm8                                  12s 901MB
Feb 05 23:48:23 Starting compiler/encoders/mips
Feb 05 23:48:40 Finished compiler/encoders/mips                                  16s 953MB
Feb 05 23:48:40 Starting compiler/encoders/riscv
Feb 05 23:48:54 Finished compiler/encoders/riscv                                 13s 769MB
Feb 05 23:48:54 Starting compiler/encoders/ag32
Feb 05 23:49:12 Finished compiler/encoders/ag32                                  17s 595MB
Feb 05 23:49:12 Starting compiler/backend/x64
Feb 05 23:49:29 Finished compiler/backend/x64                                    16s   1GB
Feb 05 23:49:29 Starting compiler/backend/arm7
Feb 05 23:49:48 Finished compiler/backend/arm7                                   19s   1GB
Feb 05 23:49:48 Starting compiler/backend/arm8
Feb 05 23:50:06 Finished compiler/backend/arm8                                   17s   1GB
Feb 05 23:50:06 Starting compiler/backend/mips
Feb 05 23:50:24 Finished compiler/backend/mips                                   18s   1GB
Feb 05 23:50:24 Starting compiler/backend/riscv
Feb 05 23:50:43 Finished compiler/backend/riscv                                  18s   1GB
Feb 05 23:50:43 Starting compiler/backend/ag32
Feb 05 23:51:58 Finished compiler/backend/ag32                                 1m14s   1GB
Feb 05 23:51:58 Starting compiler/parsing/proofs
Feb 05 23:57:46 Finished compiler/parsing/proofs                               5m48s 924MB
Feb 05 23:57:46 Starting compiler/inference/proofs
Feb 06 00:00:50 Finished compiler/inference/proofs                             3m03s   1GB
Feb 06 00:00:50 Starting compiler/backend/semantics
Feb 06 01:37:08 Finished compiler/backend/semantics                         1h36m17s   2GB
Feb 06 01:37:08 Starting compiler/backend/reg_alloc/proofs
Feb 06 01:40:48 Finished compiler/backend/reg_alloc/proofs                     3m39s 799MB
Feb 06 01:40:48 Starting compiler/backend/proofs
Feb 06 11:43:17 Finished compiler/backend/proofs                           10h02m28s  16GB
Feb 06 11:43:17 Starting compiler/encoders/x64/proofs
Feb 06 11:55:01 Finished compiler/encoders/x64/proofs                         11m43s   2GB
Feb 06 11:55:01 Starting compiler/encoders/arm7/proofs
Feb 06 12:08:51 Finished compiler/encoders/arm7/proofs                        13m50s   3GB
Feb 06 12:08:51 Starting compiler/encoders/arm8/proofs
Feb 06 12:16:06 Finished compiler/encoders/arm8/proofs                         7m14s   1GB
Feb 06 12:16:06 Starting compiler/encoders/mips/proofs
Feb 06 12:26:45 Finished compiler/encoders/mips/proofs                        10m38s   2GB
Feb 06 12:26:45 Starting compiler/encoders/riscv/proofs
Feb 06 12:36:20 Finished compiler/encoders/riscv/proofs                        9m35s   1GB
Feb 06 12:36:20 Starting compiler/encoders/ag32/proofs
Feb 06 12:38:52 Finished compiler/encoders/ag32/proofs                         2m31s 975MB
Feb 06 12:38:52 Starting compiler/backend/x64/proofs
Feb 06 12:39:11 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 06 12:39:12 Starting compiler/backend/arm7/proofs
Feb 06 12:39:33 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 06 12:39:33 Starting compiler/backend/arm8/proofs
Feb 06 12:39:53 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 06 12:39:53 Starting compiler/backend/mips/proofs
Feb 06 12:40:13 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 06 12:40:14 Starting compiler/backend/riscv/proofs
Feb 06 12:40:34 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 06 12:40:34 Starting compiler/backend/ag32/proofs
Feb 06 12:55:38 Finished compiler/backend/ag32/proofs                         15m04s   2GB
Feb 06 12:55:38 Starting compiler/proofs
Feb 06 12:57:09 Finished compiler/proofs                                       1m30s   4GB
Feb 06 12:57:10 Starting candle/set-theory
Feb 06 12:57:36 Finished candle/set-theory                                       26s 816MB
Feb 06 12:57:36 Starting candle/syntax-lib
Feb 06 12:57:47 Finished candle/syntax-lib                                       10s 620MB
Feb 06 12:57:47 Starting candle/standard/syntax
Feb 06 12:59:31 Finished candle/standard/syntax                                1m44s   1GB
Feb 06 12:59:31 Starting candle/standard/semantics
Feb 06 13:01:10 Finished candle/standard/semantics                             1m38s   1GB
Feb 06 13:01:10 Starting candle/standard/monadic
Feb 06 13:03:40 Finished candle/standard/monadic                               2m29s   1GB
Feb 06 13:03:40 Starting candle/standard/ml_kernel
Feb 06 13:18:55 Finished candle/standard/ml_kernel                            15m15s   4GB
Feb 06 13:18:55 Starting candle/standard/opentheory
Feb 06 13:30:21 Finished candle/standard/opentheory                           11m26s   3GB
Feb 06 13:30:21 Starting candle/standard/opentheory/compilation
Feb 06 14:03:52 Finished candle/standard/opentheory/compilation               33m30s  13GB
Feb 06 14:03:52 Starting candle/standard/opentheory/compilation/proofs
Feb 06 14:04:32 Finished candle/standard/opentheory/compilation/proofs           40s   4GB
Feb 06 14:04:32 Starting characteristic/examples
Feb 06 14:06:01 Finished characteristic/examples                               1m28s   2GB
Feb 06 14:06:01 Starting tutorial/solutions
Feb 06 14:21:21 Finished tutorial/solutions                                   15m19s   7GB
Feb 06 14:21:21 Starting translator/monadic/examples
Feb 06 14:24:37 Finished translator/monadic/examples                           3m16s   3GB
Feb 06 14:24:37 Starting examples
Feb 06 14:33:17 Finished examples                                              8m39s   3GB
Feb 06 14:33:17 Starting examples/compilation/x64
Feb 06 16:55:08 Finished examples/compilation/x64                           2h21m51s  16GB
Feb 06 16:55:08 Starting examples/compilation/x64/proofs
Feb 06 16:56:43 Finished examples/compilation/x64/proofs                       1m35s   3GB
Feb 06 16:56:43 Starting examples/compilation/ag32
Feb 06 17:29:40 Finished examples/compilation/ag32                            32m56s   6GB
Feb 06 17:29:40 Starting examples/compilation/ag32/proofs
Feb 06 17:30:49 Finished examples/compilation/ag32/proofs                      1m09s   4GB
Feb 06 17:30:50 Starting examples/cost
Feb 06 18:12:20 Finished examples/cost                                        41m30s   6GB
Feb 06 18:12:20 Starting examples/lpr_checker
Feb 06 18:16:09 Finished examples/lpr_checker                                  3m48s   2GB
Feb 06 18:16:09 Starting examples/lpr_checker/compilation
Feb 06 18:33:51 Finished examples/lpr_checker/compilation                     17m41s   9GB
Feb 06 18:33:51 Starting examples/lpr_checker/compilation/proofs
Feb 06 18:34:27 Finished examples/lpr_checker/compilation/proofs                 36s   3GB
Feb 06 18:34:27 Starting examples/lpr_checker/array
Feb 06 18:44:45 Finished examples/lpr_checker/array                           10m17s   2GB
Feb 06 18:44:45 Starting examples/lpr_checker/array/compilation
Feb 06 19:00:38 Finished examples/lpr_checker/array/compilation               15m53s   8GB
Feb 06 19:00:38 Starting examples/lpr_checker/array/compilation/proofs
Feb 06 19:02:55 Finished examples/lpr_checker/array/compilation/proofs         2m16s   4GB
Feb 06 19:02:55 Starting translator/okasaki-examples
Feb 06 19:09:18 Finished translator/okasaki-examples                           6m23s   1GB
Feb 06 19:09:18 Starting translator/other-examples
Feb 06 19:09:41 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 copying_gcTheory
Starting work on ninetyOneTheory
Starting work on regexpMatchTheory
Starting work on slr_parser_genTheory
copying_gcTheory                                real:    1s  user:    1s     OK
Starting work on README.md
README.md                                       real:    0s  user:    0s     OK
Starting work on example_balanced_bstTheory
ninetyOneTheory                                 real:    2s  user:    1s     OK
Starting work on example_copying_gcTheory
slr_parser_genTheory                            real:    2s  user:    1s     OK
Starting work on example_parser_genTheory
regexpMatchTheory                               real:    5s  user:    4s     OK
Starting work on example_91Theory
example_91Theory                                real:   10s  user:    9s     OK
Starting work on example_primality_testTheory
example_balanced_bstTheory                      real:   17s  user:   16s     OK
Starting work on example_qsortTheory
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-1173/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)"
example_copying_gcTheory                                                M-KILLED
example_parser_genTheory                                                M-KILLED
example_qsortTheory                                                     M-KILLED