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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
