Email Gateway (Aug 19 2022 at 11:47): Email Gateway (Aug 19 2022 at 11:47):From: Christoph LANGE <math.semantic.web@gmail.com>
Dear Tobias, dear all,
let me divert one aspect of our private conversation back to the list,
as it may be of general interest.
You had pointed out that some of the lemmas in our *Utils.thy theories
at https://github.com/formare/auctions/tree/master/isabelle/Auction,
which provide useful additions to library concepts, were redundant with
the library.
You said that recent jEdit versions, like ProofGeneral, would point this
out automatically. Please excuse my stupid question, if it is stupid,
but this probably only holds for the post-2013 development version. In
Isabelle2013 I don't see any warnings displayed for such redundant
lemmas, but I would have to call "solve_direct" manually. (So, @Tobias,
sorry for wasting your time with making you review redundant lemmas!)
Some of the redundancies you'd pointed out (including
Relation.converse_mono) only exist in post-2013.
But this makes me wonder:
What is the best way for a 3rd party library maintainer (which I
consider myself) to cope with such improvements?
So far I had been reluctant to do so, as I had considered myself a
mere end user. I had been afraid of wasting time with bugs in the
development version, which I wouldn't understand as a non-expert, but
now it seems that I'm reinventing library functionality that already
exists in the development version.
We would like our formalisation to be reusable. There are no other
users so far, but we are advertising our library. And we are preparing
a submission of parts of it to the AFP. All that suggests that our
library should probably work with the last stable Isabelle release. And
that any functionality that's redundant with the latest development
version should only be removed once the next Isabelle release is out.
What would you recommend? Thanks for your advice!
Christoph
Email Gateway (Aug 19 2022 at 11:47):From: René Neumann <rene.neumann@in.tum.de>
In ProofGeneral at last (but probably also in jEdit), there is the
Isabelle setting "Auto Solve Direct" -- which has also been present in
Isabelle-2012 and -2013.
Email Gateway (Aug 19 2022 at 11:47):From: Tobias Nipkow <nipkow@in.tum.de>
Am 17/09/2013 10:33, schrieb Christoph LANGE:
Dear Tobias, dear all,
let me divert one aspect of our private conversation back to the list,
as it may be of general interest.You had pointed out that some of the lemmas in our *Utils.thy theories
at https://github.com/formare/auctions/tree/master/isabelle/Auction,
which provide useful additions to library concepts, were redundant with
the library.You said that recent jEdit versions, like ProofGeneral, would point this
out automatically. Please excuse my stupid question, if it is stupid,
but this probably only holds for the post-2013 development version. In
Isabelle2013 I don't see any warnings displayed for such redundant
lemmas, but I would have to call "solve_direct" manually. (So, @Tobias,
sorry for wasting your time with making you review redundant lemmas!)
I wasn't complaining. I did say that this was only added to jedit recently,
being unsure which version your are on.
Clearly you should only ship a version of your theories that work with a release
version of Isabelle. Putting your library into the AFP lets you have two
versions, release and development. We discussed that recently here:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-September/msg00013.html
In another project (CAVA) we decided to stick with the release version and I now
feel it would have been better to update to the development version more frequently.
Tobias
Some of the redundancies you'd pointed out (including
Relation.converse_mono) only exist in post-2013.But this makes me wonder:
- Should I switch to the development version?
What is the best way for a 3rd party library maintainer (which I
consider myself) to cope with such improvements?So far I had been reluctant to do so, as I had considered myself a
mere end user. I had been afraid of wasting time with bugs in the
development version, which I wouldn't understand as a non-expert, but
now it seems that I'm reinventing library functionality that already
exists in the development version.We would like our formalisation to be reusable. There are no other
users so far, but we are advertising our library. And we are preparing
a submission of parts of it to the AFP. All that suggests that our
library should probably work with the last stable Isabelle release. And
that any functionality that's redundant with the latest development
version should only be removed once the next Isabelle release is out.What would you recommend? Thanks for your advice!
Christoph
Email Gateway (Aug 19 2022 at 11:48):From: Makarius <makarius@sketis.net>
On Tue, 17 Sep 2013, Christoph LANGE wrote:
You said that recent jEdit versions, like ProofGeneral, would point this
out automatically.
Again an important official announcement about proper names:
* "jEdit" is a sophisticated text editor written in Java, see also
http://www.jedit.org/
* "Isabelle/jEdit" uses regular jEdit with some plugin and some
outermost application wrapper to deliver an implementation of the
idea of "Prover IDE" for Isabelle.
So "Isabelle/jEdit" is the name of the product, not "jEdit". Or do you
call "Proof General" after its editor just "Emacs"?
Since jEdit as a text editor is not as widely known as Emacs, I can
understand that people who get exposed to it for the first time via
Isabelle/jEdit then think the "jEdit" aspect would be sufficient to name
the product. Due to this potential of confusion, it is particularly
important to get the names right.
"jEdit" means http://www.jedit.org/ and "Isabelle/jEdit" means the default
Prover IDE of Isabelle.
More deeply, the main functionality of Isabelle/jEdit is actually provided
by the Prover IDE infrastructure of Isabelle/Scala and its Isabelle/ML
counterpart, which has replaced the old READ-EVAL-PRINT loop some years
ago. Thus other projects like Isabelle/Eclipse (from Newcastle) or Clide
(from Bremen) can benefit from many of its concepts, independently of the
Isabelle/jEdit front-end.
When you say "recent jEdit versions ... would point this out
automatically", it is actually the document-oriented prover infrastructure
of Isabelle PIDE that will support certain notions of "asynchronous print
function" and "query operation" natively in the coming Isabelle2013-1
release. On the surface this will give you spontaneous feedback from a
suite of "automatically tried" tools, but there is much more behind it
than a former quick-and-dirty implementation for Proof General done right.
I do have to insist in careful terminology here, since these are
scientifically relevant steps forward in the general understanding of
interactive theorem proving. (People who don't follow this are welcome to
go back to the HOL-Light TTY loop, CoqIDE, or even Proof General if they
enrol it its mailing list to help the last maintainers there to hold out.)
But this makes me wonder:
- Should I switch to the development version?
You should say "a development version", or "some development version" --
the latter in the sense of Hilber Choice in HOL (which is in constrast to
definite description from a singleton set).
Everybody is welcome to test-drive Isabelle repository snapshots at any
time, but one needs to develop a sense what a proper release is and what
an arbitrary snapshot is.
Presently we are getting close to release candidates for Isabelle2013-1,
so joining now on isabelle-dev you will participate in sorting out the
remaining problems, until Isabelle2013-1-RC1 ... RCn (n approximately 4)
become available for public testing in October / November 2013 (which will
be again on isabelle-users, not isabelle-dev.)
Note that I keep pointing out the difference of proper releases versus
arbitrary snapshots, because the very idea of software releases is
seriously endangered in recent years. We see that in particular with
Linux distributions, where the noisy masses are demanding more and more
"rolling releases" to get latest things more quickly (including latest
problems). That has done great harm to many Linux distributions, even
Ubuntu, and many of its bundled applications. The pressure to produce
things ever faster leads to a continous decline of software quality -- it
is just impossible to make a system that is "always on" stable and robust
for serious applications.
Testing Linux distributions for the coming Isabelle2013-1, I've already
reached a new level of desparation: not just Fedora again, but also plain
Ubuntu 13.04, which put my nicely working 12.04 LTS laptop into a totally
unstable system after update; and this is not even 13.10 beta, just
"stable" 13.04. This is getting close to Windows 95 quality -- and
Windows 8 is actually not too bad these days.
- What is the best way for a 3rd party library maintainer (which I
consider myself) to cope with such improvements?
That is a question of somewhat different dimension. AFP already does a
pretty good job to absorb many "library" things. Its content can grow for
a given, fixed Isabelle release. The AFP editors and contributors need to
develop this further over the years.
The key question right now and probably the start of this thread, is what
is the relation of adhoc additions to the core libraries of main
Isabelle/HOL vs. AFP. Only then you have to cope with arbitrary
repository snapshots.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC