From 14be4137a9cb423bc65d1547d153bba19d419861 Mon Sep 17 00:00:00 2001 From: filliatr Date: Sat, 11 Dec 1999 18:43:48 +0000 Subject: mise en place des outils git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@236 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .cvsignore | 1 + .depend | 20 ++++++++++++-------- Makefile | 52 ++++++++++++++++++++++++++++++++++++++++++++++++--- config/coq_config.mli | 1 + configure | 3 +++ 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 @@ -184,6 +203,24 @@ minicoq: $(MINICOQCMO) $(OCAMLC) $(INCLUDES) -o minicoq -custom $(CMA) $(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) -- cgit v1.2.3