Email Gateway (Nov 29 2024 at 08:30): Email Gateway (Nov 29 2024 at 08:30):From: i n <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
I'm wondering if there's a method to execute ML code without keeping its bindings while keeping state changes.
This is meant to replace code that was done by Fabian immler/Jonas Rädle in their HOL4 in isabelle which I'm working on for the use of it as an IDE for HOL4.
The code in question does ML ‹fun with_temp_ML_env f x =
let
val context = Context.the_generic_context()
val res = f x
val () = Context.>> (ML_Env.inherit [context])
in res end
›which I believe is wrong due to it messing up synchronized variables and making them unusable.
I think I should be using a Proof context, is that the right path?.
Thanks,
Irvin
Email Gateway (Dec 03 2024 at 06:05):From: Fabian Immler <fabian.immler@gmail.com>
Hi Irvin,
I‘m not entirely sure what you mean by “state changes”.
Synchronized variables (in the sense of Synchronized.var) are mutable
reference cells, i.e., a pointer to some memory location, and therefore not
managed by Isabelle/ML’s context. If your code uses those, Isabelle’s IDE
will “mess” with the contents of those cells, as they are not tied to the
command that modifies them.
As far as I know, this can only be achieved by storing the values of such
“variables” in the context. See section 3.1 of our paper [1]. There we
describe how we mapped the type “ref” to a context-managed variables
“Context_Var.var”. I believe that you could achieve similar things by
re-defining Synchronized.var for your purposes.
But also note the trick that we describe in section 3.2: it is critical for
performance and to avoid memory leaks to distinguish “local state”
variables and mark them explicitly in the HOL4 sources as Uref.t. But if
there was a need to declare a variable as synchronized, it’s probably not
“local” in that sense…
Let me know if that information helps.
Best wishes,
Fabian
On Fri, Nov 29, 2024 at 10:14 i n <cl-isabelle-users@lists.cam.ac.uk> wrote:
Hi all,
I'm wondering if there's a method to execute ML code without keeping
its bindings while keeping state changes.
This is meant to replace code that was done by Fabian immler/Jonas Rädle
in their HOL4 in isabelle which I'm working on for the use of it as an IDE
for HOL4.The code in question does
ML ‹fun with_temp_ML_env f x = let val context = Context.the_generic_context() val res = f x val () = Context.>> (ML_Env.inherit [context]) in res end›
which I believe is wrong due to it messing up synchronized variables and
making them unusable.I think I should be using a Proof context, is that the right path?.
Thanks,
Irvin
Last updated: Jan 04 2025 at 20:18 UTC