Email Gateway (Aug 19 2022 at 13:47): Email Gateway (Aug 19 2022 at 13:47):From: Van Staden Stephan <stephan.vanstaden@inf.ethz.ch>
Dear all,
I have some trouble configuring a fresh Isabelle2013-2/jedit installation:
It seems that sledgehammer only invokes "e" and "spass". How can I configure it to invoke more solvers (e.g. those that Isabelle2011 invoked by default)? It would be best if this is a persistent configuration setting, so that I don't have to repeat it every time I launch Isabelle or sledgehammer.
Auto completion used to show a drop-down box with the sigma character when I typed "sig". Similarly, it used to show an existential quantifier when I typed "exists". This does not work anymore. How can I turn it on again?
Many thanks,
Stephan
Email Gateway (Aug 19 2022 at 13:47):From: John Wickerson <johnwickerson@cantab.net>
I know the answer to the second: you have to type "\sig" rather than "sig" nowadays.
John
Email Gateway (Aug 19 2022 at 13:48):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Stephan,
for 1,
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/sledgehammer.pdf
gives you details on how to set the necessary shell variables. If on Windows, you should start the batch file that gives you a cygwin prompt and then go ahead. Read the section 2 Installation.
Email Gateway (Aug 19 2022 at 13:48):From: Van Staden Stephan <stephan.vanstaden@inf.ethz.ch>
Hi Buday,
I'm afraid this does not solve my problem. The shell variables help to locate local (as opposed to remove) solvers, but I want to invoke remote ones plus the standard ones that come with Isabelle2013-2.
Stephan
Email Gateway (Aug 19 2022 at 13:48):From: Makarius <makarius@sketis.net>
That actually depends on your number of Isabelle/ML worker threads, which
is determined from the number of harware cores.
Sledgehammer has some builtin smartness to guess which provers you want.
But that is not immediately obvious, and based on assumptions from TTY /
Proof General interaction, where the ML process is idle waiting to process
the next command, and then has all cores available. These assumptions no
longer hold in Isabelle/jEdit, where many things can run in parallel all
the time --- which was the whole point of the exercise to go beyond TTY /
Proof General several years ago.
Sledgehammer defaults need to be sorted out again for the next release
(summer 2014), to make it clear and simple what the configuration is, and
where it is actually configured.
Until then, you can write the list of provers for Sledgehammer into the
"Provers" entry field in the Isabelle/jEdit Sledgehammer panel. Then type
RETURN to run it and make that content persistent in the history of the
text field. Next time, the field content will default again to the
dynamic smart value provided by Sledeghammer from Isabelle/ML, but you can
select an alternative from your GUI history, using the triangle or
right-click on the field as usual in jEdit.
Makarius
Email Gateway (Aug 19 2022 at 13:48):From: Makarius <makarius@sketis.net>
The last two sentences are the typical user-reflex to get back to
something familiar as quick as possible, and missing the main points of
improvements that happened in the meantime.
Whenever there is a user-relevant change, the NEWS file is the first point
to look. It is easily available via the Documentation panel, entry
"NEWS", in particular it says:
* Improved completion mechanism, which is now managed by the
Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
Moreover, it is vital to look around what is new, otherwise important NEWS
are missed like this one:
* New manual "jedit" for Isabelle/jEdit, see isabelle doc or
Documentation panel.
That manual also has some section on completion, but it still demands some
study and experimentation to see how the mechanism actually works. That
time is well-invested, though, since typing stuff into the text-buffer is
done all the time, and knowing its options and possibilities helps to
become more productive.
That does not mean that it is the final word to completion in
Isabelle/jEdit. I have already further ideas in the back-hand, and more
might emerge from experience reports by people who have worked with it for
some time, leaving old things behind and looking towards new things.
Makarius
Email Gateway (Aug 19 2022 at 13:48):From: Makarius <makarius@sketis.net>
You can press the Apply button, but it does not mean you must. Just
because there is one (obvious) way does not mean that there are no others.
When the Sledgehammer panel gains focus, its "Provers" field becomes
active, and RETURN will run the main operation.
I leave it as an exercise to find out more than one way to have a jEdit
dockable window gain focus, just by keyboard control. I don't even know
all this myself -- jEdit is very flexible, without making it too heavy or
bloated.
Moreover the specific "action" isabelle-sledgehammer might help to apply
general principles of jEdit. See again the Isabelle/jEdit manual and its
included link to the jEdit documentation.
Makarius
Email Gateway (Aug 19 2022 at 13:48):From: Makarius <makarius@sketis.net>
That seems to be mostly outdated, from long ago when there were no
"Isabelle components" yet. I don't know anything about the practical
relevance of the zoo of exotic provers, but the main ones are already
included in the Isabelle distribution.
The remote Z3 server at TUM disappeared without anybody taking notice.
Makarius
Email Gateway (Aug 19 2022 at 13:49):From: Gergely Buday <gbuday@gmail.com>
Some people would like to use higher-order provers Satallax and
LEO-II. Would it be possible to include them in the distribution? I
guess relying on ocaml is not necessary welcome as it would add an
additional dependency. What do you think? At the end of March I would
have some free time for creating the automatic building.
Email Gateway (Aug 19 2022 at 13:59):From: Makarius <makarius@sketis.net>
There is no need for automatic building -- Isabelle is not another Linux
distribution or package repository. What is required is routine
multi-platform support as described in
http://isabelle.in.tum.de/repos/isabelle/file/972f0aa7091b/Admin/PLATFORMS
By coincidence Jasmin and myself are maintaining most of these Isabelle
components that end up in the final release. Ultimately, such components
need to be work routinely for all users on all platforms according to the
above specification.
Makarius
Email Gateway (Aug 19 2022 at 13:59):From: Gergely Buday <gbuday@gmail.com>
Makarius wrote:
But how to provide this multiplatform support other than building it
for the different platforms? Should I provide binaries only?
Last updated: Apr 30 2024 at 04:19 UTC