Re: [isabelle-dev] Recent instabilities of HOL-Decision_Procs
On Wed, 1 Sep 2010, Johannes Hölzl wrote: The Approximation theory only uses relfection and the code generator (with setup for code integer and efficient nat). Last year the usage of Unsynchronized.ref was remove in reflection. Since this time the approximation method should not use any references. The special things about the approximation method are: * uses reflection (i.e. the generated code as an oracle) * probably the only user of large ML-integers and division * long running proofs This means it could be some problem almost everywhere, say in the code generator. Or if the proofs are driving the system to the edege concerning memory requirements (which are also higher in parallel mode) it could be some spurious Interrupt that is handled accidentally by the infamous "handle _" still lurking in code occasionally. In the end it could as well be a side-effect of some (ongoing) rearrangements of how the system manages theory and proof checking. Another possibility: side-effect of an adhoc change that I did on your oracle code (see 3c3b4ad683d5) that fits perfectly well into the presumed time range of introducing the problem. Is it possible to get a more detailed exception trace? With Toplevel.debug := true (in ROOT.ML) you get global exception traces for actual failures. This does not cover plain empty result sequence of proof method application, because that is not a failure in the execution only in the search process. Makarius___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Recent instabilities of HOL-Decision_Procs
Am Mittwoch, den 01.09.2010, 15:40 +0200 schrieb Makarius: > For some week or so there are sparadic failures of HOL-Decision_Procs like > this: [..] > This only happenes when running in parallel mode, which is the default > on modern hardware for quite some time already. I estimate the > probability of the incident 5-10% -- which makes it a bit hard to > bisect in the change history. If we add 6 times the test cases to Approximate_Ex we would get a incident rate of 50% (or 21 times for 90%). I don't know if this is a good idea. > In general there are two main ways to make the behaviour of proof tools > depend on the weather: > >* real-time timeouts > >* Unsynchronized.ref > > The latter are being shot at since 2-3 years already, and need to > disappear altogether for tools that care about surviving the next big > reform in user interaction, where the assumption of a single execution > path is plain wrong. (For the moment Proof General still incurs a drastic > sequentialization that makes unsafes tool appear to work.) The Approximation theory only uses relfection and the code generator (with setup for code integer and efficient nat). Last year the usage of Unsynchronized.ref was remove in reflection. Since this time the approximation method should not use any references. The special things about the approximation method are: * uses reflection (i.e. the generated code as an oracle) * probably the only user of large ML-integers and division * long running proofs Is it possible to get a more detailed exception trace? - Johannes > The "configuration option" concept introduced some time ago provides an > easy drop-in replacement for bool/int/string options, even with the > possibility for process-global defaults (such as for simp trace etc.). It > also does the proper job concerning "localization". This avoids one > obsolete concept (Unsynchronized.ref) being replaced by another one > (global theory-only parameters). > > Going beyond bool/in/string is also possible, but requires a bit extra > work with attribute syntax (and Generic_Data). > > > Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
I always intended auto to be initial rather than terminal. I'm not aware of the unsafe mode you refer to, but it may have been introduced later. Larry On 1 Sep 2010, at 14:40, Thomas Sewell wrote: > Good point - I think of auto as terminal. My understanding was that auto had > both a safe and unsafe mode internally, where safe exploration is > clarsimp-like and seen by the user, and unsafe exploration is fastsimp-like > and kept only if it solves the goal. For tactics which continue after auto, > this would put it in the clarsimp/safe group. This fits with my experience in > writing the supplied patch, where some subgoal_tacs which came after autos > had to be adjusted slightly. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Recent instabilities of HOL-Decision_Procs
For some week or so there are sparadic failures of HOL-Decision_Procs like this: HOL-Decision_Procs FAILED (see also /Users/makarius/.isabelle/heaps//polyml-5.4.0_x86_64-darwin/log/HOL-Decision_Procs) (Var 0)) (replicate 3 None) [0, 0, 0] approx_tse_form 30 3 1 (Bound (Var 0) (Num (Float 0 0)) (Num (Float 1 0)) (LessEqual (Power (Var 0) 2) (Var 0))) ### Ignoring duplicate rewrite rule: ### Suc ?n1 == ?n1 + 1 ### Ignoring duplicate rewrite rule: ### Suc ?n1 == ?n1 + 1 ### Ignoring duplicate rewrite rule: ### Suc ?n1 == ?n1 + 1 ### Ignoring duplicate rewrite rule: ### Suc ?n1 == ?n1 + 1 ### Ignoring duplicate rewrite rule: ### Suc ?n1 == ?n1 + 1 *** Theory loader: undefined theory entry for "Approximation_Ex" *** Failed to finish proof *** At command "by" (line 42 of "/Users/makarius/isabelle/repos/src/HOL/Decision_Procs/ex/Approximation_Ex.thy") Exception- TOPLEVEL_ERROR raised *** ML error This only happenes when running in parallel mode, which is the default on modern hardware for quite some time already. I estimate the probability of the incident 5-10% -- which makes it a bit hard to bisect in the change history. The line 42 above is an invocation of the "approximation" method, but it might also happen in other places. Does anybody have any idea what could be wrong in this particular situation? In general there are two main ways to make the behaviour of proof tools depend on the weather: * real-time timeouts * Unsynchronized.ref The latter are being shot at since 2-3 years already, and need to disappear altogether for tools that care about surviving the next big reform in user interaction, where the assumption of a single execution path is plain wrong. (For the moment Proof General still incurs a drastic sequentialization that makes unsafes tool appear to work.) The "configuration option" concept introduced some time ago provides an easy drop-in replacement for bool/int/string options, even with the possibility for process-global defaults (such as for simp trace etc.). It also does the proper job concerning "localization". This avoids one obsolete concept (Unsynchronized.ref) being replaced by another one (global theory-only parameters). Going beyond bool/in/string is also possible, but requires a bit extra work with attribute syntax (and Generic_Data). Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution
This sounds logical. But what about auto? Like the other three, it is used to perform obvious steps in a proof, and it is not terminal. Larry On 1 Sep 2010, at 14:17, Thomas Sewell wrote: > Let me try to explain the difference from the perspective of a user. There > are three classical tools that will behave differently: safe, clarify and > clarsimp. Each of these will, when it would have substituted and removed > equalities in the past, now substitute those equalities, possibly reorient > them, and leave them as hypotheses. ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] FW: Safe approach to hypothesis substitution
Let me try to explain the difference from the perspective of a user. There are three classical tools that will behave differently: safe, clarify and clarsimp. Each of these will, when it would have substituted and removed equalities in the past, now substitute those equalities, possibly reorient them, and leave them as hypotheses. The additional equality will then be seen at all later points throughout tactic proofs. Given the ubiquity of clarsimp in my work, I suspect this changes the subgoal state at a significant number of points. The additional hypothesis will have little impact on most tools, but there are three kinds of tactic step with which it is a problem: 1) Subgoals where a bound variable (typically 'x' or 'y') is renamed (to 'xa' or 'ya') because facts about x or y persist in the goal. This means that explicit instantiations in subgoal_tac etc may need to be updated. 2) Explicit use of a drule or erule which can unify with an equality hypothesis (drule sym, drule_tac f=... in arg_cong, etc). 3) Induction steps, where additional hypotheses complicate the induction hypothesis generated. The changes to the HOL sources in the patch I sent reflect these three issues. None of these issues seem to be common, but maintainers of large repositories (HOL, the AFP, L4.verified etc) may still find them inconvenient. The main advantage of the preserving an equality on a free variable is if that variable is reintroduced via facts from the context at a later point in the proof script. I think this is unlikely to occur in a terminal tactic (auto, blast, fastsimp, etc) and thus they are unlikely to benefit from the change. For this reason I added an unsafe wrapper which simulated the old behaviour. I haven't tested whether this was really necessary. I may do that tomorrow. Yours, Thomas. From: Lawrence Paulson [l...@cam.ac.uk] Sent: Tuesday, August 31, 2010 8:21 PM To: Thomas Sewell Cc: Isabelle Developers Mailing List Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution Thanks for looking into this problem, which has been around in one way or another from the very beginning. Lost in all the technical discussions is the question of what the user will see. We have the option of leaving blast and force as they are now to minimise danger of incompatibility, though it would be disappointing if existing calls to these stopped working after what should be an improvement. I would expect them, on the contrary, to solve more problems than before. Anyway, the main methods to be affected are presumably safe and auto. I have made a small table showing the number of times the classical proof methods are used in the HOL distribution: safe956 auto23389 clarify 1403 force 1692 fastsimp 560 blast 7609 fast1079 best43 If the only method that behaves differently is safe, I wonder whether there's any point to doing this. It would be better to improve all the methods. If the new version is identical to the old one except that occasionally some equalities persist, then it ought to work as a drop-in replacement in nearly every instance. Is this what you see? Larry On 23 Aug 2010, at 08:52, Thomas Sewell wrote: > As previously discussed in the thread "Safe for boolean equality", the > current strategy for using equality hypotheses 'x = expr', in which > substitution for x is done and then the hypothesis is discarded, is unsafe. > The conclusion of that discussion was that the problem was annoying but > fairly rare, that there is some concern it may become more common as local > are used more extensively, and that fixing it would probably require a > painful change to the behaviour of auto. > > The problem is that by forgetting what x equates to in our goal, we lose the > connection from the goal to the context outside our goal. There may be other > facts available that name x. There may also be schematic variables which > could be instantiated to "hd x" but not the bound variable replacing it. > > The simple solution in my mind is to keep the equality in the goal, and since > noone else seemed interested I thought I'd attempt to do this myself and see > how difficult it was. I attach the resulting patch. After several rounds of > bugfixes and compatibility improvements, it requires 23 lines of changes to > theories to rebuild HOL, HOL-ex and HOL-Word. > > The code change in Provers/hypsubst.ML adds code for counting the free and > bound variables in a goal, and checking whether either side of an equality > hypothesis is a unique variable, occuring nowhere else. The main substitution > algorithms avoid using such equalities and also preserve rather than delete > the hypothesis they select. There is a new tactic for discarding these > equalities, which is added as an unsafe wrapper in Context_Rules, allowing > all unsafe tactics to behave roughly as before. The version of hypsubst > called
