Email Gateway (Aug 18 2022 at 10:27): Email Gateway (Aug 18 2022 at 10:27):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
A question to the Isabelle developers:
Would it be possible to do bugfix-only Isabelle releases (like Isabelle
2005.1)?
Background: A while ago I had trouble using full proof objects with AWE
and was advised to replace src/Pure/proofterm.ML with the development
version of that file. Now everything is working perfectly, but I can't
give my work to others easily, because they first have to rebuild
Isabelle.
So if someone did an Isabelle point release whenever some bugfixes
accumulate, that would be really cool!
Thomas
PS: A small irregularity I just encountered: 'use_thy "SomeTheory"' only
works in interactive mode, not when creating PDFs. For these, I have to
wrap the command in 'ML {* *}'. Would be nice to make this consistent.
signature.asc
Email Gateway (Aug 18 2022 at 10:27):From: Makarius <makarius@sketis.net>
On Fri, 27 Apr 2007, Thomas Bleher wrote:
Isabelle 2005.1?
The next Isabelle release will be Isabelle2007. By leaving out
Isabelle2006 we have certainly created a number of problems, forcing some
users of the testing-unstable path of unofficial Isabelle development
snapshots. A proper Isabelle2007 is to be expected within the next few
months. After that, we will try hard to get back to the old release
scheme of 6-12 months between official versions.
Background: A while ago I had trouble using full proof objects with AWE
and was advised to replace src/Pure/proofterm.ML with the development
version of that file. Now everything is working perfectly, but I can't
give my work to others easily, because they first have to rebuild
Isabelle.
What is the problem? Just put this on your website an tell people how to
use your system. Building Isabelle is as easy as running Isabelle/build
(assuming that the underlying ML system has worked at some point).
Makarius
Email Gateway (Aug 18 2022 at 10:27):From: Makarius <makarius@sketis.net>
I don't understand what you are trying to do here. Importing theories
into the current theory works via the "imports" header specification.
The use_thy ML function should only occur in ROOT.ML to tell the system
where to start processing theories (it also allows to adjust some external
flags, such as no_document).
Makarius
Email Gateway (Aug 18 2022 at 10:28):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
An example from my theories:
theory NI imports Main
begin
typedecl "domain"
consts policy :: "domain => domain => bool" ("(_\ \<leadsto>\ _)" [46,46] 45)
axioms policy_refl: "u \<leadsto> u"
(* many more lemmas and defs *)
end
theory Example imports AWE
begin
ML {*
use_thy "NI";
*}
datatype "dom" = A | B | C
consts policy :: "dom => dom => bool" ("(_\ \<leadsto>\ _)" [46,46] 45)
primrec
"(A \<leadsto> y) = True"
"(B \<leadsto> y) = (y \<noteq> A)"
"(C \<leadsto> y) = (y = C)"
theorem policy_refl: "u \<leadsto> u"
by (induct u, auto)
thymorph s: NI \<longrightarrow> Example
maps [("NI.domain" \<mapsto> "dom")]
(* do something with it here... *)
end
I'd like to use the \<leadsto> abbreviation both in the original theory
and the translated one. For me it only worked when using "use_thy"
instead of "imports".
Anyway, this is all working very fine for me now, my (very small) point
was just that I was surprised that a plain "use_thy" worked in Proof
General, but not in document preparation mode (I had to wrap it in "ML
{* *}" when generating PDFs). I just had assumed that the two use the
same parser.
Thomas
signature.asc
Email Gateway (Aug 18 2022 at 10:28):From: Makarius <makarius@sketis.net>
Compiling takes 1-10 min. Producing an official Isabelle release takes
several days, and has further consequences on other derived distributions
(e.g. AFP).
That's a rather bad balance for something that is not really a problem in
the first place.
Makarius
Email Gateway (Aug 18 2022 at 10:28):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
It would, indeed, put additional strain on the developers to try to
isolate bug-fix improvements in the event of releasing a patch.
However, Thomas is one who has squashed the bug without introducing any
new features. How easy would it be for him to create and submit a patch
of his bugfix to the developers, to be made available in the same places
as the canonical Isabelle code?
To be fair: I can take no credit for fixing the problem. I mailed the
Isabelle developers in private and within a few hours Stefan Berghofer
had mailed me the fix. So they were very responsive in fixing the
problem.
The ML code which is handling the proofterms is way beyond my current
understanding of Isabelle, so I can't comment on the fix, except that it
is working very fine for me.
This way, the established developers get to verify the code and make it
available to all, without the maintenance overhead, and it /is/
distributed in a central forum. To me, this is the spirit of Free software.
Obviously I would like that very much, but I can understand that it may
be impossible due to time constraints.
Lawrence Paulson wrote:
All of your points are valid. With commercial software, patches are
(sometimes!) released for the last full version, so that people do not
have to buy the next one. This is not so easy for us, for we are all
volunteers. To issue releases that just fix bugs but involve no
development would force us to manage two development threads.Recompilation isn't that difficult, and you can of course post the
binaries on your Web site so that your users can pick them up.
Yeah, I will probably do that.
Thank you very much for your time and assistance!
Thomas
On 3 May 2007, at 14:55, Thomas Bleher wrote:
That's possible of course, but I think it would be better if you put out
an updated release. Reasons I think this would be useful:
- Psychological reasons. It just _feels_ wrong to modify a core part of
the prover just to use a theory.- The issue I mentioned is a bug in Isabelle2005, right? So why not fix
it once for all users, so noone else trips over it?- I'd rather download a precompiled package than spend the time to
compile it. Guess I have been spoiled by Debian ;-)
signature.asc
Email Gateway (Aug 18 2022 at 10:30):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
Makarius <makarius@sketis.net> [2007-04-30 13:12]:
That's possible of course, but I think it would be better if you put out
an updated release. Reasons I think this would be useful:
Psychological reasons. It just _feels_ wrong to modify a core part of
the prover just to use a theory.
The issue I mentioned is a bug in Isabelle2005, right? So why not fix
it once for all users, so noone else trips over it?
I'd rather download a precompiled package than spend the time to
compile it. Guess I have been spoiled by Debian ;-)
Thomas
signature.asc
Email Gateway (Aug 18 2022 at 10:32):From: Lawrence Paulson <lp15@cam.ac.uk>
All of your points are valid. With commercial software, patches are
(sometimes!) released for the last full version, so that people do
not have to buy the next one. This is not so easy for us, for we are
all volunteers. To issue releases that just fix bugs but involve no
development would force us to manage two development threads.
Recompilation isn't that difficult, and you can of course post the
binaries on your Web site so that your users can pick them up.
Larry
Email Gateway (Aug 18 2022 at 10:33):From: Robert Lamar <rlamar@stetson.edu>
It would, indeed, put additional strain on the developers to try to
isolate bug-fix improvements in the event of releasing a patch.
However, Thomas is one who has squashed the bug without introducing any
new features. How easy would it be for him to create and submit a patch
of his bugfix to the developers, to be made available in the same places
as the canonical Isabelle code?
This way, the established developers get to verify the code and make it
available to all, without the maintenance overhead, and it /is/
distributed in a central forum. To me, this is the spirit of Free software.
Robert
Lawrence Paulson wrote:
Last updated: May 03 2024 at 04:19 UTC