Email Gateway (Aug 19 2022 at 11:50): Email Gateway (Aug 19 2022 at 11:50):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Isabelle community,
as a part of our work on formalising auctions
(http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/) we
implemented an algorithm that computes all partitions of a given set and
proved its correctness. This is joint work with Marco B. Caminati,
Manfred Kerber and Colin Rowat.
Even though this is just one small building block of our soundness proof
of a combinatorial auction (see http://arxiv.org/abs/1308.1779 for the
big picture), it is self-contained, and we believe that it is of general
interest. We are further working on a verified algorithm to compute all
injective functions between two given sets.
Our main reason for defining these functions in a computable way is the
ability to use Isabelle's code generator to generate verified auction
software. Please see
http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/isabelle/Auction/code/
for executable Scala demos.
The sources can be found in our GitHub repository
https://github.com/formare/auctions/ at
https://github.com/formare/auctions/blob/master/isabelle/Auction/Partitions.thy.
I'm sure Partitions.thy is of interest for the AFP. However, other
parts of our Auction Theory Toolbox (maintained on GitHub) depend on it.
Do you have a good recommendation for how to submit Partitions.thy to
the AFP without breaking the dependencies of our Toolbox?
Furthermore, would such a theory be of interest for the Isabelle library?
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:54):From: Tobias Nipkow <nipkow@in.tum.de>
You can always modify the development version of your AFP entry to keep it in
sync with the rest of your toolbox.
Parts of IsaFoR, the Isabelle Formalization of Rewriting by Christian Sternagel
and René Thiemann, live in the AFP. Either of them should share their experience
with this arrangement.
Tobias
Email Gateway (Aug 19 2022 at 11:55):From: René Thiemann <rene.thiemann@uibk.ac.at>
So far, we are quite satisfied with our setup, that some parts of IsaFoR are in the AFP and
others are not. Here are my personal opinions on our setup:
1) If you are always working with the development version of Isabelle, then there
is no problem at all to put parts of your work in the AFP. Because then you can
at any time change your AFP entries.
2) Putting theories in the AFP has the big advantage that updates for your theories
in AFP w.r.t. changes in Isabelle will most likely done by someone else, namely
the person who did the change in Isabelle.
Moreover, you get feedback by other Isabelle users who want to use your AFP-theories,
and the visibility of your development is increased.
3) If you are working with a release version of Isabelle, then one problem might be
that changes in the AFP-part of your theories will only become visible in the AFP
at the next release. To this end, we usually only put those parts into the AFP
which are quite stable. Moreover, in our local development we accumulate changes
for the AFP-part, which are then integrated into the AFP shortly before the next
release. In this way, other persons (students) can always work with IsaFoR and
a release version of Isabelle. (Exceptions are shortly before the next release where
we merge our theories with the AFP)
Hope this helps,
René
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
Here you should swap the articles and say "a development version" vs. "the
release version".
Development versions are many: more than 50000 right now. When you make
an arbitrary shot at some of them, you get "the" version on your machine
in some directory, while the public repository keeps moving. You need to
care about keeping it in sync with other snapshots of other projects (e.g.
AFP), tell other people about the changeset id you happen to have etc.
To work smoothly, you need to follow ongoing changes frequently. Staying
behind too long means your "latest development version" becomes more
outdated than the last public Isabelle release version. (You IsaFoR guys
manage all that very well, and there is even a formal COMPATIBILITY file
with changeset ids of Isabelle and AFP within your repository.)
In contrast, Isabelle releases are well-defined stable checkpoints that
happen every 6-10 months and remain "current" over a longer time. When
someone posts on the mailing list, there is no need to say "I am using the
latest release" (or one or two releases behind), since that can be easily
guessed or tried out quickly against 2 or 3 alternatives (instead of
thousands above). Someone who happens to have some project based on some
proper release from a few years ago can still be helped out. (Archeology
on repository versions that are more than a few months old is much
harder.)
Anyway, we are presently again in a state of confusion about
isabelle-users vs. isabelle-dev, proper releases vs. arbitrary repository
snapshots. I've just myself posted ongoing repository changes about a
mostly administrative tool "isabelle components" on this mailing list by
accident.
Makarius
Last updated: May 07 2024 at 01:07 UTC