Email Gateway (Aug 22 2022 at 12:23): Email Gateway (Aug 22 2022 at 12:23):From: Makarius <makarius@sketis.net>
Did the situation change in the past 2 weaks? Supposedly not, since the
cvc4 component in Isabelle2016-RC2 did not change in the meantime.
The question remains, if there is a problem with that cvc4 compilation, or
something else on that particular Ubuntu 14.04 installation.
Jasmin, if you want to change anything for Isabelle2016, the remaining
time is about 1 week.
Makarius
Email Gateway (Aug 22 2022 at 12:24):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
It is still crashing frequently, both on this system at home and
on my office system (similar hardware, same OS, but installed at
different times and with a somewhat different set of applications
installed).
I sent Jasmin one of the problem files that he asked for, but I
didn't hear if it was useful to him.
By the way, perhaps this is associated with the crashing, but I
find that hundreds and hundreds of megabytes of files are left in
/tmp/isabelle-xxx folders. Examples: kodkodiXXXXXX.kki",
"kodkodiXXXXXX.err", "bash_errXXXXXXX", etc. Yesterday after a
5-hour session, there were about 3GB of such files that were not
deleted when I exited Isabelle -- enough to fill up my root
partition.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:33):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Just a quick note to mention I am experiencing fairly frequent
crashes of cvc4 using stock Isabelle2016-RC0 on Ubuntu 14.04.
FWIW, below is the initial text part of the "whoopsie" file.
The cvc4 on Isabelle2015 also exhibited crashes, but not on this
machine, as far as I know.
If anyone needs info on library versions, let me know and I can
probably collect it.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,
What would help me the most would be a CVC4 problem file. You can get it by writing
sledgehammer [overlord]
and picking up the file "~/.isabelle/prob_cvc4.smt_in".
I might need additional information later, but for the moment let's see if I can reproduce the crash on one of my machines.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 12:33):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Where do I put this magic incantation?
Presumably it has to be in force throughout the entire session,
since there is no telling when the crash will occur.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Right after the proof goal or lemma you are trying to prove, directly in the text editor (at the point where you would normally invoke Sledgehammer through its dedicated panel). E.g.
lemma "x = x"
sledgehammer [overlord]
Jasmin
Email Gateway (Aug 22 2022 at 12:33):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I will see what I can do, but it is not deterministically repeatable,
and I usually just invoke sledgehammer by typing "try" or "try0".
- Gene Stark
Email Gateway (Aug 22 2022 at 12:33):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I see. Then I recommend you instead add
sledgehammer_params [overlord]
somewhere upstream (e.g. at the top of your file or in a theory file all your other theory files depend on). This will also affect "try".
Be aware that this option is not thread-safe -- i.e. if you have several Sledgehammers running at the same time somehow (e.g. several jEdits running), the problem or proof files might overwrite each other. Which is not the end of the world. I have never run into problems myself and use this option often (hence its name ;)), but I thought I'd mention this.
Jasmin
Email Gateway (Aug 22 2022 at 12:44):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,
I'm bringing back this to the mailing list, since it might be of general interest.
I see! Then I think this is something that is potential affecting everybody. CVC4 doesn't like being killed. This I have experienced first hand, when invoking it from the command line. I will investigate and report this to the CVC4 developers.
I hope you can find a workaround to avoid any distraction from the Ubuntu launcher. Otherwise, there's always the option of swapping CVC4 out and Z3 in...
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 12:48):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Makarius,
Did the situation change in the past 2 weaks? Supposedly not, since the cvc4 component in Isabelle2016-RC2 did not change in the meantime.
(Nothing changed, except that 2 weeks ago was 1 week before the IJCAR deadline, whereas now is 6 hours before the extended deadline...)
The question remains, if there is a problem with that cvc4 compilation, or something else on that particular Ubuntu 14.04 installation.
Jasmin, if you want to change anything for Isabelle2016, the remaining time is about 1 week.
The issue is not a regression -- the binaries are identical in Isabelle2015 and Isabelle2016-RC*. I'd rather not do anything that might break things for other users at this point. I'll investigate things privately with Eugene and hopefully have a satisfactory fix for him and for Isabelle2016-1.
Jasmin
Email Gateway (Aug 22 2022 at 12:49):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Eugene,
I sent Jasmin one of the problem files that he asked for, but I didn't hear if it was useful to him.
It is still on my radar, but due to a seminar this week it might still take some time before I come back to you.
By the way, perhaps this is associated with the crashing, but I
find that hundreds and hundreds of megabytes of files are left in
/tmp/isabelle-xxx folders. Examples: kodkodiXXXXXX.kki",
"kodkodiXXXXXX.err", "bash_errXXXXXXX", etc. Yesterday after a
5-hour session, there were about 3GB of such files that were not
deleted when I exited Isabelle -- enough to fill up my root
partition
This is somewhat puzzling. The "kodkodi*" files, for example, should all be removed as soon as Nitpick has come back to you. Could there be an issue with the permissions?
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:12):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
You have embarrassed me into attempting to merge my stuff and try Isabelle2016-1-RC0.
But now before I can get back to what I was doing and report on whether CVC4 is still
crashing, I need to know what the new warning "Not a proper equation" means in a
datatype definition as follows (also attached):
theory Barf
imports Main Category
begin
locale foo =
fixes X
assumes "X = X"
context foo
begin
datatype (discs_sels) 't "term" =
C
| T "'t term * 't term"
end
Another issue I noticed: JEdit now forcibly resets the indentations of lines
with keywords such as "locale" when I type the keyword, or, what is even
more irritating, when I type ENTER at the end of the line. I think this
new behavior is fairly disruptive of the typing habits I have established
to this point.
- Gene Stark
Barf.thy
Email Gateway (Aug 22 2022 at 14:12):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,
But now before I can get back to what I was doing and report on whether CVC4 is still crashing,
Please let us know how this goes. Regardless, the next release candidate will likely feature a new version of CVC4.
I need to know what the new warning "Not a proper equation" means in a
datatype definition as follows (also attached):
Thank you for your report. In short, the code generator is now more verbose, and the "datatype" package interacts with it. I have a solution locally to get rid of the warning that is likely to be part of the next release candidate.
Another issue I noticed: JEdit now forcibly resets the indentations of lines
with keywords such as "locale" when I type the keyword, or, what is even
more irritating, when I type ENTER at the end of the line. I think this
new behavior is fairly disruptive of the typing habits I have established
to this point.
I guess this is for Makarius to answer.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:12):From: Lars Hupel <hupel@in.tum.de>
Dear Gene,
I am myself trying to get used to this, but in case you don't want the
new behaviour, there is a way of switching it off.
Open the global options in jEdit ("Utilities" in the menu bar). In the
left tree, pick "jEdit"/"Shortcuts". Filter for "newline". You'll find a
command "Newline with indentation of ..." associated to "ENTER". Click
on "ENTER" and then on "Remove Current".
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:12):From: Makarius <makarius@sketis.net>
I generally recommend to resist the first impulse to get back to old
habits on the spot, and first get used to new behavior, unless that
turns out to be utterly wrong.
It is part of the Isabelle development model that there is a constant
flow of changes imposed on users. This keeps both the system and the
users live and vigorous. After 30 years, Isabelle is still young and
emerging towards ultimate perfection. Just compare Isabelle98 with
Isabelle2016 for example, and compare that difference with other more
conservative systems, and than decide if you want to be back in 1998
with the established habits from that time.
More concretely on indentation: there used to be a canonical scheme
built into Proof General / Emacs over many years. When that was
superseded by Isabelle/jEdit several years ago, I did not immediately
re-implement the traditional Isar indentation for various accidental
reasons, but it was clear it would happen one day.
The current indentation scheme of Isabelle2016-1-RC0 conforms to the old
Proof General / Emacs scheme from 1998 about 98%, but there are also
additional cases, since the Isar language has changed significantly
during all these years. When implementing it, some consequences turned
out different from what I considered canonical Isar indentation over
many years -- so I also had to change a few of my old habits.
With the new default indentation always on, live has become so much
easier so that I never look back again. Suddenly there is so little to
type to get indentation right. There are still a few cases, where manual
indentation with C+i is required, but that is the opposite of the old
Isabelle/jEdit scheme to do everything manually -- and every user in a
slightly different way.
Note that the indentation of keywords performed by ENTER is meant to be
always right, while extra indentation via C+i is only a 90%
approximation: the full syntax and its delicate details are not known to
the editor (and not even to the prover).
Makarius
Email Gateway (Aug 22 2022 at 14:21):From: Simon Wimmer <wimmersimon@gmail.com>
Hi Jasmin,
did you make an attempt to resolve this for the next release?
I just noticed that I find reports of CVC4 crashing on my Mac (running OSX
Sierra now) a few times per day.
I am not sure if I had this before or if this resurfaced with Sierra.
Cheers,
Simon
Email Gateway (Aug 22 2022 at 14:21):From: Simon Wimmer <wimmersimon@gmail.com>
I forgot to mention: the crashes are caused by Isabelle-2016 and
Isabelle-2016-1-RC0 alike.
Email Gateway (Aug 22 2022 at 14:23):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Simon,
Thanks for reminding me of this. I have about 12 unanswered emails on Isabelle Users which I haven't fully processed yet and Eugene's report is probably one of them.
We will soon recompile CVC4 and other provers. We can then check if the problem has automagically gone away in the past two years of CVC4 development. I must say, I always use the repository version of Isabelle on my Mac, and I used to have many CVC4 zombies lying around (a symptom of the crash, I believe), but in the past N months things have gone quiet, so I'm wondering if something has improved on the Isabelle side.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:23):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
CVC4 still crashes regularly with Isabelle2016 on Ubuntu 16.04 LTS.
For some reason it seems to still be useful, though. I believe this
is because (as surmised earlier in this thread) the crashing seems to
occur when Isabelle kills a no-longer-needed CVC4 process, not during
actual useful work.
- Gene Stark
Email Gateway (Aug 22 2022 at 14:23):From: Makarius <makarius@sketis.net>
Did you try Isabelle2016-1-RC0 from
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0 already?
There is now also a daily snapshot at http://isabelle.in.tum.de/devel --
it will quickly converge to Isabelle2016-1-RC1 at the end of the week.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC