aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/misc')
-rwxr-xr-xtest-suite/misc/coq_environment.sh51
1 files changed, 51 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