<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
On 10/19/2012 04:35 PM, Makarius wrote:
<blockquote
cite="mid:alpine.LNX.2.00.1210191634360.14042@macbroy21.informatik.tu-muenchen.de"
type="cite">On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
<br>
<br>
<blockquote type="cite">
<blockquote type="cite">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.
<br>
<br>
</blockquote>
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.
<br>
</blockquote>
<br>
Historically, the weak warning was a necessity due to too many
simprocs still not working with the context.
<br>
<br>
Let's hope that it can be easily switched to an explicit error
after so many years now.
<br>
<br>
</blockquote>
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.<br>
<br>
Two examples:<br>
- the hypsubst_tac internally uses the simplifier, but the interface
does not allow to pass the current simpset to this tactic.<br>
- An implementer has to avoid certain functions, such as<span
style="color:#cc0000;"> Raw_Simplifier.rewrite</span>, that assume
to be used only in a non-nested context.<br>
<br>
<br>
Lukas<br>
</body>
</html>