*To*: Rafal Kolanski <xs at xaph.net>*Subject*: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Mon, 17 Sep 2012 09:51:49 +0200*Cc*: Makarius <makarius at sketis.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50565511.2070902@xaph.net>*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> <50565511.2070902@xaph.net>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

On 09/17/2012 12:39 AM, Rafal Kolanski wrote:

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.

Just to clarify my intentions in this example of a feature request here:

Lukas

**Follow-Ups**:

**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

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

- Previous by Date: Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)
- 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