From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- tools/beautify-archive | 0 tools/compat5.ml | 13 + tools/compat5.mlp | 23 ++ tools/compat5b.ml | 13 + tools/compat5b.mlp | 23 ++ tools/coq-syntax.el | 3 + tools/coq_makefile.ml | 714 ++++++++++++++++++++++++++++++++++++++++++++++ tools/coq_makefile.ml4 | 614 --------------------------------------- tools/coq_tex.ml4 | 4 +- tools/coqdep.ml | 11 +- tools/coqdep_boot.ml | 6 +- tools/coqdep_common.ml | 110 +++++-- tools/coqdep_common.mli | 49 ++++ tools/coqdep_lexer.mli | 27 ++ tools/coqdep_lexer.mll | 228 ++++++++++----- tools/coqdoc/alpha.ml | 4 +- tools/coqdoc/alpha.mli | 4 +- tools/coqdoc/cdglobals.ml | 46 ++- tools/coqdoc/coqdoc.css | 46 ++- tools/coqdoc/cpretty.mli | 4 +- tools/coqdoc/cpretty.mll | 156 +++++++--- tools/coqdoc/index.ml | 56 ++-- tools/coqdoc/index.mli | 6 +- tools/coqdoc/main.ml | 49 ++-- tools/coqdoc/output.ml | 100 ++++++- tools/coqdoc/output.mli | 21 +- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqwc.mll | 4 +- tools/fake_ide.ml | 84 ++++++ tools/gallina.ml | 4 +- tools/gallina_lexer.mll | 4 +- 32 files changed, 1567 insertions(+), 863 deletions(-) mode change 100644 => 100755 tools/beautify-archive create mode 100644 tools/compat5.ml create mode 100644 tools/compat5.mlp create mode 100644 tools/compat5b.ml create mode 100644 tools/compat5b.mlp create mode 100644 tools/coq_makefile.ml delete mode 100644 tools/coq_makefile.ml4 create mode 100644 tools/coqdep_common.mli create mode 100644 tools/coqdep_lexer.mli create mode 100644 tools/fake_ide.ml (limited to 'tools') diff --git a/tools/beautify-archive b/tools/beautify-archive old mode 100644 new mode 100755 diff --git a/tools/compat5.ml b/tools/compat5.ml new file mode 100644 index 00000000..641d80d8 --- /dev/null +++ b/tools/compat5.ml @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< '(KEYWORD "EXTEND", loc); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) diff --git a/tools/compat5b.ml b/tools/compat5b.ml new file mode 100644 index 00000000..f757a065 --- /dev/null +++ b/tools/compat5b.ml @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el index 5b88f6a5..8630fb3a 100644 --- a/tools/coq-syntax.el +++ b/tools/coq-syntax.el @@ -417,8 +417,10 @@ ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") + ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") + ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") @@ -497,6 +499,7 @@ ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") + ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml new file mode 100644 index 00000000..a685d6ea --- /dev/null +++ b/tools/coq_makefile.ml @@ -0,0 +1,714 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* print x + | x :: l -> print x; print sep; print_list sep l + | [] -> () + +let list_iter_i f = + let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 + +let section s = + let l = String.length s in + let sep = String.make (l+5) '#' + and sep2 = String.make (l+5) ' ' in + String.set sep (l+4) '\n'; + String.set sep2 0 '#'; + String.set sep2 (l+3) '#'; + String.set sep2 (l+4) '\n'; + print sep; + print sep2; + print "# "; print s; print " #\n"; + print sep2; + print sep; + print "\n" + +let usage () = + output_string stderr "Usage summary: + +coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ... [file.mllib] + ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath + logicalpath] ... [VARIABLE = value] ... [-arg opt] ... [-opt|-byte] + [-no-install] [-f file] [-o file] [-h] [--help] + +[file.v]: Coq file to be compiled +[file.ml[i4]?]: Objective Caml file to be compiled +[file.mllib]: ocamlbuild file that describes a Objective Caml library +[subdirectory] : subdirectory that should be \"made\" and has a + Makefile itself to do so. +[-custom command dependencies file]: add target \"file\" with command + \"command\" and dependencies \"dependencies\" +[-I dir]: look for Objective Caml dependencies in \"dir\" +[-R physicalpath logicalpath]: look for Coq dependencies resursively + starting from \"physicalpath\". The logical path associated to the + physical path is \"logicalpath\". +[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" +[-byte]: compile with byte-code version of coq +[-opt]: compile with native-code version of coq +[-arg opt]: send option \"opt\" to coqc +[-install opt]: where opt is \"user\" to force install into user directory, + \"none\" to build a makefile with no install target or + \"global\" to force install in $COQLIB directory +[-f file]: take the contents of file as arguments +[-o file]: output should go in file file + Output file outside the current directory is forbidden. +[-h]: print this usage summary +[--help]: equivalent to [-h]\n"; + exit 1 + +let is_genrule r = + let genrule = Str.regexp("%") in + Str.string_match genrule r 0 + +let string_prefix a b = + let rec aux i = try if a.[i] = b.[i] then aux (i+1) else i with |Invalid_argument _ -> i in + String.sub a 0 (aux 0) + +let is_prefix dir1 dir2 = + let l1 = String.length dir1 in + let l2 = String.length dir2 in + dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') + +let physical_dir_of_logical_dir ldir = + let le = String.length ldir - 1 in + let pdir = if ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in + for i = 0 to le - 1 do + if pdir.[i] = '.' then pdir.[i] <- '/'; + done; + pdir + +let standard opt = + print "byte:\n"; + print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; + print "opt:\n"; + if not opt then print "\t@echo \"WARNING: opt is disabled\"\n"; + print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte"); + print "\"\n\n" + +let classify_files_by_root var files (inc_i,inc_r) = + if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then + begin + let absdir_of_files = List.rev_map + (fun x -> Minilib.canonical_path_name (Filename.dirname x)) + files in + (* files in scope of a -I option (assuming they are no overlapping) *) + let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in + if has_inc_i then + begin + printf "%sINC=" var; + List.iter (fun (pdir,absdir) -> + if List.mem absdir absdir_of_files + then printf + "$(filter $(wildcard %s/*),$(%s)) " + pdir var + ) inc_i; + printf "\n"; + end; + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix abspdir) absdir_of_files then + printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" + var i pdir pdir var) + inc_r; + end + +let install_include_by_root files_var files (inc_i,inc_r) = + try + (* All files caught by a -R . option (assuming it is the only one) *) + let ldir = match inc_r with + |[(".",t,_)] -> t + |l -> let out = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in + let () = prerr_string "Warning: install rule assumes that -R . _ is the only -R option" in + out in + let pdir = physical_dir_of_logical_dir ldir in + printf "\tfor i in $(%s); do \\\n" files_var; + printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir; + printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir; + printf "\tdone\n" + with Not_found -> + let absdir_of_files = List.rev_map + (fun x -> Minilib.canonical_path_name (Filename.dirname x)) + files in + let has_inc_i_files = + List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_i in + let install_inc_i d = + printf "\tinstall -d $(DSTROOT)$(COQLIBINSTALL)/%s; \\\n" d; + printf "\tfor i in $(%sINC); do \\\n" files_var; + printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" d; + printf "\tdone\n" + in + if inc_r = [] then + if has_inc_i_files then + begin + (* Files in the scope of a -I option *) + install_inc_i "$(INSTALLDEFAULTROOT)"; + end else () + else + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + let has_inc_r_files = List.exists (is_prefix abspdir) absdir_of_files in + let pdir' = physical_dir_of_logical_dir ldir in + if has_inc_r_files then + begin + printf "\tcd %s; for i in $(%s%d); do \\\n" pdir files_var i; + printf "\t install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/%s/$$i`; \\\n" pdir'; + printf "\t install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/%s/$$i; \\\n" pdir'; + printf "\tdone\n"; + end; + if has_inc_i_files then install_inc_i pdir' + ) inc_r + +let install_doc some_vfiles some_mlifiles (_,inc_r) = + let install_one_kind kind dir = + printf "\tinstall -d $(DSTROOT)$(COQDOCINSTALL)/%s/%s\n" dir kind; + printf "\tfor i in %s/*; do \\\n" kind; + printf "\t install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/%s/$$i;\\\n" dir; + print "\tdone\n" in + print "install-doc:\n"; + let () = match inc_r with + |[] -> + if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; + if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; + |(_,lp,_)::q -> + let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in + if (pr <> "") && + ((List.exists (fun(_,b,_) -> b = pr) inc_r) || pr.[String.length pr - 1] = '.') + then begin + let rt = physical_dir_of_logical_dir pr in + if some_vfiles then install_one_kind "html" rt; + if some_mlifiles then install_one_kind "mlihtml" rt; + end else begin + prerr_string "Warning: -R options don't have a correct common prefix, + install-doc will put anything in $INSTALLDEFAULTROOT"; + if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)"; + if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)"; + end in + print "\n" + +let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function + |Project_file.NoInstall -> () + |is_install -> + let () = if is_install = Project_file.UnspecInstall then + print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in + let not_empty = function |[] -> false |_::_ -> true in + let cmofiles = mlpackfiles@mlfiles@ml4files in + let cmifiles = mlifiles@cmofiles in + let cmxsfiles = cmofiles@mllibfiles in + if (not_empty cmxsfiles) then begin + print "install-natdynlink:\n"; + install_include_by_root "CMXSFILES" cmxsfiles inc; + print "\n"; + end; + print "install:"; + if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; + print "\n"; + if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; + if (not_empty cmofiles) then + install_include_by_root "CMOFILES" cmofiles inc; + if (not_empty cmifiles) then + install_include_by_root "CMIFILES" cmifiles inc; + if (not_empty mllibfiles) then + install_include_by_root "CMAFILES" mllibfiles inc; + List.iter + (fun x -> + printf "\t(cd %s; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) + sds; + print "\n"; + install_doc (not_empty vfiles) (not_empty mlifiles) inc + +let make_makefile sds = + if !make_name <> "" then begin + printf "%s: %s\n" !makefile_name !make_name; + print "\tmv -f $@ $@.bak\n"; + print "\t$(COQBIN)coq_makefile -f $< -o $@\n\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") + sds; + print "\n"; + end + +let clean sds sps = + print "clean:\n"; + if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin + print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; + print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; + print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; + end; + if !some_vfile then + print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"; + print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; + print "\t- rm -rf html mlihtml\n"; + List.iter + (fun (file,_,_) -> + if not (is_genrule file) then + (print "\t- rm -rf "; print file; print "\n")) + sps; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") + sds; + print "\n"; + print "archclean:\n"; + print "\trm -f *.cmx *.o\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") + sds; + print "\n"; + print "printenv:\n\t@$(COQBIN)coqtop -config\n"; + print "\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n\t@echo PP =\t$(PP)\n\t@echo COQFLAGS =\t$(COQFLAGS)\n"; + print "\t@echo COQLIBINSTALL =\t$(COQLIBINSTALL)\n\t@echo COQDOCINSTALL =\t$(COQDOCINSTALL)\n\n" + +let header_includes () = () + +let implicit () = + section "Implicit rules."; + let mli_rules () = + print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "%.mli.d: %.mli\n"; + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let ml4_rules () = + print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "%.ml4.d: %.ml4\n"; + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let ml_rules () = + print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "%.ml.d: %.ml\n"; + print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let cmxs_rules () = + print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in + let mllib_rules () = + print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; + print "%.mllib.d: %.mllib\n"; + print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + let mlpack_rules () = + print "%.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "%.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "%.mlpack.d: %.mlpack\n"; + print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; +in + let v_rules () = + print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "%.g: %.v\n\t$(GALLINA) $<\n\n"; + print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; + print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; + print "%.v.d: %.v\n"; + print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + in + if !some_mlifile then mli_rules (); + if !some_ml4file then ml4_rules (); + if !some_mlfile then ml_rules (); + if !some_mlfile || !some_ml4file then cmxs_rules (); + if !some_mllibfile then mllib_rules (); + if !some_mlpackfile then mlpack_rules (); + if !some_vfile then v_rules () + +let variables is_install opt (args,defs) = + let var_aux (v,def) = print v; print "="; print def; print "\n" in + section "Variables definitions."; + List.iter var_aux defs; + print "\n"; + if not opt then + print "override OPT:=-byte\n" + else + print "OPT?=\n"; + begin + match args with + |[] -> () + |h::t -> print "OTHERFLAGS="; + print h; + List.iter (fun s -> print " ";print s) t; + print "\n"; + end; + (* Coq executables and relative variables *) + if !some_vfile then begin + print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "COQCHKFLAGS?=-silent -o\n"; + print "COQC?=$(COQBIN)coqc\n"; + print "COQDEP?=$(COQBIN)coqdep -c\n"; + print "GALLINA?=$(COQBIN)gallina\n"; + print "COQDOC?=$(COQBIN)coqdoc\n"; + print "COQCHK?=$(COQBIN)coqchk\n\n"; + end; + (* Caml executables and relative variables *) + if !some_ml4file || !some_mlfile || !some_mlifile then begin + print "COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \\ + -I $(COQLIB)library -I $(COQLIB)parsing \\ + -I $(COQLIB)pretyping -I $(COQLIB)interp \\ + -I $(COQLIB)proofs -I $(COQLIB)tactics \\ + -I $(COQLIB)toplevel"; + List.iter (fun c -> print " \\ + -I $(COQLIB)plugins/"; print c) Coq_config.plugins_dirs; print "\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; + print "CAMLC?=$(OCAMLC) -c -rectypes\n"; + print "CAMLOPTC?=$(OCAMLOPT) -c -rectypes\n"; + print "CAMLLINK?=$(OCAMLC) -rectypes\n"; + print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; + print "GRAMMARS?=grammar.cma\n"; + print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; + print "CAMLP4OPTIONS?=\n"; + print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n"; + end; + match is_install with + | Project_file.NoInstall -> () + | Project_file.UnspecInstall -> + section "Install Paths."; + print "ifdef USERINSTALL\n"; + print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; + print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; + print "else\n"; + print "COQLIBINSTALL=${COQLIB}user-contrib\n"; + print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "endif\n\n" + | Project_file.TraditionalInstall -> + section "Install Paths."; + print "COQLIBINSTALL=${COQLIB}user-contrib\n"; + print "COQDOCINSTALL=${DOCDIR}user-contrib\n"; + print "\n" + | Project_file.UserInstall -> + section "Install Paths."; + print "XDG_DATA_HOME?=$(HOME)/.local/share\n"; + print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; + print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; + print "\n" + +let parameters () = + print ".DEFAULT_GOAL := all\n\n# \n"; + print "# This Makefile may take arguments passed as environment variables:\n"; + print "# COQBIN to specify the directory where Coq binaries resides;\n"; + print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n"; + print "# DSTROOT to specify a prefix to install path.\n\n"; + print "# Here is a hack to make $(eval $(shell works:\n"; + print "define donewline\n\n\nendef\n"; + print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\\n' '@'; })))\n"; + print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n" + +let include_dirs (inc_i,inc_r) = + let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in + let parse_rec_includes l = + List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l') + l in + let inc_i' = List.filter (fun (_,i) -> not (List.exists (fun (_,_,i') -> is_prefix i' i) inc_r)) inc_i in + let str_i = parse_includes inc_i in + let str_i' = parse_includes inc_i' in + let str_r = parse_rec_includes inc_r in + section "Libraries definitions."; + if !some_ml4file || !some_mlfile || !some_mlifile then begin + print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n"; + end; + if !some_vfile then begin + print "COQLIBS?="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; + print "COQDOCLIBS?="; print_list "\\\n " str_r; print "\n\n"; + end + +let custom sps = + let pr_path (file,dependencies,com) = + print file; print ": "; print dependencies; print "\n"; + if com <> "" then (print "\t"; print com); print "\n\n" + in + if sps <> [] then section "Custom targets."; + List.iter pr_path sps + +let subdirs sds = + let pr_subdir s = + print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" + in + if sds <> [] then section "Subdirectories."; + List.iter pr_subdir sds + +let forpacks l = + let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in + List.iter (fun it -> + let h = Filename.chop_extension it in + printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h; + printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" (String.capitalize (Filename.basename h)); + printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h; + printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" (String.capitalize (Filename.basename h)) + ) l + +let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc = + let decl_var var = function + |[] -> () + |l -> + printf "%s:=" var; print_list "\\\n " l; print "\n"; + printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var + in + section "Files dispatching."; + decl_var "VFILES" vfiles; + begin match vfiles with + |[] -> () + |l -> + print "VOFILES:=$(VFILES:.v=.vo)\n"; + classify_files_by_root "VOFILES" l inc; + print "GLOBFILES:=$(VFILES:.v=.glob)\n"; + print "VIFILES:=$(VFILES:.v=.vi)\n"; + print "GFILES:=$(VFILES:.v=.g)\n"; + print "HTMLFILES:=$(VFILES:.v=.html)\n"; + print "GHTMLFILES:=$(VFILES:.v=.g.html)\n" + end; + decl_var "ML4FILES" ml4files; + decl_var "MLFILES" mlfiles; + decl_var "MLPACKFILES" mlpackfiles; + decl_var "MLLIBFILES" mllibfiles; + decl_var "MLIFILES" mlifiles; + let mlsfiles = match ml4files,mlfiles,mlpackfiles with + |[],[],[] -> [] + |[],[],_ -> Printf.eprintf "Mlpack cannot work without ml[4]?"; [] + |[],ml,[] -> + print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n"; + ml + |ml4,[],[] -> + print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n"; + ml4 + |ml4,ml,[] -> + print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n"; + List.rev_append ml ml4 + |[],ml,mlpack -> + print "ALLCMOFILES:=$(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; + List.rev_append mlpack ml + |ml4,[],mlpack -> + print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; + List.rev_append mlpack ml4 + |ml4,ml,mlpack -> + print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; + List.rev_append mlpack (List.rev_append ml ml4) in + begin match mlsfiles with + |[] -> () + |l -> + print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n"; + classify_files_by_root "CMOFILES" l inc; + print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n"; + print "OFILES=$(CMXFILES:.cmx=.o)\n"; + end; + begin match mllibfiles with + |[] -> () + |l -> + print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n"; + classify_files_by_root "CMAFILES" l inc; + print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n"; + end; + begin match mlifiles,mlsfiles with + |[],[] -> () + |l,[] -> + print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n"; + classify_files_by_root "CMIFILES" l inc; + |[],l -> + print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n"; + classify_files_by_root "CMIFILES" l inc; + |l1,l2 -> + print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n"; + classify_files_by_root "CMIFILES" (l1@l2) inc; + end; + begin match mllibfiles,mlsfiles with + |[],[] -> () + |l,[] -> + print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n"; + classify_files_by_root "CMXSFILES" l inc; + |[],l -> + print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n"; + classify_files_by_root "CMXSFILES" l inc; + |l1,l2 -> + print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; + classify_files_by_root "CMXSFILES" (l1@l2) inc; + end; + print "\n"; + section "Definition of the toplevel targets."; + print "all: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; + if !some_mllibfile then print "$(CMAFILES) "; + if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile + then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; + print_list "\\\n " other_targets; print "\n\n"; + if !some_mlifile then + begin + print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; + print "\t mkdir $@ || rm -rf $@/*\n"; + print "\t$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; + print "\t$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; + end; + if !some_vfile then + begin + print "spec: $(VIFILES)\n\n"; + print "gallina: $(GFILES)\n\n"; + print "html: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir -p html\n"; + print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; + print "\t- mkdir -p html\n"; + print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "all.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "all-gal.ps: $(VFILES)\n"; + print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "all.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "all-gal.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "validate: $(VOFILES)\n"; + print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n"; + print "beautify: $(VFILES:=.beautified)\n"; + print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n"; + print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n"; + print "\t@echo \'If there were a problem, execute \"for file in $$(find . -name \\*.v.old -print); do mv $${file} $${file%.old}; done\" in your shell/'\n\n" + end + +let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = + let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in + let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in + main_targets vfiles mlfiles other_targets inc; + print ".PHONY: "; + print_list " " + ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" + :: "userinstall" :: "depend" :: "html" :: "validate" :: sds); + print "\n\n"; + custom sps; + subdirs sds; + forpacks mlpackfiles + +let banner () = + print (Printf.sprintf +"############################################################################# +## v # The Coq Proof Assistant ## +## print x; print " ") l + +let command_line args = + print "#\n# This Makefile was generated by the command line :\n"; + print "# coq_makefile "; + print_list args; + print "\n#\n\n" + +let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((i_inc,r_inc) as l) = + let here = Sys.getcwd () in + let not_tops =List.for_all (fun s -> s <> Filename.basename s) in + if List.exists (fun (_,x) -> x = here) i_inc + or List.exists (fun (_,_,x) -> is_prefix x here) r_inc + or (not_tops v && not_tops mli && not_tops ml4 && not_tops ml + && not_tops mllib && not_tops mlpack) then + l + else + ((".",here)::i_inc,r_inc) + +let warn_install_at_root_directory + (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_i,inc_r) = + let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in + let inc_top = List.map (fun (p,_,_) -> p) inc_r_top in + let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in + if inc_r = [] || List.exists (fun f -> List.mem (Filename.dirname f) inc_top) files + then + Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" + (if inc_r_top = [] then "" else "with non trivial logical root ") + +let check_overlapping_include (_,inc_r) = + let pwd = Sys.getcwd () in + let rec aux = function + | [] -> () + | (pdir,_,abspdir)::l -> + if not (is_prefix pwd abspdir) then + Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; + List.iter (fun (pdir',_,abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + in aux inc_r + +let do_makefile args = + let has_file var = function + |[] -> var := false + |_::_ -> 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 + 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 + + let () = match project_file with |None -> () |Some f -> make_name := f in + let () = match makefile with + |None -> () + |Some f -> makefile_name := f; output_channel := open_out f in + has_file some_vfile v_f; has_file some_mlifile mli_f; + has_file some_mlfile ml_f; has_file some_ml4file ml4_f; + has_file some_mllibfile mllib_f; has_file some_mlpackfile mlpack_f; + let check_dep f = + if Filename.check_suffix f ".v" then some_vfile := true + else if (Filename.check_suffix f ".mli") then some_mlifile := true + else if (Filename.check_suffix f ".ml4") then some_ml4file := true + else if (Filename.check_suffix f ".ml") then some_mlfile := true + else if (Filename.check_suffix f ".mllib") then some_mllibfile := true + else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true + in + List.iter (fun (_,dependencies,_) -> + 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 warn_install_at_root_directory targets inc; + check_overlapping_include inc; + banner (); + header_includes (); + warning (); + command_line args; + parameters (); + include_dirs inc; + variables is_install opt defs; + all_target targets inc; + section "Special targets."; + standard opt; + install targets inc is_install; + clean sds sps; + make_makefile sds; + implicit (); + warning (); + if not (makefile = None) then close_out !output_channel; + exit 0 + +let main () = + let args = + if Array.length Sys.argv = 1 then usage (); + List.tl (Array.to_list Sys.argv) + in + do_makefile args + +let _ = Printexc.catch main () diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 deleted file mode 100644 index 50f0344b..00000000 --- a/tools/coq_makefile.ml4 +++ /dev/null @@ -1,614 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (ML "foo") *) - | V of string (* V file : foo.v -> (V "foo") *) - | Special of string * string * string (* file, dependencies, command *) - | Subdir of string - | Def of string * string (* X=foo -> Def ("X","foo") *) - | Include of string - | RInclude of string * string (* -R physicalpath logicalpath *) - -let output_channel = ref stdout -let makefile_name = ref "Makefile" -let make_name = ref "" - -let some_file = ref false -let some_vfile = ref false -let some_mlfile = ref false - -let opt = ref "-opt" -let impredicative_set = ref false -let no_install = ref false - -let print x = output_string !output_channel x -let printf x = Printf.fprintf !output_channel x - -let rec print_list sep = function - | [ x ] -> print x - | x :: l -> print x; print sep; print_list sep l - | [] -> () - -let list_iter_i f = - let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 - -let best_ocamlc = - if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc" -let best_ocamlopt = - if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt" - -let section s = - let l = String.length s in - let sep = String.make (l+5) '#' - and sep2 = String.make (l+5) ' ' in - String.set sep (l+4) '\n'; - String.set sep2 0 '#'; - String.set sep2 (l+3) '#'; - String.set sep2 (l+4) '\n'; - print sep; - print sep2; - print "# "; print s; print " #\n"; - print sep2; - print sep; - print "\n" - -let usage () = - output_string stderr "Usage summary: - -coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom - command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] - ... [VARIABLE = value] ... [-opt|-byte] [-impredicative-set] [-no-install] - [-f file] [-o file] [-h] [--help] - -[file.v]: Coq file to be compiled -[file.ml]: Objective Caml file to be compiled -[subdirectory] : subdirectory that should be \"made\" -[-custom command dependencies file]: add target \"file\" with command - \"command\" and dependencies \"dependencies\" -[-I dir]: look for dependencies in \"dir\" -[-R physicalpath logicalpath]: look for dependencies resursively starting from - \"physicalpath\". The logical path associated to the physical path is - \"logicalpath\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-impredicative-set]: compile with option -impredicative-set of coq -[-no-install]: build a makefile with no install target -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; - exit 1 - -let is_genrule r = - let genrule = Str.regexp("%") in - Str.string_match genrule r 0 - -let absolute_dir dir = - let current = Sys.getcwd () in - Sys.chdir dir; - let dir' = Sys.getcwd () in - Sys.chdir current; - dir' - -let is_prefix dir1 dir2 = - let l1 = String.length dir1 in - let l2 = String.length dir2 in - dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') - -let canonize f = - let l = String.length f in - if l > 2 && f.[0] = '.' && f.[1] = '/' then - let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in - String.sub f n (l-n) - else f - -let is_absolute_prefix dir dir' = - is_prefix (absolute_dir dir) (absolute_dir dir') - -let is_included dir = function - | RInclude (dir',_) -> is_absolute_prefix dir' dir - | Include dir' -> absolute_dir dir = absolute_dir dir' - | _ -> false - -let has_top_file = function - | ML s | V s -> s = Filename.basename s - | _ -> false - -let physical_dir_of_logical_dir ldir = - let pdir = String.copy ldir in - for i = 0 to String.length ldir - 1 do - if pdir.[i] = '.' then pdir.[i] <- '/'; - done; - pdir - -let standard ()= - print "byte:\n"; - print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; - print "opt:\n"; - if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n" - -let is_prefix_of_file dir f = - is_prefix dir (absolute_dir (Filename.dirname f)) - -let classify_files_by_root var files (inc_i,inc_r) = - if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then - begin - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - if List.exists (is_prefix_of_file abspdir) files then - printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" - var i pdir pdir var) - inc_r; - (* Files not in the scope of a -R option *) - let pat_of_dir (pdir,_,_) = pdir^"/%" in - let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in - printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var - end - -let install_include_by_root var files (_,inc_r) = - try - (* All files caught by a -R . option (assuming it is the only one) *) - let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in - let pdir = physical_dir_of_logical_dir ldir in - printf "\t(for i in $(%s); do \\\n" var; - printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir; - printf "\t done)\n" - with Not_found -> - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,ldir,abspdir) -> - if List.exists (is_prefix_of_file abspdir) files then - begin - let pdir' = physical_dir_of_logical_dir ldir in - printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i; - printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir'; - printf "\t done)\n" - end) inc_r; - (* Files not in the scope of a -R option *) - printf "\t(for i in $(%s0); do \\\n" var; - printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; - printf "\t done)\n" - -let install (vfiles,mlfiles,_,sds) inc = - print "install:\n"; - print "\tmkdir -p $(COQLIB)/user-contrib\n"; - if !some_vfile then install_include_by_root "VOFILES" vfiles inc; - if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc; - if !some_mlfile then install_include_by_root "CMIFILES" mlfiles inc; - if Coq_config.has_natdynlink && !some_mlfile then - install_include_by_root "CMXSFILES" mlfiles inc; - List.iter - (fun x -> - printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) - sds; - print "\n" - -let make_makefile sds = - if !make_name <> "" then begin - printf "%s: %s\n" !makefile_name !make_name; - printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; - printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name; - print "\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") - sds; - print "\n"; - end - -let clean sds sps = - print "clean:\n"; - print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n"; - print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ - $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; - if !some_mlfile then - print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n"; - print "\t- rm -rf html\n"; - List.iter - (fun (file,_,_) -> - if not (is_genrule file) then - (print "\t- rm -f "; print file; print "\n")) - sps; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") - sds; - print "\n"; - print "archclean:\n"; - print "\trm -f *.cmx *.o\n"; - List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") - sds; - print "\n\n"; - print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n"; - print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n" - -let header_includes () = () - -let footer_includes () = - if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; - if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n" - -let implicit () = - let ml_rules () = - print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; - print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; - print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; - print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; - print "%.ml.d: %.ml\n"; - print "\t$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n" - and v_rule () = - print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "%.g: %.v\n\t$(GALLINA) $<\n\n"; - print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; - print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; - print "%.v.d: %.v\n"; - print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - if !some_mlfile then ml_rules (); - if !some_vfile then v_rule () - -let variables defs = - let var_aux (v,def) = print v; print "="; print def; print "\n" in - section "Variables definitions."; - print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; - if !opt = "-byte" then - print "override OPT:=-byte\n" - else - print "OPT:=\n"; - if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; - (* Coq executables and relative variables *) - print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; - print "ifdef CAMLBIN\n COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n"; - print "COQC:=$(COQBIN)coqc\n"; - print "COQDEP:=$(COQBIN)coqdep -c\n"; - print "GALLINA:=$(COQBIN)gallina\n"; - print "COQDOC:=$(COQBIN)coqdoc\n"; - print "COQMKTOP:=$(COQBIN)coqmktop\n"; - (* Caml executables and relative variables *) - printf "CAMLLIB:=$(shell $(CAMLBIN)%s -where)\n" best_ocamlc; - printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc; - printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt; - printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; - printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; - print "GRAMMARS:=grammar.cma\n"; - print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS:=\n"; - List.iter var_aux defs; - print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; - print "\n" - -let parameters () = - print "# \n"; - print "# This Makefile may take 3 arguments passed as environment variables:\n"; - print "# - COQBIN to specify the directory where Coq binaries resides;\n"; - print "# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n"; - print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n"; - print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n"; - print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n"; - print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n" - -let include_dirs (inc_i,inc_r) = - let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in - let parse_rec_includes l = - List.map (fun (p,l,_) -> - let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l') - l in - let inc_i' = List.filter (fun (i,_) -> not (List.exists (fun (i',_,_) -> is_absolute_prefix i' i) inc_r)) inc_i in - let str_i = parse_includes inc_i in - let str_i' = parse_includes inc_i' in - let str_r = parse_rec_includes inc_r in - section "Libraries definitions."; - print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n"; - print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ - -I $(COQLIB)/library -I $(COQLIB)/parsing \\ - -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\ - -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\ - -I $(COQLIB)/toplevel"; - List.iter (fun c -> print " \\ - -I $(COQLIB)/plugins/"; print c) Coq_config.plugins_dirs; print "\n"; - print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; - print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n" - - -let rec special = function - | [] -> [] - | Special (file,deps,com) :: r -> (file,deps,com) :: (special r) - | _ :: r -> special r - -let custom sps = - let pr_path (file,dependencies,com) = - print file; print ": "; print dependencies; print "\n"; - if com <> "" then (print "\t"; print com); print "\n\n" - in - if sps <> [] then section "Custom targets."; - List.iter pr_path sps - -let subdirs sds = - let pr_subdir s = - print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n" - in - if sds <> [] then section "Subdirectories."; - List.iter pr_subdir sds; - section "Special targets."; - print ".PHONY: "; - print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" - :: "depend" :: "html" :: sds); - print "\n\n" - -let rec split_arguments = function - | V n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d) - | ML n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d) - | Special (n,dep,c) :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) - | Subdir n :: r -> - let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) - | Include p :: r -> - let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d) - | RInclude (p,l) :: r -> - let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d) - | Def (v,def) :: r -> - let t,i,d = split_arguments r in (t,i,(v,def)::d) - | [] -> ([],[],[],[]),([],[]),[] - -let main_targets vfiles mlfiles other_targets inc = - if !some_vfile then - begin - print "VFILES:="; print_list "\\\n " vfiles; print "\n"; - print "VOFILES:=$(VFILES:.v=.vo)\n"; - classify_files_by_root "VOFILES" vfiles inc; - print "GLOBFILES:=$(VFILES:.v=.glob)\n"; - print "VIFILES:=$(VFILES:.v=.vi)\n"; - print "GFILES:=$(VFILES:.v=.g)\n"; - print "HTMLFILES:=$(VFILES:.v=.html)\n"; - print "GHTMLFILES:=$(VFILES:.v=.g.html)\n" - end; - if !some_mlfile then - begin - print "MLFILES:="; print_list "\\\n " mlfiles; print "\n"; - print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; - classify_files_by_root "CMOFILES" mlfiles inc; - print "CMIFILES:=$(MLFILES:.ml=.cmi)\n"; - classify_files_by_root "CMIFILES" mlfiles inc; - print "CMXFILES:=$(MLFILES:.ml=.cmx)\n"; - print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n"; - classify_files_by_root "CMXSFILES" mlfiles inc; - print "OFILES:=$(MLFILES:.ml=.o)\n"; - end; - print "\nall: "; - if !some_vfile then print "$(VOFILES) "; - if !some_mlfile then print "$(CMOFILES) "; - if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) "; - print_list "\\\n " other_targets; print "\n"; - if !some_vfile then - begin - print "spec: $(VIFILES)\n\n"; - print "gallina: $(GFILES)\n\n"; - print "html: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "all.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "all-gal.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; - print "\n\n" - end - -let all_target (vfiles, mlfiles, sps, sds) inc = - let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in - let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in - section "Definition of the \"all\" target."; - main_targets vfiles mlfiles other_targets inc; - custom sps; - subdirs sds - -let parse f = - let rec string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string s) - | [< >] -> "" - and string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string2 s) - and skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> skip_comment s - | [< >] -> [< >] - and args = parser - | [< '' ' | '\n' | '\t'; s >] -> args s - | [< ''#'; s >] -> args (skip_comment s) - | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s - | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) - | [< >] -> [] - in - let c = open_in f in - let res = args (Stream.of_channel c) in - close_in c; - res - -let rec process_cmd_line = function - | [] -> - some_file := !some_file or !some_mlfile or !some_vfile; [] - | ("-h"|"--help") :: _ -> - usage () - | ("-no-opt"|"-byte") :: r -> - opt := "-byte"; process_cmd_line r - | ("-full"|"-opt") :: r -> - opt := "-opt"; process_cmd_line r - | "-impredicative-set" :: r -> - impredicative_set := true; process_cmd_line r - | "-no-install" :: r -> - no_install := true; process_cmd_line r - | "-custom" :: com :: dependencies :: file :: r -> - let check_dep f = - if Filename.check_suffix f ".v" then - some_vfile := true - else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then - some_mlfile := true - in - List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); - Special (file,dependencies,com) :: (process_cmd_line r) - | "-I" :: d :: r -> - Include d :: (process_cmd_line r) - | "-R" :: p :: l :: r -> - RInclude (p,l) :: (process_cmd_line r) - | ("-I"|"-custom") :: _ -> - usage () - | "-f" :: file :: r -> - make_name := file; - process_cmd_line ((parse file)@r) - | ["-f"] -> - usage () - | "-o" :: file :: r -> - makefile_name := file; - output_channel := (open_out file); - (process_cmd_line r) - | v :: "=" :: def :: r -> - Def (v,def) :: (process_cmd_line r) - | f :: r -> - if Filename.check_suffix f ".v" then begin - some_vfile := true; - V f :: (process_cmd_line r) - end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin - some_mlfile := true; - ML f :: (process_cmd_line r) - end else if (Filename.check_suffix f ".mli") then begin - Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f; - process_cmd_line r - end else - Subdir f :: (process_cmd_line r) - -let banner () = - print (Printf.sprintf -"############################################################################# -## v # The Coq Proof Assistant ## -## print x; print " ") l - -let command_line args = - print "#\n# This Makefile was generated by the command line :\n"; - print "# coq_makefile "; - print_list args; - print "\n#\n\n" - -let directories_deps l = - let print_dep f dep = - if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end - in - let rec iter ((dirs,before) as acc) = function - | [] -> - () - | (Subdir d) :: l -> - print_dep d before; iter (d :: dirs, d :: before) l - | (ML f) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | (V f) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | (Special (f,_,_)) :: l -> - print_dep f dirs; iter (dirs, f :: before) l - | _ :: l -> - iter acc l - in - iter ([],[]) l - -let ensure_root_dir l = - if List.exists (is_included ".") l or not (List.exists has_top_file l) then - l - else - Include "." :: l - -let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) = - let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in - let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in - let files = vfiles @ mlfiles in - if not !no_install && - List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files - then - Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" - (if inc_r_top = [] then "" else "with non trivial logical root ") - -let check_overlapping_include (inc_i,inc_r) = - let pwd = Sys.getcwd () in - let rec aux = function - | [] -> () - | (pdir,_,abspdir)::l -> - if not (is_prefix pwd abspdir) then - Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir; - List.iter (fun (pdir',_,abspdir') -> - if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; - List.iter (fun (pdir',abspdir') -> - if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i - in aux inc_r - -let do_makefile args = - let l = process_cmd_line args in - let l = ensure_root_dir l in - let (_,_,sps,sds as targets), inc, defs = split_arguments l in - warn_install_at_root_directory targets inc; - check_overlapping_include inc; - banner (); - header_includes (); - warning (); - command_line args; - parameters (); - include_dirs inc; - variables defs; - all_target targets inc; - implicit (); - standard (); - if not !no_install then install targets inc; - clean sds sps; - make_makefile sds; - (* TEST directories_deps l; *) - footer_includes (); - warning (); - if not (!output_channel == stdout) then close_out !output_channel; - exit 0 - -let main () = - let args = - if Array.length Sys.argv = 1 then usage (); - List.tl (Array.to_list Sys.argv) - in - do_makefile args - -let _ = Printexc.catch main () diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4 index 14a37a2e..485162ee 100644 --- a/tools/coq_tex.ml4 +++ b/tools/coq_tex.ml4 @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let name = log_dir@[basename] in + let name = log_dir@[basename] in let paths = suffixes name in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () @@ -192,6 +190,7 @@ let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); if not Coq_config.has_natdynlink then option_natdynlk := false; + (* NOTE: These directories are searched from last to first *) if !Flags.boot then begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"] @@ -200,7 +199,9 @@ let coqdep () = add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_rec_dir add_coqlib_known user [] + if Sys.file_exists user then add_rec_dir add_coqlib_known user []; + List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs; + List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 68197e0c..2834af81 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) + | "-mldep" :: ocamldep :: ll -> + option_mldep := Some ocamldep; option_c := true; parse ll | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 5d06b888..e412bc8f 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "", "" -let traite_fichier_ML md ext = +let soustraite_fichier_ML dep md ext = + try + let chan = open_process_in (dep^" -modules "^md^ext) in + let list = ocamldep_parse (Lexing.from_channel chan) in + let a_faire = ref "" in + let a_faire_opt = ref "" in + List.iter + (fun str -> + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt) + (List.rev list); + (!a_faire, !a_faire_opt) + with + | Sys_error _ -> ("","") + | _ -> + Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext; + exit 1 + +let autotraite_fichier_ML md ext = try let chan = open_in (md ^ ext) in let buf = Lexing.from_channel chan in @@ -203,22 +227,29 @@ let traite_fichier_ML md ext = (!a_faire, !a_faire_opt) with Sys_error _ -> ("","") -let traite_fichier_mllib md ext = +let traite_fichier_ML md ext = + match !option_mldep with + | Some dep -> soustraite_fichier_ML dep md ext + | None -> autotraite_fichier_ML md ext + +let traite_fichier_modules md ext = try let chan = open_in (md ^ ext) in let list = mllib_list (Lexing.from_channel chan) in - let a_faire = ref "" in - let a_faire_opt = ref "" in - List.iter - (fun str -> match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire := !a_faire^" "^file^".cmo"; - a_faire_opt := !a_faire_opt^" "^file^".cmx" - | None -> ()) list; - (!a_faire, !a_faire_opt) - with Sys_error _ -> ("","") - + List.fold_left + (fun a_faire str -> match search_mlpack_known str with + | Some mldir -> + let file = file_name str mldir in + 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 + with + | Sys_error _ -> "" + | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while @@ -302,9 +333,12 @@ let traite_fichier_Coq verbose f = match search_mllib_known s with | Some mldir -> declare ".cma" mldir s | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str + match search_mlpack_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> + match search_ml_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> warning_declare f str end in List.iter decl sl | Load str -> @@ -316,9 +350,10 @@ let traite_fichier_Coq verbose f = printf " %s.v" (canonize file_str) with Not_found -> () end + | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () done - with Fin_fichier -> (); - close_in chan + with Fin_fichier -> close_in chan + | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j) with Sys_error _ -> () @@ -346,19 +381,30 @@ let mL_dependencies () = List.iter (fun (name,dirname) -> let fullname = file_name name dirname in - let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in + let dep = traite_fichier_modules fullname ".mllib" in + let efullname = escape fullname in + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; + printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; + printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname; + flush stdout) + (List.rev !mllibAccu); + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let dep = traite_fichier_modules fullname ".mlpack" in let efullname = escape fullname in - printf "%s.cma:%s\n" efullname dep; - printf "%s.cmxa %s.cmxs:%s\n" efullname efullname dep_opt; + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep; + printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; + printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname; flush stdout) - (List.rev !mllibAccu) + (List.rev !mlpackAccu) let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in let glob = if !option_noglob then "" else " "^ename^".glob" in - printf "%s%s%s: %s.v" ename !suffixe glob ename; + printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename; traite_fichier_Coq true (name ^ ".v"); printf "\n"; flush stdout) @@ -370,7 +416,7 @@ let rec suffixes = function | dir::suffix as l -> l::suffixes suffix let add_known phys_dir log_dir f = - match get_extension f [".v";".ml";".mli";".ml4";".mllib"] with + match get_extension f [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with | (basename,".v") -> let name = log_dir@[basename] in let file = phys_dir//basename in @@ -380,6 +426,7 @@ let add_known phys_dir log_dir f = | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) | (basename,".mli") -> add_mli_known basename (Some phys_dir) | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) + | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir) | _ -> () (* Visits all the directories under [dir], including [dir], @@ -432,7 +479,7 @@ let rec treat_file old_dirname old_name = while true do treat_file (Some newdirname) (readdir dir) done with End_of_file -> closedir dir) | S_REG -> - (match get_extension name [".v";".ml";".mli";".ml4";".mllib"] with + (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with | (base,".v") -> let name = file_name base dirname and absname = absolute_file_name base dirname in @@ -440,5 +487,6 @@ let rec treat_file old_dirname old_name = | (base,(".ml"|".ml4" as ext)) -> addQueue mlAccu (base,ext,dirname) | (base,".mli") -> addQueue mliAccu (base,dirname) | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> ()) | _ -> () diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli new file mode 100644 index 00000000..53c3ba17 --- /dev/null +++ b/tools/coqdep_common.mli @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string -> string +val get_extension : string -> string list -> string * string +val basename_noext : string -> string +val mlAccu : (string * string * dir) list ref +val mliAccu : (string * dir) list ref +val mllibAccu : (string * dir) list ref +val vAccu : (string * string) list ref +val addQueue : 'a list ref -> 'a -> unit +val add_ml_known : string -> dir -> unit +val iter_ml_known : (string -> dir -> unit) -> unit +val search_ml_known : string -> dir option +val add_mli_known : string -> dir -> unit +val iter_mli_known : (string -> dir -> unit) -> unit +val search_mli_known : string -> dir option +val add_mllib_known : string -> dir -> unit +val search_mllib_known : string -> dir option +val vKnown : (string list, string) Hashtbl.t +val coqlibKnown : (string list, unit) Hashtbl.t +val file_name : string -> string option -> string +val escape : string -> string +val canonize : string -> string +val mL_dependencies : unit -> unit +val coq_dependencies : unit -> unit +val suffixes : 'a list -> 'a list list +val add_known : string -> string list -> string -> unit +val add_directory : + bool -> + (string -> string list -> string -> unit) -> string -> string list -> unit +val add_dir : + (string -> string list -> string -> unit) -> string -> string list -> unit +val add_rec_dir : + (string -> string list -> string -> unit) -> string -> string list -> unit +val treat_file : dir -> string -> unit diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli new file mode 100644 index 00000000..6b6e0da9 --- /dev/null +++ b/tools/coqdep_lexer.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* coq_token +val caml_action : Lexing.lexbuf -> mL_token +val mllib_list : Lexing.lexbuf -> string list +val ocamldep_parse : Lexing.lexbuf -> string list diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 28ea4200..159c6d3c 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* char -> int diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5cb670dc..6b8a3f5e 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + coqlib + | Some _ | None -> + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let rpath = if Coq_config.local then [] else + (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in + let coqlib = List.fold_left Filename.concat prefix rpath in + if Sys.file_exists (Filename.concat coqlib file) then coqlib + else prefix let header_trailer = ref true let header_file = ref "" @@ -90,6 +109,7 @@ let toc_depth = (ref None : int option ref) let lib_name = ref "Library" let lib_subtitles = ref false let interpolate = ref false +let inline_notmono = ref false let charset = ref "iso-8859-1" let inputenc = ref "" @@ -103,7 +123,7 @@ let set_latin1 () = let set_utf8 () = charset := "utf-8"; - inputenc := "utf8"; + inputenc := "utf8x"; utf8 := true (* Parsing options *) diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 24b514b7..ccd285f1 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -101,8 +101,13 @@ h4.section { color: rgb(30%,30%,70%); font-family: monospace } -.doc .inlinecode .id { - color: rgb(30%,30%,70%); +.doc .inlinecode .id { + color: rgb(30%,30%,70%); +} + +.inlinecodenm { + display: inline; + color: #444444; } .doc .code { @@ -124,6 +129,32 @@ h4.section { font-family: monospace; } +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: monospace; + text-align: center; +/* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + /* Pied de page */ #footer { font-size: 65%; @@ -231,4 +262,13 @@ h4.section { position: absolute; bottom: 0; text-align: bottom; -} \ No newline at end of file +} + +.paragraph { + height: 0.75em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli index 085ae122..cb511c16 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 63850bd5..89047e83 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ignore (doc None (from_string s))); if eol then doc_bol lexbuf else doc None lexbuf } - | space* nl space* '-'+ - { (* adding this production instead of just letting the paragraph - production and the begin list production fire eliminates - extra vertical whitespace. *) - let buf' = lexeme lexbuf in - let buf = - let bufs = Str.split_delim (Str.regexp "['\n']") buf' in - match bufs with - | (_ :: s :: []) -> s - | (_ :: _ :: s :: _) -> s - | _ -> eprintf "Internal error bad_split1 - please report\n"; - exit 1 + | space_nl* '-'+ + { let buf' = lexeme lexbuf in + let bufs = Str.split_delim (Str.regexp "['\n']") buf' in + let lines = (List.length bufs) - 1 in + let line = + match bufs with + | [] -> eprintf "Internal error bad_split1 - please report\n"; + exit 1 + | _ -> List.nth bufs lines in - match check_start_list buf with + match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.item 1; doc (Some [n]) lexbuf - | Rule -> Output.rule (); doc None lexbuf - } - | space* '-'+ - { let buf = lexeme lexbuf in - match check_start_list buf with - | Neither -> backtrack lexbuf; doc None lexbuf - | List n -> Output.item 1; doc (Some [n]) lexbuf + | List n -> Output.paragraph (); + Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } + | space* nl+ + { Output.paragraph (); doc_bol lexbuf } | "<<" space* { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } | eof @@ -728,6 +717,8 @@ and doc_list_bol indents = parse Output.end_inline_coq_block (); formatted := false; doc_list_bol indents lexbuf } + | "[[[" nl + { inf_rules (Some indents) lexbuf } | space* nl space* '-' { (* Like in the doc_bol production, these two productions exist only to deal properly with whitespace *) @@ -763,9 +754,16 @@ and doc_list_bol indents = parse backtrack_past_newline lexbuf; doc_list_bol indents lexbuf end - | Before -> Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf + | Before -> + (* Here we were at the beginning of a line, and it was blank. + The next line started before any list items. So: insert + a paragraph for the empty line, rewind to whatever's just + after the newline, then toss over to doc_bol for whatever + comes next. *) + Output.stop_item (); + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_bol lexbuf } | space* _ @@ -774,7 +772,10 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - Output.reach_item_level (n-1); + (if n = 1 then + Output.stop_item () + else + Output.reach_item_level (n-1)); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> @@ -802,6 +803,8 @@ and doc indents = parse | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf else doc indents lexbuf)} + | "[[[" nl + { inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } | "[" @@ -817,6 +820,18 @@ and doc indents = parse let eol = comment lexbuf in if eol then bol_parse lexbuf else doc indents lexbuf } + | '*'* "*)" space_nl* "(**" + {(match indents with + | Some _ -> Output.stop_item () + | None -> ()); + (* this says - if there is a blank line between the two comments, + insert one in the output too *) + let lines = List.length (Str.split_delim (Str.regexp "['\n']") + (lexeme lexbuf)) + in + if lines > 2 then Output.paragraph (); + doc_bol lexbuf + } | '*'* "*)" space* nl { true } | '*'* "*)" @@ -905,10 +920,16 @@ and escaped_coq = parse { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } - | space - { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0); - escaped_coq lexbuf } - | _ + | space_nl* + { let str = lexeme lexbuf in + Tokens.flush_sublexer(); + (if !Cdglobals.inline_notmono then () + else Output.end_inline_coq ()); + String.iter Output.char str; + (if !Cdglobals.inline_notmono then () + else Output.start_inline_coq ()); + escaped_coq lexbuf } + | _ { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf); escaped_coq lexbuf } @@ -1135,6 +1156,71 @@ and printing_token_body = parse | _ { Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } +(*s These handle inference rules, parsing the body segments of things + enclosed in [[[ ]]] brackets *) +and inf_rules indents = parse + | space* nl (* blank line, before or between definitions *) + { inf_rules indents lexbuf } + | "]]]" nl (* end of the inference rules block *) + { match indents with + | Some ls -> doc_list_bol ls lexbuf + | None -> doc_bol lexbuf } + | _ + { backtrack lexbuf; (* anything else must be the first line in a rule *) + inf_rules_assumptions indents [] lexbuf} + +(* The inference rule parsing just collects the inference rule and then + calls the output function once, instead of doing things incrementally + like the rest of the lexer. If only there were a real parsing phase... +*) +and inf_rules_assumptions indents assumptions = parse + | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let dashes_and_name = + cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) + in + let ldn = String.length dashes_and_name in + let (dashes,name) = + try (let i = String.index dashes_and_name ' ' in + let d = String.sub dashes_and_name 0 i in + let n = cut_head_tail_spaces + (String.sub dashes_and_name (i+1) (ldn-i-1)) + in + (d, Some n)) + with _ -> (dashes_and_name, None) + + in + inf_rules_conclusion indents (List.rev assumptions) + (spaces, dashes, name) [] lexbuf } + | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let assumption = cut_head_tail_spaces + (String.sub line 0 (String.length line - 1)) + in + inf_rules_assumptions indents ((spaces,assumption)::assumptions) + lexbuf } + +(*s The conclusion is required to come immediately after the + horizontal bar. It is allowed to contain multiple lines of + text, like the assumptions. The conclusion ends when we spot a + blank line or a ']]]'. *) +and inf_rules_conclusion indents assumptions middle conclusions = parse + | space* nl | space* "]]]" nl (* end of conclusions. *) + { backtrack lexbuf; + Output.inf_rule assumptions middle (List.rev conclusions); + inf_rules indents lexbuf } + | space* [^ '\n']+ nl (* this is a line in the conclusion *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let conc = cut_head_tail_spaces (String.sub line 0 + (String.length line - 1)) + in + inf_rules_conclusion indents assumptions middle + ((spaces,conc) :: conclusions) lexbuf + } + (*s A small scanner to support the chapter subtitle feature *) and st_start m = parse | "(*" "*"+ space+ "*" space+ diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index a2cb995e..c8e7770a 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) - (* Encoded notations have the form section:sc:x_'++'_x where: *) - (* - the section, if any, ends with a "." *) - (* - the scope can be empty *) - (* - tokens are separated with "_" *) - (* - non-terminal symbols are conventionally represented by "x" *) - (* - terminals are enclosed within simple quotes *) - (* - existing simple quotes (that necessarily are parts of terminals) *) - (* are doubled *) + (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* - the section, if any, ends with a "." *) + (* - the scope can be empty *) + (* - tokens are separated with "_" *) + (* - non-terminal symbols are conventionally represented by "x" *) + (* - terminals are enclosed within simple quotes *) + (* - existing simple quotes (that necessarily are parts of *) + (* terminals) are doubled *) (* (as a consequence, when a terminal contains "_" or "x", these *) (* necessarily appear enclosed within non-doubled simple quotes) *) - (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) - (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) + (* - non-printable characters < 32 are left encoded so that they *) + (* are human-readable in index files *) + (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) + (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in @@ -268,10 +267,10 @@ let prepare_entry s = function | _ -> assert false) end else - if s.[!j] = '\'' then begin - if (!j = l || s.[!j+1] <> '\'') then quoted := false - else (ntn.[!k] <- s.[!j]; incr k; incr j) - end else begin + if s.[!j] = '\'' then + if (!j = l || s.[!j+1] = '_') then quoted := false + else (incr j; ntn.[!k] <- s.[!j]; incr k) + else begin ntn.[!k] <- s.[!j]; incr k end; @@ -324,8 +323,27 @@ let type_of_string = function | "sec" -> Section | s -> raise (Invalid_argument ("type_of_string:" ^ s)) -let read_glob f = +let ill_formed_glob_file f = + eprintf "Warning: ill-formed file %s (links will not be available)\n" f +let outdated_glob_file f = + eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f + +let correct_file vfile f c = + let s = input_line c in + if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then + (ill_formed_glob_file f; false) + else + let s = String.sub s 7 (String.length s - 7) in + match vfile, s with + | None, "NO" -> true + | Some _, "NO" -> ill_formed_glob_file f; false + | None, _ -> ill_formed_glob_file f; false + | Some vfile, s -> + s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false) + +let read_glob vfile f = let c = open_in f in + if correct_file vfile f c then let cur_mod = ref "" in try while true do diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index a009e9dc..bb775d26 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> unit +val read_glob : Digest.t option -> string -> unit (*s Indexes *) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 23dadbc1..b1303f18 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) * - coq_module: chop ./// (arbitrary amount of slashes), not only "./" @@ -53,6 +50,7 @@ let usage () = prerr_endline " -p insert in LaTeX preamble"; prerr_endline " --files-from read file names to process in "; prerr_endline " --glob-from read globalization information from "; + prerr_endline " --no-glob don't use any globalization information (no links will be inserted at identifiers)"; prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; @@ -73,6 +71,7 @@ let usage () = prerr_endline " --no-lib-name don't display \"Library\" before library names in the toc"; prerr_endline " --lib-name call top level toc entries instead of \"Library\""; prerr_endline " --lib-subtitles first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles"; + prerr_endline " --inline-notmono use a proportional width font for inline code (possibly with a different color)"; prerr_endline ""; exit 1 @@ -107,25 +106,6 @@ let check_if_file_exists f = end -(*s Manipulations of paths and path aliases *) - -let normalize_path p = - (* We use the Unix subsystem to normalize a physical path (relative - or absolute) and get rid of symbolic links, relative links (like - ./ or ../ in the middle of the path; it's tricky but it - works... *) - (* Rq: Sys.getcwd () returns paths without '/' at the end *) - let orig = Sys.getcwd () in - Sys.chdir p; - let res = Sys.getcwd () in - Sys.chdir orig; - res - -let normalize_filename f = - let basename = Filename.basename f in - let dirname = Filename.dirname f in - normalize_path dirname, basename - (* [paths] maps a physical path to a name *) let paths = ref [] @@ -303,6 +283,9 @@ let parse () = | ("-lib-subtitles" | "--lib-subtitles") :: rem -> Cdglobals.lib_subtitles := true; parse_rec rem + | ("-inline-notmono" | "--inline-notmono") :: rem -> + Cdglobals.inline_notmono := true; + parse_rec rem | ("-latin1" | "--latin1") :: rem -> Cdglobals.set_latin1 (); parse_rec rem @@ -341,6 +324,8 @@ let parse () = glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () + | ("-no-glob" | "--no-glob") :: rem -> + glob_source := NoGlob; parse_rec rem | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> Cdglobals.externals := false; parse_rec rem | ("--external" | "-external") :: u :: logicalpath :: rem -> @@ -350,7 +335,11 @@ let parse () = | ("--coqlib" | "-coqlib") :: [] -> usage () | ("--boot" | "-boot") :: rem -> - Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem + Cdglobals.coqlib_path := normalize_path ( + Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + ); parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> @@ -458,13 +447,13 @@ let gen_mult_files l = end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) -let read_glob_file x = - try Index.read_glob x - with Sys_error s -> - eprintf "Warning: %s (links will not be available)\n" s +let read_glob_file vfile f = + try Index.read_glob vfile f + with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s let read_glob_file_of = function - | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob") + | Vernac_file (f,_) -> + read_glob_file (Some f) (Filename.chop_extension f ^ ".glob") | Latex_file _ -> () let index_module = function @@ -486,7 +475,7 @@ let produce_document l = (match !Cdglobals.glob_source with | NoGlob -> () | DotGlob -> List.iter read_glob_file_of l - | GlobFile f -> read_glob_file f); + | GlobFile f -> read_glob_file None f); List.iter index_module l; match !out_to with | StdOut -> diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index eefcfd11..e3d5741a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Notation then + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s) + else + (* Glob file still not able to say the exact extent of the definition *) + (* so we currently renounce to highlight the notation location *) + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{%s}" s s) let reference s = function | Def (fullid,typ) -> @@ -478,6 +490,8 @@ module Html = struct end let trailer () = + if !index && (get_module false) <> "Index" then + printf "\n\n
\n
Index" !index_name; if !header_trailer then if !footer_file_spec then let cin = Pervasives.open_in !footer_file in @@ -489,8 +503,6 @@ module Html = struct with End_of_file -> Pervasives.close_in cin else begin - if !index && (get_module false) <> "Index" then - printf "
\n\n
\n
Index" !index_name; printf "
This page has been generated by "; printf "coqdoc\n" Coq_config.wwwcoq; printf "
\n\n\n\n\n" @@ -624,7 +636,7 @@ module Html = struct let rec reach_item_level n = if !item_level < n then begin - printf "
    \n
  • "; incr item_level; + printf "
      \n
    • "; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n
      • \n
    \n"; decr item_level; @@ -662,7 +674,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "" + let start_inline_coq () = + if !inline_notmono then printf "" + else printf "" let end_inline_coq () = printf "" @@ -670,7 +684,50 @@ module Html = struct let end_inline_coq_block () = end_inline_coq () - let paragraph () = printf "\n

    \n" + let paragraph () = printf "\n
    \n\n" + + (* inference rules *) + let inf_rule assumptions (_,_,midnm) conclusions = + (* this first function replaces any occurance of 3 or more spaces + in a row with " "s. We do this to the assumptions so that + people can put multiple rules on a line with nice formatting *) + let replace_spaces str = + let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in + let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in + let strs = List.map (fun r -> match r with + | Str.Text s -> [s] + | Str.Delim s -> + copy " " (String.length s)) + results + in + String.concat "" (List.concat strs) + in + let start_assumption line = + (printf "\n"; + printf " %s\n" (replace_spaces line)) in + let end_assumption () = + (printf " \n"; + printf "\n") in + let rec print_assumptions hyps = + match hyps with + | [] -> start_assumption "  " + | [(_,hyp)] -> start_assumption hyp + | ((_,hyp) :: hyps') -> (start_assumption hyp; + end_assumption (); + print_assumptions hyps') in + printf "
    \n"; + print_assumptions assumptions; + printf " " + | Some s -> printf " %s  \n " s); + printf "\n"; + printf "\n"; + printf " \n"; + printf "\n"; + print_assumptions conclusions; + end_assumption (); + printf "
    \n"; + (match midnm with + | None -> printf "  \n
    " let section lev f = let lab = new_label () in @@ -1136,6 +1193,21 @@ let verbatim_char = select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char +let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = + start_verbatim (); + let dumb_line = + function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln); + char '\n') + in + (List.iter dumb_line assumptions; + dumb_line (midsp, midln ^ (match midnm with + | Some s -> " " ^ s + | None -> "")); + List.iter dumb_line conclusions); + stop_verbatim () + +let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb + let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index dcd9072d..53d88666 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val start_verbatim : unit -> unit val stop_verbatim : unit -> unit +(* this outputs an inference rule in one go. You pass it the list of + assumptions, then the middle line info, then the conclusion (which + is allowed to span multiple lines). + + In each case, the int is the number of spaces before the start of + the line's text and the string is the text of the line with the + leading trailing space trimmed. For the middle rule, you can + also optionally provide a name. + + We need the space info so that in modes where we aren't doing + something smart we can just format the rule verbatim like the user did +*) +val inf_rule : (int * string) list + -> (int * string * (string option)) + -> (int * string) list + -> unit + val make_multi_index : unit -> unit val make_index : unit -> unit val make_toc : unit -> unit diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index 9de39083..a228797e 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* exit 1 | _ -> () + +let commands = + [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s))); + "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s))); + "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s))); + "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); + "GOALS", (fun _ -> eval_call Ide_intf.goals); + "HINTS", (fun _ -> eval_call Ide_intf.hints); + "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options); + "STATUS", (fun _ -> eval_call Ide_intf.status); + "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); + "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); + "#", (fun _ -> raise Comment); + ] + +let read_eval_print line = + let lline = String.length line in + let rec find_cmd = function + | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1 + | (cmd,fn) :: cmds -> + let lcmd = String.length cmd in + if lline >= lcmd && String.sub line 0 lcmd = cmd then + let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> "" + in fn arg + else find_cmd cmds + in + find_cmd commands + +let usage () = + Printf.printf + "A fake coqide process talking to a coqtop -ideslave.\n\ + Usage: %s []\n\ + Input syntax is one API call per line, the keyword coming first,\n\ + with the rest of the line as string argument (e.g. INTERP Check plus.)\n\ + Supported API keywords are:\n" (Filename.basename Sys.argv.(0)); + List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands; + exit 1 + +let main = + Sys.set_signal Sys.sigpipe + (Sys.Signal_handle + (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); + let coqtop_name = match Array.length Sys.argv with + | 1 -> "coqtop" + | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1) + | _ -> usage () + in + coqtop := Unix.open_process (coqtop_name^" -ideslave"); + while true do + let l = try read_line () with End_of_file -> exit 0 + in + try read_eval_print l + with + | Comment -> () + | e -> + prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1 + done diff --git a/tools/gallina.ml b/tools/gallina.ml index 161d86a8..3d7b1a2c 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*