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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
