[isabelle-dev] New (Co)datatypes: Status & Plan 2

[Makarius]

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 
two parts.

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?


 	Makarius