On 10/19/2012 04:35 PM, Makarius wrote:
On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
Operations like Simplifier.context, Simplifier.inherit_context
should help here. Once that is repaired, I will see if the warning
can now be made an error that is more explicit about the reasons.
I am certainly in favour of this. First, tool developers mainly react
on errors with test runs, but do not see the warnings. Secondly,
users do not know who to report those warnings and do not know if
they are caused by their scripts or the tools.
Historically, the weak warning was a necessity due to too many
simprocs still not working with the context.
Let's hope that it can be easily switched to an explicit error after
so many years now.
On the weekend, I had a look at this issue in the
set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and
already noticed what could make things difficult turning this into an error.
Two examples:
- the hypsubst_tac internally uses the simplifier, but the interface
does not allow to pass the current simpset to this tactic.
- An implementer has to avoid certain functions, such
asRaw_Simplifier.rewrite, that assume to be used only in a non-nested
context.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
