From 7a25cc5f29a16e05a3289ad66dca2817b63649ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 22 Jan 2021 17:04:19 +0100
Subject: Properly implement local references in Summary.

---
 library/summary.ml  | 25 ++++++++++++-------------
 library/summary.mli |  2 +-
 2 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/library/summary.ml b/library/summary.ml
index 221ac868fa..572467ada3 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -131,28 +131,27 @@ let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
 
 module Local = struct
 
-type 'a local_ref = ('a CEphemeron.key * 'a Dyn.tag) ref
+type 'a local_ref = 'a CEphemeron.key ref * 'a CEphemeron.key Dyn.tag
 
-let set r v = r := (CEphemeron.create v, snd !r)
+let set (r, tag) v = r := CEphemeron.create v
 
-let get r =
-  let key, name = !r in
-  try CEphemeron.get key
+let get (key, name) =
+  try CEphemeron.get !key
   with CEphemeron.InvalidKey ->
     let { init_function } = DynMap.find name !sum_map in
     init_function ();
-    CEphemeron.get (fst !r)
+    CEphemeron.get !key
 
-let ref ?(freeze=fun x -> x) ~name init =
+let ref (type a) ~name (init : a) : a local_ref =
   let () = check_name (mangle name) in
-  let tag : 'a Dyn.tag = Dyn.create (mangle name) in
-  let r = pervasives_ref (CEphemeron.create init, tag) in
+  let tag : a CEphemeron.key Dyn.tag = Dyn.create (mangle name) in
+  let r = pervasives_ref (CEphemeron.create init) in
   let () = sum_map := DynMap.add tag
-    { freeze_function = (fun ~marshallable -> freeze (get r));
-      unfreeze_function = (set r);
-      init_function = (fun () -> set r init) } !sum_map
+    { freeze_function = (fun ~marshallable -> !r);
+      unfreeze_function = (fun v -> r := v);
+      init_function = (fun () -> r := CEphemeron.create init) } !sum_map
   in
-  r
+  (r, tag)
 
 let (!) = get
 let (:=) = set
diff --git a/library/summary.mli b/library/summary.mli
index 7c5e1bee6f..a6f94a49ae 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -53,7 +53,7 @@ val ref_tag : ?freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a
 module Local : sig
 
   type 'a local_ref
-  val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+  val ref : name:string -> 'a -> 'a local_ref
   val (:=) : 'a local_ref -> 'a -> unit
   val (!) : 'a local_ref -> 'a
 
-- 
cgit v1.2.3


From a631b260c54e78faadc5dfc1ef3d319f19e1b615 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 25 Jan 2021 15:25:48 +0100
Subject: add test

---
 test-suite/misc/non-marshalable-state.sh           | 30 ++++++++++++++++++++++
 test-suite/misc/non-marshalable-state/_CoqProject  |  9 +++++++
 test-suite/misc/non-marshalable-state/src/evil.mlg | 15 +++++++++++
 .../non-marshalable-state/src/evil_plugin.mlpack   |  1 +
 test-suite/misc/non-marshalable-state/src/good.mlg | 16 ++++++++++++
 .../non-marshalable-state/src/good_plugin.mlpack   |  1 +
 .../misc/non-marshalable-state/theories/evil.v     |  5 ++++
 .../misc/non-marshalable-state/theories/good.v     |  5 ++++
 8 files changed, 82 insertions(+)
 create mode 100755 test-suite/misc/non-marshalable-state.sh
 create mode 100644 test-suite/misc/non-marshalable-state/_CoqProject
 create mode 100644 test-suite/misc/non-marshalable-state/src/evil.mlg
 create mode 100644 test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
 create mode 100644 test-suite/misc/non-marshalable-state/src/good.mlg
 create mode 100644 test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
 create mode 100644 test-suite/misc/non-marshalable-state/theories/evil.v
 create mode 100644 test-suite/misc/non-marshalable-state/theories/good.v

diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh
new file mode 100755
index 0000000000..eef7786ebc
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state.sh
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/non-marshalable-state/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cmxs
+make src/good_plugin.cmxs
+
+RC=1
+# must fail
+coqc -async-proofs on  -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0
+#   for this reason
+grep -q 'Marshalling error' log1 || RC=1
+
+# must work
+coqc -async-proofs off -I src -Q theories Marshal theories/evil.v
+
+# must work
+coqc -async-proofs on  -I src -Q theories Marshal theories/good.v
+
+
+exit $RC
diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject
new file mode 100644
index 0000000000..09e68d866c
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/_CoqProject
@@ -0,0 +1,9 @@
+-Q theories Marshal
+-I src
+
+src/evil.mlg
+src/good.mlg
+src/evil_plugin.mlpack
+src/good_plugin.mlpack
+theories/evil.v
+theories/good.v
diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg
new file mode 100644
index 0000000000..59b2b5a8ac
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil.mlg
@@ -0,0 +1,15 @@
+DECLARE PLUGIN "evil_plugin"
+
+{
+
+let state = Summary.ref
+  ~name:"elpi-compiler-cache"
+  None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+    state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..6382aa69e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
@@ -0,0 +1 @@
+Evil
diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg
new file mode 100644
index 0000000000..c6b9cbefd5
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good.mlg
@@ -0,0 +1,16 @@
+DECLARE PLUGIN "good_plugin"
+
+{
+
+let state = Summary.Local.ref
+  ~name:"elpi-compiler-cache"
+  None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+    let open Summary.Local in
+    state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
new file mode 100644
index 0000000000..cd9dd73b78
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
@@ -0,0 +1 @@
+Good
diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v
new file mode 100644
index 0000000000..661482a975
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/evil.v
@@ -0,0 +1,5 @@
+Declare ML Module "evil_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v
new file mode 100644
index 0000000000..eab9a043e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/good.v
@@ -0,0 +1,5 @@
+Declare ML Module "good_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
-- 
cgit v1.2.3