Thank you for investigating. I have been waiting for Alex to present his view.
Naturally, the current treatment resembles ML's. I continue to believe that reference to IDEs is a distraction. I've seen several instances now (in student work) of nonsensical function definitions caused by putting a “default" case too early in the function definition. Anybody who reads the resulting proof document could easily misinterpret what has been proved. There is no reason to allow a specification to contain material that may contradict another part of the specification. It is precisely analogous to allowing, while ignoring, redefinitions of constants. Larry On 31 May 2012, at 21:23, Makarius wrote: > Generally, the best "strength" of messages by the system is difficult to > determine. Proof General and the OCaml toplevel are very rude in the sense > that they stop at the first hard error. Compared to that, Poly/ML is much > better at error recovery, say to present a partially type-checked piece of > source with IDE markup. (I've recently shown the Isabelle/ML IDE to some > local OCaml experts and they were quite impressed by the quality of the > feedback from its static analysis produced in real time as the user types the > text.) > > The Isabelle Prover IDE for logical part is still a bit crude here: it skips > over failed commands and retains any of the markup produced so far. > > This also means a hard error is not so hard after all, and can sometimes > cause more confusion than a soft one, because the binding of the formal > entity to be defined will be absent from the context. Thus the scoping in > later text can change unexpectedly for the user: e.g. a bad function "foo" > used later in formal text becomes a free variable (luckily with the Haribo > color effect, which will gradually include more and more details about scopes > etc.) _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
