[isabelle-dev] NEWS: asynchronous print functions etc.

[Tobias Nipkow]

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?

Tobias

> 
>>> Maybe Florian also has some ideas about codegen.
>>
>> One answer would be to eliminate this meanwhile somehow ridiculous warning
>> entirely.
> 
> 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).
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev