*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)*From*: Rafal Kolanski <xs at xaph.net>*Date*: Mon, 17 Sep 2012 08:39:13 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1209162038000.7897@macbroy20.informatik.tu-muenchen.de>*References*: <504D885D.2060503@xaph.net> <alpine.LNX.2.00.1209122003440.6649@macbroy21.informatik.tu-muenchen.de> <5051381B.6000609@xaph.net> <5051D037.4020403@prolingua.co.uk> <5052651B.3090909@xaph.net> <5052761B.4020001@nicta.com.au> <alpine.LNX.2.00.1209162038000.7897@macbroy20.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120827 Thunderbird/15.0

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.

**Follow-Ups**:**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Lukas Bulwahn

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Makarius

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Makarius

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Makarius

**References**:**[isabelle] Parallel proofs issue, potentially in subst method***From:*Rafal Kolanski

**Re: [isabelle] Parallel proofs issue, potentially in subst method***From:*Makarius

**Re: [isabelle] Parallel proofs issue, potentially in subst method***From:*Rafal Kolanski

**Re: [isabelle] Parallel proofs issue, potentially in subst method***From:*David Matthews

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Rafal Kolanski

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*David Greenaway

**Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)***From:*Makarius

- Previous by Date: [isabelle] "distinct" for Datatype
- Next by Date: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
- Previous by Thread: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
- Next by Thread: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list