Re: [isabelle] Behavior of configuration options in local theories

On 06/09/16 13:48, Dmitriy Traytel wrote:
> I was surprised by the fact that configuration options seem to be reset when closing a local target:
> ML â
> val foo = Attrib.setup_config_int @{binding foo} (K 6);
> â
> local_setup âfn lthy =>
>   let
>     val _ = Config.get lthy foo |> @{print}
>     val _ = Config.get (Config.put foo 7 lthy) foo |> @{print}
>     val _ = Config.get (Config.put foo 7 lthy |> Local_Theory.open_target |> snd) foo |> @{print}
>     val _ = Config.get (Config.put foo 7 lthy |> Local_Theory.open_target |> snd |> Local_Theory.close_target) foo |> @{print}
>   in
>     lthy
>   end
> â
> This prints
> 6
> 7
> 7
> 6.
> I had expected the last one to be 7 as well. Is there a way to make the changes to configuration options persistent in this respect?

If you really mean persistent in the sense of local theory targets, the
declaration needs to be applied via Local_Theory.declaration -- this
corresponds to Isar commands like 'declare' or 'declaration'.

Nonetheless, there is a slightly odd detail above for updates of the
hypothetical context on the surface: Local_Theory.open_target ..
Local_Theory.close_target is more disruptive than it needs to be. This
can be explained from the historical situation of still not fully
consolidated Local_Theory.restore / Local_Theory.reset.

See also this NEWS entry for the coming release

* Local_Theory.restore has been renamed to Local_Theory.reset to
emphasize its disruptive impact on the cumulative context, notably the
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
only appropriate when targets are managed, e.g. starting from a global
theory and returning to it. Regular definitional packages should use
balanced blocks of Local_Theory.open_target versus
Local_Theory.close_target instead. Rare INCOMPATIBILITY.

I will try to get rid of this extra Local_Theory.reset in

I will also try harder to motivate other people to eliminate remaining
uses of Local_Theory.restore / Local_Theory.reset from their own tools.

Lets see if we can finally sort this out for the coming release.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.