Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Behavior of configuration options in local the...

Email Gateway (Aug 22 2022 at 14:04):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 14:05):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 22 2022 at 14:37):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Makarius,

sure, this is fine. We have a workaround not to rely on configuration options (but instead pass a Boolean flag around) for the problem I reported originally anyway.

Dmitriy

Last updated: Apr 24 2024 at 08:20 UTC