From cd8f10fe54c956f1e797da3d165c3b29ffee615b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 22 Jan 2017 10:10:39 +0100 Subject: configure: -local set coqdoc destination dir to ./doc rather than "" --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 679f524179..7af18cb858 100644 --- a/configure.ml +++ b/configure.ml @@ -897,7 +897,7 @@ let do_one_instdir (var,msg,r,dflt,suff) = let do_one_noinst (var,msg,_,_,_) = if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true) - else (var,msg,"",false) + else (var,msg,coqtop^"/doc",false) let install_dirs = let f = if !Prefs.local then do_one_noinst else do_one_instdir in -- cgit v1.2.3 From e9156da20ec5332b1b53a6c44127e0f822891d16 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Jan 2017 17:18:39 +0100 Subject: test suite for coq_makefile --- .gitignore | 8 ++++ Makefile | 1 + test-suite/Makefile | 19 +++++++- test-suite/coq-makefile/compat-subdirs/_CoqProject | 11 +++++ test-suite/coq-makefile/compat-subdirs/run.sh | 10 ++++ .../coq-makefile/compat-subdirs/src/test.ml4 | 13 ++++++ .../coq-makefile/compat-subdirs/src/test.mli | 0 .../coq-makefile/compat-subdirs/src/test_aux.ml | 1 + .../coq-makefile/compat-subdirs/src/test_aux.mli | 1 + .../compat-subdirs/src/test_plugin.mlpack | 2 + .../coq-makefile/compat-subdirs/subdir/Makefile | 3 ++ .../coq-makefile/compat-subdirs/theories/test.v | 7 +++ test-suite/coq-makefile/coqdoc1/_CoqProject | 11 +++++ test-suite/coq-makefile/coqdoc1/run.sh | 53 ++++++++++++++++++++++ test-suite/coq-makefile/coqdoc1/src/test.ml4 | 13 ++++++ test-suite/coq-makefile/coqdoc1/src/test.mli | 0 test-suite/coq-makefile/coqdoc1/src/test_aux.ml | 1 + test-suite/coq-makefile/coqdoc1/src/test_aux.mli | 1 + .../coq-makefile/coqdoc1/src/test_plugin.mlpack | 2 + .../coq-makefile/coqdoc1/theories/sub/testsub.v | 1 + test-suite/coq-makefile/coqdoc1/theories/test.v | 7 +++ test-suite/coq-makefile/merlin1/_CoqProject | 10 ++++ test-suite/coq-makefile/merlin1/run.sh | 13 ++++++ test-suite/coq-makefile/merlin1/src/test.ml4 | 13 ++++++ test-suite/coq-makefile/merlin1/src/test.mli | 0 test-suite/coq-makefile/merlin1/src/test_aux.ml | 1 + test-suite/coq-makefile/merlin1/src/test_aux.mli | 1 + .../coq-makefile/merlin1/src/test_plugin.mlpack | 2 + test-suite/coq-makefile/merlin1/theories/test.v | 7 +++ test-suite/coq-makefile/mllib1/_CoqProject | 9 ++++ test-suite/coq-makefile/mllib1/run.sh | 30 ++++++++++++ test-suite/coq-makefile/mllib1/src/test.ml4 | 13 ++++++ test-suite/coq-makefile/mllib1/src/test.mli | 0 test-suite/coq-makefile/mllib1/src/test_aux.ml | 1 + test-suite/coq-makefile/mllib1/src/test_aux.mli | 1 + .../coq-makefile/mllib1/src/test_plugin.mllib | 2 + test-suite/coq-makefile/mllib1/theories/test.v | 7 +++ test-suite/coq-makefile/mlpack1/_CoqProject | 10 ++++ test-suite/coq-makefile/mlpack1/run.sh | 25 ++++++++++ test-suite/coq-makefile/mlpack1/src/test.ml4 | 13 ++++++ test-suite/coq-makefile/mlpack1/src/test.mli | 0 test-suite/coq-makefile/mlpack1/src/test_aux.ml | 1 + test-suite/coq-makefile/mlpack1/src/test_aux.mli | 1 + .../coq-makefile/mlpack1/src/test_plugin.mlpack | 2 + test-suite/coq-makefile/mlpack1/theories/test.v | 7 +++ test-suite/coq-makefile/uninstall1/_CoqProject | 11 +++++ test-suite/coq-makefile/uninstall1/run.sh | 20 ++++++++ test-suite/coq-makefile/uninstall1/src/test.ml4 | 13 ++++++ test-suite/coq-makefile/uninstall1/src/test.mli | 0 test-suite/coq-makefile/uninstall1/src/test_aux.ml | 1 + .../coq-makefile/uninstall1/src/test_aux.mli | 1 + .../coq-makefile/uninstall1/src/test_plugin.mlpack | 2 + .../coq-makefile/uninstall1/theories/sub/testsub.v | 1 + test-suite/coq-makefile/uninstall1/theories/test.v | 7 +++ 54 files changed, 389 insertions(+), 1 deletion(-) create mode 100644 test-suite/coq-makefile/compat-subdirs/_CoqProject create mode 100755 test-suite/coq-makefile/compat-subdirs/run.sh create mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.ml4 create mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.mli create mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.ml create mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.mli create mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/compat-subdirs/subdir/Makefile create mode 100644 test-suite/coq-makefile/compat-subdirs/theories/test.v create mode 100644 test-suite/coq-makefile/coqdoc1/_CoqProject create mode 100755 test-suite/coq-makefile/coqdoc1/run.sh create mode 100644 test-suite/coq-makefile/coqdoc1/src/test.ml4 create mode 100644 test-suite/coq-makefile/coqdoc1/src/test.mli create mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.ml create mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.mli create mode 100644 test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v create mode 100644 test-suite/coq-makefile/coqdoc1/theories/test.v create mode 100644 test-suite/coq-makefile/merlin1/_CoqProject create mode 100755 test-suite/coq-makefile/merlin1/run.sh create mode 100644 test-suite/coq-makefile/merlin1/src/test.ml4 create mode 100644 test-suite/coq-makefile/merlin1/src/test.mli create mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.ml create mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.mli create mode 100644 test-suite/coq-makefile/merlin1/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/merlin1/theories/test.v create mode 100644 test-suite/coq-makefile/mllib1/_CoqProject create mode 100755 test-suite/coq-makefile/mllib1/run.sh create mode 100644 test-suite/coq-makefile/mllib1/src/test.ml4 create mode 100644 test-suite/coq-makefile/mllib1/src/test.mli create mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.ml create mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.mli create mode 100644 test-suite/coq-makefile/mllib1/src/test_plugin.mllib create mode 100644 test-suite/coq-makefile/mllib1/theories/test.v create mode 100644 test-suite/coq-makefile/mlpack1/_CoqProject create mode 100755 test-suite/coq-makefile/mlpack1/run.sh create mode 100644 test-suite/coq-makefile/mlpack1/src/test.ml4 create mode 100644 test-suite/coq-makefile/mlpack1/src/test.mli create mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.ml create mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.mli create mode 100644 test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/mlpack1/theories/test.v create mode 100644 test-suite/coq-makefile/uninstall1/_CoqProject create mode 100755 test-suite/coq-makefile/uninstall1/run.sh create mode 100644 test-suite/coq-makefile/uninstall1/src/test.ml4 create mode 100644 test-suite/coq-makefile/uninstall1/src/test.mli create mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.ml create mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.mli create mode 100644 test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/uninstall1/theories/sub/testsub.v create mode 100644 test-suite/coq-makefile/uninstall1/theories/test.v diff --git a/.gitignore b/.gitignore index 371136fc73..8bbfce5d80 100644 --- a/.gitignore +++ b/.gitignore @@ -60,6 +60,14 @@ test-suite/.nra.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt +test-suite/coq-makefile/*/actual +test-suite/coq-makefile/*/desired +test-suite/coq-makefile/*/Makefile +test-suite/coq-makefile/*/Makefile.conf +test-suite/coq-makefile/*/src/test.ml +test-suite/coq-makefile/*/html +test-suite/coq-makefile/*/mlihtml +test-suite/coq-makefile/*/subdir/done # documentation diff --git a/Makefile b/Makefile index 826ed17b05..7ba2c80f1c 100644 --- a/Makefile +++ b/Makefile @@ -54,6 +54,7 @@ FIND_VCS_CLAUSE:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' \ + -name 'coq-makefile' \ ')' -prune -o define find diff --git a/test-suite/Makefile b/test-suite/Makefile index afaa48463b..8a3d383cb4 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 0000000000..700d59d642 --- /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 0000000000..38e54d03eb --- /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 0000000000..8ddc9b0956 --- /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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..846c9b791b --- /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 0000000000..7753b56aae --- /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 0000000000..35792066bb --- /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 0000000000..bbe9717ab9 --- /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 < ()) "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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..755fc343f2 --- /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 0000000000..7753b56aae --- /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 0000000000..cb1ad4a4ba --- /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 0000000000..3b5d388c93 --- /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 0000000000..8ddc9b0956 --- /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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..7753b56aae --- /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 0000000000..6b2046d686 --- /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 0000000000..8f6b8e7ea5 --- /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 < ()) "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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..7753b56aae --- /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 0000000000..cb1ad4a4ba --- /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 0000000000..43d03be4a4 --- /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 < ()) "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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..7753b56aae --- /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 0000000000..706cf75cc7 --- /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 0000000000..a3bfe182b2 --- /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 < ()) "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 0000000000..e69de29bb2 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 0000000000..a01d0865a8 --- /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 0000000000..10020f27de --- /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 0000000000..cf94d851bb --- /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 0000000000..755fc343f2 --- /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 0000000000..7753b56aae --- /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. -- cgit v1.2.3 From 74176c031295893d705b4afe7ea45579a50e9a7b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jan 2017 10:38:57 +0100 Subject: ide/project_fie.ml4: include standard banner with copyright --- ide/project_file.ml4 | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index de0720e033..d32273bc20 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo.ml") *) | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) @@ -200,3 +208,5 @@ let args_from_project file project_files default_name = let newdir = Filename.dirname dir in if dir = newdir then "",[] else find_project_file newdir in find_project_file (Filename.dirname file) + +(* vim:set ft=ocaml: *) -- cgit v1.2.3 From 79bb444169f0ac919cf9672fb371ee42d98ead2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jan 2017 10:53:59 +0100 Subject: ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli The .mli only acknowledges the current API. I'm not guilty your honor! --- .gitignore | 2 +- Makefile.build | 2 +- ide/coqide.ml | 4 +- ide/ide.mllib | 2 + ide/project_file.ml4 | 212 ------------------------------------------------ lib/clib.mllib | 1 + lib/coqProject_file.ml4 | 212 ++++++++++++++++++++++++++++++++++++++++++++++++ lib/coqProject_file.mli | 68 ++++++++++++++++ tools/coq_makefile.ml | 22 ++--- 9 files changed, 298 insertions(+), 227 deletions(-) delete mode 100644 ide/project_file.ml4 create mode 100644 lib/coqProject_file.ml4 create mode 100644 lib/coqProject_file.mli diff --git a/.gitignore b/.gitignore index 8bbfce5d80..6e6f01a434 100644 --- a/.gitignore +++ b/.gitignore @@ -128,7 +128,7 @@ ide/xml_lexer.ml g_*.ml -ide/project_file.ml +lib/coqProject_file.ml parsing/cLexer.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml diff --git a/Makefile.build b/Makefile.build index 56f1fb8b49..8aedd9ceca 100644 --- a/Makefile.build +++ b/Makefile.build @@ -377,7 +377,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo +COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' diff --git a/ide/coqide.ml b/ide/coqide.ml index 0b7567a5ae..e47db8d192 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -84,7 +84,7 @@ let pr_exit_status = function let make_coqtop_args = function |None -> "", !sup_args |Some the_file -> - let get_args f = Project_file.args_from_project f + let get_args f = CoqProject_file.args_from_project f !custom_project_files project_file_name#get in match read_project#get with @@ -1346,7 +1346,7 @@ let read_coqide_args argv = else (output_string stderr "Error: multiple -coqtop options"; exit 1) |"-f" :: file :: args -> let d = CUnix.canonical_path_name (Filename.dirname file) in - let p = Project_file.read_project_file file in + let p = CoqProject_file.read_project_file file in filter_coqtop coqtop ((d,p) :: project_files) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 diff --git a/ide/ide.mllib b/ide/ide.mllib index 78b4c01e8c..57e9fe5adc 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,6 +9,8 @@ Config_lexer Utf8_convert Preferences Project_file +Serialize +Richprinter Xml_lexer Xml_parser Xml_printer diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 deleted file mode 100644 index d32273bc20..0000000000 --- a/ide/project_file.ml4 +++ /dev/null @@ -1,212 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = - | NoInstall - | TraditionalInstall - | UserInstall - | UnspecInstall - -exception Parsing_error -let rec parse_string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string s) - | [< >] -> "" -and parse_string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error -and parse_skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> parse_skip_comment s - | [< >] -> [< >] -and parse_args = parser - | [< '' ' | '\n' | '\t'; s >] -> parse_args s - | [< ''#'; s >] -> parse_args (parse_skip_comment s) - | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s - | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) - | [< >] -> [] - - -let parse f = - let c = open_in f in - let res = parse_args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts, l - | ("-h"|"--help") :: _ -> - raise Parsing_error - | ("-no-opt"|"-byte") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); - process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r - | "-no-install" :: r -> - Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); - process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r - | "-install" :: d :: r -> - if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); - let install = - match d with - | "user" -> UserInstall - | "none" -> NoInstall - | "global" -> TraditionalInstall - | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); - install - in - process_cmd_line orig_dir (project_file,makefile,install,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - Feedback.msg_warning (Pp.app - (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") - (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") - ); - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra" :: file :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra-phony" :: target :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r - | "-Q" :: d :: lp :: r -> - process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r - | "-I" :: d :: r -> - process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r - | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> - raise Parsing_error - | "-f" :: file :: r -> - let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in - let () = match project_file with - | None -> () - | Some _ -> Feedback.msg_warning (Pp.str - "Several features will not work with multiple project files.") - in - let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in - process_cmd_line orig_dir opts' l' r - | ["-f"] -> - raise Parsing_error - | "-o" :: file :: r -> - begin try - let _ = String.index file '/' in - raise Parsing_error - with Not_found -> - let () = match makefile with - |None -> () - |Some f -> - Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) - in process_cmd_line orig_dir (project_file,Some file,install,opt) l r - end - | v :: "=" :: def :: r -> - process_cmd_line orig_dir opts (Def (v,def) :: l) r - | "-arg" :: a :: r -> - process_cmd_line orig_dir opts (Arg a :: l) r - | f :: r -> - let f = CUnix.correct_path f orig_dir in - process_cmd_line orig_dir opts (( - if Filename.check_suffix f ".v" then V f - else if (Filename.check_suffix f ".ml") then ML f - else if (Filename.check_suffix f ".ml4") then ML4 f - else if (Filename.check_suffix f ".mli") then MLI f - else if (Filename.check_suffix f ".mllib") then MLLIB f - else if (Filename.check_suffix f ".mlpack") then MLPACK f - else Subdir f) :: l) r - -let process_cmd_line orig_dir opts l args = - let (opts, l) = process_cmd_line orig_dir opts l args in - opts, List.rev l - -let rec post_canonize f = - if Filename.basename f = Filename.current_dir_name - then let dir = Filename.dirname f in - if dir = Filename.current_dir_name then f else post_canonize dir - else f - -(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) -let split_arguments args = - List.fold_right - (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), - (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> - match a with - | V n -> - ((CUnix.remove_path_dot n::v,m,o,s),i,d) - | ML n -> - ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) - | MLI n -> - ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) - | ML4 n -> - ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) - | MLLIB n -> - ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) - | MLPACK n -> - ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) - | Special (n,dep,is_phony,c) -> - ((v,m,(n,dep,is_phony,c)::o,s),i,d) - | Subdir n -> - ((v,m,o,n::s),i,d) - | MLInclude p -> - let ml_new = (CUnix.remove_path_dot (post_canonize p), - CUnix.canonical_path_name p) in - (t,(ml_new::ml_inc,q_inc,r_inc),d) - | Include (p,l) -> - let q_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_new::q_inc,r_inc),d) - | RInclude (p,l) -> - let r_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_inc,r_new::r_inc),d) - | Def (v,def) -> - (t,i,(args,(v,def)::defs)) - | Arg a -> - (t,i,(a::args,defs))) - args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) - -let read_project_file f = - split_arguments - (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) - -let args_from_project file project_files default_name = - let build_cmd_line ml_inc i_inc r_inc args = - List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc - (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc - (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc - (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) - in try - let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in - fname, build_cmd_line ml_inc i_inc r_inc args - with Failure _ -> - let rec find_project_file dir = try - let fname = Filename.concat dir default_name in - let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file fname in - fname, build_cmd_line ml_inc i_inc r_inc args - with Sys_error s -> - let newdir = Filename.dirname dir in - if dir = newdir then "",[] else find_project_file newdir - in find_project_file (Filename.dirname file) - -(* vim:set ft=ocaml: *) diff --git a/lib/clib.mllib b/lib/clib.mllib index c73ae9b904..71f728291e 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -32,3 +32,4 @@ CUnix Envars Aux_file Monad +CoqProject_file diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 new file mode 100644 index 0000000000..d32273bc20 --- /dev/null +++ b/lib/coqProject_file.ml4 @@ -0,0 +1,212 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo.ml") *) + | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) + | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) + | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) + | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Arg of string + | Special of string * string * bool * string + (* file, dependencies, is_phony, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | MLInclude of string (* -I physicalpath *) + | Include of string * string (* -Q physicalpath logicalpath *) + | RInclude of string * string (* -R physicalpath logicalpath *) + +type install = + | NoInstall + | TraditionalInstall + | UserInstall + | UnspecInstall + +exception Parsing_error +let rec parse_string = parser + | [< '' ' | '\n' | '\t' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(parse_string s) + | [< >] -> "" +and parse_string2 = parser + | [< ''"' >] -> "" + | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) + | [< >] -> raise Parsing_error +and parse_skip_comment = parser + | [< ''\n'; s >] -> s + | [< 'c; s >] -> parse_skip_comment s + | [< >] -> [< >] +and parse_args = parser + | [< '' ' | '\n' | '\t'; s >] -> parse_args s + | [< ''#'; s >] -> parse_args (parse_skip_comment s) + | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s + | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) + | [< >] -> [] + + +let parse f = + let c = open_in f in + let res = parse_args (Stream.of_channel c) in + close_in c; + res + +let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function + | [] -> opts, l + | ("-h"|"--help") :: _ -> + raise Parsing_error + | ("-no-opt"|"-byte") :: r -> + process_cmd_line orig_dir (project_file,makefile,install,false) l r + | ("-full"|"-opt") :: r -> + process_cmd_line orig_dir (project_file,makefile,install,true) l r + | "-impredicative-set" :: r -> + Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); + process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r + | "-no-install" :: r -> + Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); + process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r + | "-install" :: d :: r -> + if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); + let install = + match d with + | "user" -> UserInstall + | "none" -> NoInstall + | "global" -> TraditionalInstall + | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); + install + in + process_cmd_line orig_dir (project_file,makefile,install,opt) l r + | "-custom" :: com :: dependencies :: file :: r -> + Feedback.msg_warning (Pp.app + (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") + (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") + ); + process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r + | "-extra" :: file :: dependencies :: com :: r -> + process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r + | "-extra-phony" :: target :: dependencies :: com :: r -> + process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r + | "-Q" :: d :: lp :: r -> + process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r + | "-I" :: d :: r -> + process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r + | "-R" :: p :: lp :: r -> + process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r + | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> + raise Parsing_error + | "-f" :: file :: r -> + let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in + let () = match project_file with + | None -> () + | Some _ -> Feedback.msg_warning (Pp.str + "Several features will not work with multiple project files.") + in + let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in + process_cmd_line orig_dir opts' l' r + | ["-f"] -> + raise Parsing_error + | "-o" :: file :: r -> + begin try + let _ = String.index file '/' in + raise Parsing_error + with Not_found -> + let () = match makefile with + |None -> () + |Some f -> + Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) + in process_cmd_line orig_dir (project_file,Some file,install,opt) l r + end + | v :: "=" :: def :: r -> + process_cmd_line orig_dir opts (Def (v,def) :: l) r + | "-arg" :: a :: r -> + process_cmd_line orig_dir opts (Arg a :: l) r + | f :: r -> + let f = CUnix.correct_path f orig_dir in + process_cmd_line orig_dir opts (( + if Filename.check_suffix f ".v" then V f + else if (Filename.check_suffix f ".ml") then ML f + else if (Filename.check_suffix f ".ml4") then ML4 f + else if (Filename.check_suffix f ".mli") then MLI f + else if (Filename.check_suffix f ".mllib") then MLLIB f + else if (Filename.check_suffix f ".mlpack") then MLPACK f + else Subdir f) :: l) r + +let process_cmd_line orig_dir opts l args = + let (opts, l) = process_cmd_line orig_dir opts l args in + opts, List.rev l + +let rec post_canonize f = + if Filename.basename f = Filename.current_dir_name + then let dir = Filename.dirname f in + if dir = Filename.current_dir_name then f else post_canonize dir + else f + +(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) +let split_arguments args = + List.fold_right + (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), + (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> + match a with + | V n -> + ((CUnix.remove_path_dot n::v,m,o,s),i,d) + | ML n -> + ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) + | MLI n -> + ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) + | ML4 n -> + ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) + | MLLIB n -> + ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) + | MLPACK n -> + ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) + | Special (n,dep,is_phony,c) -> + ((v,m,(n,dep,is_phony,c)::o,s),i,d) + | Subdir n -> + ((v,m,o,n::s),i,d) + | MLInclude p -> + let ml_new = (CUnix.remove_path_dot (post_canonize p), + CUnix.canonical_path_name p) in + (t,(ml_new::ml_inc,q_inc,r_inc),d) + | Include (p,l) -> + let q_new = (CUnix.remove_path_dot (post_canonize p),l, + CUnix.canonical_path_name p) in + (t,(ml_inc,q_new::q_inc,r_inc),d) + | RInclude (p,l) -> + let r_new = (CUnix.remove_path_dot (post_canonize p),l, + CUnix.canonical_path_name p) in + (t,(ml_inc,q_inc,r_new::r_inc),d) + | Def (v,def) -> + (t,i,(args,(v,def)::defs)) + | Arg a -> + (t,i,(a::args,defs))) + args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) + +let read_project_file f = + split_arguments + (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) + +let args_from_project file project_files default_name = + let build_cmd_line ml_inc i_inc r_inc args = + List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc + (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc + (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc + (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) + in try + let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in + fname, build_cmd_line ml_inc i_inc r_inc args + with Failure _ -> + let rec find_project_file dir = try + let fname = Filename.concat dir default_name in + let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = + read_project_file fname in + fname, build_cmd_line ml_inc i_inc r_inc args + with Sys_error s -> + let newdir = Filename.dirname dir in + if dir = newdir then "",[] else find_project_file newdir + in find_project_file (Filename.dirname file) + +(* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli new file mode 100644 index 0000000000..36513dbde5 --- /dev/null +++ b/lib/coqProject_file.mli @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (ML "foo.ml") *) + | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) + | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) + | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) + | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) + | V of string (* V file : foo.v -> (V "foo") *) + | Arg of string + | Special of string * string * bool * string + (* file, dependencies, is_phony, command *) + | Subdir of string + | Def of string * string (* X=foo -> Def ("X","foo") *) + | MLInclude of string (* -I physicalpath *) + | Include of string * string (* -Q physicalpath logicalpath *) + | RInclude of string * string (* -R physicalpath logicalpath *) + +type install = + | NoInstall + | TraditionalInstall + | UserInstall + | UnspecInstall + +exception Parsing_error + +val args_from_project : + string -> + (string * + ('a * + (('b * string) list * ('c * string * string) list * + ('d * string * string) list) * + (string list * 'e))) + list -> string -> string * string list + +val read_project_file : + string -> + (string list * + (string list * string list * string list * string list * + string list) * + (string * string * bool * string) list * string list) * + ((string * string) list * (string * string * string) list * + (string * string * string) list) * + (string list * (string * string) list) + +val process_cmd_line : + string -> + string option * string option * install * bool -> + target list -> + string list -> + (string option * string option * install * bool) * target list + +val split_arguments : + target list -> + (string list * + (string list * string list * string list * string list * + string list) * + (string * string * bool * string) list * string list) * + ((string * string) list * (string * string * string) list * + (string * string * string) list) * + (string list * (string * string) list) + diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4875cb62bf..d729162328 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -282,7 +282,7 @@ let where_put_doc = function "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function - |Project_file.NoInstall -> () + |CoqProject_file.NoInstall -> () |is_install -> let not_empty = function |[] -> false |_::_ -> true in let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in @@ -295,7 +295,7 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in - if is_install = Project_file.UnspecInstall then begin + if is_install = CoqProject_file.UnspecInstall then begin print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" end; if not_empty cmxss then begin @@ -533,8 +533,8 @@ let variables is_install opt (args,defs) = \n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with - | Project_file.NoInstall -> () - | Project_file.UnspecInstall -> + | CoqProject_file.NoInstall -> () + | CoqProject_file.UnspecInstall -> section "Install Paths."; print "ifdef USERINSTALL\n"; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; @@ -545,13 +545,13 @@ let variables is_install opt (args,defs) = print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "endif\n\n" - | Project_file.TraditionalInstall -> + | CoqProject_file.TraditionalInstall -> section "Install Paths."; print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "\n" - | Project_file.UserInstall -> + | CoqProject_file.UserInstall -> section "Install Paths."; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; @@ -895,11 +895,11 @@ let do_makefile args = |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = try - Project_file.process_cmd_line Filename.current_dir_name - (None,None,Project_file.UnspecInstall,true) [] args - with Project_file.Parsing_error -> usage () in + CoqProject_file.process_cmd_line Filename.current_dir_name + (None,None,CoqProject_file.UnspecInstall,true) [] args + with CoqProject_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs = - Project_file.split_arguments l in + CoqProject_file.split_arguments l in let () = match project_file with |None -> () |Some f -> make_name := f in let () = match makefile with @@ -920,7 +920,7 @@ let do_makefile args = List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in - if is_install <> Project_file.NoInstall then begin + if is_install <> CoqProject_file.NoInstall then begin warn_install_at_root_directory targets inc; end; check_overlapping_include inc; -- cgit v1.2.3 From 088ddea70d2d9121d76f0f3c6c0412fd2a67ff0a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 3 Jan 2017 16:15:40 +0100 Subject: CoqProject_file: API and code cleanup (tuples -> records) --- ide/coqide.ml | 44 ++++--- lib/coqProject_file.ml4 | 320 ++++++++++++++++++++++++------------------------ lib/coqProject_file.mli | 91 ++++++-------- tools/coq_makefile.ml | 50 +++++--- 4 files changed, 260 insertions(+), 245 deletions(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index e47db8d192..ec3ea69bb9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -46,7 +46,7 @@ open Session (** The arguments that will be passed to coqtop. No quoting here, since no /bin/sh when using create_process instead of open_process. *) -let custom_project_files = ref [] +let custom_project_file = ref None let sup_args = ref [] let logfile = ref None @@ -81,17 +81,27 @@ let pr_exit_status = function | Unix.WEXITED 0 -> " succeeded" | _ -> " failed" -let make_coqtop_args = function - |None -> "", !sup_args - |Some the_file -> - let get_args f = CoqProject_file.args_from_project f - !custom_project_files project_file_name#get - in - match read_project#get with - |Ignore_args -> "", !sup_args - |Append_args -> - let fname, args = get_args the_file in fname, args @ !sup_args - |Subst_args -> get_args the_file +let make_coqtop_args fname = + let open CoqProject_file in + let base_args = match read_project#get with + | Ignore_args -> !sup_args + | Append_args -> !sup_args + | Subst_args -> [] in + if read_project#get = Ignore_args then "", base_args + else + match !custom_project_file, fname with + | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args + | None, None -> "", base_args + | None, Some the_file -> + match + CoqProject_file.find_project_file + ~from:(Filename.dirname the_file) + ~projfile_name:project_file_name#get + with + | None -> "", base_args + | Some proj -> + proj, coqtop_args_from_project (read_project_file proj) @ base_args +;; (** Setting drag & drop on widgets *) @@ -1345,9 +1355,11 @@ let read_coqide_args argv = if coqtop = None then filter_coqtop (Some prog) project_files out args else (output_string stderr "Error: multiple -coqtop options"; exit 1) |"-f" :: file :: args -> + if project_files <> None then + (output_string stderr "Error: multiple -f options"; exit 1); let d = CUnix.canonical_path_name (Filename.dirname file) in let p = CoqProject_file.read_project_file file in - filter_coqtop coqtop ((d,p) :: project_files) out args + filter_coqtop coqtop (Some (d,p)) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 |"-coqtop" :: [] -> @@ -1364,11 +1376,11 @@ let read_coqide_args argv = (* argument added by MacOS during .app launch *) filter_coqtop coqtop project_files out args |arg::args -> filter_coqtop coqtop project_files (arg::out) args - |[] -> (coqtop,List.rev project_files,List.rev out) + |[] -> (coqtop,project_files,List.rev out) in - let coqtop,project_files,argv = filter_coqtop None [] [] argv in + let coqtop,project_files,argv = filter_coqtop None None [] argv in Ideutils.custom_coqtop := coqtop; - custom_project_files := project_files; + custom_project_file := project_files; argv diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index d32273bc20..9327f173e8 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -6,29 +6,77 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type target = - | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = +type project = { + project_file : string option; + makefile : string option; + install_kind : install option; + use_ocamlopt : bool; + + v_files : string list; + mli_files : string list; + ml4_files : string list; + ml_files : string list; + mllib_files : string list; + mlpack_files : string list; + + extra_targets : extra_target list; + subdirs : string list; + ml_includes : path list; + r_includes : (path * logic_path) list; + q_includes : (path * logic_path) list; + extra_args : string list; + defs : (string * string) list; +} +and extra_target = { + target : string; + dependencies : string; + phony : bool; + command : string; +} +and logic_path = string +and path = { path : string; canonical_path : string } +and install = | NoInstall | TraditionalInstall | UserInstall - | UnspecInstall -exception Parsing_error +(* TODO generate with PPX *) +let mk_project project_file makefile install_kind use_ocamlopt = { + project_file; + makefile; + install_kind; + use_ocamlopt; + + v_files = []; + mli_files = []; + ml4_files = []; + ml_files = []; + mllib_files = []; + mlpack_files = []; + extra_targets = []; + subdirs = []; + ml_includes = []; + r_includes = []; + q_includes = []; + extra_args = []; + defs = []; +} + +(********************* utils ********************************************) + +let rec post_canonize f = + if Filename.basename f = Filename.current_dir_name + then let dir = Filename.dirname f in + if dir = Filename.current_dir_name then f else post_canonize dir + else f + +(* Avoid Sys.is_directory raise an exception (if the file does not exists) *) +let is_directory f = Sys.file_exists f && Sys.is_directory f + +(********************* parser *******************************************) + +exception Parsing_error of string + let rec parse_string = parser | [< '' ' | '\n' | '\t' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string s) @@ -36,7 +84,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise Parsing_error + | [< >] -> raise (Parsing_error "unterminated string") and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s @@ -48,165 +96,117 @@ and parse_args = parser | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) | [< >] -> [] - let parse f = let c = open_in f in let res = parse_args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function - | [] -> opts, l - | ("-h"|"--help") :: _ -> - raise Parsing_error - | ("-no-opt"|"-byte") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,false) l r - | ("-full"|"-opt") :: r -> - process_cmd_line orig_dir (project_file,makefile,install,true) l r - | "-impredicative-set" :: r -> - Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform."); - process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r - | "-no-install" :: r -> - Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead"))); - process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r + close_in c; + res +;; + +let process_cmd_line orig_dir proj args = + let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in + let mk_path d = + let p = CUnix.correct_path d orig_dir in + { path = CUnix.remove_path_dot (post_canonize p); + canonical_path = CUnix.canonical_path_name p } in + let rec aux proj = function + | [] -> proj + | "-impredicative-set" :: _ -> + error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\"" + | "-no-install" :: _ -> + error "Use \"-install none\" instead of \"-no-install\"" + | "-custom" :: _ -> + error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\"" + + | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r + | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> - if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once."); - let install = - match d with - | "user" -> UserInstall - | "none" -> NoInstall - | "global" -> TraditionalInstall - | _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install."))); - install - in - process_cmd_line orig_dir (project_file,makefile,install,opt) l r - | "-custom" :: com :: dependencies :: file :: r -> - Feedback.msg_warning (Pp.app - (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".") - (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.") - ); - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra" :: file :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r - | "-extra-phony" :: target :: dependencies :: com :: r -> - process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r + if proj.install_kind <> None then + Feedback.msg_warning (Pp.str "-install set more than once."); + let install = match d with + | "user" -> UserInstall + | "none" -> NoInstall + | "global" -> TraditionalInstall + | _ -> error ("invalid option \""^d^"\" passed to -install") in + aux { proj with install_kind = Some install } r + | "-extra" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = false; command } in + aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + | "-extra-phony" :: target :: dependencies :: command :: r -> + let tgt = { target; dependencies; phony = true; command } in + aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + | "-Q" :: d :: lp :: r -> - process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r + aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r | "-I" :: d :: r -> - process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: lp :: r -> - process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r - | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> - raise Parsing_error + aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r + | "-R" :: d :: lp :: r -> + aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r + | "-f" :: file :: r -> let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in - let () = match project_file with + let () = match proj.project_file with | None -> () | Some _ -> Feedback.msg_warning (Pp.str - "Several features will not work with multiple project files.") + "Multiple project files are deprecated.") in - let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in - process_cmd_line orig_dir opts' l' r - | ["-f"] -> - raise Parsing_error + let proj = aux { proj with project_file = Some file } (parse file) in + aux proj r + | "-o" :: file :: r -> - begin try - let _ = String.index file '/' in - raise Parsing_error - with Not_found -> - let () = match makefile with - |None -> () - |Some f -> - Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be."))) - in process_cmd_line orig_dir (project_file,Some file,install,opt) l r - end + if String.contains file '/' then + error "Output file must be in the current directory"; + if proj.makefile <> None then + error "Option -o given more than once"; + aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> - process_cmd_line orig_dir opts (Def (v,def) :: l) r + aux { proj with defs = proj.defs @ [v,def] } r | "-arg" :: a :: r -> - process_cmd_line orig_dir opts (Arg a :: l) r + aux { proj with extra_args = proj.extra_args @ [a] } r | f :: r -> let f = CUnix.correct_path f orig_dir in - process_cmd_line orig_dir opts (( - if Filename.check_suffix f ".v" then V f - else if (Filename.check_suffix f ".ml") then ML f - else if (Filename.check_suffix f ".ml4") then ML4 f - else if (Filename.check_suffix f ".mli") then MLI f - else if (Filename.check_suffix f ".mllib") then MLLIB f - else if (Filename.check_suffix f ".mlpack") then MLPACK f - else Subdir f) :: l) r - -let process_cmd_line orig_dir opts l args = - let (opts, l) = process_cmd_line orig_dir opts l args in - opts, List.rev l + let proj = + if is_directory f then { proj with subdirs = proj.subdirs @ [f] } + else match CUnix.get_extension f with + | ".v" -> { proj with v_files = proj.v_files @ [f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [f] } + | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] } + | _ -> raise (Parsing_error ("Unknown option "^f)) in + aux proj r + in + aux proj args -let rec post_canonize f = - if Filename.basename f = Filename.current_dir_name - then let dir = Filename.dirname f in - if dir = Filename.current_dir_name then f else post_canonize dir - else f + (******************************* API ************************************) -(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *) -let split_arguments args = - List.fold_right - (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t), - (ml_inc,q_inc,r_inc as i),(args,defs as d)) -> - match a with - | V n -> - ((CUnix.remove_path_dot n::v,m,o,s),i,d) - | ML n -> - ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d) - | MLI n -> - ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d) - | ML4 n -> - ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d) - | MLLIB n -> - ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d) - | MLPACK n -> - ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d) - | Special (n,dep,is_phony,c) -> - ((v,m,(n,dep,is_phony,c)::o,s),i,d) - | Subdir n -> - ((v,m,o,n::s),i,d) - | MLInclude p -> - let ml_new = (CUnix.remove_path_dot (post_canonize p), - CUnix.canonical_path_name p) in - (t,(ml_new::ml_inc,q_inc,r_inc),d) - | Include (p,l) -> - let q_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_new::q_inc,r_inc),d) - | RInclude (p,l) -> - let r_new = (CUnix.remove_path_dot (post_canonize p),l, - CUnix.canonical_path_name p) in - (t,(ml_inc,q_inc,r_new::r_inc),d) - | Def (v,def) -> - (t,i,(args,(v,def)::defs)) - | Arg a -> - (t,i,(a::args,defs))) - args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[])) +let cmdline_args_to_project ~curdir args = + process_cmd_line curdir (mk_project None None None true) args let read_project_file f = - split_arguments - (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) - -let args_from_project file project_files default_name = - let build_cmd_line ml_inc i_inc r_inc args = - List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc - (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc - (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc - (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) - in try - let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in - fname, build_cmd_line ml_inc i_inc r_inc args - with Failure _ -> - let rec find_project_file dir = try - let fname = Filename.concat dir default_name in - let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file fname in - fname, build_cmd_line ml_inc i_inc r_inc args - with Sys_error s -> - let newdir = Filename.dirname dir in - if dir = newdir then "",[] else find_project_file newdir - in find_project_file (Filename.dirname file) + process_cmd_line (Filename.dirname f) + (mk_project (Some f) None (Some NoInstall) true) (parse f) + +let rec find_project_file ~from ~projfile_name = + let fname = Filename.concat from projfile_name in + if Sys.file_exists fname then Some fname + else + let newdir = Filename.dirname from in + if newdir = "" || newdir = "/" then None + else find_project_file ~from:newdir ~projfile_name +;; + +let coqtop_args_from_project + { ml_includes; r_includes; q_includes; extra_args } += + let map = List.map in + let args = + map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ + map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ + map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ + [extra_args] in + List.flatten args +;; (* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 36513dbde5..2bcf658fcf 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -6,63 +6,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type target = - | ML of string (* ML file : foo.ml -> (ML "foo.ml") *) - | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *) - | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *) - | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *) - | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Arg of string - | Special of string * string * bool * string - (* file, dependencies, is_phony, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | MLInclude of string (* -I physicalpath *) - | Include of string * string (* -Q physicalpath logicalpath *) - | RInclude of string * string (* -R physicalpath logicalpath *) - -type install = +exception Parsing_error of string + +type project = { + project_file : string option; + makefile : string option; + install_kind : install option; + use_ocamlopt : bool; + + v_files : string list; + mli_files : string list; + ml4_files : string list; + ml_files : string list; + mllib_files : string list; + mlpack_files : string list; + + extra_targets : extra_target list; + subdirs : string list; + ml_includes : path list; + r_includes : (path * logic_path) list; + q_includes : (path * logic_path) list; + extra_args : string list; + defs : (string * string) list; +} +and extra_target = { + target : string; + dependencies : string; + phony : bool; + command : string; +} +and logic_path = string +and path = { path : string; canonical_path : string } +and install = | NoInstall | TraditionalInstall | UserInstall - | UnspecInstall - -exception Parsing_error - -val args_from_project : - string -> - (string * - ('a * - (('b * string) list * ('c * string * string) list * - ('d * string * string) list) * - (string list * 'e))) - list -> string -> string * string list - -val read_project_file : - string -> - (string list * - (string list * string list * string list * string list * - string list) * - (string * string * bool * string) list * string list) * - ((string * string) list * (string * string * string) list * - (string * string * string) list) * - (string list * (string * string) list) - -val process_cmd_line : - string -> - string option * string option * install * bool -> - target list -> - string list -> - (string option * string option * install * bool) * target list -val split_arguments : - target list -> - (string list * - (string list * string list * string list * string list * - string list) * - (string * string * bool * string) list * string list) * - ((string * string) list * (string * string * string) list * - (string * string * string) list) * - (string list * (string * string) list) +val cmdline_args_to_project : curdir:string -> string list -> project +val read_project_file : string -> project +val coqtop_args_from_project : project -> string list +val find_project_file : from:string -> projfile_name:string -> string option diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d729162328..0b2c401706 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -282,7 +282,7 @@ let where_put_doc = function "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function - |CoqProject_file.NoInstall -> () + |Some CoqProject_file.NoInstall -> () |is_install -> let not_empty = function |[] -> false |_::_ -> true in let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in @@ -295,7 +295,7 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in - if is_install = CoqProject_file.UnspecInstall then begin + if is_install = None then begin print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" end; if not_empty cmxss then begin @@ -533,8 +533,8 @@ let variables is_install opt (args,defs) = \n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with - | CoqProject_file.NoInstall -> () - | CoqProject_file.UnspecInstall -> + | Some CoqProject_file.NoInstall -> () + | None -> section "Install Paths."; print "ifdef USERINSTALL\n"; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; @@ -545,13 +545,13 @@ let variables is_install opt (args,defs) = print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "endif\n\n" - | CoqProject_file.TraditionalInstall -> + | Some CoqProject_file.TraditionalInstall -> section "Install Paths."; print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; print "\n" - | CoqProject_file.UserInstall -> + | Some CoqProject_file.UserInstall -> section "Install Paths."; print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; @@ -890,16 +890,38 @@ let merlin targets (ml_inc,_,_) = print "\n" let do_makefile args = + let open CoqProject_file in let has_file var = function |[] -> var := false |_::_ -> var := true in - let (project_file,makefile,is_install,opt),l = - try - CoqProject_file.process_cmd_line Filename.current_dir_name - (None,None,CoqProject_file.UnspecInstall,true) [] args - with CoqProject_file.Parsing_error -> usage () in - let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs = - CoqProject_file.split_arguments l in + let { + project_file = project_file; + makefile; + install_kind = is_install; + use_ocamlopt = opt; + v_files = v_f; + mli_files = mli_f; + ml4_files = ml4_f; + ml_files = ml_f; + mllib_files = mllib_f; + mlpack_files = mlpack_f; + extra_targets; + subdirs = sds; + ml_includes; + r_includes; + q_includes; + extra_args; + defs; + } = + try cmdline_args_to_project Filename.current_dir_name args + with Parsing_error s -> prerr_endline s; usage () in + let sps = List.map (fun { target = fn; dependencies = d; phony = p; command = c } -> fn, d, p, c) extra_targets in + let targets = (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds) in + let inc = + List.map (fun ({ path = p; canonical_path = c }) -> p,c) ml_includes, + List.map (fun ({ path = p; canonical_path = c },l) -> p,l,c) q_includes, + List.map (fun ({ path = p; canonical_path = c },l) -> p,l,c) r_includes in + let defs = extra_args, defs in let () = match project_file with |None -> () |Some f -> make_name := f in let () = match makefile with @@ -920,7 +942,7 @@ let do_makefile args = List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in - if is_install <> CoqProject_file.NoInstall then begin + if is_install <> (Some CoqProject_file.NoInstall) then begin warn_install_at_root_directory targets inc; end; check_overlapping_include inc; -- cgit v1.2.3 From da5ac9169d0c65ff389104dfd983311b85e059e2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Jan 2017 17:03:37 +0100 Subject: CoqProject_file: document in API deprecated features --- lib/coqProject_file.ml4 | 5 +++-- lib/coqProject_file.mli | 7 +++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 9327f173e8..64076d6049 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -19,13 +19,14 @@ type project = { mllib_files : string list; mlpack_files : string list; - extra_targets : extra_target list; - subdirs : string list; ml_includes : path list; r_includes : (path * logic_path) list; q_includes : (path * logic_path) list; extra_args : string list; defs : (string * string) list; + + extra_targets : extra_target list; + subdirs : string list; } and extra_target = { target : string; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 2bcf658fcf..8c8fc068a3 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -21,13 +21,16 @@ type project = { mllib_files : string list; mlpack_files : string list; - extra_targets : extra_target list; - subdirs : string list; ml_includes : path list; r_includes : (path * logic_path) list; q_includes : (path * logic_path) list; extra_args : string list; defs : (string * string) list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target list; + subdirs : string list; + } and extra_target = { target : string; -- cgit v1.2.3 From b2b4e85ec6607d7364a0da9c65ae9303b9f73c03 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 4 Jan 2017 14:35:51 +0100 Subject: Usage.print_config moved to Envars --- lib/envars.ml | 15 +++++++++++++++ lib/envars.mli | 3 +++ tools/coqc.ml | 2 +- toplevel/coqtop.ml | 2 +- toplevel/usage.ml | 13 ------------- toplevel/usage.mli | 2 -- 6 files changed, 20 insertions(+), 17 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index 89ce528318..330b0fbd60 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -207,3 +207,18 @@ let xdg_config_dirs warn = let xdg_dirs ~warn = List.filter Sys.file_exists (xdg_data_dirs warn) + +(* Print the configuration information *) + +let print_config f = + let open Printf in + fprintf f "LOCAL=%s\n" (if Coq_config.local then "1" else "0"); + fprintf f "COQLIB=%s/\n" (coqlib ()); + fprintf f "DOCDIR=%s/\n" (docdir ()); + fprintf f "OCAMLFIND=%s\n" (ocamlfind ()); + fprintf f "CAMLP4=%s\n" Coq_config.camlp4; + fprintf f "CAMLP4O=%s\n" Coq_config.camlp4o; + fprintf f "CAMLP4BIN=%s/\n" (camlp4bin ()); + fprintf f "CAMLP4LIB=%s\n" (camlp4lib ()); + fprintf f "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat; + fprintf f "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") diff --git a/lib/envars.mli b/lib/envars.mli index 90a42859b9..b9cc534f97 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -69,3 +69,6 @@ val xdg_data_home : (string -> unit) -> string val xdg_config_dirs : (string -> unit) -> string list val xdg_data_dirs : (string -> unit) -> string list val xdg_dirs : warn : (string -> unit) -> string list + +(** {6 Prints the configuration information } *) +val print_config : out_channel -> unit diff --git a/tools/coqc.ml b/tools/coqc.ml index 552a943c8c..e9f79212b7 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -83,7 +83,7 @@ let parse_args () = | ("-config" | "--config") :: _ -> Envars.set_coqlib ~fail:(fun x -> x); - Usage.print_config (); + Envars.print_config stdout; exit 0 (* Options for coqtop : a) options with 0 argument *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 41d370ea57..4237ef3601 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -620,7 +620,7 @@ let init_toplevel arglist = Spawned.init_channels (); Envars.set_coqlib ~fail:CErrors.error; if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); - if !print_config then (Usage.print_config (); exit (exitcode ())); + if !print_config then (Envars.print_config stdout; exit (exitcode ())); if !print_tags then (print_style_tags (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); init_load_path (); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e290480354..67701d73ea 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -115,16 +115,3 @@ let print_usage_coqc () = flush stderr ; exit 1 -(* Print the configuration information *) - -let print_config () = - if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); - Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); - Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ()); - Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; - Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o; - Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ()); - Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ()); - Printf.printf "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat; - Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") diff --git a/toplevel/usage.mli b/toplevel/usage.mli index dccb40e713..c46c7a79c0 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -21,5 +21,3 @@ val add_to_usage : string -> string -> unit val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit -(** {6 Prints the configuration information } *) -val print_config : unit -> unit -- cgit v1.2.3 From 11ec801fa17434b0a3aad2c88a4422a22f1c4c44 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 4 Jan 2017 14:46:52 +0100 Subject: Put the list of Coq sources subdirectories in one place and avoid duplication --- lib/envars.ml | 10 ++++++++-- lib/envars.mli | 3 +++ tools/coq_makefile.ml | 8 +------- toplevel/coqinit.ml | 8 ++------ 4 files changed, 14 insertions(+), 15 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index 330b0fbd60..b20d39fb55 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -146,8 +146,6 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind") - let ocamlfind () = if !Flags.ocamlfind_spec then !Flags.ocamlfind else if !Flags.boot then Coq_config.ocamlfind else @@ -210,6 +208,13 @@ let xdg_dirs ~warn = (* Print the configuration information *) +let coq_src_subdirs = [ + "config" ; "dev" ; "lib" ; "kernel" ; "library" ; + "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ; + "tactics" ; "toplevel" ; "printing" ; "intf" ; + "grammar" ; "ide" ; "stm"; "vernac" ] @ + Coq_config.plugins_dirs + let print_config f = let open Printf in fprintf f "LOCAL=%s\n" (if Coq_config.local then "1" else "0"); @@ -222,3 +227,4 @@ let print_config f = fprintf f "CAMLP4LIB=%s\n" (camlp4lib ()); fprintf f "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat; fprintf f "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") + diff --git a/lib/envars.mli b/lib/envars.mli index b9cc534f97..d158407b46 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -72,3 +72,6 @@ val xdg_dirs : warn : (string -> unit) -> string list (** {6 Prints the configuration information } *) val print_config : out_channel -> unit + +(** Directories in which coq sources are found *) +val coq_src_subdirs : string list diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0b2c401706..379cc856b5 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -47,13 +47,7 @@ let section s = (* These are the Coq library directories that are used for * plugin development *) -let lib_dirs = - ["kernel"; "lib"; "library"; "parsing"; - "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; - "vernac"; "stm"; "toplevel"; "grammar"; "config"; - "engine"] - +let lib_dirs = Envars.coq_src_subdirs let usage () = output_string stderr "Usage summary:\ diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 2b9a04dad8..8fca302687 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -121,14 +121,10 @@ let init_library_roots () = find the "include" file in the *source* directory *) let init_ocaml_path () = let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) + Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl]) in Mltop.add_ml_dir (Envars.coqlib ()); - List.iter add_subdir - [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; - [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; - [ "grammar" ]; [ "ide" ]; [ "ltac" ]; [ "vernac" ]; ] + List.iter add_subdir Envars.coq_src_subdirs let get_compat_version = function | "8.7" -> Flags.Current -- cgit v1.2.3 From 577f6d0e5c4eecca3a3cd46dfc37084123f4adf6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Jan 2017 16:57:58 +0100 Subject: Document --print-version in Usage --- tools/coqc.ml | 3 +++ toplevel/usage.ml | 3 ++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/tools/coqc.ml b/tools/coqc.ml index e9f79212b7..9857d43188 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -85,6 +85,9 @@ let parse_args () = Envars.set_coqlib ~fail:(fun x -> x); Envars.print_config stdout; exit 0 + + |"--print-version" :: _ -> + Usage.machine_readable_version 0 (* Options for coqtop : a) options with 0 argument *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 67701d73ea..c43f0ff058 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -56,7 +56,8 @@ let print_usage_channel co command = \n\ \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ -\n -v print Coq version and exit\ +\n -v, --version print Coq version and exit\ +\n --print-version print Coq version in easy to parse format and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ \n -quiet unset display of extra information (implies -w \"-all\")\ -- cgit v1.2.3 From cd6dd06789139ee0ff5c2b79a280476999fe2bf1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Jan 2017 17:03:10 +0100 Subject: print_config: print COQ_SRC_SUBDIRS This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile --- lib/envars.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/envars.ml b/lib/envars.ml index b20d39fb55..8654ee1a51 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -226,5 +226,7 @@ let print_config f = fprintf f "CAMLP4BIN=%s/\n" (camlp4bin ()); fprintf f "CAMLP4LIB=%s\n" (camlp4lib ()); fprintf f "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat; - fprintf f "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") + fprintf f "HASNATDYNLINK=%s\n" + (if Coq_config.has_natdynlink then "true" else "false"); + fprintf f "COQ_SRC_SUBDIRS=%s\n" (String.concat " " coq_src_subdirs) -- cgit v1.2.3 From e94334670c7aa9c96e40d678fcc7a7a70cfd0099 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 5 Jan 2017 17:01:13 +0100 Subject: coqdep: set FOR_PACK variable for files that need to be packed This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack. --- tools/coqdep_common.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 93b25e2ede..281644d23e 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -293,15 +293,15 @@ let traite_fichier_modules md ext = (fun a_faire str -> match search_mlpack_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file + a_faire @ [file] | None -> match search_ml_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file - | None -> a_faire) "" list + a_faire @ [file] + | None -> a_faire) [] list with - | Sys_error _ -> "" + | Sys_error _ -> [] | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) (* Makefile's escaping rules are awful: $ is escaped by doubling and @@ -443,7 +443,7 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mllib" in let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; flush stdout) @@ -453,9 +453,13 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mlpack" in let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; + let efullname_capital = String.capitalize (Filename.basename efullname) in + List.iter (fun dep -> + printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) + dep; flush stdout) (List.rev !mlpackAccu) -- cgit v1.2.3 From 046657081fb769fcf033c7d7c6b3fb6e861a0996 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 6 Jan 2017 14:57:40 +0100 Subject: ocamlfind: coqtop -config prints ocamlfind as found by ./configure Used to guess again the ocamlfind location at Coq's execution time. An option to override the value (inferred at ./configure time) is available. So, what is the point of guessing it? Either it stays there, or the user is doing a hack, and has a flag to do it. --- lib/envars.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/lib/envars.ml b/lib/envars.ml index 8654ee1a51..47d9670da1 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -147,9 +147,7 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else - if !Flags.boot then Coq_config.ocamlfind else - try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind + if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind (** {2 Camlp4 paths} *) -- cgit v1.2.3 From 4252789c77479b9d4a9ac5a12e9a24067b086040 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Jan 2017 10:35:09 +0100 Subject: coqdep: remove optimization making makefiles harder to write --- tools/coqdep.ml | 2 +- tools/coqdep_common.ml | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 1c1c1be6aa..930b092d3b 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -435,7 +435,7 @@ let usage () = ML Module\" commands in coq files.\n"; *) (* Does not work anymore: *) (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) - eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; + eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 281644d23e..6e7935d099 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -219,7 +219,6 @@ let register_dir_logpath,find_dir_logpath = let file_name s = function | None -> s - | Some "." -> s | Some d -> d // s let depend_ML str = -- cgit v1.2.3 From 352c23666babc7dd8f0136b02d9ef1893f9bde5c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 Jan 2017 17:32:58 +0100 Subject: test suite for coq_makefile2 --- .gitignore | 3 +- test-suite/Makefile | 2 +- test-suite/coq-makefile/compat-subdirs/_CoqProject | 4 +- test-suite/coq-makefile/compat-subdirs/run.sh | 3 +- .../coq-makefile/compat-subdirs/src/test.ml4 | 13 ----- .../coq-makefile/compat-subdirs/src/test.mli | 0 .../coq-makefile/compat-subdirs/src/test_aux.ml | 1 - .../coq-makefile/compat-subdirs/src/test_aux.mli | 1 - .../compat-subdirs/src/test_plugin.mlpack | 2 - .../coq-makefile/compat-subdirs/theories/test.v | 7 --- test-suite/coq-makefile/coqdoc1/run.sh | 4 +- test-suite/coq-makefile/coqdoc1/src/test.ml4 | 13 ----- test-suite/coq-makefile/coqdoc1/src/test.mli | 0 test-suite/coq-makefile/coqdoc1/src/test_aux.ml | 1 - test-suite/coq-makefile/coqdoc1/src/test_aux.mli | 1 - .../coq-makefile/coqdoc1/src/test_plugin.mlpack | 2 - .../coq-makefile/coqdoc1/theories/sub/testsub.v | 1 - test-suite/coq-makefile/coqdoc1/theories/test.v | 7 --- test-suite/coq-makefile/coqdoc2/_CoqProject | 11 ++++ test-suite/coq-makefile/coqdoc2/run.sh | 53 +++++++++++++++++++ .../coq-makefile/extend-subdirs/Makefile.local | 4 ++ test-suite/coq-makefile/extend-subdirs/_CoqProject | 10 ++++ test-suite/coq-makefile/extend-subdirs/run.sh | 10 ++++ .../coq-makefile/extend-subdirs/subdir/Makefile | 5 ++ test-suite/coq-makefile/latex1/_CoqProject | 11 ++++ test-suite/coq-makefile/latex1/run.sh | 15 ++++++ test-suite/coq-makefile/merlin1/_CoqProject | 4 +- test-suite/coq-makefile/merlin1/run.sh | 10 ++-- test-suite/coq-makefile/merlin1/src/test.ml4 | 13 ----- test-suite/coq-makefile/merlin1/src/test.mli | 0 test-suite/coq-makefile/merlin1/src/test_aux.ml | 1 - test-suite/coq-makefile/merlin1/src/test_aux.mli | 1 - .../coq-makefile/merlin1/src/test_plugin.mlpack | 2 - test-suite/coq-makefile/merlin1/theories/test.v | 7 --- test-suite/coq-makefile/mllib1/_CoqProject | 9 ---- test-suite/coq-makefile/mllib1/run.sh | 30 ----------- test-suite/coq-makefile/mllib1/src/test.ml4 | 13 ----- test-suite/coq-makefile/mllib1/src/test.mli | 0 test-suite/coq-makefile/mllib1/src/test_aux.ml | 1 - test-suite/coq-makefile/mllib1/src/test_aux.mli | 1 - .../coq-makefile/mllib1/src/test_plugin.mllib | 2 - test-suite/coq-makefile/mllib1/theories/test.v | 7 --- test-suite/coq-makefile/mlpack1/_CoqProject | 4 +- test-suite/coq-makefile/mlpack1/run.sh | 4 +- test-suite/coq-makefile/mlpack1/src/test.ml4 | 13 ----- test-suite/coq-makefile/mlpack1/src/test.mli | 0 test-suite/coq-makefile/mlpack1/src/test_aux.ml | 1 - test-suite/coq-makefile/mlpack1/src/test_aux.mli | 1 - .../coq-makefile/mlpack1/src/test_plugin.mlpack | 2 - test-suite/coq-makefile/mlpack1/theories/test.v | 7 --- test-suite/coq-makefile/mlpack2/_CoqProject | 10 ++++ test-suite/coq-makefile/mlpack2/run.sh | 25 +++++++++ test-suite/coq-makefile/multiroot/_CoqProject | 12 +++++ test-suite/coq-makefile/multiroot/run.sh | 61 ++++++++++++++++++++++ test-suite/coq-makefile/native1/_CoqProject | 11 ++++ test-suite/coq-makefile/native1/run.sh | 34 ++++++++++++ test-suite/coq-makefile/plugin1/_CoqProject | 10 ++++ test-suite/coq-makefile/plugin1/run.sh | 31 +++++++++++ test-suite/coq-makefile/plugin2/_CoqProject | 10 ++++ test-suite/coq-makefile/plugin2/run.sh | 31 +++++++++++ test-suite/coq-makefile/plugin3/_CoqProject | 10 ++++ test-suite/coq-makefile/plugin3/run.sh | 31 +++++++++++ test-suite/coq-makefile/template/init.sh | 16 ++++++ test-suite/coq-makefile/template/src/test.ml4 | 14 +++++ test-suite/coq-makefile/template/src/test.mli | 0 test-suite/coq-makefile/template/src/test_aux.ml | 1 + test-suite/coq-makefile/template/src/test_aux.mli | 1 + .../coq-makefile/template/src/test_plugin.mlpack | 2 + .../coq-makefile/template/theories/sub/testsub.v | 1 + test-suite/coq-makefile/template/theories/test.v | 7 +++ test-suite/coq-makefile/uninstall1/_CoqProject | 4 +- test-suite/coq-makefile/uninstall1/run.sh | 4 +- test-suite/coq-makefile/uninstall1/src/test.ml4 | 13 ----- test-suite/coq-makefile/uninstall1/src/test.mli | 0 test-suite/coq-makefile/uninstall1/src/test_aux.ml | 1 - .../coq-makefile/uninstall1/src/test_aux.mli | 1 - .../coq-makefile/uninstall1/src/test_plugin.mlpack | 2 - .../coq-makefile/uninstall1/theories/sub/testsub.v | 1 - test-suite/coq-makefile/uninstall1/theories/test.v | 7 --- test-suite/coq-makefile/uninstall2/_CoqProject | 11 ++++ test-suite/coq-makefile/uninstall2/run.sh | 20 +++++++ test-suite/coq-makefile/validate1/_CoqProject | 10 ++++ test-suite/coq-makefile/validate1/run.sh | 10 ++++ 83 files changed, 512 insertions(+), 207 deletions(-) delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.ml4 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.mli delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack delete mode 100644 test-suite/coq-makefile/compat-subdirs/theories/test.v delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test.ml4 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test.mli delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack delete mode 100644 test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v delete mode 100644 test-suite/coq-makefile/coqdoc1/theories/test.v create mode 100644 test-suite/coq-makefile/coqdoc2/_CoqProject create mode 100755 test-suite/coq-makefile/coqdoc2/run.sh create mode 100644 test-suite/coq-makefile/extend-subdirs/Makefile.local create mode 100644 test-suite/coq-makefile/extend-subdirs/_CoqProject create mode 100755 test-suite/coq-makefile/extend-subdirs/run.sh create mode 100644 test-suite/coq-makefile/extend-subdirs/subdir/Makefile create mode 100644 test-suite/coq-makefile/latex1/_CoqProject create mode 100755 test-suite/coq-makefile/latex1/run.sh delete mode 100644 test-suite/coq-makefile/merlin1/src/test.ml4 delete mode 100644 test-suite/coq-makefile/merlin1/src/test.mli delete mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/merlin1/src/test_plugin.mlpack delete mode 100644 test-suite/coq-makefile/merlin1/theories/test.v delete mode 100644 test-suite/coq-makefile/mllib1/_CoqProject delete mode 100755 test-suite/coq-makefile/mllib1/run.sh delete mode 100644 test-suite/coq-makefile/mllib1/src/test.ml4 delete mode 100644 test-suite/coq-makefile/mllib1/src/test.mli delete mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/mllib1/src/test_plugin.mllib delete mode 100644 test-suite/coq-makefile/mllib1/theories/test.v delete mode 100644 test-suite/coq-makefile/mlpack1/src/test.ml4 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test.mli delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack delete mode 100644 test-suite/coq-makefile/mlpack1/theories/test.v create mode 100644 test-suite/coq-makefile/mlpack2/_CoqProject create mode 100755 test-suite/coq-makefile/mlpack2/run.sh create mode 100644 test-suite/coq-makefile/multiroot/_CoqProject create mode 100755 test-suite/coq-makefile/multiroot/run.sh create mode 100644 test-suite/coq-makefile/native1/_CoqProject create mode 100755 test-suite/coq-makefile/native1/run.sh create mode 100644 test-suite/coq-makefile/plugin1/_CoqProject create mode 100755 test-suite/coq-makefile/plugin1/run.sh create mode 100644 test-suite/coq-makefile/plugin2/_CoqProject create mode 100755 test-suite/coq-makefile/plugin2/run.sh create mode 100644 test-suite/coq-makefile/plugin3/_CoqProject create mode 100755 test-suite/coq-makefile/plugin3/run.sh create mode 100644 test-suite/coq-makefile/template/init.sh create mode 100644 test-suite/coq-makefile/template/src/test.ml4 create mode 100644 test-suite/coq-makefile/template/src/test.mli create mode 100644 test-suite/coq-makefile/template/src/test_aux.ml create mode 100644 test-suite/coq-makefile/template/src/test_aux.mli create mode 100644 test-suite/coq-makefile/template/src/test_plugin.mlpack create mode 100644 test-suite/coq-makefile/template/theories/sub/testsub.v create mode 100644 test-suite/coq-makefile/template/theories/test.v delete mode 100644 test-suite/coq-makefile/uninstall1/src/test.ml4 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test.mli delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.ml delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.mli delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack delete mode 100644 test-suite/coq-makefile/uninstall1/theories/sub/testsub.v delete mode 100644 test-suite/coq-makefile/uninstall1/theories/test.v create mode 100644 test-suite/coq-makefile/uninstall2/_CoqProject create mode 100755 test-suite/coq-makefile/uninstall2/run.sh create mode 100644 test-suite/coq-makefile/validate1/_CoqProject create mode 100755 test-suite/coq-makefile/validate1/run.sh diff --git a/.gitignore b/.gitignore index 6e6f01a434..c55ad24f84 100644 --- a/.gitignore +++ b/.gitignore @@ -64,7 +64,8 @@ test-suite/coq-makefile/*/actual test-suite/coq-makefile/*/desired test-suite/coq-makefile/*/Makefile test-suite/coq-makefile/*/Makefile.conf -test-suite/coq-makefile/*/src/test.ml +test-suite/coq-makefile/*/src +test-suite/coq-makefile/*/theories test-suite/coq-makefile/*/html test-suite/coq-makefile/*/mlihtml test-suite/coq-makefile/*/subdir/done diff --git a/test-suite/Makefile b/test-suite/Makefile index 8a3d383cb4..c2d6e540c6 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -486,7 +486,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh)) coq-makefile/%.log : coq-makefile/%/run.sh - @echo "TEST $*" + @echo "TEST coq-makefile/$*" $(HIDE)(\ cd coq-makefile/$* && \ ./run.sh 2>&1; \ diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 700d59d642..4f44bde22a 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 38e54d03eb..ccb348c6fa 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -3,8 +3,7 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh 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 deleted file mode 100644 index 8ddc9b0956..0000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/compat-subdirs/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index bbe9717ab9..e071f1db7a 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/coqdoc1/src/test.ml4 b/test-suite/coq-makefile/coqdoc1/src/test.ml4 deleted file mode 100644 index 8ddc9b0956..0000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index 755fc343f2..0000000000 --- a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v +++ /dev/null @@ -1 +0,0 @@ -Require Import test. diff --git a/test-suite/coq-makefile/coqdoc1/theories/test.v b/test-suite/coq-makefile/coqdoc1/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/coqdoc1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject new file mode 100644 index 0000000000..d2a547d47b --- /dev/null +++ b/test-suite/coq-makefile/coqdoc2/_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/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh new file mode 100755 index 0000000000..e071f1db7a --- /dev/null +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -0,0 +1,53 @@ +#!/bin/bash + +#set -x +set -e + +. ../template/init.sh + +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 < desired -echo S $PWD/src >> desired +cat > desired < 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 deleted file mode 100644 index 8ddc9b0956..0000000000 --- a/test-suite/coq-makefile/merlin1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.ml b/test-suite/coq-makefile/merlin1/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/merlin1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/merlin1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/merlin1/theories/test.v b/test-suite/coq-makefile/merlin1/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/merlin1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -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 deleted file mode 100644 index 6b2046d686..0000000000 --- a/test-suite/coq-makefile/mllib1/_CoqProject +++ /dev/null @@ -1,9 +0,0 @@ --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 deleted file mode 100755 index 8f6b8e7ea5..0000000000 --- a/test-suite/coq-makefile/mllib1/run.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/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 < ()) "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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.ml b/test-suite/coq-makefile/mllib1/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/mllib1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/mllib1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/mllib1/theories/test.v b/test-suite/coq-makefile/mllib1/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/mllib1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -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 index cb1ad4a4ba..69f47302e1 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 43d03be4a4..418a2fb775 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/mlpack1/src/test.ml4 b/test-suite/coq-makefile/mlpack1/src/test.ml4 deleted file mode 100644 index 8ddc9b0956..0000000000 --- a/test-suite/coq-makefile/mlpack1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.ml b/test-suite/coq-makefile/mlpack1/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Test_aux -Test diff --git a/test-suite/coq-makefile/mlpack1/theories/test.v b/test-suite/coq-makefile/mlpack1/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/mlpack1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject new file mode 100644 index 0000000000..51864a87ae --- /dev/null +++ b/test-suite/coq-makefile/mlpack2/_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/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh new file mode 100755 index 0000000000..418a2fb775 --- /dev/null +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -0,0 +1,25 @@ +#!/bin/sh + +#set -x +set -e + +. ../template/init.sh + +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 </dev/null; find; popd >/dev/null; done) | sort -u > actual +sort > desired < actual +sort > desired < actual +sort > desired < actual +sort > desired < actual +sort > desired < ()) "test_plugin";; + +VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF + | [ "TestCommand" ] -> [ () ] +END + +TACTIC EXTEND test +| [ "test_tactic" ] -> [ Test_aux.tac ] +END + + + diff --git a/test-suite/coq-makefile/template/src/test.mli b/test-suite/coq-makefile/template/src/test.mli new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml new file mode 100644 index 0000000000..a01d0865a8 --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -0,0 +1 @@ +let tac = Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli new file mode 100644 index 0000000000..10020f27de --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -0,0 +1 @@ +val tac : unit Proofview.tactic diff --git a/test-suite/coq-makefile/template/src/test_plugin.mlpack b/test-suite/coq-makefile/template/src/test_plugin.mlpack new file mode 100644 index 0000000000..cf94d851bb --- /dev/null +++ b/test-suite/coq-makefile/template/src/test_plugin.mlpack @@ -0,0 +1,2 @@ +Test_aux +Test diff --git a/test-suite/coq-makefile/template/theories/sub/testsub.v b/test-suite/coq-makefile/template/theories/sub/testsub.v new file mode 100644 index 0000000000..755fc343f2 --- /dev/null +++ b/test-suite/coq-makefile/template/theories/sub/testsub.v @@ -0,0 +1 @@ +Require Import test. diff --git a/test-suite/coq-makefile/template/theories/test.v b/test-suite/coq-makefile/template/theories/test.v new file mode 100644 index 0000000000..744b5aad78 --- /dev/null +++ b/test-suite/coq-makefile/template/theories/test.v @@ -0,0 +1,7 @@ +Declare ML Module "test_plugin". +TestCommand. +Goal True. +Proof. +test_tactic. +exact I. +Qed. diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 706cf75cc7..35792066bb 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -1,5 +1,5 @@ --R src/ test --R theories/ test +-R src test +-R theories test -I src src/test_plugin.mlpack diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index a3bfe182b2..d241762791 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -3,8 +3,8 @@ #set -x set -e -export PATH=../../../bin/:$PATH -git clean -dfx . +. ../template/init.sh + coq_makefile -f _CoqProject -o Makefile make make html mlihtml diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4 deleted file mode 100644 index 8ddc9b0956..0000000000 --- a/test-suite/coq-makefile/uninstall1/src/test.ml4 +++ /dev/null @@ -1,13 +0,0 @@ -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 deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml deleted file mode 100644 index a01d0865a8..0000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.ml +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index 10020f27de..0000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_aux.mli +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index cf94d851bb..0000000000 --- a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index 755fc343f2..0000000000 --- a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v +++ /dev/null @@ -1 +0,0 @@ -Require Import test. diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v deleted file mode 100644 index 7753b56aae..0000000000 --- a/test-suite/coq-makefile/uninstall1/theories/test.v +++ /dev/null @@ -1,7 +0,0 @@ -Declare ML Module "test_plugin". -Test. -Goal True. -Proof. -test. -exact I. -Qed. diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject new file mode 100644 index 0000000000..d2a547d47b --- /dev/null +++ b/test-suite/coq-makefile/uninstall2/_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/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh new file mode 100755 index 0000000000..d241762791 --- /dev/null +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -0,0 +1,20 @@ +#!/bin/bash + +#set -x +set -e + +. ../template/init.sh + +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 <