[isabelle-dev] New (Co)datatypes: Status & Plan 2
makarius at sketis.net
Wed Nov 20 14:12:00 CET 2013
On Mon, 18 Nov 2013, Jasmin Christian Blanchette wrote:
> A question that arises is whether we should have only "datatype_new"
> (and "primrec_new"; i.e. the LFP part) in "HOL" or also "codatatype"
> (and "primcorec"; i.e. the GFP part). The BNF package is organized in
> such a way that it can be split in the middle, so we really have both
> options. The "HOL" build time is a criterion. On my 4-core laptop from
> 2010, running LFP (+ dependencies) on top of HOL takes 18 to 20 s of
> wall-clock time; adding GFP adds about 6 s. This leaves us under our
> planned budget of 30 s.
Last time when we have discussed that privately, I was slightly in favour
of having it all in HOL, without the extra complexity of splitting up in
Dmitriy had sent me some explanations which sessions represent the
material to be moved to HOL in either case, but I never tried it out
myself. It is high time to do that now. In particularly I would like to
get a feeling for HOL-Proofs. We also had some obscure drop-outs in
summer with TTY / Proof General, if that is still relevant.
Can you say again which sessions/theories in which repository version
constitute the datatype vs. codatatype part?
More information about the isabelle-dev