Re: [isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks
None of us reported my problem, because it concerned a somewhat elaborate case in some somewhat elaborate code I wrote, which we never managed to conveniently reproduce. Noone realised at the time that the exception-printing mechanism was at fault all by itself. This would be an archetypal bad bug report. By comparison, David is providing you with what would be considered a good bug report in most open-source communities. It comes with a clear explanation not only of what the problem is but what causes it to occur, and how it might be fixed. In such communities, the proposed patches are nearly never applied as-is, but they provide a far more useful starting point than the average bug report. I suppose Isabelle is interesting in that it is largely deterministic, so if a complaint can be minimised it can usually be easily reported. On the topic of mailing lists: we do indeed have a highly reactive mailing list, but many of us find that the usual reactions are rarely useful. We attempt to improve the quality of information in both directions by focusing on issues where there is a quantity of evidence. In particular, you do not want a running blog from me of every occasion on which Isabelle thwarts me. Finally, on the issue of WWW_find, I know that Raf has had a look at it, and declared that it isn't a triviality. I think it might be a while before any serious work on it is done. Yours, Thomas. On 04/04/13 21:42, Makarius wrote: On Thu, 4 Apr 2013, Thomas Sewell wrote: David's investigation explains a problem we had a few years ago where some custom tactics of mine were killing my colleagues' ProofGeneral sessions when they encountered errors. The workaround at the time was to remove all potentially useful debugging information (terms, in particular) from the relevant exceptions. Unfortunately this made tracking down the bugs in the tactics somewhat challenging. In hindsight, I should probably put the debug terms in the tracebuffer and thrown a vanilla exception. Hindsight is perfect, of course. So why did none of you guys ever report that? We have a very reactive isabelle-users mailing list, compared to most other project's issue trackers. It is also possible to discuss anything for inter-release Isabelle versions here on isabelle-dev, although its reactivity needs to be specifically slowed down to avoid hazards in the development process. Having a certain observation or undesirable behaviour on someone's TODO list for 1-2 years already, it is like to be a matter of the past now. Instead we have a lot of wasted time here with patches that are proposed in a way to make it an urgent and immediate issue to be fixed while you wait. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] auto raises a TYPE exception
Hi, In Isabelle2013 as well as the current development revision (#0a7b4e0384d0) the following call to auto raises a TYPE exception in envir.ML 8 theory Scratch imports Main begin class test = fixes P :: 'a set ⇒ bool lemma shows P_UNIV [intro]: P UNIV and P_Int [intro]: P S ⟹ P T ⟹ P (S ∩ T) and P_Union [intro]: ∀S∈K. P S ⟹ P (⋃ K) and P_INT [intro]: finite A ⟹ ∀x∈A. P (B x) ⟹ P (⋂x∈A. B x) sorry lemma fixes Q :: 'b ⇒ bool and f :: 'a::test ⇒ 'b shows (∃S. P S ∧ x ∈ S ∧ (∀xa∈S. Q (f xa))) apply (auto simp only:) oops It looks like the problem is somewhere in the call to Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML): clasimp.ML fun nodup_depth_tac ctxt m i st = SELECT_GOAL (Classical.safe_steps_tac ctxt 1 THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac ctxt m 1), Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1 i st; --- Dmitriy and I tried to simplify the testcase by replicating the goal on which inst0_step_tac is called but could not replicated the failure. * Has anybody a idea what is causing this exception? * Any helpful tips how to continue to debug this bug? * How can I activate backtraces in ML to get an better understand of the problem? I tried declare [[ML_trace = true]] but I didn't get a backtrace. Greetings, Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
On Fri, 5 Apr 2013, Johannes Hölzl wrote: It looks like the problem is somewhere in the call to Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML): clasimp.ML fun nodup_depth_tac ctxt m i st = SELECT_GOAL (Classical.safe_steps_tac ctxt 1 THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac ctxt m 1), Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1 i st; --- Dmitriy and I tried to simplify the testcase by replicating the goal on which inst0_step_tac is called but could not replicated the failure. * How can I activate backtraces in ML to get an better understand of the problem? I tried declare [[ML_trace = true]] but I didn't get a backtrace. ML_trace is only for the static phase, to say what is the actual ML source after expanding antiquotations. In principle ML Toplevel.debug := true gives you an exception trace (only visible on Raw Output), but it is hidden behind lazy sequence evaluation here. So you should try the exception_trace combinator in the deeper parts of the ML code, where you suspect a problem. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks
On Fri, 5 Apr 2013, Thomas Sewell wrote: By comparison, David is providing you with what would be considered a good bug report in most open-source communities. It comes with a clear explanation not only of what the problem is but what causes it to occur, and how it might be fixed. In such communities, the proposed patches are nearly never applied as-is, but they provide a far more useful starting point than the average bug report. All my complaints on this (and related) mail threads can be reduced to this assumption about most open-source comminities. This universal standard simply does not exist, and the average open-source project just produces junk. Especially people from NICTA / L4.verified should care about the platform(s) they depend on -- this also includes Poly/ML. Here we have a very unusual project -- it still exists after 25 years and the system is in fairly good shape. This is not an accident, it is the consequence of a certain development process. But the air is getting thinner and thinner as we still move on. Larry had quite visionary ideas in his initial 1989 sketch of Isabelle, including Programs like Isabelle are not products: when they have served their purpose, they are discarded. Historically, my biggest mistake was to disregard that when there was still a chance. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
