Job 608

CakeML:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name) [Dec 03 04:19:52]
HOL:0f41b430dba6521a505fd78da96fbf00252bfaa9
  Fix errors introduced by over-enthusiastic reformatting in 97b7d1900 [Dec 04 03:50:15]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 04 09:28:41 Claimed job
Dec 04 09:29:56 Building HOL
Dec 04 09:38:55 Starting developers
Dec 04 09:38:58 Finished developers                                               2s  20MB
Dec 04 09:38:58 Starting developers/bin
Dec 04 09:40:15 Finished developers/bin                                        1m15s 916MB
Dec 04 09:40:16 Starting semantics/ffi
Dec 04 09:40:53 Finished semantics/ffi                                           36s 498MB
Dec 04 09:40:54 Starting semantics
Dec 04 09:42:24 Finished semantics                                             1m29s 924MB
Dec 04 09:42:25 Starting semantics/proofs
Dec 04 09:45:17 Finished semantics/proofs                                      2m51s   1GB
Dec 04 09:45:18 Starting basis/pure
Dec 04 11:37:32 FAILED: basis/pure
Starting work on balanced_mapTheory
balanced_mapTheory                                                           OK
Starting work on osetTheory
osetTheory                                                                   OK
]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
Starting work on FormalLangTheory
FormalLangTheory                                                             OK
]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0f41b430dba6521a505fd78da96fbf00252bfaa9/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on charsetTheory
Starting work on eq_cmp_bmapTheory
Starting work on vec_mapTheory
vec_mapTheory                                                                OK
eq_cmp_bmapTheory                                                            OK
charsetTheory                                                                OK
Starting work on regexpTheory
regexpTheory                                                 FAILED! <Signal F>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 Saved theorem _____ "regexp_compareW_eq"
 Saved theorem _____ "regexp_compare_eq"
 Saved theorem _____ "regexp_compareW_antisym"
 Saved theorem _____ "regexp_compare_antisym"
 Saved theorem _____ "regexp_compareW_trans"
 Saved theorem _____ "regexp_compare_trans"
 Saved theorem _____ "regexp_compareW_trans_eq"
 Saved theorem _____ "regexp_compare_trans"
]0;Holmake: .