Discussion:
[isabelle] Behavior of configuration options in local theories
(too old to reply)
Dmitriy Traytel
2016-09-06 12:02:28 UTC
Permalink
Raw Message
Dear all,

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?

Thanks for any hints,
Dmitriy
Makarius
2016-09-14 21:58:44 UTC
Permalink
Raw Message
Post by Dmitriy Traytel
ML ‹

local_setup ‹fn lthy =>
let
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
(http://isabelle.in.tum.de/repos/isabelle/rev/aae510e9a698):

* 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
Local_Theory.close_target.

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.


Makarius

Loading...