[isabelle-dev] Towards the next release

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Mar 16 21:27:30 CET 2012


Hi *,

I am currently busy with stocktaking the results of my visit to TUM last
Wednesday, and I have updated the current state of two affairs in the wiki:

* The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back
Not everything mentioned there is an ultimate need, but we should strive
to pick as many fruits as we can from the set type constructor – the
more likely this will compensate users if they have to adjust their theories

* The numeral story: https://isabelle.in.tum.de/community/Numerals
It looks quite good (preliminary tests of the AFP did not reveal much
problems).  The fork should be done by the end of April.  The further
perspectives listed there are no need-to-haves for the next release.

I further did some doodling around with mira; after 14 staying away from
there  I did not encountered fundamental difficulties, but my original
intent, operative configurations for distribution build and docs, did
not grow very far.  I will set aside this as it is by now and would
appreciate if anybody would continue on this, sooner or later.  After
this experience I will keep mira on my screen, but when I will return to
it I plan to focus on
* re-learn what the current deployment at TUM is
* improve the notoriously annoying settings mechanisms
* minor technical improvements
before doing anything end-user visible.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120316/1d1e999e/attachment.sig>


More information about the isabelle-dev mailing list