diff options
Diffstat (limited to 'test-suite/misc')
9 files changed, 133 insertions, 0 deletions
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh new file mode 100755 index 0000000000..667d11f89e --- /dev/null +++ b/test-suite/misc/coq_environment.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +TMP=`mktemp -d` +cd $TMP + +cat > coq_environment.txt <<EOT +# we override COQLIB because we can +COQLIB="$TMP/overridden" # bla bla +OCAMLFIND="$TMP/overridden" +FOOBAR="one more" +EOT + +cp $BIN/coqc . +cp $BIN/coq_makefile . +mkdir -p overridden/tools/ +cp $COQLIB/tools/CoqMakefile.in overridden/tools/ + +unset COQLIB +N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by coq_environment + coqc -config + exit 1 +fi +N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo OCAMLFIND not overridden by coq_environment + coqc -config + exit 1 +fi +./coq_makefile -o CoqMakefile -R . foo > /dev/null +N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQMF_OCAMLFIND not overridden by coq_environment + cat CoqMakefile.conf + exit 1 +fi + +export COQLIB="/overridden2" +N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by COQLIB when coq_environment present + coqc -config + exit 1 +fi + +rm -rf $TMP +exit 0 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. |