Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions

On Wed, 31 Oct 2012, Christoph LANGE wrote:


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 process.

If you need a hosting platform for the development process, I can recommend (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 human brain.

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 MHonArc.