test suite for coq_makefile

52 files changed, 380 insertions, 1 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index afaa48463..8a3d383cb 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -87,7 +87,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -151,6 +151,7 @@ summary:
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
+	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -481,3 +482,19 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
+
+coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
+
+coq-makefile/%.log : coq-makefile/%/run.sh
+	@echo "TEST      $*"
+	$(HIDE)(\
+	  cd coq-makefile/$* && \
+	  ./run.sh 2>&1; \
+       	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	  fi; \
+	) > "$@"
diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject
new file mode 100644
index 000000000..700d59d64
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject
@@ -0,0 +1,11 @@
+-R src/ test
+-R theories/ test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+subdir/
diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh
new file mode 100755
index 000000000..38e54d03e
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/run.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make
+exec test -f "subdir/done"
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 b/test-suite/coq-makefile/compat-subdirs/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.mli b/test-suite/coq-makefile/compat-subdirs/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/src/test.mli
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/compat-subdirs/subdir/Makefile b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile
new file mode 100644
index 000000000..846c9b791
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile
@@ -0,0 +1,3 @@
+all:
+	test -f ../theories/test.vo
+	touch done
diff --git a/test-suite/coq-makefile/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject
new file mode 100644
index 000000000..35792066b
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/_CoqProject
@@ -0,0 +1,11 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+theories/sub/testsub.v
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
new file mode 100755
index 000000000..bbe9717ab
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -0,0 +1,53 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+make install-doc DSTROOT="$PWD/tmp"
+#make debug
+(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual
+sort -u > desired <<EOT
+.
+./test
+./test/test_plugin.cmi
+./test/test_plugin.cmo
+./test/test_plugin.cmx
+./test/test_plugin.cmxs
+./test/test.glob
+./test/test.v
+./test/test.vo
+./test/sub
+./test/sub/testsub.glob
+./test/sub/testsub.v
+./test/sub/testsub.vo
+./test/mlihtml
+./test/mlihtml/index_exceptions.html
+./test/mlihtml/index.html
+./test/mlihtml/index_class_types.html
+./test/mlihtml/type_Test_aux.html
+./test/mlihtml/index_module_types.html
+./test/mlihtml/index_classes.html
+./test/mlihtml/type_Test.html
+./test/mlihtml/style.css
+./test/mlihtml/index_attributes.html
+./test/mlihtml/index_types.html
+./test/mlihtml/Test_aux.html
+./test/mlihtml/index_values.html
+./test/mlihtml/Test.html
+./test/mlihtml/index_extensions.html
+./test/mlihtml/index_methods.html
+./test/mlihtml/index_modules.html
+./test/html
+./test/html/index.html
+./test/html/test.sub.testsub.html
+./test/html/toc.html
+./test/html/coqdoc.css
+./test/html/test.test.html
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/coqdoc1/src/test.ml4 b/test-suite/coq-makefile/coqdoc1/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/coqdoc1/src/test.mli b/test-suite/coq-makefile/coqdoc1/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/src/test.mli
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli b/test-suite/coq-makefile/coqdoc1/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack b/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v b/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v
new file mode 100644
index 000000000..755fc343f
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v
@@ -0,0 +1 @@
+Require Import test.
diff --git a/test-suite/coq-makefile/coqdoc1/theories/test.v b/test-suite/coq-makefile/coqdoc1/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject
new file mode 100644
index 000000000..cb1ad4a4b
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/_CoqProject
@@ -0,0 +1,10 @@
+-R src/ test
+-R theories/ test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh
new file mode 100755
index 000000000..3b5d388c9
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -0,0 +1,13 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make .merlin
+echo B $PWD/src > desired
+echo S $PWD/src >> desired
+tail -2 .merlin > actual
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/merlin1/src/test.ml4 b/test-suite/coq-makefile/merlin1/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/merlin1/src/test.mli b/test-suite/coq-makefile/merlin1/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/src/test.mli
diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.ml b/test-suite/coq-makefile/merlin1/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.mli b/test-suite/coq-makefile/merlin1/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack b/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/merlin1/theories/test.v b/test-suite/coq-makefile/merlin1/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/mllib1/_CoqProject b/test-suite/coq-makefile/mllib1/_CoqProject
new file mode 100644
index 000000000..6b2046d68
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/_CoqProject
@@ -0,0 +1,9 @@
+-R theories test
+-I src
+
+src/test_plugin.mllib
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/mllib1/run.sh b/test-suite/coq-makefile/mllib1/run.sh
new file mode 100755
index 000000000..8f6b8e7ea
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/run.sh
@@ -0,0 +1,30 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+sort > desired <<EOT
+.
+./test
+./test/test.glob
+./test/test.cmi
+./test/test.cmo
+./test/test.cmx
+./test/test_aux.cmi
+./test/test_aux.cmo
+./test/test_aux.cmx
+./test/test_plugin.cma
+./test/test_plugin.cmxa
+./test/test_plugin.cmxs
+./test/test.v
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mllib1/src/test.ml4 b/test-suite/coq-makefile/mllib1/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/mllib1/src/test.mli b/test-suite/coq-makefile/mllib1/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/src/test.mli
diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.ml b/test-suite/coq-makefile/mllib1/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.mli b/test-suite/coq-makefile/mllib1/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib b/test-suite/coq-makefile/mllib1/src/test_plugin.mllib
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/src/test_plugin.mllib
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/mllib1/theories/test.v b/test-suite/coq-makefile/mllib1/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/mllib1/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject
new file mode 100644
index 000000000..cb1ad4a4b
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/_CoqProject
@@ -0,0 +1,10 @@
+-R src/ test
+-R theories/ test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
new file mode 100755
index 000000000..43d03be4a
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -0,0 +1,25 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+sort > desired <<EOT
+.
+./test
+./test/test.glob
+./test/test_plugin.cmi
+./test/test_plugin.cmo
+./test/test_plugin.cmx
+./test/test_plugin.cmxs
+./test/test.v
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack1/src/test.ml4 b/test-suite/coq-makefile/mlpack1/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/mlpack1/src/test.mli b/test-suite/coq-makefile/mlpack1/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/src/test.mli
diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.ml b/test-suite/coq-makefile/mlpack1/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.mli b/test-suite/coq-makefile/mlpack1/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack b/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/mlpack1/theories/test.v b/test-suite/coq-makefile/mlpack1/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject
new file mode 100644
index 000000000..706cf75cc
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/_CoqProject
@@ -0,0 +1,11 @@
+-R src/ test
+-R theories/ test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+theories/sub/testsub.v
diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
new file mode 100755
index 000000000..a3bfe182b
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/run.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+export PATH=../../../bin/:$PATH
+git clean -dfx .
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+make install-doc DSTROOT="$PWD/tmp"
+make uninstall DSTROOT="$PWD/tmp"
+make uninstall-doc DSTROOT="$PWD/tmp"
+#make debug
+(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual
+sort -u > desired <<EOT
+.
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4
new file mode 100644
index 000000000..8ddc9b095
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/src/test.ml4
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "Test" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/uninstall1/src/test.mli b/test-suite/coq-makefile/uninstall1/src/test.mli
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/src/test.mli
diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.mli b/test-suite/coq-makefile/uninstall1/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v
new file mode 100644
index 000000000..755fc343f
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v
@@ -0,0 +1 @@
+Require Import test.
diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v
new file mode 100644
index 000000000..7753b56aa
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+Test.
+Goal True.
+Proof.
+test.
+exact I.
+Qed.