Overview

Job 608

CakeML:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name)
HOL:0f41b430dba6521a505fd78da96fbf00252bfaa9
  Fix errors introduced by over-enthusiastic reformatting in 97b7d1900
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  20MB
 Starting developers/bin
 Finished developers/bin                                        1m15s 916MB
 Starting semantics/ffi
 Finished semantics/ffi                                           36s 498MB
 Starting semantics
 Finished semantics                                             1m29s 924MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m51s   1GB
 Starting basis/pure
 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: .