Job 1034

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Sep 11 19:58:10 Claimed job
Sep 11 19:58:18 Building HOL
Sep 11 20:07:45 Starting developers
Sep 11 20:07:49 Finished developers                                               3s  76MB
Sep 11 20:07:50 Starting developers/bin
Sep 11 20:07:56 Finished developers/bin                                           6s 960MB
Sep 11 20:07:56 Starting semantics/ffi
Sep 11 20:08:35 Finished semantics/ffi                                           38s 504MB
Sep 11 20:08:35 Starting semantics
Sep 11 20:10:12 Finished semantics                                             1m36s   1GB
Sep 11 20:10:12 Starting semantics/proofs
Sep 11 20:13:10 Finished semantics/proofs                                      2m58s   1GB
Sep 11 20:13:11 Starting semantics/alt_semantics
Sep 11 20:13:19 Finished semantics/alt_semantics                                  8s 324MB
Sep 11 20:13:19 Starting semantics/alt_semantics/proofs
Sep 11 20:15:07 Finished semantics/alt_semantics/proofs                        1m48s 723MB
Sep 11 20:15:07 Starting basis/pure
Sep 11 20:18:57 Finished basis/pure                                            3m49s 912MB
Sep 11 20:18:57 Starting translator
Sep 11 20:20:44 Finished translator                                            1m46s   1GB
Sep 11 20:20:45 Starting compiler/parsing
Sep 11 20:21:42 Finished compiler/parsing                                        57s   1GB
Sep 11 20:21:42 Starting characteristic
Sep 11 20:26:57 Finished characteristic                                        5m14s   1GB
Sep 11 20:26:58 Starting translator/monadic
Sep 11 20:28:28 Finished translator/monadic                                    1m30s   1GB
Sep 11 20:28:28 Starting basis
Sep 11 20:47:58 Finished basis                                                19m29s   3GB
Sep 11 20:47:58 Starting compiler/inference
Sep 11 20:49:55 Finished compiler/inference                                    1m56s   1GB
Sep 11 20:49:55 Starting compiler/backend/reg_alloc
Sep 11 20:50:56 Finished compiler/backend/reg_alloc                            1m00s   1GB
Sep 11 20:50:56 Starting compiler/backend/gc
Sep 11 21:00:15 Finished compiler/backend/gc                                   9m19s   2GB
Sep 11 21:00:16 Starting compiler/backend
Sep 11 21:00:18 Finished compiler/backend                                         2s  15MB
Sep 11 21:00:18 Starting compiler/encoders/asm
Sep 11 21:00:20 Finished compiler/encoders/asm                                    1s  14MB
Sep 11 21:00:20 Starting compiler/encoders/x64
Sep 11 21:01:20 Finished compiler/encoders/x64                                   59s 987MB
Sep 11 21:01:20 Starting compiler/encoders/arm7
Sep 11 21:03:02 Finished compiler/encoders/arm7                                1m41s   1GB
Sep 11 21:03:02 Starting compiler/encoders/arm8
Sep 11 21:03:34 Finished compiler/encoders/arm8                                  31s 544MB
Sep 11 21:03:34 Starting compiler/encoders/mips
Sep 11 21:04:40 Finished compiler/encoders/mips                                1m06s 818MB
Sep 11 21:04:41 Starting compiler/encoders/riscv
Sep 11 21:05:59 Finished compiler/encoders/riscv                               1m18s 821MB
Sep 11 21:05:59 Starting compiler/encoders/ag32
Sep 11 21:06:17 Finished compiler/encoders/ag32                                  17s 771MB
Sep 11 21:06:17 Starting compiler/backend/x64
Sep 11 21:06:35 Finished compiler/backend/x64                                    18s   1GB
Sep 11 21:06:35 Starting compiler/backend/arm7
Sep 11 21:06:57 Finished compiler/backend/arm7                                   20s   1GB
Sep 11 21:06:57 Starting compiler/backend/arm8
Sep 11 21:07:15 Finished compiler/backend/arm8                                   18s   1GB
Sep 11 21:07:16 Starting compiler/backend/mips
Sep 11 21:07:35 Finished compiler/backend/mips                                   19s   1GB
Sep 11 21:07:35 Starting compiler/backend/riscv
Sep 11 21:07:55 Finished compiler/backend/riscv                                  19s   1GB
Sep 11 21:07:55 Starting compiler/backend/ag32
Sep 11 21:09:02 Finished compiler/backend/ag32                                 1m06s   1GB
Sep 11 21:09:03 Starting compiler/parsing/proofs
Sep 11 21:14:41 Finished compiler/parsing/proofs                               5m38s 908MB
Sep 11 21:14:41 Starting compiler/inference/proofs
Sep 11 21:17:27 Finished compiler/inference/proofs                             2m45s   1GB
Sep 11 21:17:27 Starting compiler/backend/semantics
Sep 11 21:23:22 Finished compiler/backend/semantics                            5m54s   1GB
Sep 11 21:23:22 Starting compiler/backend/reg_alloc/proofs
Sep 11 21:26:37 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Sep 11 21:26:37 Starting compiler/backend/proofs
Sep 11 22:06:28 Finished compiler/backend/proofs                              39m50s   3GB
Sep 11 22:06:28 Starting compiler/encoders/x64/proofs
Sep 11 22:16:28 Finished compiler/encoders/x64/proofs                          9m59s   4GB
Sep 11 22:16:28 Starting compiler/encoders/arm7/proofs
Sep 11 22:30:04 Finished compiler/encoders/arm7/proofs                        13m36s   3GB
Sep 11 22:30:05 Starting compiler/encoders/arm8/proofs
Sep 11 22:36:42 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
Sep 11 22:36:42 Starting compiler/encoders/mips/proofs
Sep 11 22:46:29 Finished compiler/encoders/mips/proofs                         9m46s   2GB
Sep 11 22:46:29 Starting compiler/encoders/riscv/proofs
Sep 11 22:54:49 Finished compiler/encoders/riscv/proofs                        8m19s   1GB
Sep 11 22:54:49 Starting compiler/encoders/ag32/proofs
Sep 11 22:57:15 Finished compiler/encoders/ag32/proofs                         2m25s 658MB
Sep 11 22:57:15 Starting compiler/backend/x64/proofs
Sep 11 22:57:35 Finished compiler/backend/x64/proofs                             19s   1GB
Sep 11 22:57:35 Starting compiler/backend/arm7/proofs
Sep 11 22:57:56 Finished compiler/backend/arm7/proofs                            20s   1GB
Sep 11 22:57:56 Starting compiler/backend/arm8/proofs
Sep 11 22:58:16 Finished compiler/backend/arm8/proofs                            19s   1GB
Sep 11 22:58:16 Starting compiler/backend/mips/proofs
Sep 11 22:58:37 Finished compiler/backend/mips/proofs                            20s   1GB
Sep 11 22:58:37 Starting compiler/backend/riscv/proofs
Sep 11 22:58:57 Finished compiler/backend/riscv/proofs                           19s   1GB
Sep 11 22:58:58 Starting compiler/backend/ag32/proofs
Sep 11 23:07:46 Finished compiler/backend/ag32/proofs                          8m48s   2GB
Sep 11 23:07:47 Starting compiler/proofs
Sep 11 23:09:24 Finished compiler/proofs                                       1m37s   2GB
Sep 11 23:09:24 Starting candle/set-theory
Sep 11 23:09:51 Finished candle/set-theory                                       27s 729MB
Sep 11 23:09:52 Starting candle/syntax-lib
Sep 11 23:10:02 Finished candle/syntax-lib                                       10s 476MB
Sep 11 23:10:02 Starting candle/standard/syntax
Sep 11 23:11:46 Finished candle/standard/syntax                                1m43s   1GB
Sep 11 23:11:46 Starting candle/standard/semantics
Sep 11 23:13:24 Finished candle/standard/semantics                             1m37s 917MB
Sep 11 23:13:24 Starting candle/standard/monadic
Sep 11 23:14:58 Finished candle/standard/monadic                               1m33s   1GB
Sep 11 23:14:58 Starting candle/standard/ml_kernel
Sep 11 23:18:48 Finished candle/standard/ml_kernel                             3m50s   4GB
Sep 11 23:18:49 Starting candle/standard/opentheory
Sep 11 23:27:31 Finished candle/standard/opentheory                            8m42s   3GB
Sep 11 23:27:32 Starting candle/standard/opentheory/compilation
Sep 11 23:57:27 Finished candle/standard/opentheory/compilation               29m55s  16GB
Sep 11 23:57:27 Starting candle/standard/opentheory/compilation/proofs
Sep 11 23:58:20 Finished candle/standard/opentheory/compilation/proofs           52s   2GB
Sep 11 23:58:20 Starting characteristic/examples
Sep 11 23:59:47 Finished characteristic/examples                               1m26s   2GB
Sep 11 23:59:47 Starting tutorial/solutions
Sep 12 00:12:50 Finished tutorial/solutions                                   13m03s   6GB
Sep 12 00:12:50 Starting translator/monadic/examples
Sep 12 00:15:49 Finished translator/monadic/examples                           2m58s   2GB
Sep 12 00:15:49 Starting examples
Sep 12 00:19:18 FAILED: examples
]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1034/basis]0;Holmake: ~/oven/regression/cakeml-1034/basis/pure]0;Holmake: ~/oven/regression/cakeml-1034/misc]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-1034/misc]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-c85f70b455b780c53c478eba1f68982e89cc3c61/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-1034/misc]0;Holmake: ~/oven/regression/cakeml-1034/developers]0;Holmake: ~/oven/regression/cakeml-1034/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-1034/misc]0;Holmake: ~/oven/regression/cakeml-1034/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1034/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-1034/misc]0;Holmake: ~/oven/regression/cakeml-1034/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-1034/basis/pure]0;Holmake: ~/oven/regression/cakeml-1034/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-1034/basis]0;Holmake: ~/oven/regression/cakeml-1034/characteristic]0;Holmake: ~/oven/regression/cakeml-1034/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1034/semantics]0;Holmake: ~/oven/regression/cakeml-1034/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1034/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-1034/semantics]0;Holmake: ~/oven/regression/cakeml-1034/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-1034/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1034/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-1034/characteristic]0;Holmake: ~/oven/regression/cakeml-1034/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1034/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-1034/characteristic]0;Holmake: ~/oven/regression/cakeml-1034/translator]0;Holmake: ~/oven/regression/cakeml-1034/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-1034/characteristic]0;Holmake: ~/oven/regression/cakeml-1034/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-1034/basis]0;Holmake: ~/oven/regression/cakeml-1034/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1034/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-1034/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-1034/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1034/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-1034/basis]0;Holmake: ~/oven/regression/cakeml-1034/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples
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
filterProgTheory                                                    FAILED! <1>
                               (0w :word64))))))))))]
 
 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
 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"}
doubleProgTheory                                                       M-KILLED
array_searchProgTheory                                                 M-KILLED
echoProgTheory                                                         M-KILLED