Job 1035

CakeML:9632f9daf78d00dd6ae6bacafbdf0947a67e442f
  Fix too many open files error [Sep 12 07:17:19]
#690 (close-files)
Merging into:f8746ce03b63e2867d62acf3ea403ea5414963c7
  Merge pull request #688 from CakeML/issue683 [Sep 08 06:17:31]
HOL:c85f70b455b780c53c478eba1f68982e89cc3c61
  Remove a stray trailing whitespace in examples/.../regexpScript.sml [Sep 11 00:41:52]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Sep 12 07:53:16 Claimed job
Sep 12 07:53:22 Building HOL
Sep 12 08:01:30 Starting developers
Sep 12 08:01:33 Finished developers                                               1s  74MB
Sep 12 08:01:33 Starting developers/bin
Sep 12 08:01:37 Finished developers/bin                                           3s 238MB
Sep 12 08:01:37 Starting semantics/ffi
Sep 12 08:02:11 Finished semantics/ffi                                           33s 336MB
Sep 12 08:02:12 Starting semantics
Sep 12 08:03:46 Finished semantics                                             1m34s   1GB
Sep 12 08:03:47 Starting semantics/proofs
Sep 12 08:06:51 Finished semantics/proofs                                      3m04s   1GB
Sep 12 08:06:52 Starting semantics/alt_semantics
Sep 12 08:06:58 Finished semantics/alt_semantics                                  6s 265MB
Sep 12 08:06:59 Starting semantics/alt_semantics/proofs
Sep 12 08:08:46 Finished semantics/alt_semantics/proofs                        1m47s 799MB
Sep 12 08:08:47 Starting basis/pure
Sep 12 08:12:37 Finished basis/pure                                            3m50s 673MB
Sep 12 08:12:37 Starting translator
Sep 12 08:14:23 Finished translator                                            1m45s   1GB
Sep 12 08:14:23 Starting compiler/parsing
Sep 12 08:15:21 Finished compiler/parsing                                        57s   2GB
Sep 12 08:15:21 Starting characteristic
Sep 12 08:20:42 Finished characteristic                                        5m19s   1GB
Sep 12 08:20:42 Starting translator/monadic
Sep 12 08:22:09 Finished translator/monadic                                    1m26s   1GB
Sep 12 08:22:09 Starting basis
Sep 12 08:41:23 Finished basis                                                19m13s   2GB
Sep 12 08:41:24 Starting compiler/inference
Sep 12 08:43:14 Finished compiler/inference                                    1m50s   1GB
Sep 12 08:43:15 Starting compiler/backend/reg_alloc
Sep 12 08:44:13 Finished compiler/backend/reg_alloc                              57s   1GB
Sep 12 08:44:13 Starting compiler/backend/gc
Sep 12 08:53:15 Finished compiler/backend/gc                                   9m01s   1GB
Sep 12 08:53:16 Starting compiler/backend
Sep 12 08:53:17 Finished compiler/backend                                         0s  44MB
Sep 12 08:53:17 Starting compiler/encoders/asm
Sep 12 08:53:17 Finished compiler/encoders/asm                                    0s  35MB
Sep 12 08:53:18 Starting compiler/encoders/x64
Sep 12 08:54:15 Finished compiler/encoders/x64                                   56s 730MB
Sep 12 08:54:15 Starting compiler/encoders/arm7
Sep 12 08:55:51 Finished compiler/encoders/arm7                                1m35s   1GB
Sep 12 08:55:51 Starting compiler/encoders/arm8
Sep 12 08:56:19 Finished compiler/encoders/arm8                                  28s 677MB
Sep 12 08:56:20 Starting compiler/encoders/mips
Sep 12 08:57:24 Finished compiler/encoders/mips                                1m04s 980MB
Sep 12 08:57:25 Starting compiler/encoders/riscv
Sep 12 08:58:41 Finished compiler/encoders/riscv                               1m16s   1GB
Sep 12 08:58:42 Starting compiler/encoders/ag32
Sep 12 08:58:56 Finished compiler/encoders/ag32                                  14s 815MB
Sep 12 08:58:57 Starting compiler/backend/x64
Sep 12 08:59:12 Finished compiler/backend/x64                                    15s 842MB
Sep 12 08:59:13 Starting compiler/backend/arm7
Sep 12 08:59:30 Finished compiler/backend/arm7                                   17s   1GB
Sep 12 08:59:31 Starting compiler/backend/arm8
Sep 12 08:59:47 Finished compiler/backend/arm8                                   16s   1GB
Sep 12 08:59:47 Starting compiler/backend/mips
Sep 12 09:00:04 Finished compiler/backend/mips                                   16s   1GB
Sep 12 09:00:05 Starting compiler/backend/riscv
Sep 12 09:00:21 Finished compiler/backend/riscv                                  16s   1GB
Sep 12 09:00:22 Starting compiler/backend/ag32
Sep 12 09:01:28 Finished compiler/backend/ag32                                 1m05s   1GB
Sep 12 09:01:28 Starting compiler/parsing/proofs
Sep 12 09:07:00 Finished compiler/parsing/proofs                               5m31s 821MB
Sep 12 09:07:00 Starting compiler/inference/proofs
Sep 12 09:09:40 Finished compiler/inference/proofs                             2m39s   1GB
Sep 12 09:09:41 Starting compiler/backend/semantics
Sep 12 09:15:43 Finished compiler/backend/semantics                            6m02s   2GB
Sep 12 09:15:43 Starting compiler/backend/reg_alloc/proofs
Sep 12 09:18:58 Finished compiler/backend/reg_alloc/proofs                     3m14s   1GB
Sep 12 09:18:58 Starting compiler/backend/proofs
Sep 12 10:00:21 Finished compiler/backend/proofs                              41m21s   3GB
Sep 12 10:00:21 Starting compiler/encoders/x64/proofs
Sep 12 10:10:28 Finished compiler/encoders/x64/proofs                         10m07s   4GB
Sep 12 10:10:28 Starting compiler/encoders/arm7/proofs
Sep 12 10:24:13 Finished compiler/encoders/arm7/proofs                        13m44s   3GB
Sep 12 10:24:13 Starting compiler/encoders/arm8/proofs
Sep 12 10:30:55 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Sep 12 10:30:56 Starting compiler/encoders/mips/proofs
Sep 12 10:41:07 Finished compiler/encoders/mips/proofs                        10m10s   2GB
Sep 12 10:41:07 Starting compiler/encoders/riscv/proofs
Sep 12 10:49:50 Finished compiler/encoders/riscv/proofs                        8m42s   1GB
Sep 12 10:49:50 Starting compiler/encoders/ag32/proofs
Sep 12 10:52:17 Finished compiler/encoders/ag32/proofs                         2m26s 677MB
Sep 12 10:52:18 Starting compiler/backend/x64/proofs
Sep 12 10:52:34 Finished compiler/backend/x64/proofs                             16s 995MB
Sep 12 10:52:35 Starting compiler/backend/arm7/proofs
Sep 12 10:52:52 Finished compiler/backend/arm7/proofs                            17s   1GB
Sep 12 10:52:52 Starting compiler/backend/arm8/proofs
Sep 12 10:53:08 Finished compiler/backend/arm8/proofs                            15s   1GB
Sep 12 10:53:08 Starting compiler/backend/mips/proofs
Sep 12 10:53:25 Finished compiler/backend/mips/proofs                            16s   1GB
Sep 12 10:53:25 Starting compiler/backend/riscv/proofs
Sep 12 10:53:42 Finished compiler/backend/riscv/proofs                           16s   1GB
Sep 12 10:53:43 Starting compiler/backend/ag32/proofs
Sep 12 11:02:36 Finished compiler/backend/ag32/proofs                          8m53s   2GB
Sep 12 11:02:36 Starting compiler/proofs
Sep 12 11:03:52 Finished compiler/proofs                                       1m14s   3GB
Sep 12 11:03:52 Starting candle/set-theory
Sep 12 11:04:17 Finished candle/set-theory                                       25s 758MB
Sep 12 11:04:18 Starting candle/syntax-lib
Sep 12 11:04:27 Finished candle/syntax-lib                                        8s 432MB
Sep 12 11:04:27 Starting candle/standard/syntax
Sep 12 11:06:07 Finished candle/standard/syntax                                1m39s   1GB
Sep 12 11:06:07 Starting candle/standard/semantics
Sep 12 11:07:39 Finished candle/standard/semantics                             1m31s   1GB
Sep 12 11:07:39 Starting candle/standard/monadic
Sep 12 11:09:11 Finished candle/standard/monadic                               1m31s   1GB
Sep 12 11:09:12 Starting candle/standard/ml_kernel
Sep 12 11:12:57 Finished candle/standard/ml_kernel                             3m45s   3GB
Sep 12 11:12:57 Starting candle/standard/opentheory
Sep 12 11:21:26 Finished candle/standard/opentheory                            8m28s   4GB
Sep 12 11:21:26 Starting candle/standard/opentheory/compilation
Sep 12 11:50:42 Finished candle/standard/opentheory/compilation               29m15s  16GB
Sep 12 11:50:42 Starting candle/standard/opentheory/compilation/proofs
Sep 12 11:51:24 Finished candle/standard/opentheory/compilation/proofs           42s   2GB
Sep 12 11:51:25 Starting characteristic/examples
Sep 12 11:52:50 Finished characteristic/examples                               1m24s   2GB
Sep 12 11:52:50 Starting tutorial/solutions
Sep 12 12:06:01 Finished tutorial/solutions                                   13m10s   6GB
Sep 12 12:06:01 Starting translator/monadic/examples
Sep 12 12:08:52 Finished translator/monadic/examples                           2m50s   2GB
Sep 12 12:08:52 Starting examples
Sep 12 12:12:25 FAILED: examples
]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1035/basis]0;Holmake: ~/regression/cakeml-1035/basis/pure]0;Holmake: ~/regression/cakeml-1035/misc]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-1035/misc]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1035/misc]0;Holmake: ~/regression/cakeml-1035/developers]0;Holmake: ~/regression/cakeml-1035/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1035/misc]0;Holmake: ~/regression/cakeml-1035/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1035/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1035/misc]0;Holmake: ~/regression/cakeml-1035/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1035/basis/pure]0;Holmake: ~/regression/cakeml-1035/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1035/basis]0;Holmake: ~/regression/cakeml-1035/characteristic]0;Holmake: ~/regression/cakeml-1035/compiler/parsing]0;Holmake: ~/regression/cakeml-1035/semantics]0;Holmake: ~/regression/cakeml-1035/semantics/ffi]0;Holmake: ~/regression/cakeml-1035/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1035/semantics]0;Holmake: ~/regression/cakeml-1035/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1035/compiler/parsing]0;Holmake: ~/regression/cakeml-1035/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1035/characteristic]0;Holmake: ~/regression/cakeml-1035/semantics/proofs]0;Holmake: ~/regression/cakeml-1035/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1035/characteristic]0;Holmake: ~/regression/cakeml-1035/translator]0;Holmake: ~/regression/cakeml-1035/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1035/characteristic]0;Holmake: ~/regression/cakeml-1035/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1035/basis]0;Holmake: ~/regression/cakeml-1035/translator/monadic]0;Holmake: ~/regression/cakeml-1035/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1035/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1035/translator/monadic]0;Holmake: ~/regression/cakeml-1035/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1035/basis]0;Holmake: ~/regression/cakeml-1035/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on divTheory
lcsTheory                                                                                                                                               OK
Starting work on diffTheory
diffTheory                                                                                                                                              OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                           OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                     OK
Starting work on array_searchProgTheory
diffProgTheory                                                                                                                                          OK
Starting work on echoProgTheory
divTheory                                                                                                                                               OK
Starting work on filterProgTheory
doubleProgTheory                                                                                                                                        OK
Starting work on grepProgTheory
filterProgTheory                                                                                                                               FAILED! <1>
 on line 40, characters 42-63
 
 which has type
 
 :regexp list
 
 unification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list
 error in quse /home/myreen/regression/cakeml-1035/examples/filterProgScript.sml : HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load filterProgScript : HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
array_searchProgTheory                                                                                                                            M-KILLED
echoProgTheory                                                                                                                                    M-KILLED
grepProgTheory                                                                                                                                    M-KILLED