Email Gateway (Aug 18 2022 at 20:33): Email Gateway (Aug 18 2022 at 20:33):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
how does sledgehammer decide which provers to use by default? After
installing yices, I can do
sledgehammer [yices]
to explicitly call yices. However, when using
sledgehammer
it seems that "just" spass, e, remote_vampire, remote_e_sine, and z3 are
run; but not yices. Can I change this globally (e.g., in my
etc/settings) without having to use sledgehammer_params or explicitly
setting options when calling sledgehammer?
cheers
chris
Email Gateway (Aug 18 2022 at 20:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
If you change it through the good old Proof General settings, I think it will do the right thing and remember it across sessions. Otherwise, no: That's what "sledgehammer_params" is for, and it would be tedious to emulate its functionality in "etc/settings" (e.g. to change the default timeout or whatever else...).
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 20:34):From: Lars Noschinski <noschinl@in.tum.de>
I'm fine with the default settings, so I don't have a need for this
functionality; but could you not just reuse the parser for
sledgehammer_params to parse a $SLEDGEHAMMER_PARAMS environment
variable, when you setup the default values?
-- Lars
Email Gateway (Aug 18 2022 at 20:34):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Let me reformulate ;). Why not use all installed provers by default? (If
I wouldn't want to use it I would hardly install a prover.)
-cheers chris
Email Gateway (Aug 18 2022 at 20:34):From: Makarius <makarius@sketis.net>
Note again that Isabelle Proof General is umaintained since October 2011,
so it has reached End-of-Life unless someone else stands forward to
continue its maintenance. (Pretty soon I will stop reminding people of
this, and then it is really dead.)
Concerning the current Isabelle/Scala and Prover IDE infrastructure, there
is still no persistent preferences mechanisms, but I am working on it.
Righ now one can imitate what Proof General did here by hand:
ML {* Sledgehammer_Isar.provers := "e spass vampire" *}
Makarius
Email Gateway (Aug 18 2022 at 20:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Christian,
It's a bit tricky -- e.g. we ship CVC3, which is then installed but it doesn't mean you want to use it. CVC3 and Yices don't yield unsat cores or usable proofs, so we have to use brute-force minimalization to get usable Metis proofs, which can be quite expensive.
How many cores do you have on your machine? If you have only 4, then E, SPASS, Vampire, Z3 is probably the best combination anyway. If you have 8, then what you describe would probably make sense. I think I'll change the default to do something along those lines.
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 20:34):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Yes, but then why not do it for Nitpick, Quickcheck, Refute? And what about other options, e.g. simplifier traces? Whatever we do, it's going to be tedious, inconsistent, or both.
Jasmin
Email Gateway (Aug 18 2022 at 20:34):From: Makarius <makarius@sketis.net>
That would indeed stretch the Isabelle system settings concept a bit far.
There are also physical limitations on the process environment size,
notably on Windows.
No need to worry about the above problems, though. At the next stage, the
Isabelle/Scala infrastructure will provide a concept of externalized
options, somehow in correspondence to internal configuration options, with
some support to make them persistent as preferences. So the tendency will
be to declare such options once and for all, and let the user modify them
either within the theory context, or as background default for the running
session.
Stay tuned ...
Makarius
Email Gateway (Aug 18 2022 at 20:35):From: Tobias Nipkow <nipkow@in.tum.de>
It is customary to continue maintaining a tool until the replacement is ready
for prime time. Currently jedit is not at the point (and PG still works). I
expect that PG will be kept in a working state until key jedit problems like
"Workaround: Cut/paste larger parts or reload buffer" and the absence of menus
(which force people to remember and type commands) have been eliminated.
Tobias
Email Gateway (Aug 19 2022 at 07:46):From: Makarius <makarius@sketis.net>
So who is continuing the maintenance of Proof General? It won't continue
to work magically without doing anything.
One of the reasons why Isabelle/jEdit is still not as complete as I would
like to have is the extra time that I have spent to keep Isabelle Proof
General working in the last 4 years.
This is why I have now stopped its maintenance after the Isabelle2011-1
release; the Isabelle2012 version of Isabelle/jEdit is sufficient to be
outside the critical range.
And again: I have now reason to see Isabelle Proof General broken too
early after so many years taking care of it. So I would welcome someone
standing forward to continue its maintenance. (It needs to be someone who
understands what maintenance of sofware systems means in general.)
Makarius
Email Gateway (Aug 19 2022 at 07:46):From: Tobias Nipkow <nipkow@in.tum.de>
Am 20/07/2012 16:43, schrieb Makarius:
On Fri, 20 Jul 2012, Tobias Nipkow wrote:
It is customary to continue maintaining a tool until the replacement is ready
for prime time. Currently jedit is not at the point (and PG still works). I
expect that PG will be kept in a working state until key jedit problems like
"Workaround: Cut/paste larger parts or reload buffer" and the absence of menus
(which force people to remember and type commands) have been eliminated.So who is continuing the maintenance of Proof General? It won't continue to
work magically without doing anything.
By default the person who introduced the tool in the first place or the one who
is responsible for the change that stops it functioning. That is you, I should
think.
One of the reasons why Isabelle/jEdit is still not as complete as I would like
to have is the extra time that I have spent to keep Isabelle Proof General
working in the last 4 years.This is why I have now stopped its maintenance after the Isabelle2011-1 release;
the Isabelle2012 version of Isabelle/jEdit is sufficient to be outside the
critical range.
For teaching it is still withing the critical range. We have first-hand
experience with students who are really frustrated because Isabelle/jedit
complains that there is something wrong with their text, but there isn't, the
incremental parsing has gone wrong.
And again: I have now reason to see Isabelle Proof General broken too early
after so many years taking care of it. So I would welcome someone standing
forward to continue its maintenance. (It needs to be someone who understands
what maintenance of sofware systems means in general.)
Of course it would be great if somebody did volunteer, but Larry pointed out
some of the obstacles.
Tobias
Email Gateway (Aug 19 2022 at 07:47):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
My personal preference would be for somebody who will be around in Chair 21 for the next 2 or 3 years at least. But if none of the people meeting this criterion (and the maintenance criterion) step forward, I'd be willing to step in at least for the next year and do the minimal amount of work needed to keep it running on our three main platforms with the latest Isabelle.
Being the maintainer of several binary packages already (e.g. E 1.6 this week again), I'm not exactly thrilled about the prospect, but I think we all agree that Proof General has to be maintained for a couple of years, until the late adopters run out of reasons not to use jEdit/PIDE.
Jasmin
Email Gateway (Aug 19 2022 at 07:47):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Larry wrote off-list that he would be willing to help with occasional Emacs Lisp programming.
Both of us are fervent adepts of Aquamacs. One of the first things we'd like to do is make that the default on the Mac again. Some issues were mentioned on the list but don't seem to affect me (with PG 3.7.1.1) or Larry (with PG 4.0?). Do you remember anything specific from the top of your head?
Jasmin
Email Gateway (Aug 19 2022 at 07:47):From: Makarius <makarius@sketis.net>
OK, so Jasmin and Larry will take care of it in the near future, until
some more Proof General adherents will join eventually. Some people could
also share their experience with old versions of PG and old versions of
Emacs on the Isabelle community wiki.
Jasmin and Larry, you should also get in touch with David Aspinall,
concerning recent PG repository versions. There has been quite some
activity recently, and last time I've checked it did not work on stock
Linux distributions with slightly old Emcas 23 anymore. (This is not
surprising, it has happenend routinely over the years.)
Makarius
Email Gateway (Aug 19 2022 at 07:47):From: Makarius <makarius@sketis.net>
Odd. I am not responsible for Apple changing Mac OS every 1-2 years,
Linux distributors changing Emacs versions, Emacs changing, PG itself
changing upstream etc. The few Isabelle changes that have ever affected
some PG version in the past are negligible compared to that, and are
usually quick and easy to repair if people report them quickly and
constructively.
It seems I have done maintainence too efficiently in the past, so that it
was almost invisible, and one could think systems just work on their own
and continue indefinitely.
Change is sometimes annyoing, but part of the normal software life-cycle.
An alternative to that is embalming of old versions in stasis: just last
year I've taken a stock Isabelle2005 release and made it work again with
XEmacs 21.x in the classic manner, with 100% of its nastalgic look and
feel, even real "X-Symbol" and the bitmap fonts of that time. But that
just showed again that there is subjective bit rot as well: what was fine
10 years ago is hardly bearable today. Even the most conservative PG user
would not want to continue 10 years with the same old version.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC