add test

8 files changed, 82 insertions, 0 deletions

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.