Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- To: Christoph LANGE <c.lange at cs.bham.ac.uk>
- Subject: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- From: Makarius <makarius at sketis.net>
- Date: Fri, 16 Nov 2012 22:49:16 +0100 (CET)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <50916DB3.firstname.lastname@example.org>
- References: <50916DB3.email@example.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Wed, 31 Oct 2012, Christoph LANGE wrote:
QUESTIONS FOR ISABELLE COMMUNITY
We would like to contribute our formalisation to the AFP, but are unsure
about the procedure: once accepted and published, can we submit updates?
We could imagine submitting this formalisation soon (as it is
self-contained and covers a relevant field), but still we are planning
to evolve and improve it.
I am not an editor of AFP, but it is generally a good idea to refine and
consilidate some development several times, before entering the submission
If you need a hosting platform for the development process, I can
recommend https://bitbucket.org/ (with Mercurial).
As this was our first major Isabelle formalisation, we may have got a
lot of things wrong. We would be grateful if any of you were able to
look into the source and tell us of any "anti-patterns" we shouldn't
use. I will also follow up on this mail with a number of mails asking
specific questions on how certain things in Isabelle work, and with some
jEdit bug reports.
Looking only briefly over your Vickrey.thy, it already looks quite good as
a start. There are many fine points to be considered; we should go
through it gradually and without attacking everything at the same time.
Since Christoph is also a CICM person, I would like to point out the MKM
2008 paper by myself and Stefan Berghofer on "Logic-free reasoning in
Isabelle/Isar". It shows how to deflate your theories by a significant
factor, by removing unnecessary fluff. (Informal people sometimes think
they are doing formal logic when writing a lot of logical connectives
around there meterial, but this is not the real point of it.)
When doing functional programming properly, you also don't write funny
tuple arguments all the time, just to please ousiders, you use currying.
Can you write your sources with 80 char per line, or 100 maximum? These
exceedingly long lines are hard to read. The physicial parameters of
cinema displays have changed a lot recently, but not the parameters of the
jEdit is not very good at soft line-breaks, and it is better to layout
your formal sources explicitly yourself. (The jEdit indentation
facilities still need to be activated for Isar sources, like I did many
years ago for Proof General / Emacs.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and