Email Gateway (Oct 02 2026 at 16:01): Email Gateway (Oct 02 2026 at 16:01):From: Lawrence Paulson via isabelle-dev <isabelle-dev@proof.cit.tum.de>
I am looking forward to the new support for CVC5 through Alethe. But could all those files be put in their own directory before the freeze tomorrow? We are putting up with 12 BNF files in the top level directory, but we don't need to do this again.
Larry
Email Gateway (Oct 02 2026 at 21:04):From: Makarius <makarius@sketis.net>
-------- Forwarded Message --------
Subject: Re: Alethe
Date: Fri, 2 Oct 2026 23:00:29 +0200
From: Makarius <makarius@sketis.net>
To: Lawrence Paulson <lp15@cam.ac.uk>, Lawrence Paulson via isabelle-dev
<isabelle-dev@proof.cit.tum.de>
On 02/10/2026 18:00, Lawrence Paulson via isabelle-dev wrote:
I am looking forward to the new support for CVC5 through Alethe. But could all those files be put in their own directory before the freeze tomorrow? We are putting up with 12 BNF files in the top level directory, but we don't need to do this again.
You probably mean the many .thy files of the HOL session: this is the proper
representation of its structure. I count session sub directories with theories
here and there as a bad thing --- it introduces an uncertainty what the
sources really are, and also makes the session hard to browse.
At this stage of the release process we should also concentrate on really
important things, like the Sledgehammer observations by Peter Lammich
01-Oct-2026 (RC2).
Makarius
Email Gateway (Oct 03 2026 at 09:36):From: Makarius <makarius@sketis.net>
On 02/10/2026 23:02, Makarius wrote:
-------- Forwarded Message --------
Subject: Re: Alethe
Date: Fri, 2 Oct 2026 23:00:29 +0200
From: Makarius <makarius@sketis.net>
To: Lawrence Paulson <lp15@cam.ac.uk>, Lawrence Paulson via isabelle-dev
<isabelle-dev@proof.cit.tum.de>On 02/10/2026 18:00, Lawrence Paulson via isabelle-dev wrote:
I am looking forward to the new support for CVC5 through Alethe. But could
all those files be put in their own directory before the freeze tomorrow? We
are putting up with 12 BNF files in the top level directory, but we don't
need to do this again.
You probably mean the many .thy files of the HOL session: this is the proper
representation of its structure. I count session sub directories with theories
here and there as a bad thing --- it introduces an uncertainty what the
sources really are, and also makes the session hard to browse.
I have spent 5 more minutes o Alethe: there are approx. 10 relatively small
.thy files, most of them could be just one Alethe.thy and another one for
Alethe_Real.thy, for example. This is not relevant for the release, and won't
happen now.
After the release we shall have an appointment with Hanna Lachnit to sort out
various questions. Notably about generated sources by the IsaRARE tool, the
use of 'named_theorems" etc.
Makarius
Email Gateway (Oct 05 2026 at 08:43):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
At this stage of the release process we should also concentrate on really important things, like the Sledgehammer observations by Peter Lammich 01-Oct-2026 (RC2).
Indeed. I'm looking into the Sledgehammer issue.
Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette
On 2. Oct 2026, at 23:02, Makarius <makarius@sketis.net> wrote:
-------- Forwarded Message --------
Subject: Re: Alethe
Date: Fri, 2 Oct 2026 23:00:29 +0200
From: Makarius <makarius@sketis.net>
To: Lawrence Paulson <lp15@cam.ac.uk>, Lawrence Paulson via isabelle-dev <isabelle-dev@proof.cit.tum.de>On 02/10/2026 18:00, Lawrence Paulson via isabelle-dev wrote:
I am looking forward to the new support for CVC5 through Alethe. But could all those files be put in their own directory before the freeze tomorrow? We are putting up with 12 BNF files in the top level directory, but we don't need to do this again.
You probably mean the many .thy files of the HOL session: this is the proper representation of its structure. I count session sub directories with theories here and there as a bad thing --- it introduces an uncertainty what the sources really are, and also makes the session hard to browse.At this stage of the release process we should also concentrate on really important things, like the Sledgehammer observations by Peter Lammich 01-Oct-2026 (RC2).
Makarius
Last updated: Oct 05 2026 at 16:54 UTC