[isabelle-dev] Proposing extensions to the Isabelle library?
coglio at kestrel.edu
Tue Jul 2 00:13:23 CEST 2013
Hello Florian et al.,
I finally got around to work on what we discussed back in December (see email below) and now I have a patch that works with changeset 52498:d802431fe356. The command
./bin/isabelle build -a -o browser_info -o document=pdf -o document_graph
succeeds (after applying the patch), even though the output says that some theories are skipped due to what look like some undefined environment variables -- I can send more precise information on this.
The patch follows exactly Florian's suggestion below, and also slightly redefines class complete_lattice in a perhaps cleaner way, taking advantage of the new syntactic type classes. A few proofs here and there had to be adapted.
These changes may affect the AFP, but I haven't looked at that. What is the process for testing and propagating library changes to the AFP?
Should I send the patch for review to anyone in particular, or to this whole mailing list?
On Dec 18, 2012, at 12:18 PM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Alessandro,
>> Is there any plan to make things in the library more uniform (one way or
>> the other)? Is there a preference for new type classes should be
>> developed (purely syntactic or with assumptions)?
> well, there is no big masterplan. Usually things evolve: somebody
> thinks about an extended or more fine-grained hierarchy and thinks how
> to accomplish things without breaking more than necessary.
>> Personally, I like syntactic classes because they are more modular. For
>> example, in the library extensions that I sent the other day, the
>> definition of type class finite_lattice_complete would be perhaps
>> slightly cleaner if bot and top were syntactic classes like Inf and Sup.
>> Just my 2 cents.
> I.e. something like
> class bot ~> class order_bot
> class top ~> class order_top
> class bot = fixes bot :: "'a"
> class top = fixes top :: "'a"
> Could make sense. The question is whether somebody is willing to
> undertake this change. If you would consider this, you find the first
> clues at
> Get back here if questions remain.
> Note that currently we are heading towards a next release in January or
> February, and time might be too terse to polish and incorporate a change
> like the one sketched above.
> Hope this helps,
> PGP available:
More information about the isabelle-dev