[isabelle-dev] Isabelle root access

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu May 8 12:45:03 CEST 2014

Hi Makarius,

Am 08.05.2014 um 12:32 schrieb Makarius <makarius at sketis.net>:

> On Thu, 8 May 2014, mta-proj wrote:
>> die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury erweitert
> Membership of the "isabelle" Unix group means full root access to many administrative resources.  Usually neither the one who grants the rights nor the one who receives them knows what that means.
> So just the canonical questions: Who is responsible for these users? What are their projects within Isabelle?

I sent an email ahead of time, but now I realize I sent it to the wrong mailing list (isabelle-group instead of isabelle-dev). So here is the description:

 * * *

The "isabelle" group has been (or will be shortly) extended with two new users, both of them working as summer interns under my (co)supervision:

   Martin Desharnais (co-supervisor: Dmitriy Traytel)
   Mathias Fleury

They will need to push changes to the (co)datatypes resp. Sledgehammer. More specifically, Martin will enrich the list of theorems generated by the new (co)datatype package, and Mathias will integrate Sledgehammer better with some more exotic ATPs (e.g. Zipperposition, veriT, LEO-II, Satallax).

 * * *

Sorry for the mixup.


More information about the isabelle-dev mailing list