Email Gateway (Aug 22 2022 at 09:08): Email Gateway (Aug 22 2022 at 09:08):From: "W. Douglas Maurer" <maurer@gwu.edu>
Under NEWS, in Release notes, there is a history of user-relevant
changes in Isabelle2014. Now that Isabelle2015 is available for
testing, can the changes in Isabelle2015 also appear under NEWS? That
way, we all should be able to produce modified versions of our
Isabelle2014 files before Isabelle2015 actually comes out, so we can,
as the expression goes, "hit the ground running." -WDMaurer
Email Gateway (Aug 22 2022 at 09:08):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Douglas,
Release notes are available in the NEWS file that is part of
Isabelle2015-RC0 (the tar-archive Makarius put online) in case you are
still interested.
cheers
chris
Email Gateway (Aug 22 2022 at 09:08):From: Makarius <makarius@sketis.net>
The NEWS file is already more than 99% finished and in its usual place: in
the top-level directory of the Isabelle distribution or in the
Documentation panel, the one that is wide open on first startup.
There is now also a note in the NEWS:
Isabelle/jEdit shows a tree-view of this file in Sidekick.
Makarius
Email Gateway (Aug 22 2022 at 09:09):From: Makarius <makarius@sketis.net>
Yes, the 'private' keyword is exactly for this kind of application. The
isar-ref manual adds this explanation:
Neither a global @{command theory} nor a @{command locale} target
provides a local scope by itself: an extra unnamed context is required
to use @{keyword "private"} or @{keyword "qualified"} here.
Makarius
Email Gateway (Aug 22 2022 at 09:09):From: Christian Sternagel <c.sternagel@gmail.com>
It would be nice to have a concrete version (i.e., changeset id) of the
AFP to test against, since most of my work is built on top of the AFP.
Otherwise I can only test the RC against contrived examples.
cheers
chris
Email Gateway (Aug 22 2022 at 09:09):From: Christian Sternagel <c.sternagel@gmail.com>
One minor issue (that has been there before; but it seems a good time to
change it now) is that sometimes when a pop-up is involved (e.g., saving
for the first time, searching, etc.) afterwards the focus is lost (from
the current buffer, that is).
It would be more convenient if the focus would return to the "widget"
that had it before any pop-up occurred.
cheers
chris
Email Gateway (Aug 22 2022 at 09:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Makarius,
export_code "gcd::int⇒int⇒int" in SML
fails in Isabelle2015-RC0, with message:
Dependency "int" :: "semiring_div_parity" -> "int" ::
"semiring_parity" would result in module dependency cycle
while it works fine in Isabelle2014.
Best,
Wenda
Email Gateway (Aug 22 2022 at 09:09):From: Lars Noschinski <noschinl@in.tum.de>
I just noticed that oops does not work in a notepad:
theory Scratch imports Main begin
notepad begin
have False
oops
The oops fails with the following error message:
Illegal application of command "oops"⌂ in proof mode
I find this error message irritating (because usually oops works just
fine in proof mode). Also, I would like to use oops in notepads to mark
failed proof attempts (in contrast to incomplete ones, where I would use
sorry).
-- Lars
Email Gateway (Aug 22 2022 at 09:09):From: Lars Hupel <hupel@in.tum.de>
I encountered a similar problem a while ago:
<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/9323>
Sometimes, these kinds of cycles cannot be avoided in the code generator
setup. The workaround is trivial, though:
export_code "gcd::int⇒int⇒int"
in SML module_name GCD
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:09):From: Lars Noschinski <noschinl@in.tum.de>
On 13.04.2015 15:06, Lars Noschinski wrote:
On 11.04.2015 21:49, Makarius wrote:
Any problems, observations etc. can be discussed here on the mailing
list. Quite often a change of behaviour is perceived as a problem, and
sometimes it is one, sometimes not. In any case, open discussion
helps to figure out what is potentially confusing to users.
I just noticed that oops does not work in a notepad:
This is documented in the NEWS file, but the error message is still
irritating.
The oops fails with the following error message:Illegal application of command "oops"⌂ in proof mode
I find this error message irritating (because usually oops works just
fine in proof mode).
Email Gateway (Aug 22 2022 at 09:10):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius
I found an inconvenient jEdit error reporting behavior:
I loaded theory A
theory A imports B C D E
Isabelle does not load my theory A and stops processing. I get the
same behavior as if there is an error somewhere in the imported files
B C D E. However, jEdit does not show me an error message. Let's say
theory C starts the following:
theory C imports "$VAR/XYZ"
where $VAR is an environment variable usually set in my Linux
environment, which I accidentally misspelled. When I open theory C, I
get the expected error message "Undefined environment variable: VAR".
However, it is hard to find that the error is in theory C because the
theory panel does not display an error and in theory A, there is also
no indication why isabelle does not process it.
Expected behavior: Red error shown in theory panel at theory C
Observed behavior: No error in theory panel
Cornelius
Email Gateway (Aug 22 2022 at 09:10):From: Makarius <makarius@sketis.net>
On Mon, 13 Apr 2015, Christian Sternagel wrote:
It would be nice to have a concrete version (i.e., changeset id) of the
AFP to test against, since most of my work is built on top of the AFP.
Unfortunately, I don't know any corresponding AFP version. I had so many
unexpected problems to make the Isabelle2015-RC0 at all that I forgot to
relate it to AFP formally --- and the snapshot itself is semiformal
anyway.
After some weeks of relative quiet and stable repositories for Isabelle
and AFP, the rumor of the coming release deadline has aroused many
last-minute changes. I hope that towards the end of the week we can see a
truely stable Isabelle2015-RC1 together with a working AFP.
Otherwise I can only test the RC against contrived examples.
Maybe it is better to try with arbitrary repository snapshots at the
moment, shooting blindly into the erratic movements.
Makarius
Email Gateway (Aug 22 2022 at 09:11):From: Makarius <makarius@sketis.net>
It would be interesting to know in which sense jEdit locked up.
Sometimes there is just a deadlock on the GUI thread. Sometimes the JVM
is blocked in a way that it requires a kill -9; jps and jconsole might
help to guess in the right direction.
For example, I routinely get the following GUI lock-up on Xubuntu 14.10
with GTK look-and-feel: if Isabelle/jEdit is started up and its main
window de-focused before it is fully there, it will never get back to a
normal state, where user input is possible. It might be a fundamental
problem of the unsupported XFCE window manager together with the almost
unsupported GTK L&F, but I need the latter to get proper GUI scaling for
my brand-new 4K display -- the newer Nimbus L&F can't do that.
Java/AWT on Linux is not the best combination -- we know this already for
approx. 3 years. Even though I am mostly Linux user myself, it is only a
secondary platform for fancy GUI and IDE stuff. Mac OS X and Windows work
much better in many respects.
Makarius
Email Gateway (Aug 22 2022 at 09:11):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The last time the AFP tested cleanly was
AFP version: development -- hg id c1fe405c1a0d
Isabelle version: devel -- hg id 070f04c94b2e
Test ended on: macbroy2, Thu Apr 9 14:50:44 CEST 2015.
Since then things have fluctuated, but hopefully converging to a working AFP version again soonish.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:12):From: Lars Hupel <hupel@in.tum.de>
Hello,
I have not worked with RC0 extensively yet. So far I've noticed a small
oddity:
ML‹Local_Theory.note›
The markup produced for the type of this expression is
val it = fn: ?.binding * thm list -> local_theory -> (string * thm list)
I expected to see 'Attrib.binding' there. OTOH, if I explicitly
construct a value of that type:
ML‹(@{binding foo}, []): Attrib.binding›
... the markup correctly reports
val it = ("foo", []): Attrib.binding
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:12):From: Lars Noschinski <noschinl@in.tum.de>
I have occasionally problems with hovering, in the sense that popups do
not appear (at least not in a reasonable amount of time). I have not
been able to discern a pattern, so here are some observations:
* Most of the time, everything works fine.
* Sometimes, I do not get popups at all (but clicking still works).
* Sometimes, I get popups at some places, but not in other places
(even in the same file on the same screen).
* Forcing Isabelle to reprocess by changing some part above (or
cutting and pasting the relevant part) does not seem to help.
* Once, popups didn't work for some part at the top of the screen.
Scrolling up helped. When I scrolled down again, I couldn't get the
popup anymore. This was repeatable.
* Usually, it vanishes after a restart, but some files seem to trigger
this behaviour more easily (or there are some external conditions
which cause this?). While writing this mail, I had to restart jEdit
a few times, till I got working popups in a certain file.
Afterwards, I worked reliably; even after more restarts.
This is not due to a grey-out or pink-out.
I had this behaviour with 2015-RC0 in an almost standard configuration
(smaller fontsize and a few additional keybindings)
-- Lars
Email Gateway (Aug 22 2022 at 09:12):From: Lars Noschinski <noschinl@in.tum.de>
on a Debian testing with a standard Gnome 3.14.
Email Gateway (Aug 22 2022 at 09:14):From: Makarius <makarius@sketis.net>
The Sledgehammer panel takes exactly the provers that are specified in the
input field, taking the system option "sledgehammer_provers" as default.
The 'sledgehammer' command takes a prefix of certain default provers,
depending on the nominal number of ML worker threads (which is derived
from the system option "threads").
It is up to Jasmin Blanchette to unify/simplify this further. Note that
in Isabelle2015, Sledgehammer still has various old modes stemming from
the TTY age (which has already ended).
Generally, Isabelle2015 has various changes of parallel document
processing, such that long-running print functions should no longer lead
to exhaustion of worker threads as before. This should improve the degree
of parallelism with the Sledgehammer panel vs. ongoing edits. If there are
remaining problems with it, the coming weeks of Isabelle2015-RC testing
are an opportunity to report them.
Makarius
Email Gateway (Aug 22 2022 at 09:14):From: Makarius <makarius@sketis.net>
On Sun, 12 Apr 2015, C. Diekmann wrote:
I found a "feature request" for the jEdit interface: I loaded
WordLemmaBucket from autocorres, a file with 5900 lines. There are at
least two errors near the end of the file when loading with 2015-RC0.
However, it is nearly impossible to locate the errors in the .thy.
Where can I see this file?
Is it possible to have some sort of "jump to next error" or an automatic
jump to the error when I click on the red spot (left of the jEdit scroll
bar)?
This feature is still not there after several years, because other things
had a much higher priority.
Also, when I have an error in my theory, e.g. writing "where f=..." but
in 2015-RC0 it should be "where f1=...", only the "f" is underlined,
this makes the error quite hard to spot for me.
That is a consequence of a more precise error position: it is a normal
trend in ongoing PIDE conformity improvements.
What is your font size? (Mine is 30px on a 4K display.) The error should
be also visible in the Output panel.
Makarius
Email Gateway (Aug 22 2022 at 09:14):From: Makarius <makarius@sketis.net>
This sounds like another episode of Linux window manager forks vs.
Java/AWT/Swing/look-and-feel. What is your local configuration in this
respect?
I've made some basic tests with some jEdit dialogs on Mac OS X, Windows,
Xbuntu, and did not encounter any problems.
Makarius
Email Gateway (Aug 22 2022 at 09:14):From: Christian Sternagel <c.sternagel@gmail.com>
Same old:
Fedora 21
GNOME Version 3.14.2
3.19.3-200.fc21.x86_64 GNU/Linux
cheers
chris
Email Gateway (Aug 22 2022 at 09:14):From: Lars Hupel <hupel@in.tum.de>
I've toyed around with the various '_deps' commands a bit. I do like the
new graph viewer. Here are my observations:
The new viewer is a jEdit panel, which means it always stays on top
unless it's minimized (my environment: KDE 4.x). Could this be changed,
possibly for all panels, so that it does not stay on top, or is this a
jEdit limitation? Most desktop environments offer a shortkey to force
such behaviour anyway, so I could just enable it on the spot if I wanted to.
'thy_deps' offers no possibility to fold heaps. Was that a deliberate
decision? In my current development I have about 3-4 layered images and
would like to fold them.
Most applications offer zooming by scrolling while pressing Ctrl. In
the viewer, I can't do that. (For the records, the old graph viewer also
didn't offer this.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:14):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 17 Apr 2015, at 12:09 am, Makarius <makarius@sketis.net> wrote:
On Sun, 12 Apr 2015, C. Diekmann wrote:
I found a "feature request" for the jEdit interface: I loaded WordLemmaBucket from autocorres, a file with 5900 lines. There are at least two errors near the end of the file when loading with 2015-RC0. However, it is nearly impossible to locate the errors in the .thy.
Where can I see this file?
I think Cornelius means this file:
https://github.com/seL4/l4v/blob/master/lib/WordLemmaBucket.thy
I’ve just started a 2015 branch of this whole development for catching up with Isabelle and hope to be able to publish it later today with at least Simpl updated.
If there is anyone else already working on updating C-Parser/AutoCorres, please let me know. I’d very much like to avoid duplication of work.
We plan to make C-Parser and AutoCorres AFP submissions after the 2015 release, but that will still need some cleanup work before. (For instance the infamous WordLemmaBucket above).
Is it possible to have some sort of "jump to next error" or an automatic jump to the error when I click on the red spot (left of the jEdit scroll bar)?
This feature is still not there after several years, because other things had a much higher priority.
I’ve also found errors a bit hard to find for large files in the past, but yes, there are probably higher priority items for now.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:14):From: Lars Hupel <hupel@in.tum.de>
I've attached a small demo theory which exhibits some strange behaviour
when using Sledgehammer on a goal containing a conjunction. I've marked
the problematic statement with (* HERE *).
Steps to reproduce:
1) Go to the blank line between 'defer' and 'sorry'.
2) In the Sledgehammer panel, select provers 'e spass z3 remote_vampire
cvc4' and click 'Apply'.
3) All provers will suggest 'apply simp'.
4) 'apply simp' doesn't solve the first subgoal.
What's even more confusing is that if I invoke sledgehammer via the
command, I get different results for cvc4:
"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).
I've suspected that somehow the 'defer' is at fault here, but even if it
is removed, there's more strange behaviour. In that case, the panel
correctly suggests 'apply auto[1]' (which in fact solves the subgoal),
but the sledgehammer command suggests:
"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).
"remote_vampire": Try this: using term.collapse(1) apply presburger (0.0
ms).
The latter invocation does not solve the subgoal. While I know that
sometimes Sledgehammer suggests an invocation of 'metis' which takes too
long (and might not be able to solve it?), I've never encountered this
with the new (and very helpful) suggestions of 'simp' or 'auto'.
Cheers
Lars
Scratch.thy
Email Gateway (Aug 22 2022 at 09:16):From: Makarius <makarius@sketis.net>
On Fri, 17 Apr 2015, Lars Hupel wrote:
I've toyed around with the various '_deps' commands a bit. I do like the
new graph viewer.
I have made more last-minute refinements of it in Isabelle2015-RC1, and
subsequently I refer to that version.
- The new viewer is a jEdit panel, which means it always stays on top
unless it's minimized (my environment: KDE 4.x). Could this be
changed, possibly for all panels, so that it does not stay on top, or
is this a jEdit limitation? Most desktop environments offer a shortkey
to force such behaviour anyway, so I could just enable it on the spot
if I wanted to.
This panel behaviour was newly introduced in Isabelle2014 -- I
specifically patched the jEdit docking framework for that (most of that
was accepted by the jEdit maintainers for a future release). The problem
is that Java/AWT does not really know about window managers. There are
three different classes doing similar things: JWindow, JFrame, JDialog --
they merely differ in accidental window manager hints.
Since Isabelle2014 we are using JDialog instead of JFrame, because these
windows stay on top of the main editor frame. This might be occasionally
odd, especially on Linux, but on Mac OS X and Windows it is essential to
work properly. Otherwise, windows could end up in an unreachable position
behind the main window, e.g. when working in the full-screen mode that is
now very common on these platforms.
All this behaviour is somehow hardwired into JWindow, JFrame, JDialog, and
cannot be changed. It is just a matter of choosing the smallest evil by
default. Once on Stackoverflow in the "java" and "swing" areas, I asked
critical questions about these three classes, but I got quickly removed
by some guys with a lot of points, although someone else had marked this
as "favourite question".
- 'thy_deps' offers no possibility to fold heaps. Was that a deliberate
decision? In my current development I have about 3-4 layered images
and would like to fold them.
Both thy_deps and class_deps have ways to specify intervals of the
hierarchy to be visualized. It would be better to have that in the GUI,
but that is more work and experimental tinkering, instead of a bit of
filtering output in Isabelle/ML.
For Isabelle2015, the priority was to have the new graphview (new since
Sep-2012) in a usable state. So I spent about 2-3 weeks on it, and the
TODO list was longer afterwards than before. Nonetheless, it should be
usable now, and actually do the same graph layout than the old browser
from 1996.
- Most applications offer zooming by scrolling while pressing Ctrl. In
the viewer, I can't do that.
The new Graphview did have some Google-Maps-style zooming before I started
working on it, but it did not quite work, so I removed it (like many other
unfinished things). The present version is meant to approximate the old
browser from the bottom, although many add-on features have again crept
into it.
I would also like to see better zooming, but instead of C-mouse-wheel, I
find myself looking for zoom-width or zoom-height buttons like good old
Evince on Linux, before it got changed into unusablity about 1-2 years
ago.
I would also like to see all zoom facilities moving uniformly in
Isabelle/jEdit, e.g. the zoom for the Output panel and others. But that
is avantgarde, and for a later release.
Makarius
Email Gateway (Aug 22 2022 at 09:16):From: Stephen Westfold <westfold@kestrel.edu>
I would vote to make this feature a higher priority. I’ve wasted a lot of time dragging the scroll bar to find hidden errors, but I suppose my use case is unusual in that I am automatically generating large proof files.
Stephen
Email Gateway (Aug 22 2022 at 09:17):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Doing things similar to Stephen, I would also like this feature. In a large theory you lose
precision with the scroll bar and clicking red marks does not take you to exactly where the error is.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:17):From: Makarius <makarius@sketis.net>
On Fri, 17 Apr 2015, Stephen Westfold wrote:
On Apr 16, 2015, at 4:09 PM, Makarius <makarius@sketis.net> wrote:
On Sun, 12 Apr 2015, C. Diekmann wrote:
Is it possible to have some sort of "jump to next error" or an
automatic jump to the error when I click on the red spot (left of the
jEdit scroll bar)?This feature is still not there after several years, because other
things had a much higher priority.I would vote to make this feature a higher priority.
It has already a relatively high priority (for some years), but there are
more important things in the pipeline system that prevented it from
getting through so far. The question is about scaling to large
developments. There are at least two dimensions: (1) length of individual
files, (2) total number of files within a session (or "project").
jEdit as a text editor is not very good at handling files that are longer
than 100-500Kb. Isabelle/jEdit as a Prover IDE is also struggling to
render the rich markup in real-time for big files. Both has improved a
bit over the years, but there are fundamental limitations.
Instead it is better to scale into the dimension of the project size and
structure. Maintenance of existing Isabelle and AFP sessions has many
awkward limitations that don't have to be there. Like the artificial
division into "session base images". I would like to see an easy way to
open the IDE and edit all Isabelle + AFP theories on the spot, without
having to think much about it something as artificial as "compiled logic
images".
I’ve wasted a lot of time dragging the scroll bar to find hidden errors,
but I suppose my use case is unusual in that I am automatically
generating large proof files.
Here we are back to the canonical question: What is the purpose of
generated files? Is there no better way?
For some reason, generating source files is the first idea that most
people have, and cannot imagine other ways. It is like a spell that needs
to be broken. There might be occasionally good reasons to do that, but
one should look critically at the problem, and prove that it really has to
be done like that.
Isabelle/HOL-SPARK is a simple example to do better. More such work can
be imagined in integrating different tools into the Isabelle Prover IDE,
without having machine-generated sources edited by humans.
Makarius
Email Gateway (Aug 22 2022 at 09:17):From: Lars Hupel <hupel@in.tum.de>
I'd also like to point out again my ongoing work on 'libisabelle' [0].
The README is slightly outdated, since the library is in fact able to
fetch and unpack an Isabelle distribution (setting appropriate
environment variables and building sessions is not implemented yet). I'm
also working on supporting multiple Isabelle versions at the same time.
It has already been demonstrated that this way of interaction works well
for sending proof obligations generated via other means to the prover to
have them checked. Right now, I'm also investigating how much useful
information I can get from the prover for performing further (syntactic)
analysis on theory sources. From that perspective, I tend to agree with
Makarius: There are very few remaining use cases of textual code
generation or manual interaction with the prover [2].
NB: Viorel's use case from earlier this month [1] can also be trivially
modelled with libisabelle.
Cheers
Lars
[0] <https://github.com/larsrh/libisabelle>
[1]
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-April/msg00066.html>
[2] Lem (<https://bitbucket.org/Peter_Sewell/lem/>) comes to mind.
Email Gateway (Aug 22 2022 at 09:17):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
I can't speak of Stephen's use case, but I myself am generating C code and, at the same time,
generating correctness proofs of such code. The generated C code interoperates with hand-written C
code. A goal is for the generated lemmas to be usable in a manual proof of a top-level hand-written
correctness statement.
While it is true that generating textual theories like this is not the only way, it still seems the
path of least resistance to me. We are using a translation validation style approach to verify this
generation process, so it is important that we can inspect the resulting artefact. It is also
helpful for users to be able to inspect these theories and see lemmas and proofs in the manner they
would be expecting to have written them themselves. Alternatively we could be generating proof terms
directly or using something like libisabelle. While not a fundamental obstacle, it is a pragmatic
barrier that our code generator (which also produces Isabelle theories) is written in Python and is
not easily portable to a JVM language.
It's perhaps also worth noting that manual interaction within these large theories is _not_ the
intended use case. I am primarily exploring these theories within Isabelle/jEdit when debugging a
broken proof the theory generator has produced. Overall, I'm not wed to my current approach, but
from my current understanding it is still the most feasible way for me to pursue this. If someone
wants to try to persuade me otherwise, I am more than happy to listen :)
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:18):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
This indicates that “max_threads” is 2. By default, Sledgehammer will use only as many cores as are reported to it. “max_threads” itself is set up through various options, about which I have little clue. If you have more than 2 cores on your machine, something is fishy.
Incidentally, this behavior of Sledgehammer is nothing new. Is the issue really new with Isabelle2015-RC0? What happens if you write
ML {* Multithreading.max_threads_value () *}
in Isabelle2014 vs. Isabelle2015-RC0?
Jasmin
Email Gateway (Aug 22 2022 at 09:18):From: "C. Diekmann" <diekmann@in.tum.de>
Both report "2". I have a dual core cpu with 2 physical cores and
thanks to hyperthreading two additional virtual cores. /proc/cpuinfo
lists 4 processors.
Cornelius
Email Gateway (Aug 22 2022 at 09:19):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Then I presume Sledgehammer also invoked only two ATPs in Isabelle2014?
Irrespective of this, you probably want to check the Isabelle system manual to find out how to change the number of threads. 2 is perhaps needlessly low.
Jasmin
Email Gateway (Aug 22 2022 at 09:19):From: "C. Diekmann" <diekmann@in.tum.de>
2015-04-20 18:26 GMT+02:00 Jasmin Blanchette <jasmin.blanchette@inria.fr>:
On 20.04.2015, at 16:19, C. Diekmann <diekmann@in.tum.de> wrote:
Incidentally, this behavior of Sledgehammer is nothing new. Is the issue really new with Isabelle2015-RC0? What happens if you write
ML {* Multithreading.max_threads_value () *}
in Isabelle2014 vs. Isabelle2015-RC0?
Both report "2". I have a dual core cpu with 2 physical cores and
thanks to hyperthreading two additional virtual cores. /proc/cpuinfo
lists 4 processors.Then I presume Sledgehammer also invoked only two ATPs in Isabelle2014?
Yes
Irrespective of this, you probably want to check the Isabelle system manual to find out how to change the number of threads. 2 is perhaps needlessly low.
Thanks for the pointer.
Cornelius
Email Gateway (Aug 22 2022 at 09:21):From: Makarius <makarius@sketis.net>
This nominal number of ML threads is critical for overall system
performance. CPUs today usually have much more virtual hardware threads
than actual CPU cores (due to Intel hyperthreading and similar AMD
technology). Asking the system about the CPU number in old-fashioned ways
leads to a number of threads that maximizes CPU cycle burning, without
much gain of performance, often a loss of it. CPU cycle burning is
particularly bad on mobile devices.
This also explains why PIDE was often perceived as unbearably slow in the
past: the defaults were not right, and most users did not know how to tune
the Harley Davidson themselves.
David Matthews has already provided more refined CPU query operations for
the Poly/ML runtime system already for Isabelle2014. It should be mostly
the same for Isabelle2015-RC1. This means the default
Multithreading.max_threads_value is the preferred one for most purposes.
Generally, the threads number should be just a matter of performance, and
not of change of semantics.
My impression is that the auto-adaptive mode of the slegehammer command is
coming from a time when there was still a TTY loop and at most one command
active, so one could rely on all threads being free, before starting the
next command. Now many things can be active all the time, and the thread
pool continuously busy with many different tasks.
Makarius
Email Gateway (Aug 22 2022 at 09:25):From: Makarius <makarius@sketis.net>
This should work in Isabelle2015-RC2.
Makarius
Email Gateway (Aug 22 2022 at 09:25):From: Makarius <makarius@sketis.net>
This is an odd effect caused by a change in the bootstrap order of
Isabelle/Pure: the ML environment and compiler invocation changes several
times, until it converges to proper Isabelle/ML and theory Pure.
We've occasionally had question marks in Poly/ML type output before, but I
never quite understood the reasons behind it. It is an imperfection, but
harmless.
Makarius
Email Gateway (Aug 22 2022 at 09:27):From: Tobias Nipkow <nipkow@in.tum.de>
For the paper I just advertised we used the old graph viewer to display the AFP
graph because it looks a bit better. I have attached both versions. Look at
nodes 55 and 85 to see some of the differences. The new placement leads to more
lines intersecting.
I am also not sold on the splines used in some cases, they are a bit wavy. Look
at the lines emerging from 63 or 33 in the new viewer.
However, these are just small blemishes and in other situation the new layout
may actually look better.
Tobias
afp_num_graph.pdf
new.pdf
smime.p7s
Email Gateway (Aug 22 2022 at 09:40):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
we are heading towards Isabelle2015, hopefully to appear at the end of May
2015. To get started with public testing of release candidates there is
now http://isabelle.in.tum.de/website-Isabelle2015-RC0
RC0 is still relatively early in the process: the website has no content
yet, and some documentation is not yet updated. The NEWS file is already
ready for inspection (using the tree-view of Sidekick).
Any problems, observations etc. can be discussed here on the mailing list.
Quite often a change of behaviour is perceived as a problem, and sometimes
it is one, sometimes not. In any case, open discussion helps to figure
out what is potentially confusing to users.
Makarius
Email Gateway (Aug 22 2022 at 09:41):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius
I found a "feature request" for the jEdit interface:
I loaded WordLemmaBucket from autocorres, a file with 5900 lines.
There are at least two errors near the end of the file when loading
with 2015-RC0. However, it is nearly impossible to locate the errors
in the .thy. Is it possible to have some sort of "jump to next error"
or an automatic jump to the error when I click on the red spot (left
of the jEdit scroll bar)?
Also, when I have an error in my theory, e.g. writing "where f=..."
but in 2015-RC0 it should be "where f1=...", only the "f" is
underlined, this makes the error quite hard to spot for me.
Forther minor observations:
Another question: Sometimes I have some helper lemmas
Email Gateway (Aug 22 2022 at 09:41):From: "C. Diekmann" <diekmann@in.tum.de>
[message continues (how do I email?)]
Another question: Sometimes I have some helper lemmas and at the end
of my theory I declare
hide_fact helper_lemma
to clean up the namespace.
Can I use the new private keyword to accomplish the same or is it only
considered for special cases when I already use context blocks?
Overall, RC0 looks very nice. Great job!
Cornelius
Email Gateway (Aug 22 2022 at 09:41):From: "C. Diekmann" <diekmann@in.tum.de>
jEdit crashed (stopped responding to anything).
What I did:
Closed jEdit with unsaved changes.
jEdit asked what to do. I clicked "select all" followed by "save
selected". jEdit simply hung. Screenshot:
http://i.imgur.com/6W3zr8n.png
OS: Ubuntu 14.04.2 with Linux 3.13.0 and unity
Email Gateway (Aug 22 2022 at 09:51):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
The auto-adaptive mode of Sledgehammer is unfortunately still necessary. Let me explain why, using my 4-core MacBook Pro as an example.
First,
ML {* Multithreading.max_threads_value () *}
prints
val it = 4: int
which means that Sledgehammer will, by default, use four provers. Given a nontrivial unprovable goal, if I go into the Sledgehammer panel and enter
cvc4 e spass remote_vampire
in the “Provers” field, then press “Apply”, it takes about 30-35 s before all four provers have come back with “Timed out”. (I just checked it. Of course, one could load the machine or even Isabelle/jEdit in such a way that this takes longer, but I’m talking about the typical, 95%-of-cases scenario.)
So far so good. Now if I add Z3 to the mix, i.e.,
cvc4 e spass remote_vampire z3
then it takes about 60-65 s before the little wheel stops spinning and we get the last answer.
The philosophy behind Sledgehammer is that humans have a limited patience, they want to wait 30 seconds and then move on with their lives. For that 30 seconds, they want as much CPU as possible to be allocated to automatic provers. This is somewhat at odds with the Isabelle/jEdit/PIDE philosophy, but I think it makes sense. Take a web browser. It might have several tabs, all loading different pages, playing videos, etc. If I try to connect to a server that’s not responsive in one of the tabs, it will try for about half a minute before giving up — irrespective of whether 1, 2, 3, 4, or 5 tabs are already open.
This is the default behavior. Users who do want to run Z3 and wait an extra 30 second are free to specify “z3” in the list.
Jasmin
Email Gateway (Aug 22 2022 at 09:54):From: Makarius <makarius@sketis.net>
The question is why the user should wait for the spinning wheel to stop:
it would be some kind of TTY-mode imitation.
In Isabelle2014 there was actually a technical snag, but for Isabelle2015
I've refined that once again. The NEWS and ANNOUNCE files say:
* Improved scheduling for asynchronous print commands (e.g. provers
managed by the Sledgehammer panel) wrt. ongoing document processing.
So it would be interesting to see if it actually works as advertized.
Makarius
Email Gateway (Aug 22 2022 at 09:55):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
The question is why the user should wait for the spinning wheel to stop: it would be some kind of TTY-mode imitation.
But as you know, Sledgehammer has been asynchronous for much of its life even in the old Proof General days. And yet Larry’s experience from 2010 is, to the best of my knowledge, still as actual as ever:
“Parallelism was another design objective, both to exploit the abundance of cheap processing power and so that users would not have to wait. Sledgehammer was intended to run in the background; Isabelle would continue to respond to commands, and users could keep working. This idea has turned out to be somewhat misconceived: thinking is difficult, and users typically wait for Sledgehammer to return, hoping to get a proof for free.”
I’d be curious to hear what actual users have to say on this.
Jasmin
Email Gateway (Aug 22 2022 at 09:56):From: Makarius <makarius@sketis.net>
This is very interesting and funny in several respects: the "abundance of
cheap processing power" in particular. It has never been as difficult as
today to turn raw computing power into proper use. Most CPUs are running
applications at 10% or less. The "market" has already reacted on that,
and we don't get the tons of cores that Intel/AMD could in principle
provide. A cheap GPU for gaming has thousands of cores, and regular CPU
only a handful.
We should tell Intel that ATP is an important game, too.
Makarius
Email Gateway (Aug 22 2022 at 09:57):From: Harry Butterworth <heb1001@gmail.com>
OpenCL/CUDA is pretty easy to use. Is there any scope for moving some of
the heavy lifting onto the GPU?
Email Gateway (Aug 22 2022 at 09:59):From: Tjark Weber <tjark.weber@it.uu.se>
In my view, the idea isn't misconceived at all, but the current UI is
not quite there yet. I still envision a version of Sledgehammer (or
try) that runs continuously in the background, working away on all
subgoals as they are generated by user input, and reports a proof when
(and if) it finds one. Importantly, there should be zero UI overhead
when it is unsuccessful. Ideally, this would obviate the need to even
think about invoking Sledgehammer.
Best,
Tjark
Email Gateway (Aug 22 2022 at 10:01):From: Larry Paulson <lp15@cam.ac.uk>
Part of my vision was to use idle capacity on nearby machines. But that’s another tricky thing, and was never implemented.
I also never envisaged proving theorems in front of the television. Sledgehammer makes that pretty easy.
Larry
Email Gateway (Aug 22 2022 at 10:03):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Tjark,
Have you tried playing with “Auto Sledgehammer” and friends? You can enable them in the Isabelle plugin options and adjust their timeouts.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 10:04):From: Tobias Nipkow <nipkow@in.tum.de>
As you know, this is my attitude. I might change if there were a smooth
invisible auto-s/h in the background, but I think that is not easy to achieve
currently.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:04):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Have you tried playing with “Auto Sledgehammer” and friends? You can enable them in the Isabelle plugin options and adjust their timeouts.
I should perhaps add for clarification that Auto Sledgehammer, like the other auto tools, works fine for top-level lemmas but not for subgoals or intermediate steps in an Isar proof. This is something that would require more work in Isabelle/jEdit.
For starters, it would be nice if Isabelle/jEdit could notice “sorry”s and attack them. I don’t think I’m the only one who introduces them regularly as placeholders to prevent the interface from showing errors.
Jasmin
Email Gateway (Aug 22 2022 at 10:04):From: Makarius <makarius@sketis.net>
On Mon, 4 May 2015, Jasmin Blanchette wrote:
I should perhaps add for clarification that Auto Sledgehammer, like the
other auto tools, works fine for top-level lemmas but not for subgoals
or intermediate steps in an Isar proof. This is something that would
require more work in Isabelle/jEdit.
There is not so much going on there. The PIDE print function for the auto
tools merely has a hardwired policy for "theory_goal" commands, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015-RC0/src/Tools/try.ML#l95
That may be understood as a relatively crude way to prevent the implicit
mode from sucking up too many resources. Even in that form it is already
quite heavy.
Nonetheless I think that implicit tools (with good scheduling policies)
are better than funny command-lines or click-panels. Too bad that we
don't have 32 or 64 cores now as we should. Damn market economy.
For starters, it would be nice if Isabelle/jEdit could notice “sorry”s
and attack them. I don’t think I’m the only one who introduces them
regularly as placeholders to prevent the interface from showing errors.
In recent Isabelle versions the idea is to eliminate the need for "sorry"
proofs. The document processing recovers at the next theory command.
Concerning auto tools: there could be some way to mark/unmark parts of the
proof document that should be attacked implicitly.
Makarius
Email Gateway (Aug 22 2022 at 10:04):From: Mathias Fleury <mathias.fleury12@gmail.com>
Le 04/05/2015 09:56, Makarius a écrit :
On Mon, 4 May 2015, Jasmin Blanchette wrote:
I should perhaps add for clarification that Auto Sledgehammer, like
the other auto tools, works fine for top-level lemmas but not for
subgoals or intermediate steps in an Isar proof. This is something
that would require more work in Isabelle/jEdit.There is not so much going on there. The PIDE print function for the
auto tools merely has a hardwired policy for "theory_goal" commands,
see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015-RC0/src/Tools/try.ML#l95That may be understood as a relatively crude way to prevent the
implicit mode from sucking up too many resources. Even in that form
it is already quite heavy.Nonetheless I think that implicit tools (with good scheduling
policies) are better than funny command-lines or click-panels. Too
bad that we don't have 32 or 64 cores now as we should. Damn market
economy.For starters, it would be nice if Isabelle/jEdit could notice
“sorry”s and attack them. I don’t think I’m the only one who
introduces them regularly as placeholders to prevent the interface
from showing errors.In recent Isabelle versions the idea is to eliminate the need for
"sorry" proofs. The document processing recovers at the next theory
command.
What is exactly a theory command? As for now, I cannot get rid of them
in Isar proofs:
have XXX
hence YYY by t
seems to be processed as "have XXX by t".
Nor on the lemma level, for example:
lemma test: "f var"
lemma "f 1"
using testby auto
Contrary to previous case "lemma 'f 1'" is not skipped. But the lemma
"test" is not defined. While this was the goal of adding a lemma (under
my workflow at least): whenever I need another lemma, I put it before
and see if it can be useful.
So what do you mean exactly by "eliminating the need for 'sorry' proofs"?
(using Isabelle RC, which is a recent Isabelle version, I assume).
Mathias
Concerning auto tools: there could be some way to mark/unmark parts of
the proof document that should be attacked implicitly.Makarius
Email Gateway (Aug 22 2022 at 10:04):From: Makarius <makarius@sketis.net>
It means that for now you still need 'sorry' in the above situations.
What you call "lemma level" above is the topmost theory structure, where
theory commands can be written. The formal keywords category is something
like "thy_decl", "thy_goal" etc. This is e.g. relevant when commands are
defined in the library, see the 'keywords' specification in theory
headers.
My terminology and jargon on this mailing list is sometimes hard to
understand. "Recent Isabelle versions" means something like a clear trend
in the past 3 years -- there are more and more moves towards elimination
of 'sorry', some tiny additional steps in Isabelle2015, but we are not
there yet. There are also diverging and conflicting attempts to achieve
similar things, e.g. the "skip_proofs" option, or the 'oops' command. It
all needs to be sorted out and disentangled carefully.
This seemingly endless process is called "reform": it can take months,
years, decades, but will happen eventually. Looking back in time, it is
surprising how far we have moved in the past 30 years.
Makarius
Email Gateway (Aug 22 2022 at 10:04):From: Makarius <makarius@sketis.net>
The aforementioned auto sledgehammer feature has zero UI overhead, but
there is significant impact on the prover backend side. With more than 16
cores we could probably have it by default, but consumer machines are not
moving forward anymore, stuck at 4 cores.
Makarius
Email Gateway (Aug 22 2022 at 10:04):From: Makarius <makarius@sketis.net>
I've experimented with an up-to-date version of my virtual Fedora 21, but
did not see any focus problems. Maybe this needs to be tried longer. Or
maybe the timing is different on a virtual machine and its slow graphics
engine.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC