Re: [isabelle] Feature suggestions: More useful output

On Fri, 23 Nov 2012, Joachim Breitner wrote:

Generally, I could imagine the output window being a bit more
informative, in particular with error messages.

For example, a failed "by method" currently just prints “Failed to
finish proof.” To fix this, I now have to change the "by" to "apply",
look at the result, fix it, and change it back. Could it not print
“Failed to finish proof. Remaining goals: ....”?

That is not a function of the output window, but of the prover to report things in a certain way. During this summer, and now in fall moving towards the coming winter release, I've made many refinements in both areas, and hopefully manage to add 2-3 more rounds of refinement before the next release. The general tendencies are like this:

  (1) Output is becoming less and less important (it is an old TTY thing).
    Instead the information is directly attached to the source.  So the
    messages are right there where things happen, while remaining
    accessible in output for nostalgic reasons (for people who want to
    make long moves with the mouse in the old way).

  (2) Error feedback of Isar commands involving search/enumertion of
    possibilities: this is an ancient issue from > 10 years ago, which I
    have re-opened some weeks ago.  So in the next release, you will see
    proper errors for "by method", and the need to use 'apply' to imitate
    that will be no longer there.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.