Email Gateway (Aug 19 2022 at 08:37): Email Gateway (Aug 19 2022 at 08:37):From: Makarius <makarius@sketis.net>
On Fri, 14 Sep 2012, David Greenaway wrote:
On 14/09/12 08:58, Rafal Kolanski wrote:
[...]I really wish that there was some way to get exception traces again when
working interactively in Isabelle.
[...]I too had previously thought that the exception traces in Isabelle had
disappeared somewhere around the Isabelle2011-1 time-frame,
Both of you seem to have taken software decay for granted, and did not
tell anybody here or on isabelle-dev. Isabelle has traditionally very
high ethical standards for software quality, so things are usually put
into shape again quickly, once the problem is known.
I have come across the issue myself last fall just after the
Isabelle2011-1 release, so in Isabelle2012 it works again. See the
typical changelog prose of mine that explains everything in one line,
quoting even the relevant Poly/ML change:
changeset: 45486:600682331b79
user: wenzelm
date: Mon Nov 14 16:16:49 2011 +0100
files: src/Pure/Isar/runtime.ML
description:
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
(Interestingly, there are actually two traces printed: the first is
the one listed above, the second seems less useful.)
That is the "more detailed" aspect above. By filtering out some less
relevant exceptions, the full trace was lost by accident. So it is now
redundant, but informative again.
So I am not sure if/when the stack traces disappeared, or if/when they
came back, but happily they seem to be working now. The key points are
to enable "Toplevel.debug", disable inlining for the code you are trying
to debug, and make sure you look in "isabelle" trace window for the
trace.
In Isabelle/jEdit this is the raw output panel, to show physical stdout
messages that are produced by the Poly/ML runtime system for the exception
trace. This is unmanaged output, and the window needs to be active when
it happens, otherwise it is lost.
On a marginally related note, PolyML also has stepping/tracing
facilities, as described in:http://www.polyml.org/docs/Debugging.html
which you can theoretically use by typing commands in the "isabelle"
window. I have personally found that the combination of Isabelle and
ProofGeneral and PolyML debugging tends to be a little unstable, so
I don't ever use these. I would be curious to know if others have had
more success, however.
In Isabelle/jEdit the support for Isabelle/ML support (including tracing
and debugging) is already better in Isabelle/jEdit of Isabelle2012 than
ever before in the history of Isabelle Proof General.
There is also clear separation of physical stdin from the protocol
channel. So in principle one could negotiate with the raw Poly/ML
toplevel loop (and its debugger) while Isabelle is running at full speed.
There is no console window for that in the Prover IDE, though.
In practice, I usually use plain writeln and PolyML.print to see what is
happening in some ML code (after recompiling), not the debugger.
Makarius
Email Gateway (Aug 19 2022 at 08:37):From: Makarius <makarius@sketis.net>
What you "throw" and "catch" on the Java Virtual Machine is slightly
different from what you "raise" and "handle" in ML. A JVM Exception
object is much more heavy than in ML. Nonetheless, you can use the
"reraise" function in Isabelle/ML to pass some of the original information
through an exception handler, most importantly the source position.
Searching through the Isabelle sources for "reraise" reveals some examples
-- typically some administrative operation.
The implementation manual section 0.5
http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf has
some further overview of the overall picture of exceptions, interrupts
etc. In particular, the infamous "handle _ => " from the SML/NJ library
book must never be used.
Makarius
Email Gateway (Aug 19 2022 at 08:37):From: Rafal Kolanski <xs@xaph.net>
On 17/09/12 04:54, Makarius wrote:
Both of you seem to have taken software decay for granted, and did not
tell anybody here or on isabelle-dev. Isabelle has traditionally very
high ethical standards for software quality, so things are usually put
into shape again quickly, once the problem is known.
This is not really "decay" as such. It is an implementation decision we
were not aware of, and I merely wonder if there isn't some way to get
detailed traces back while maintaining performance. David Matthews
explained the situation to me and said he will think about if and how it
is possible. This is all I wanted, and he has been very helpful throughout.
changeset: 45486:600682331b79
user: wenzelm
date: Mon Nov 14 16:16:49 2011 +0100
files: src/Pure/Isar/runtime.ML
description:
more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers
reset the trace (cf. Poly/ML SVN 1110);
Please be aware there are very important trade-offs both in life an
work. There is a reason you are a (the?) Isabelle guru. It has to do
with the exposure of time and investment of effort in keeping Isabelle
running, preventing aforementioned code decay while still improving the
feature set. For this reason, you were aware of this situation and tried
to do something about it already.
This is highly relevant work, and work for which we are grateful, but it
is not necessarily our work. Our work takes us further out than
Isabelle itself and into the realm of building larger projects with it.
When we identify situations where we need to automate or customise
because of project maintenance, that's when we get to dive back into the
Isabelle internals.
So we have this periodic dance:
On the one hand, we need to be periodically reminded that Isabelle can't
just have features shoved in because we want them, that they need to be
considered within the broader scope of the Isabelle system, and that
there is an "Isabelle way" of doing things. We count on that for you.
Sometimes we get a bit frustrated, but that's an acceptable price to pay.
On the other hand, I think you need to be periodically reminded that
Isabelle has users at various levels of competency/experience, whose
primary work focus is not Isabelle itself. In other words, there is more
to Isabelle than using Isabelle for the sake of Isabelle by means of
Isabelle (similarly Scala and Scala).
Such users have need of interfaces which reflect at least slightly
realistic work that they need to be doing.
Concrete example. During my visit to Munich this year, I wanted to find
out which theorems were used by fastforce to prove a lemma, because my
tactic wouldn't solve it, but fastforce did. Typical
tactical-implementation problem. So, there isn't a feature in Isabelle
called "thms_used_to_prove my_theorem". I look at the ML level, and
realise there isn't one either, there's only a generalised fold over the
proof term structure. It turns out that if you perform a partial
traversal of the proof term (first two levels), you get the required
functionality. But now I've spent the better part of an hour
understanding proof terms to make sure I got it right and bothered Lukas
(who is awesome, BTW) as a result.
So finally, I have my shiny ML function which answers the very useful
question of "which theorems were used to prove this theorem directly,
rather than the entire tree back to Pure". Lukas likes it, Tobias thinks
it is useful.
After further discussion though, Lukas and I conclude that we'll never
get it past you, because we can't substantiate a serious enough
Isabelle-reason for modifying the proof term API to provide this
commonly thought of and convenient functionality. So we put it in the
Isabelle Cookbook. After I left, Lars had the exact same problem, but
now could just look up the solution.
That is how things work for Isabelle non-gurus.
All I ask for is a bit of respect. Just because I don't understand the
entire system and its multi-year vision in-depth does not necessarily
mean that all my ideas are stupid. In fact, some of the ideas might be
good, but are in need of a guru suggesting a better implementation,
which is why I mention them anyway.
There are real issues with introspection of proofs in larger projects,
e.g. being able to reliably tag images (you are looking at the most
recent successful build of an image via the wwwfind interface... quick,
please tell me which revision that is, and if the correct image is in
fact loaded without reading through the entire theory dropdown first). I
have also tried discussing this at length, but no one cares except for
our team, so we use custom patches and I gave up. The next big project
will have the exact same problems, and these hacky solutions will get
hacked in again and again, wasting people's time, while every time we
bring them up here we'll get told they are not relevant, because the
Isabelle project itself doesn't need it, and why would you want multiple
instances of an image on the same machine anyway?
In Isabelle/jEdit the support for Isabelle/ML support (including tracing
and debugging) is already better in Isabelle/jEdit of Isabelle2012 than
ever before in the history of Isabelle Proof General.There is also clear separation of physical stdin from the protocol
channel. So in principle one could negotiate with the raw Poly/ML
toplevel loop (and its debugger) while Isabelle is running at full
speed. There is no console window for that in the Prover IDE, though.
Great, so at some point in the future when I change the theorem prover
interface I use, the functionality I'm looking for might be available.
This will be quite an improvement, to be able to run the interactive
debugger at the same time as Isabelle, and when it happens will render
my observations about exception traces mostly irrelevant (still would be
nice if David figured out a magical way to do it).
In practice, I usually use plain writeln and PolyML.print to see what is
happening in some ML code (after recompiling), not the debugger.
Yes, I do this too, in my own code. I can't just rewrite some other
person's code and rebuild, because that may take hours. Thanks to David
Matthews and the latest PolyML 5.5 though, we can now build everything
in under 3 hours (down from 8h with -q 0, and 4h with -q 1) on some
machines and then do something which you really dislike: copy the image
from the much faster machine to the much slower one. I recall on this
list someone (you?) telling me that one shouldn't copy binary images
around, and why would anyone want to do that anyway?
So in summary, I may not be the smartest person on this planet, but if
I'm not aware of the intricacies of what exactly happened in Isabelle in
every single commit, it's not because I don't care or take software
decay for granted or something. In fact, if you ask people at Munich who
have talked to me, it's almost the opposite. I have an inherent and
sometimes not-quite-sane instinct to streamline things and make them
more intuitive.
I just have four other projects to work on, and don't really feel
encouraged to try contribute when the answer is nearly always the same:
"your idea sucks || is pointless || we don't have this problem la la la
|| your implementation is not canonical || that isn't a good enough
reason to modify the interface || ...). Look what happened now: I raised
a bug report when I found one, and in the resulting discussion I get
told that I take "software decay for granted".
While your contributions are truly impressive, I would venture a
suggestion to at least try pretend to be a bit more open-minded. You
know, Bill Clinton style. He won't do what you asked for in all
probability anyway, but at least you'll walk away from the discussion
feeling like your idea was given due consideration. I don't know how
else to explain this, other than that the Isabelle users list is great,
helpful and proving stuff is fun and easy to release, working at the ML
level is a depressing experience, and trying to share the results of
one's work doubly so.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 19 2022 at 08:38):From: Lukas Bulwahn <bulwahn@in.tum.de>
Just to clarify my intentions in this example of a feature request here:
Certain features, as the one mentioned above, can be implemented
perfectly in Isabelle's "user space". For the implementing developer,
many functions then appear to be important for a decent library and we
would like to add them to "kernel" modules to make our contribution more
visible. However, Isabelle's slogan "fight features" (p.3 of the
Isabelle implementation manual) just as the often cited LCF approach
forbid to modify and extend kernel modules, just because of a temporal
state of mind. Coincidently, Makarius is the person, who enforces these
matters in our system and repository---Hence, the statement "We can't
get it past Makarius", really means we do not have any substantial
reason to modify the kernel.
Nonetheless, the story of some feature usually does not end here. If
developers are quite proud of their functionality, they try to advertise
it, as we did. One such way is certainly the Isabelle developer
tutorial, another is to find others that need the functionality. This
usually ends up in temporal clones here und there till the pressure is
large enough for one of the developers to take another round of
iteration of some subject.
Unlike some other developers, I was in the fortunate position to learn
this way of system development from Makarius and many others in the
group in Munich.
But again, this thread (as many other threads before) is getting largely
off-topic.
Lukas
Email Gateway (Aug 19 2022 at 08:38):From: Makarius <makarius@sketis.net>
Before continuing the meta-discussion, which requires more time to study
to make sense in the response, just back to the technical question:
Which aspect of ML expection trace is no longer working, camparing
Isabelle2012 to some more distant past?
David Matthews improved something on his side in SVN 1110, I followed in
my side in 600682331b79, so it should be all back. What is the remaining
problem that was not spelled out explicitly so far?
Makarius
Email Gateway (Aug 19 2022 at 08:38):From: David Matthews <dm@prolingua.co.uk>
With PolyML 5.3 and earlier, if you had a handler that caught only
exception foo but you had raised bar then exception_trace would show the
whole stack trace from the point where you raised bar. With 5.4 and
later an exception handler of the form
handle foo => ... is rewritten as though it were
handle x => (case x of foo => ... | x => reraise x)
So exception_trace only shows the stack from the point where bar was
reraised. That may well not be as helpful.
I understand the problem; it's just that making this change greatly
simplified the exception mechanism and speeded it up.
David
Email Gateway (Aug 19 2022 at 08:38):From: Rafal Kolanski <xs@xaph.net>
Consider this code:
exception TFX;
exception IRR;
fun f1 x = raise TFX;
fun f2 x = f1 x + 1;
fun f3 x = f2 x + 1;
fun f4 x = f3 x + 1;
fun f5 x = (f4 x + 1) handle IRR => raise IRR;
fun f6 x = f5 x + 1;
fun f7 x = f6 x + 1;
fun f8 x = f7 x + 1;
fun f9 x = f8 x + 1;
Output of "f9 1" in PolyML 5.3:
f1(1)
f2(1)
f3(1)
f4(1)
f5(1)
f5(1)
f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
End of trace
Output in PolyML 5.4+:
f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
End of trace
TFX has not been handled at any point, but in newer releases its origin
is obscured by the handler for IRR, and will be obscured by any handler.
David Matthews has kindly explained the design decision to me and said
he will think on whether it is possible the old behaviour back without
taking a non-trivial penalty. That's really all I hoped for in raising
the backtrace issue originally. I also considered that maybe I'm not the
first ML-level Isabelle user to run into this, and so someone might have
a (hacky) workaround.
I'll honestly say that I don't at present understand what issue your
changeset 600682331b79 addresses and do not possess the free time to
find out, but it appears to not be the one I am describing.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 19 2022 at 08:38):From: Makarius <makarius@sketis.net>
On Mon, 17 Sep 2012, Rafal Kolanski wrote:
David Matthews improved something on his side in SVN 1110, I followed in
my side in 600682331b79, so it should be all back. What is the
remaining problem that was not spelled out explicitly so far?Consider this code:
exception TFX;
exception IRR;fun f1 x = raise TFX;
fun f2 x = f1 x + 1;
fun f3 x = f2 x + 1;
fun f4 x = f3 x + 1;
fun f5 x = (f4 x + 1) handle IRR => raise IRR;
fun f6 x = f5 x + 1;
fun f7 x = f6 x + 1;
fun f8 x = f7 x + 1;
fun f9 x = f8 x + 1;Output of "f9 1" in PolyML 5.3:
f1(1)
f2(1)
f3(1)
f4(1)
f5(1)
f5(1)
f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
End of traceOutput in PolyML 5.4+:
f6(1)
f7(1)
f8(1)
f9(1)
<top level>
CODETREE().genCode(2)(1)
COMPILER_BODY().baseCompiler(4)executeCode(1)
End of traceTFX has not been handled at any point, but in newer releases its origin
is obscured by the handler for IRR, and will be obscured by any handler.
OK, this is a reasonable report on the situation after all.
I'll honestly say that I don't at present understand what issue your
changeset 600682331b79 addresses and do not possess the free time to
find out, but it appears to not be the one I am describing.
It addresses exactly that for the Isar toplevel, but it cannot change the
situation for user-code, of course.
Makarius
Email Gateway (Aug 19 2022 at 08:38):From: Makarius <makarius@sketis.net>
First of all, a citation is just a citation, not a literal statement.
The ones on the front-part of the Isabelle/Isar manual do have some
correlation with the received Isabelle development process and its
challenges, which is why I've put them there, but eveybody needs to start
his own thinking process to see behind the surface and the actual things
in the background.
I've recently come across a very interesting lecture by Alan Kay on
"Programming and Scaling" http://tele-task.de/archive/video/flash/14029/
which might lead to more citations from him ending up in that spot of the
implementation manual. I particularly like one of his explanations
(probably from another talk) about the fundamental importance of
architecture: instead of turning many bricks naively into an amorphic pile
of bricks, to make a sophisticated building you need to follow certain
structuring principles that you need to learn first. And the main focus
of that talk is then about learning and education, especially in the US,
especially science and math education.
Alan Kay is an interesting person in many respects. He has now grown old
and wise, and can go beyond the follies from his youth, most notably the
"object-oriented" movement that he started. (He is the inventor of the
term "OO", so its fun to see him bashing that a lot now.)
Makarius
Email Gateway (Aug 19 2022 at 08:41):From: Makarius <makarius@sketis.net>
This thread is already getting old, but the above paragraph sounds very
odd to me. Myself and several other people I know use routinely a lot of
different Isabelle versions and work with images from them. You have the
regular settings that can be modified locally, and tools like "isabelle
version -i" to get more specific identification of repository snapshots.
This should give sufficient flexibility to organize images in many ways.
In the next release that will be perfected even further, thanks to the new
build system.
I don't think any of your local "hacks" are actually needed. IIRC, this
was also what I hinted at when the discussion was coming up some years
ago, but it was not taken to the end, just cancelled in frustration
probably.
Makarius
Email Gateway (Aug 19 2022 at 08:41):From: Makarius <makarius@sketis.net>
This has already become a running gag: someone, maybe even Gerwin, decided
at some point that Isabelle has an "Isar level for users" and an "ML level
for developers". But I've myself never introduced anything like that.
The very first Isar command I implemented in the distant past was 'ML'.
And today Isabelle/Isar and Isabelle/ML are neatly intertwined such that
you can go back and forth between the languages as you need in your tool
implementations. The Prover IDE is also a fairly good IDE for ML inside
regular Isar source.
So you have Isabelle/Pure/HOL/ML/Isar/Scala etc but it is difficult to
assign "levels" to them. In practice you work with several of these
Isabelle aspects at the same time. The delicate bootstrapping process in
the Isabelle/Pure implementation is a different story -- the machine room
down there is definitely not user-space.
Makarius
Email Gateway (Aug 19 2022 at 08:41):From: Rafal Kolanski <xs@xaph.net>
You are entirely missing my point here. You keep referring to Isabelle
versions as if they are the only versions anyone might care about. We
run a project using Isabelle. The project has its own revision control
versions, and Isabelle is just one subrepo.
What you are describing is the isabelle version used to build a
particular image. We know which version this is. What we don't know is
which repository version of the project built the image we are
presenting to the user.
Trivially: on port 8193 we have the wwwfind server presenting an
interface to users wishing to search through the latest CREFINE image
the regression test server was able to build with the current version of
Isabelle. Question: given that you know which Isabelle version and
PolyML version built it (obvious from the image path and from Isabelle
being a subrepo), which repository version are you looking at? Sometimes
an image can be broken for a few days, and people need to tell they are
not looking at the latest source version, but at the latest successfully
built version.
I really can't get the point across any more clearly. I have repeatedly
tried to explain that Isabelle is a tool upon which we run a project,
and it is not the only project in existence. It should be evident that
simply knowing the revision of Isabelle used to build something is not
the only revision one should know, as Isabelle was used to build
something and the version of that something is in fact more
important, henceforth "isabelle version -i" really does nothing here.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 19 2022 at 08:41):From: Makarius <makarius@sketis.net>
This is getting a bit far off the Isabelle track.
I claimed that Isabelle has sufficiently many ways to identify itself
precisely, and reconfigure locations for images and other resources.
Building other projects on top should work. People have done that without
patching Isabelle.
BTW, when you say "the latest source version" my semantic spell-checker
marks it read, because that is not a well-defined notion. The changeset
id is how you identify things unambigously, or a collection of ids -- for
each repository.
Makarius
Email Gateway (Aug 19 2022 at 08:46):From: Rafal Kolanski <xs@xaph.net>
Dear Isabelle Users and Developers,
I have recently come across an issue when trying to improve the runtimes
of our regression test server. When I ran it with -q 1, the times
improved drastically, which was nice. When I ran it with -q 2 though, it
didn't build at all. Those of you who know me will not be surprised to
find it was in a theory I wrote :)
The issue affects building an image in non-interactive mode under
Isabelle 2012 and a very recent development version (2267901ae911), in
both 32-bit and 64-bit builds of PolyML versions 5.4.0, 5.4.1 and
5.4.2-dev. Breakage confirmed on three different physical machines.
Settings were:
ISABELLE_USEDIR_OPTIONS="-M 2 -p 0 -q 2 -v true"
but also confirmed to break with -M max and -p 1.
Please find attached the ROOT.ML, IsaMakefile and Loading.thy which
replicates the issue in a distilled form building on HOL only. Run with:
isabelle make MAPPED_SEP
The error should be on the line attempting the subst:
*** exception THM 0 raised (line 758 of "thm.ML"):
*** forall_intr: variable "bs" free in assumptions
*** [| length bs = sz; P (Suc p) sz bs; p # Z = Z |]
*** ==> p # load_list_basic sz (Suc p) = Z
*** [!!]
*** At command "apply" (line 30 of "/home/rafalk/t/isa_bug/Loading.thy")
The issue is definitely due to some shadowing/renaming of the variable
bs, but what else is going on is well beyond my current grasp of
comprehension.
Sincerely,
Rafal Kolanski.
IsaMakefile
Loading.thy
ROOT.ML
Email Gateway (Aug 19 2022 at 08:48):From: Makarius <makarius@sketis.net>
On Mon, 10 Sep 2012, Rafal Kolanski wrote:
I have recently come across an issue when trying to improve the runtimes
of our regression test server. When I ran it with -q 1, the times
improved drastically, which was nice. When I ran it with -q 2 though, it
didn't build at all.
Now the world knows that the top-secret proofs of L4.verified are still
checked sequentially :-)
The error should be on the line attempting the subst:
*** exception THM 0 raised (line 758 of "thm.ML"):
*** forall_intr: variable "bs" free in assumptions
*** [| length bs = sz; P (Suc p) sz bs; p # Z = Z |]
*** ==> p # load_list_basic sz (Suc p) = Z
*** [!!]
*** At command "apply" (line 30 of "/home/rafalk/t/isa_bug/Loading.thy")The issue is definitely due to some shadowing/renaming of the variable
bs, but what else is going on is well beyond my current grasp of
comprehension.
I've had a quick look at the "subst" method, but it looks very bad. That
code has not been maintained in many years. It simply ignores the
all-important Proof.context when inventing free variables that are
expected to be fresh, but aren't. There is not just one place, but many.
One could probably make a small changeset to get your example working, but
it will then crash in another situation.
The following comment in isand.ML, which is one part of the problem here
is quite representative:
THINK: are we really ok with our varify name w.r.t the prop - do
we also need to avoid names in the hidden hyps? What about
unification contraints in flex-flex pairs - might they also have
extra free vars?
The answer: hyps are necessary, but still not sufficient. One needs to
take the full Proof.context into account.
A quick fix is to do the renaming yourself in the proof, i.e. avoid
accidental overlap of blue / brown / green variables with the same name on
the surface. Then "subst" can continue its work with its archaic context
model a little longer.
Makarius
Email Gateway (Aug 19 2022 at 08:50):From: Makarius <makarius@sketis.net>
See http://isabelle.in.tum.de/repos/isabelle/rev/d1fcb4de8349 and
http://isabelle.in.tum.de/repos/isabelle/rev/25fc6e0da459 for what I've
made in the meantime. You have to see yourself how to apply this to
Isabelle2012 (via "hg import" etc). Isabelle has only a single official
release branch, and it will take a few months until the next one is
published.
I think the main problem with your example was in RWInst.mk_renamings, as
changed in 25fc6e0da459 to get rid of usednames_of_thm in particular.
There are many more situations where "subst" produces free variables on
the spot. They still don't look 100% canonical to me, even after the
change, but for this round of refurbishing tools from the Isabelle library
it should be sufficient.
Makarius
Email Gateway (Aug 19 2022 at 08:50):From: Rafal Kolanski <xs@xaph.net>
On 13/09/12 04:16, Makarius wrote:
On Mon, 10 Sep 2012, Rafal Kolanski wrote:
I have recently come across an issue when trying to improve the
runtimes of our regression test server. When I ran it with -q 1, the
times improved drastically, which was nice. When I ran it with -q 2
though, it didn't build at all.Now the world knows that the top-secret proofs of L4.verified are still
checked sequentially :-)
We generally try to run with the highest amount of parallelism that does
not make the machine thrash or PolyML segfault. Previously that was -q
0, now it's -q 1. We're tracking the svn version of the upcoming PolyML
5.5 to see if at some point we can switch to -q 2.
The issue is definitely due to some shadowing/renaming of the variable
bs, but what else is going on is well beyond my current grasp of
comprehension.I've had a quick look at the "subst" method, but it looks very bad.
That code has not been maintained in many years. It simply ignores the
all-important Proof.context when inventing free variables that are
expected to be fresh, but aren't. There is not just one place, but
many. One could probably make a small changeset to get your example
working, but it will then crash in another situation.
I made a bad joke about how I should title my post to the list "On the
improper use of context in the subst method", but then we weren't sure
if that was exactly the case. Context is really hard to get right, and
old code does accumulate these leaks.
A quick fix is to do the renaming yourself in the proof, i.e. avoid
accidental overlap of blue / brown / green variables with the same name
on the surface. Then "subst" can continue its work with its archaic
context model a little longer.
Yes, we ended up doing that, and now we're back to PolyML segfaulting
with -q 2. David seems to be applying quite a few fixes to the GC
though, so we have high hopes of getting it working soon.
I would also like to say thank you in general for the movement towards
local context and parallelism over the years. We went down from a full
test run of almost 8 hours down to 4 when switching to -q 1.
Thanks for patching it in the repository. Hopefully it will save someone
a major head-scratching in future!
Sincerely,
Rafal Kolanski
Email Gateway (Aug 19 2022 at 08:50):From: Lars Noschinski <noschinl@in.tum.de>
That is good to know. I have a student project planned (but no student
yet) to implement a subst-like tactic with the hole-selection of
ssreflects' rewrite tactic. I will keep in mind that subst's code is to
be taken with a grain of salt.
-- Lars
Email Gateway (Aug 19 2022 at 08:50):From: David Matthews <dm@prolingua.co.uk>
I have fixed all the segfaults I am aware of with the GC and I'm on the
point of releasing SVN 1594 as Poly/ML 5.5. If you have an example that
consistently fails I will investigate. However, I need as much detail
as possible and if at all possible a script that I can run to reproduce
it. Bear in mind that I know absolutely nothing about using Isabelle so
it needs to be foolproof.
David
Email Gateway (Aug 19 2022 at 08:50):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Imagine the pain we've been in all that time ;-)
We can now do this, because we have a regression test server with 128GB RAM.
My desktop machine still needs to run sessions sequentially to get things through, although poly 5.5.0 has made the situation dramatically better.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 08:50):From: Makarius <makarius@sketis.net>
It is also a natural consequence of disclosed sources, but you know this
already.
Makarius
Email Gateway (Aug 19 2022 at 08:50):From: Makarius <makarius@sketis.net>
This should read as "closed", or "nondisclosed" to make the Newspeak come
out properly.
Makarius
Email Gateway (Aug 19 2022 at 08:51):From: Rafal Kolanski <xs@xaph.net>
I will be testing that as my third task for today, so fingers crossed.
It's unlikely if anything goes wrong I'll be able to give you a
reproducible script though. The errors I've seen so far are always of
the kind "PolyML segfaults sometimes when building large images" :/
I really wish that there was some way to get exception traces again when
working interactively in Isabelle. You have already said you don't know
much about using Isabelle, but perhaps someone here knows a trick? There
already is a nice debugging interface built into PolyML, I just don't
know how to use it while working with a theorem prover.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 19 2022 at 08:51):From: David Greenaway <david.greenaway@nicta.com.au>
Hi Raf,
Email Gateway (Aug 19 2022 at 08:51):From: Rafal Kolanski <xs@xaph.net>
Hi David,
As I demonstrated in person, the exception traces only get you as far as
the first exception handler you encounter. So for example if anywhere in
the chain there was a handle BAR, then even though you threw a FOO you
still wouldn't get a trace past that handler.
I think we decided that behaviour appeared in 5.4? Dave Matthews told me
it was a design decision which improved performance and simplified code,
but I am still rather sad it is gone. I wish there was a way to enable
it again for our interactive sessions, even if we have to suffer a speed
penalty. For batch sessions with parallelism, the existing behaviour in
exchange for performance is definitely the right idea.
I guess if the problem is really massively painful, we can always
rebuild with 5.3 and trace with that while head-scratching in parallel :/
Sincerely,
Rafal Kolanski.
Last updated: Apr 25 2024 at 04:18 UTC