mise en place des outils

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@236 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 66 insertions, 11 deletions

diff --git a/.cvsignore b/.cvsignore
index 205dc23a3..5702fe96e 100644
--- a/.cvsignore
+++ b/.cvsignore
@@ -1,3 +1,4 @@
 coqtop.byte
 coqtop
 minicoq
+coqtop.opt
diff --git a/.depend b/.depend
index f61bf0e18..243a6a4b1 100644
--- a/.depend
+++ b/.depend
@@ -493,18 +493,18 @@ parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/impargs.cmx kernel/inductive.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx parsing/termast.cmi 
-pretyping/cases.cmo: parsing/ast.cmi kernel/environ.cmi \
-    pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \
-    kernel/generic.cmi library/global.cmi library/indrec.cmi \
-    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+pretyping/cases.cmo: kernel/environ.cmi pretyping/evarconv.cmi \
+    pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi library/indrec.cmi kernel/inductive.cmi \
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
     pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/cases.cmi 
-pretyping/cases.cmx: parsing/ast.cmx kernel/environ.cmx \
-    pretyping/evarconv.cmx pretyping/evarutil.cmx kernel/evd.cmx \
-    kernel/generic.cmx library/global.cmx library/indrec.cmx \
-    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+pretyping/cases.cmx: kernel/environ.cmx pretyping/evarconv.cmx \
+    pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx library/indrec.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
@@ -817,6 +817,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/generic.cmx library/global.cmx proofs/logic.cmx kernel/names.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
diff --git a/Makefile b/Makefile
index 906c2a648..36d3fea4b 100644
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,7 @@ noargument:
 # Compilation options
 ###########################################################################
 
-LOCALINCLUDES=-I config -I scripts -I lib -I kernel -I library \
+LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping -I parsing -I toplevel
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
@@ -170,7 +170,26 @@ states/barestate.coq: $(SYNTAXPP) coqtop.byte
 # tools
 ###########################################################################
 
-tools: dev/db_printers.cmo
+tools: tools/coqdep tools/coq_makefile tools/gallina tools/coq-tex \
+       tools/coq.elc dev/db_printers.cmo
+
+COQDEPCMX= config/coq_config.cmx tools/coqdep_lexer.cmx tools/coqdep.cmx
+
+tools/coqdep: $(COQDEPCMX)
+	$(OCAMLOPT) $(OPTFLAGS) -o tools/coqdep unix.cmxa $(COQDEPCMX) \
+          $(OSDEPLIBS)
+
+GALLINACMX=tools/gallina_lexer.cmx tools/gallina.cmx
+
+tools/gallina: $(GALLINACMX)
+	$(OCAMLOPT) $(OPTFLAGS) -o tools/gallina $(GALLINACMX)
+
+tools/coq_makefile: tools/coq_makefile.ml
+	$(OCAMLOPT) $(OPTFLAGS) -o tools/coq_makefile tools/coq_makefile.ml
+
+tools/coq-tex: tools/coq-tex.ml
+	$(OCAMLOPT) $(OPTFLAGS) -o tools/coq-tex str.cmxa tools/coq-tex.ml \
+          $(STRLIB)
 
 ###########################################################################
 # minicoq
@@ -185,6 +204,24 @@ minicoq: $(MINICOQCMO)
 	  $(OSDEPLIBS)
 
 ###########################################################################
+# Installation
+###########################################################################
+
+install: install-binaries install-library install-manpages
+
+install-binaries:
+	cp tools/coqdep tools/gallina tools/coq_makefile tools/coq-tex \
+	  $(BINDIR)
+
+install-library:
+	cp tools/coq.el tools/coq.elc $(EMACSLIB)
+
+MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1
+
+install-manpages:
+	cp $(MANPAGES) $(MANDIR)/man1
+
+###########################################################################
 # Documentation
 # Literate programming (with ocamlweb)
 ###########################################################################
@@ -295,7 +332,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
 # Default rules
 ###########################################################################
 
-.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4 .el .elc
 
 .ml.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -315,6 +352,12 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
 .ml4.cmx:
 	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
 
+.el.elc:
+	echo "(setq load-path (cons \".\" load-path))" > $*.compile
+	echo "(byte-compile-file \"$<\")" >> $*.compile
+	$(EMACS) -batch -l $*.compile
+	rm -f $*.compile        
+
 ###########################################################################
 # Cleaning
 ###########################################################################
@@ -329,7 +372,9 @@ archclean::
 	rm -f parsing/*.cmx parsing/*.[so]
 	rm -f pretyping/*.cmx pretyping/*.[so]
 	rm -f toplevel/*.cmx toplevel/*.[so]
+	rm -f tools/*.cmx tools/*.[so]
 	rm -f coqtop.opt coqtop.byte minicoq
+	rm -f tools/coqdep tools/gallina tools/coq-tex tools/coq_makefile
 
 cleanall:: archclean
 	rm -f *~
@@ -343,6 +388,7 @@ cleanall:: archclean
 	rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~
 	rm -f pretyping/*.cm[io] pretyping/*~
 	rm -f toplevel/*.cm[io] toplevel/*~
+	rm -f tools/*.cm[io] tools/*~
 
 cleanconfig::
 	rm -f config/Makefile config/coq_config.ml
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 4d3258e6a..be3fd4cbc 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -23,4 +23,5 @@ val date : string       (* release date *)
 val compile_date : string (* compile date *)
 
 val theories_dirs : string list
+val tactics_dirs : string list
 
diff --git a/configure b/configure
index 0ca4c98ba..c0e81c8ee 100755
--- a/configure
+++ b/configure
@@ -461,6 +461,9 @@ echo_e "\nlet theories_dirs = [" >> $mlconfig_file
 subdirs theories
 echo_e "]\n" >> $mlconfig_file
 
+echo_e "\nlet tactics_dirs = [" >> $mlconfig_file
+subdirs contrib
+echo_e "]\n" >> $mlconfig_file
 
 if test $ARCH = "win32" ; then
 # We change: / -> \\ and \ -> \\ (dos paths)