diff options
| -rw-r--r-- | .depend | 19 | ||||
| -rw-r--r-- | Makefile | 31 | ||||
| -rw-r--r-- | bin/.cvsignore | 1 | ||||
| -rw-r--r-- | config/Makefile.template | 6 | ||||
| -rwxr-xr-x | configure | 30 |
5 files changed, 83 insertions, 4 deletions
@@ -1,3 +1,4 @@ +doc/syntax.cmi: parsing/ast.cmi ide/config_parser.cmi: lib/util.cmi ide/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo @@ -435,6 +436,8 @@ contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \ pretyping/evd.cmi kernel/term.cmi contrib/xml/xmlcommand.cmi: library/libnames.cmi ide/utils/configwin.cmi: ide/utils/uoptions.cmi +tools/coqdoc/output.cmi: tools/coqdoc/index.cmi +tools/coqdoc/pretty.cmi: tools/coqdoc/index.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi @@ -455,6 +458,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \ kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx +doc/syntax.cmo: parsing/ast.cmi contrib/interface/parse.cmo doc/syntax.cmi +doc/syntax.cmx: parsing/ast.cmx contrib/interface/parse.cmx doc/syntax.cmi ide/blaster_window.cmo: ide/coq.cmi ide/ideutils.cmi ide/blaster_window.cmx: ide/coq.cmx ide/ideutils.cmx ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmi \ @@ -3239,6 +3244,20 @@ ide/utils/okey.cmo: ide/utils/okey.cmi ide/utils/okey.cmx: ide/utils/okey.cmi ide/utils/uoptions.cmo: ide/utils/uoptions.cmi ide/utils/uoptions.cmx: ide/utils/uoptions.cmi +tools/coqdoc/alpha.cmo: tools/coqdoc/alpha.cmi +tools/coqdoc/alpha.cmx: tools/coqdoc/alpha.cmi +tools/coqdoc/index.cmo: tools/coqdoc/alpha.cmi tools/coqdoc/index.cmi +tools/coqdoc/index.cmx: tools/coqdoc/alpha.cmx tools/coqdoc/index.cmi +tools/coqdoc/main.cmo: config/coq_config.cmi tools/coqdoc/index.cmi \ + tools/coqdoc/output.cmi tools/coqdoc/pretty.cmi +tools/coqdoc/main.cmx: config/coq_config.cmx tools/coqdoc/index.cmx \ + tools/coqdoc/output.cmx tools/coqdoc/pretty.cmx +tools/coqdoc/output.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi +tools/coqdoc/output.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmi +tools/coqdoc/pretty.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi \ + tools/coqdoc/pretty.cmi +tools/coqdoc/pretty.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmx \ + tools/coqdoc/pretty.cmi tactics/tauto.cmo: parsing/grammar.cma tactics/tauto.cmx: parsing/grammar.cma tactics/eqdecide.cmo: parsing/grammar.cma @@ -62,7 +62,8 @@ else HIDE = @ endif -LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ +LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ + -I scripts -I lib -I kernel -I library \ -I proofs -I tactics -I pretyping \ -I interp -I toplevel -I parsing -I ide/utils \ -I ide -I translate \ @@ -1045,10 +1046,12 @@ COQMAKEFILE=bin/coq_makefile$(EXE) GALLINA=bin/gallina$(EXE) COQTEX=bin/coq-tex$(EXE) COQWC=bin/coqwc$(EXE) +COQDOC=bin/coqdoc$(EXE) COQVO2XML=bin/coq_vo2xml$(EXE) RUNCOQVO2XML=coq_vo2xml$(EXE) # Uses the one in PATH and not the one in bin -TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) $(COQWC) +TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) \ + $(COQWC) $(COQDOC) tools:: $(TOOLS) dev/top_printers.cmo @@ -1082,6 +1085,16 @@ $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo +beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml + +COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \ + tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \ + tools/coqdoc/main.cmo + +$(COQDOC): $(COQDOCCMO) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO) + COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo $(COQVO2XML): $(COQVO2XMLCMO) @@ -1091,6 +1104,7 @@ $(COQVO2XML): $(COQVO2XMLCMO) clean:: rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml rm -f tools/coqwc.ml + rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml archclean:: rm -f $(TOOLS) @@ -1201,7 +1215,7 @@ install-allreals:: cp $$f $(FULLCOQLIB)/`dirname $$f`; \ done -install-coq-info: install-coq-manpages install-emacs +install-coq-info: install-coq-manpages install-emacs install-latex MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ @@ -1215,6 +1229,17 @@ install-emacs: $(MKDIR) $(FULLEMACSLIB) cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB) +# where to put the coqdoc style file +TEXDIR = $(BASETEXDIR)/tex/latex/misc + +# command to update TeX' kpathsea database +UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null + +install-latex: + $(MKDIR) $(TEXDIR) + cp tools/coqdoc/coqdoc.sty $(TEXDIR) + -$(UPDATETEX) + ########################################################################### # Documentation # Literate programming (with ocamlweb) diff --git a/bin/.cvsignore b/bin/.cvsignore index 32c168302..e5e3c2104 100644 --- a/bin/.cvsignore +++ b/bin/.cvsignore @@ -17,3 +17,4 @@ coqide.opt coqtopnew.opt coqtopnew.byte coqwc +coqdoc diff --git a/config/Makefile.template b/config/Makefile.template index 0749c3540..d3f853f17 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -85,6 +85,12 @@ INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION # the command MKDIR (try to replace it with mkdirhier if you have problems) MKDIR=mkdir -p +# where to put the coqdoc.sty style file +BASETEXDIR=TEXDIRECTORY + +# command to update TeX' kpathsea database +MKTEXLSR=MKTEXLSRCOMMAND + #the command STRIP # Unix systems and profiling: true # Unix systems and no profiling: strip @@ -36,6 +36,7 @@ libdir_spec=no mandir_spec=no emacslib_spec=no emacs_spec=no +texdir_spec=no reals_opt=no reals=all arch_spec=no @@ -55,6 +56,8 @@ while : ; do libdir=$2/lib/coq mandir_spec=yes mandir=$2/man + texdir_spec=yes + texdir=$2/share/texmf shift;; -local|--local) local=true bindir_spec=yes @@ -65,6 +68,8 @@ while : ; do mandir=$COQTOP/man emacslib_spec=yes emacslib=$COQTOP/tools/emacs + texdir_spec=yes + texdir=$COQTOP/share/texmf reals_opt=yes reals=all;; -src|--src) COQTOP=$2 @@ -84,6 +89,9 @@ while : ; do -emacs |--emacs) emacs_spec=yes emacs=$2 shift;; + -texdir|--texdir) texdir_spec=yes + texdir=$2 + shift;; -arch|--arch) arch_spec=yes arch=$2 shift;; @@ -151,7 +159,8 @@ case $ARCH in bindir_def=/usr/local/bin libdir_def=/usr/local/lib/coq mandir_def=/usr/local/man - emacslib_def=/usr/share/emacs/site-lisp;; + emacslib_def=/usr/share/emacs/site-lisp + texdir_def=/usr/share/texmf;; esac emacs_def=emacs @@ -200,6 +209,17 @@ case $emacslib_spec in yes) EMACSLIB=$emacslib;; esac +case $texdir_spec in + no) echo "Where should I install TeX/LaTeX files [$texdir_def] ?" + read TEXDIR + + case $TEXDIR in + "") TEXDIR=$texdir_def;; + *) true;; + esac;; + yes) TEXDIR=$texdir;; +esac + case $reals_opt in no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?" read reals_ans @@ -357,6 +377,12 @@ case $ARCH in fi esac +# mktexlsr +MKTEXLSR=`which mktexlsr` +case $MKTEXLSR in + "") MKTEXLSR=true;; +esac + # Summary of the configuration echo "" @@ -465,6 +491,8 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|MANDIRDIRECTORY|$MANDIR|" \ -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ -e "s|EMACSCOMMAND|$EMACS|" \ + -e "s|TEXDIRECTORY|$TEXDIR|" \ + -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \ -e "s|ARCHITECTURE|$ARCH|" \ -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \ -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ |