[isabelle-dev] NEWS: asynchronous print functions etc.
nipkow at in.tum.de
Fri Jul 19 15:51:47 CEST 2013
Am 18/07/2013 22:44, schrieb Makarius:
> On Thu, 18 Jul 2013, Florian Haftmann wrote:
>>>>> "Code generator: dropping subsumed code equation" by Auto Quickcheck
>>>>> I guess it would be the task the tools to omit such outbursts and not
>>>>> globally on the IDE side?
>>>> In principle Context_Position.is_visible should control that, and the
>>>> tools should observe it accordingly.
>>> The canonical way to do that is
>>> Context_Position.if_visible ctxt warning
>>> but this does not work for code equations, because the operations of
>>> src/Pure/Isar/code.ML act on a global theory, which is always "visible"
>>> in that sense.
> I have generalized the concept to allow changing the visibility of a global
> theory context as well. This is observed by unify.ML, as a guard to its many
> tracing options, find_theorems.ML then copies the Proof.context visibility over
> to a copy of the background theory of the goal state, so 'solve_direct' no
> longer produces spam from this source, see Isabelle/d68fd63bf082.
Does that mean that one could add an attribute unify_trace now?
>>> Maybe Florian also has some ideas about codegen.
>> One answer would be to eliminate this meanwhile somehow ridiculous warning
> In principle you could refer to Context_Position.is_visible_global as well, but
> it looks all a bit complicated: quickcheck would have to pass down a modified
> theory, and code.ML would have to get all these lazy theory_ref things right.
> Note that I am presently experimenting with a purely value-oriented theory type
> (Isabelle/38466f4f3483), where theory_ref is just an alias and Theory.copy /
> Theory.checkpoint just the identity. So any mistakes in rearanging the
> theory_ref management in code.ML won't be detected at first, only if I have to
> backout 38466f4f3483 (e.g. due to resoure problems).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev