Email Gateway (Aug 22 2022 at 16:12): Email Gateway (Aug 22 2022 at 16:12):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Makarius,
a student in our Isabelle-course has alerted me about the following behavior in Isabelle2017-RC2. (I'm currently traveling and can't test RC3.)
theory Scratch
imports Main
begin
lemma [simp]: "length xs = length (rev xs)"
by simp
lemma "P (length xs)"
by simp
end
The second call to simp will turn from purple to red after a few minutes on my (and the student's) machine without outputting anything. In Isabelle2016-1, I couldn't reproduce this behavior (i.e., it would stay purple). The fact that it turns red is at least better than what happened in Isabelle2013-1, but it still can be confusing. Is this happening on purpose?
Dmitriy
Email Gateway (Aug 22 2022 at 16:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,
Red errors in jedit without a message are nothing new in Isabelle2017. I've also seen them
in Isabelle2016-1 in case the PolyML runs out of memory, e.g., a non-terminating value
[code] command which constructs ever larger terms (e.g. an infinite codatatype value).
Then the command just showed a red error mark without any error message. In
Isabelle2016-1, I haven't seen this happen with simp, though, but maybe I was never
patient enough. But I suspect this is precisely what is happening in your example, simp
will create increasingly large terms.
Andreas
Email Gateway (Aug 22 2022 at 16:12):From: Peter Lammich <lammich@in.tum.de>
I have observed this behavior in 2016-1 occasionally. I believe that happens
on stack overflow and maybe some other low- level errors.
Peter
Email Gateway (Aug 22 2022 at 16:12):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Andreas,
right. But it seems that the amount of "patience" needed has reduced (compared to Isabelle2016-1). For both, I use the default ML_OPTIONS="-H 500".
Dmitriy
Email Gateway (Aug 22 2022 at 16:12):From: Makarius <makarius@sketis.net>
I have made some more experiments. This command-line invocation works
best to see the error:
$ isabelle process -T Scratch
Exception- Interrupt raised
To compare the amount of "patience" required, here are some results on
lxbroy10 (x86-linux):
97f16ada519c 2m16.102s
18f3d341f8c0 2m22.646s
Isabelle2016-1 2m19.796s
In contrast, I did see a difference on my home machine (x86-linux):
Isabelle2017-RC3: approx. 5min
Isabelle2016-1: approx. 44min
I am unsure which side-conditions can cause such an effect.
Also note that the Poly/ML version is essentially the same in all
versions above.
Of course, the example is pathological in any case. It is just a matter
how non-termination is presented to the user.
Makarius
Last updated: May 06 2024 at 08:19 UTC