summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /tools
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'tools')
-rwxr-xr-x[-rw-r--r--]tools/beautify-archive0
-rw-r--r--tools/compat5.ml13
-rw-r--r--tools/compat5.mlp23
-rw-r--r--tools/compat5b.ml13
-rw-r--r--tools/compat5b.mlp23
-rw-r--r--tools/coq-syntax.el3
-rw-r--r--tools/coq_makefile.ml720
-rw-r--r--tools/coq_makefile.ml4614
-rw-r--r--tools/coq_tex.ml (renamed from tools/coq_tex.ml4)71
-rw-r--r--tools/coqdep.ml11
-rw-r--r--tools/coqdep_boot.ml6
-rw-r--r--tools/coqdep_common.ml116
-rw-r--r--tools/coqdep_common.mli49
-rw-r--r--tools/coqdep_lexer.mli27
-rw-r--r--tools/coqdep_lexer.mll228
-rw-r--r--tools/coqdoc/alpha.ml4
-rw-r--r--tools/coqdoc/alpha.mli4
-rw-r--r--tools/coqdoc/cdglobals.ml46
-rw-r--r--tools/coqdoc/coqdoc.css46
-rw-r--r--tools/coqdoc/cpretty.mli4
-rw-r--r--tools/coqdoc/cpretty.mll233
-rw-r--r--tools/coqdoc/index.ml103
-rw-r--r--tools/coqdoc/index.mli9
-rw-r--r--tools/coqdoc/main.ml49
-rw-r--r--tools/coqdoc/output.ml292
-rw-r--r--tools/coqdoc/output.mli32
-rw-r--r--tools/coqdoc/tokens.ml2
-rw-r--r--tools/coqdoc/tokens.mli2
-rw-r--r--tools/coqwc.mll4
-rw-r--r--tools/escape_string.ml1
-rw-r--r--tools/fake_ide.ml84
-rw-r--r--tools/gallina.ml4
-rw-r--r--tools/gallina_lexer.mll4
-rw-r--r--tools/mingwpath.ml15
-rw-r--r--tools/win32hack.mllib1
-rw-r--r--tools/win32hack_filename.ml4
36 files changed, 1863 insertions, 997 deletions
diff --git a/tools/beautify-archive b/tools/beautify-archive
index ccfeb3db..ccfeb3db 100644..100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
diff --git a/tools/compat5.ml b/tools/compat5.ml
new file mode 100644
index 00000000..663f8d44
--- /dev/null
+++ b/tools/compat5.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+ add to gain camlp5 compatibility :-).
+
+ See [compat5.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
new file mode 100644
index 00000000..aabf7288
--- /dev/null
+++ b/tools/compat5.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+ - GEXTEND ... becomes EXTEND ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+ | [< '(KEYWORD "GEXTEND", loc); s >] ->
+ [< '(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..2f104da7
--- /dev/null
+++ b/tools/compat5b.ml
@@ -0,0 +1,13 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This file is meant for camlp5, for which there is nothing to
+ add to gain camlp5 compatibility :-).
+
+ See [compat5b.mlp] for the [camlp4] counterpart
+*)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
new file mode 100644
index 00000000..f7e08115
--- /dev/null
+++ b/tools/compat5b.mlp
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
+ - EXTEND ... becomes EXTEND Gram ...
+*)
+
+open Camlp4.PreCast
+
+let rec my_token_filter = parser
+ | [< '(KEYWORD "EXTEND",_ as t); s >] ->
+ [< '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..6f0071a4
--- /dev/null
+++ b/tools/coq_makefile.ml
@@ -0,0 +1,720 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* créer un Makefile pour un développement Coq automatiquement *)
+
+let output_channel = ref stdout
+let makefile_name = ref "Makefile"
+let make_name = ref ""
+
+let some_vfile = ref false
+let some_mlfile = ref false
+let some_mlifile = ref false
+let some_ml4file = ref false
+let some_mllibfile = ref false
+let some_mlpackfile = 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 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\n";
+ 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 $(HASNATDYNLINK_OR_EMPTY),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$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( 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: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n";
+ 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 "%.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) $(COQDOCFLAGS) -latex $< -o $@\n\n";
+ print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
+ print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
+ print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -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 || !some_mlpackfile || !some_mllibfile then
+ print "COQDEP?=$(COQBIN)coqdep -c\n";
+ if !some_vfile then begin
+ print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+ print "COQCHKFLAGS?=-silent -o\n";
+ print "COQDOCFLAGS?=-interpolate -utf8\n";
+ print "COQC?=$(COQBIN)coqc\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?=-loc loc\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 -d '\\r' | 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 || !some_mllibfile || !some_mlpackfile 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 "ifeq '$(HASNATDYNLINK)' 'true'\n";
+ print "HASNATDYNLINK_OR_EMPTY := yes\n";
+ print "else\n";
+ print "HASNATDYNLINK_OR_EMPTY :=\n";
+ print "endif\n\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 $(HASNATDYNLINK_OR_EMPTY),$(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 $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
+ print "\t- mkdir -p html\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "all.ps: $(VFILES)\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "all-gal.ps: $(VFILES)\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "all.pdf: $(VFILES)\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
+ print "all-gal.pdf: $(VFILES)\n";
+ print "\t$(COQDOC) -toc $(COQDOCFLAGS) -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 ##
+## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
+## \\VV/ # ##
+## // # Makefile automagically generated by coq_makefile V%s ##
+#############################################################################
+
+" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
+
+let warning () =
+ print "# WARNING\n#\n";
+ print "# This Makefile has been automagically generated\n";
+ print "# Edit at your own risks !\n";
+ print "#\n# END OF WARNING\n\n"
+
+let print_list l = List.iter (fun x -> 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: coq_makefile.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* créer un Makefile pour un développement Coq automatiquement *)
-
-type target =
- | ML of string (* ML file : foo.ml -> (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 ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \\VV/ # ##
-## // # Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
-
-let warning () =
- print "# WARNING\n#\n";
- print "# This Makefile has been automagically generated\n";
- print "# Edit at your own risks !\n";
- print "#\n# END OF WARNING\n\n"
-
-let print_list l = List.iter (fun x -> 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.ml
index 14a37a2e..350b59aa 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_tex.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* coq-tex
* JCF, 16/1/98
* adapted from caml-tex (perl script written by Xavier Leroy)
@@ -15,15 +13,6 @@
* Perl isn't as portable as it pretends to be, and is quite difficult
* to read and maintain... Let us rewrite the stuff in Caml! *)
-let _ =
- match Sys.os_type with
- | "Unix" -> ()
- | _ -> begin
- print_string "This program only runs under Unix !\n";
- flush stdout;
- exit 1
- end
-
let linelen = ref 72
let output = ref ""
let output_specified = ref false
@@ -33,6 +22,7 @@ let verbose = ref false
let slanted = ref false
let hrule = ref false
let small = ref false
+let boot = ref false
let coq_prompt = Str.regexp "Coq < "
let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
@@ -88,21 +78,23 @@ let bang = Str.regexp "!"
let expos = Str.regexp "^"
let tex_escaped s =
- let rec trans = parser
- | [< s1 = (parser
- | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
- "\\" ^ (String.make 1 c)
- | [< ''\\' >] -> "{\\char'134}"
- | [< ''^' >] -> "{\\char'136}"
- | [< ''~' >] -> "{\\char'176}"
- | [< '' ' >] -> "~"
- | [< ''<' >] -> "{<}"
- | [< ''>' >] -> "{>}"
- | [< 'c >] -> String.make 1 c);
- s2 = trans >] -> s1 ^ s2
- | [< >] -> ""
+ let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in
+ let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+ let adapt_delim = function
+ | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+ | "\\" -> "{\\char'134}"
+ | "^" -> "{\\char'136}"
+ | "~" -> "{\\char'176}"
+ | " " -> "~"
+ | "<" -> "{<}"
+ | ">" -> "{>}"
+ | _ -> assert false
in
- trans (Stream.of_string s)
+ let adapt = function
+ | Str.Text s -> s
+ | Str.Delim s -> adapt_delim s
+ in
+ String.concat "" (List.map adapt (Str.full_split delims s))
let encapsule sl c_out s =
if sl then
@@ -198,11 +190,11 @@ let insert texfile coq_output result =
else begin
if !verbose then Printf.printf "Coq < %s\n" s;
if has_match dot_end_line s then
- let bl = next_block (succ k) in
+ let bl = next_block (succ k) in
if !verbose then List.iter print_endline bl;
eval 0
else
- eval (succ k)
+ eval (succ k)
end
in
try
@@ -268,18 +260,29 @@ let parse_cl () =
"-hrule", Arg.Set hrule,
" Coq parts are written between 2 horizontal lines";
"-small", Arg.Set small,
- " Coq parts are written in small font"
+ " Coq parts are written in small font";
+ "-boot", Arg.Set boot,
+ " Launch coqtop with the -boot option"
]
(fun s -> files := s :: !files)
"coq-tex [options] file ..."
+let find_coqtop () =
+ let prog = Sys.executable_name in
+ try
+ let size = String.length prog in
+ let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in
+ (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7))
+ with Not_found -> begin
+ Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
+ "coqtop"
+ end
+
let main () =
parse_cl ();
- if !image = "" then begin
- Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
- image := "coqtop"
- end;
- if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin
+ if !image = "" then image := Filename.quote (find_coqtop ());
+ if !boot then image := !image ^ " -boot";
+ if Sys.command (!image ^ " -batch -silent") <> 0 then begin
Printf.printf "Error: ";
let _ = Sys.command (!image ^ " -batch") in
exit 1
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index d36fdae3..90cdd12d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Printf
open Coqdep_lexer
open Coqdep_common
@@ -40,7 +38,7 @@ let rec warning_mult suf iter =
let add_coqlib_known phys_dir log_dir f =
match get_extension f [".vo"] with
| (basename,".vo") ->
- 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..19aba41d 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep_boot.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Coqdep_common
(** [coqdep_boot] is a stripped-down version of [coqdep], whose
@@ -22,6 +20,8 @@ let rec parse = function
| "-natdynlink" :: "no" :: ll -> 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..4977a94c 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep_common.ml 11984 2009-03-16 13:41:49Z letouzey $ *)
-
open Printf
open Coqdep_lexer
open Unix
@@ -26,6 +24,7 @@ let option_c = ref false
let option_noglob = ref false
let option_slash = ref false
let option_natdynlk = ref true
+let option_mldep = ref None
let norecdir_list = ref ([]:string list)
@@ -63,6 +62,7 @@ let basename_noext filename =
let mlAccu = ref ([] : (string * string * dir) list)
and mliAccu = ref ([] : (string * dir) list)
and mllibAccu = ref ([] : (string * dir) list)
+and mlpackAccu = ref ([] : (string * dir) list)
(** Coq files specifies on the command line:
- first string is the full filename, with only its extension removed
@@ -108,12 +108,17 @@ let mkknown () =
let add_ml_known, iter_ml_known, search_ml_known = mkknown ()
let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
let add_mllib_known, _, search_mllib_known = mkknown ()
+let add_mlpack_known, _, search_mlpack_known = mkknown ()
let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
let clash_v = ref ([]: (string list * string list) list)
+let error_cannot_parse s (i,j) =
+ Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
+ exit 1
+
let warning_module_notfound f s =
eprintf "*** Warning: in file %s, library " f;
eprintf "%s.v is required and has not been found in loadpath!\n"
@@ -122,12 +127,12 @@ let warning_module_notfound f s =
let warning_notfound f s =
eprintf "*** Warning: in file %s, the file " f;
- eprintf "%s.v is required and has not been found !\n" s;
+ eprintf "%s.v is required and has not been found!\n" s;
flush stderr
let warning_declare f s =
eprintf "*** Warning: in file %s, declared ML module " f;
- eprintf "%s has not been found !\n" s;
+ eprintf "%s has not been found!\n" s;
flush stderr
let warning_clash file dir =
@@ -178,7 +183,26 @@ let depend_ML str =
(" "^mlifile^".cmi"," "^mlifile^".cmi")
| None, None -> "", ""
-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
@@ -257,7 +288,7 @@ let canonize f =
| (f,_) :: _ -> escape f
| _ -> escape f
-let traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq verbose f =
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
@@ -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 ->
@@ -313,12 +347,15 @@ let traite_fichier_Coq verbose f =
addQueue deja_vu_v [str];
try
let file_str = Hashtbl.find vKnown [str] in
- printf " %s.v" (canonize file_str)
+ let canon = canonize file_str in
+ printf " %s.v" canon;
+ traite_fichier_Coq true (canon ^ ".v")
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 +383,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 +418,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 +428,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 +481,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 +489,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..afc171cb
--- /dev/null
+++ b/tools/coqdep_common.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val option_c : bool ref
+val option_noglob : bool ref
+val option_slash : bool ref
+val option_natdynlk : bool ref
+val option_mldep : string option ref
+val norecdir_list : string list ref
+val suffixe : string ref
+type dir = string option
+val ( // ) : string -> 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..7cea9743
--- /dev/null
+++ b/tools/coqdep_lexer.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type mL_token = Use_module of string
+
+type qualid = string list
+
+type coq_token =
+ Require of qualid list
+ | RequireString of string
+ | Declare of string list
+ | Load of string
+ | AddLoadPath of string
+ | AddRecLoadPath of string * qualid
+
+exception Fin_fichier
+exception Syntax_error of int * int
+
+val coq_action : Lexing.lexbuf -> 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..f59d6a0f 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqdep_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
{
open Filename
@@ -15,26 +13,42 @@
type mL_token = Use_module of string
- type spec = bool
+ type qualid = string list
type coq_token =
- | Require of string list list
+ | Require of qualid list
| RequireString of string
- | Declare of string list
+ | Declare of string list (* Names are assumed to be uncapitalized *)
| Load of string
+ | AddLoadPath of string
+ | AddRecLoadPath of string * qualid
let comment_depth = ref 0
exception Fin_fichier
+ exception Syntax_error of int*int
let module_current_name = ref []
let module_names = ref []
let ml_module_name = ref ""
+ let loadpath = ref ""
let mllist = ref ([] : string list)
let field_name s = String.sub s 1 (String.length s - 1)
+ let unquote_string s =
+ String.sub s 1 (String.length s - 2)
+
+ let unquote_vfile_string s =
+ let f = unquote_string s in
+ if check_suffix f ".v" then chop_suffix f ".v" else f
+
+ let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
+ lexbuf.lex_curr_p <- lexbuf.lex_start_p
+
+ let syntax_error lexbuf =
+ raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
}
let space = [' ' '\t' '\n' '\r']
@@ -42,31 +56,71 @@ let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
let identchar =
['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
-let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+
-let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+
let caml_up_ident = uppercase identchar*
let caml_low_ident = lowercase identchar*
+
+let coq_firstchar =
+ (* This is only an approximation, refer to lib/util.ml for correct def *)
+ ['A'-'Z' 'a'-'z' '_'] |
+ (* superscript 1 *)
+ '\194' '\185' |
+ (* utf-8 latin 1 supplement *)
+ '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] |
+ (* utf-8 letters *)
+ '\206' (['\145'-'\161'] | ['\163'-'\187'])
+ '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+ | '\129' [ '\176'-'\187' ] (* superscripts *)
+ | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let coq_identchar = coq_firstchar | ['\'' '0'-'9']
+let coq_ident = coq_firstchar coq_identchar*
+let coq_field = '.' coq_ident
+
let dot = '.' ( space+ | eof)
rule coq_action = parse
| "Require" space+
- { module_names := []; opened_file lexbuf }
+ { require_file lexbuf }
| "Require" space+ "Export" space+
- { module_names := []; opened_file lexbuf}
+ { require_file lexbuf}
| "Require" space+ "Import" space+
- { module_names := []; opened_file lexbuf}
+ { require_file lexbuf}
| "Local"? "Declare" space+ "ML" space+ "Module" space+
{ mllist := []; modules lexbuf}
| "Load" space+
{ load_file lexbuf }
- | "\""
- { string lexbuf; coq_action lexbuf}
- | "(*" (* "*)" *)
+ | "Add" space+ "LoadPath" space+
+ { add_loadpath lexbuf }
+ | space+
+ { coq_action lexbuf }
+ | "(*"
{ comment_depth := 1; comment lexbuf; coq_action lexbuf }
| eof
{ raise Fin_fichier}
| _
- { coq_action lexbuf }
+ { skip_to_dot lexbuf; coq_action lexbuf }
+
+and add_loadpath = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; add_loadpath lexbuf }
+ | space+
+ { add_loadpath lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | '"' [^ '"']* '"' (*'"'*)
+ { loadpath := unquote_string (lexeme lexbuf);
+ add_loadpath_as lexbuf }
+
+and add_loadpath_as = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; add_loadpath_as lexbuf }
+ | space+
+ { add_loadpath_as lexbuf }
+ | "as"
+ { let qid = coq_qual_id lexbuf in
+ skip_to_dot lexbuf;
+ AddRecLoadPath (!loadpath,qid) }
+ | dot
+ { AddLoadPath !loadpath }
and caml_action = parse
| space +
@@ -133,7 +187,8 @@ and comment = parse
{ comment lexbuf }
| eof
{ raise Fin_fichier }
- | _ { comment lexbuf }
+ | _
+ { comment lexbuf }
and string = parse
| '"' (* '"' *)
@@ -152,69 +207,108 @@ and string = parse
and load_file = parse
| '"' [^ '"']* '"' (*'"'*)
{ let s = lexeme lexbuf in
- let f = String.sub s 1 (String.length s - 2) in
- skip_to_dot lexbuf;
- Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
+ parse_dot lexbuf;
+ Load (unquote_vfile_string s) }
| coq_ident
{ let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
| eof
- { raise Fin_fichier }
+ { syntax_error lexbuf }
| _
- { load_file lexbuf }
+ { syntax_error lexbuf }
+
+and require_file = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; require_file lexbuf }
+ | space+
+ { require_file lexbuf }
+ | coq_ident
+ { module_current_name := [Lexing.lexeme lexbuf];
+ module_names := [coq_qual_id_tail lexbuf];
+ let qid = coq_qual_id_list lexbuf in
+ parse_dot lexbuf;
+ Require qid }
+ | '"' [^'"']* '"' (*'"'*)
+ { let s = Lexing.lexeme lexbuf in
+ parse_dot lexbuf;
+ RequireString (unquote_vfile_string s) }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { syntax_error lexbuf }
and skip_to_dot = parse
| dot { () }
- | eof { () }
+ | eof { syntax_error lexbuf }
| _ { skip_to_dot lexbuf }
-and opened_file = parse
- | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file lexbuf }
+and parse_dot = parse
+ | dot { () }
+ | eof { syntax_error lexbuf }
+ | _ { syntax_error lexbuf }
+
+and coq_qual_id = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id lexbuf }
| space+
- { opened_file lexbuf }
+ { coq_qual_id lexbuf }
| coq_ident
- { module_current_name := [Lexing.lexeme lexbuf];
- opened_file_fields lexbuf }
-
- | '"' [^'"']* '"' { (*'"'*)
- let lex = Lexing.lexeme lexbuf in
- let str = String.sub lex 1 (String.length lex - 2) in
- let str =
- if Filename.check_suffix str ".v" then
- Filename.chop_suffix str ".v"
- else str in
- RequireString str }
- | eof { raise Fin_fichier }
- | _ { opened_file lexbuf }
-
-and opened_file_fields = parse
- | "(*" (* "*)" *)
- { comment_depth := 1; comment lexbuf;
- opened_file_fields lexbuf }
+ { module_current_name := [Lexing.lexeme lexbuf];
+ coq_qual_id_tail lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ let qid = List.rev !module_current_name in
+ module_current_name := [];
+ qid }
+
+and coq_qual_id_tail = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id_tail lexbuf }
| space+
- { opened_file_fields lexbuf }
+ { coq_qual_id_tail lexbuf }
| coq_field
- { module_current_name :=
- field_name (Lexing.lexeme lexbuf) :: !module_current_name;
- opened_file_fields lexbuf }
- | coq_ident { module_names :=
- List.rev !module_current_name :: !module_names;
- module_current_name := [Lexing.lexeme lexbuf];
- opened_file_fields lexbuf }
- | dot { module_names :=
- List.rev !module_current_name :: !module_names;
- Require (List.rev !module_names) }
- | eof { raise Fin_fichier }
- | _ { opened_file_fields lexbuf }
+ { module_current_name :=
+ field_name (Lexing.lexeme lexbuf) :: !module_current_name;
+ coq_qual_id_tail lexbuf }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ let qid = List.rev !module_current_name in
+ module_current_name := [];
+ qid }
+
+and coq_qual_id_list = parse
+ | "(*"
+ { comment_depth := 1; comment lexbuf; coq_qual_id_list lexbuf }
+ | space+
+ { coq_qual_id_list lexbuf }
+ | coq_ident
+ { module_current_name := [Lexing.lexeme lexbuf];
+ module_names := coq_qual_id_tail lexbuf :: !module_names;
+ coq_qual_id_list lexbuf
+ }
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { backtrack lexbuf;
+ List.rev !module_names }
and modules = parse
- | space+ { modules lexbuf }
- | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf;
- modules lexbuf }
+ | space+
+ { modules lexbuf }
+ | "(*"
+ { comment_depth := 1; comment lexbuf;
+ modules lexbuf }
| '"' [^'"']* '"'
- { let lex = (Lexing.lexeme lexbuf) in
- let str = String.sub lex 1 (String.length lex - 2) in
- mllist := str :: !mllist; modules lexbuf}
- | _ { (Declare (List.rev !mllist)) }
+ { let lex = (Lexing.lexeme lexbuf) in
+ let str = String.sub lex 1 (String.length lex - 2) in
+ mllist := str :: !mllist; modules lexbuf}
+ | eof
+ { syntax_error lexbuf }
+ | _
+ { (Declare (List.rev !mllist)) }
and qual_id = parse
| '.' [^ '.' '(' '['] {
@@ -223,10 +317,12 @@ and qual_id = parse
| _ { caml_action lexbuf }
and mllib_list = parse
- | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
+ | "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
| eof { [] }
+ | _ { syntax_error lexbuf }
-
-
+and ocamldep_parse = parse
+ | [^ ':' ]* ':' { mllib_list lexbuf }
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 83bfa5ed..8802c0ef 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: alpha.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Cdglobals
let norm_char_latin1 c = match Char.uppercase c with
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index ec5b084f..792b71fc 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: alpha.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* Alphabetic order. *)
val compare_char : char -> char -> int
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5cb670dc..f37db46b 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -49,21 +49,40 @@ type glob_source_t =
let glob_source = ref DotGlob
+(*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
+
(** A weaker analog of the function in Envars *)
let guess_coqlib () =
let file = "states/initial.coq" in
- if Sys.file_exists (Filename.concat Coq_config.coqlib file)
- then Coq_config.coqlib
- else
- let coqbin = 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
- Coq_config.coqlib
+ match Coq_config.coqlib with
+ | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
+ 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..adc49ed4 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cpretty.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Index
val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a2bcb987..d7b54fd0 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
-
(*s Utility functions for the scanners *)
{
@@ -80,8 +77,17 @@
let in_proof = ref None
let in_emph = ref false
- let start_emph () = in_emph := true; Output.start_emph ()
- let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+ let in_env start stop =
+ let r = ref false in
+ let start_env () = r := true; start () in
+ let stop_env () = if !r then stop (); r := false in
+ (fun x -> !r), start_env, stop_env
+
+ let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+ let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
+
+ let url_buffer = Buffer.create 40
+ let url_name_buffer = Buffer.create 40
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
lexbuf.lex_curr_p <- lexbuf.lex_start_p
@@ -257,7 +263,7 @@
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
let s = String.sub s isp (String.length s - isp) in
- Output.ident s (lexeme_start lexbuf + isp)
+ Output.keyword s (lexeme_start lexbuf + isp)
}
@@ -323,6 +329,7 @@ let def_token =
| "SubClass"
| "Example"
| "Fixpoint"
+ | "Function"
| "Boxed"
| "CoFixpoint"
| "Record"
@@ -371,13 +378,17 @@ let commands =
| "Drop"
| "ProtectedLoop"
| "Quit"
+ | "Restart"
| "Load"
| "Add"
| "Remove" space+ "Loadpath"
| "Print"
| "Inspect"
| "About"
+ | "SearchAbout"
+ | "SearchRewrite"
| "Search"
+ | "Locate"
| "Eval"
| "Reset"
| "Check"
@@ -405,6 +416,14 @@ let prog_kw =
| "Obligations"
| "Solve"
+let hint_kw =
+ "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+ "Printing" space+ ("Coercions" | "Universes" | "All")
+ | "Implicit" space+ "Arguments"
+
+
let gallina_kw_to_hide =
"Implicit" space+ "Arguments"
| "Ltac"
@@ -412,15 +431,16 @@ let gallina_kw_to_hide =
| "Import"
| "Export"
| "Load"
- | "Hint"
+ | "Hint" space+ hint_kw
| "Open"
| "Close"
| "Delimit"
| "Transparent"
| "Opaque"
| ("Declare" space+ ("Morphism" | "Step") )
- | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+ | ("Set" | "Unset") space+ set_kw
| "Declare" space+ ("Left" | "Right") space+ "Step"
+ | "Debug" space+ ("On" | "Off")
let section = "*" | "**" | "***" | "****"
@@ -512,7 +532,7 @@ rule coq_bol = parse
output_indented_keyword s lexbuf;
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space* notation_kw space*
+ | space* notation_kw
{ let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= start_notation_string lexbuf in
@@ -639,7 +659,7 @@ and coq = parse
Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | notation_kw space*
+ | notation_kw
{ let s = lexeme lexbuf in
Output.ident s (lexeme_start lexbuf);
let eol= start_notation_string lexbuf in
@@ -663,8 +683,6 @@ and coq = parse
(*s Scanning documentation, at beginning of line *)
and doc_bol = parse
- | space* nl+
- { Output.paragraph (); doc_bol lexbuf }
| space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
{ let eol, lex = strip_eol (lexeme lexbuf) in
let lev, s = sec_title lex in
@@ -674,33 +692,26 @@ and doc_bol = parse
else
Output.section lev (fun () -> 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 }
+ { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
| eof
{ true }
| '_'
@@ -724,8 +735,8 @@ and doc_list_bol indents = parse
backtrack lexbuf; doc_bol lexbuf
}
| "<<" space*
- { Output.start_verbatim ();
- verbatim lexbuf;
+ { Output.start_verbatim false;
+ verbatim false lexbuf;
doc_list_bol indents lexbuf }
| "[[" nl
{ formatted := true;
@@ -734,6 +745,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 *)
@@ -769,9 +782,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* _
@@ -780,7 +800,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,_) ->
@@ -808,8 +831,11 @@ 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 }
+ | "{{" { url lexbuf; doc indents lexbuf }
| "["
{ if !Cdglobals.plain_comments then Output.char '['
else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf;
@@ -823,6 +849,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 }
| '*'* "*)"
@@ -857,6 +895,15 @@ and doc indents = parse
{ if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
+ | "<<" space*
+ { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+ | '"'
+ { if !Cdglobals.plain_comments
+ then Output.char '"'
+ else if in_quote ()
+ then stop_quote ()
+ else start_quote ();
+ doc indents lexbuf }
| eof
{ false }
| _
@@ -883,11 +930,22 @@ and escaped_html = parse
| eof { () }
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-and verbatim = parse
- | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
- | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
- | eof { Output.stop_verbatim () }
- | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+and verbatim inline = parse
+ | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+ | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+ | ">>" { Output.stop_verbatim inline }
+ | eof { Output.stop_verbatim inline }
+ | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+
+and url = parse
+ | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
+ | "}" { url_name lexbuf }
+ | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
+
+and url_name = parse
+ | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
+ Buffer.clear url_buffer; Buffer.clear url_name_buffer }
+ | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
(*s Coq, inside quotations *)
@@ -911,10 +969,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 }
@@ -1081,7 +1145,7 @@ and body = parse
if eol
then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
else body lexbuf }
- | "where" space*
+ | "where"
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
start_notation_string lexbuf }
@@ -1105,6 +1169,8 @@ and body = parse
body lexbuf }
and start_notation_string = parse
+ | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+ start_notation_string lexbuf }
| '"' (* a true notation *)
{ Output.sublexer '"' (lexeme_start lexbuf);
notation_string lexbuf;
@@ -1141,6 +1207,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..14447b06 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Filename
open Lexing
open Printf
@@ -38,17 +35,18 @@ type entry_type =
type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
- | Mod of coq_module * string
let current_type : entry_type ref = ref Library
let current_library = ref ""
(** refers to the file being parsed *)
-(** [deftable] stores only definitions and is used to interpolate idents
- inside comments, which are not globalized otherwise. *)
-
+(** [deftable] stores only definitions and is used to build the index *)
let deftable = Hashtbl.create 97
+(** [byidtable] is used to interpolate idents inside comments, which are not
+ globalized otherwise. *)
+let byidtable = Hashtbl.create 97
+
(** [reftable] stores references and definitions *)
let reftable = Hashtbl.create 97
@@ -62,25 +60,25 @@ let full_ident sp id =
else ""
let add_def loc1 loc2 ty sp id =
+ let fullid = full_ident sp id in
+ let def = Def (fullid, ty) in
for loc = loc1 to loc2 do
- Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+ Hashtbl.add reftable (!current_library, loc) def
done;
- Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+ Hashtbl.add deftable !current_library (fullid, ty);
+ Hashtbl.add byidtable id (!current_library, fullid, ty)
let add_ref m loc m' sp id ty =
+ let fullid = full_ident sp id in
if Hashtbl.mem reftable (m, loc) then ()
- else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+ else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty));
let idx = if id = "<>" then m' else id in
- if Hashtbl.mem deftable idx then ()
- else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
- Hashtbl.add reftable (m, loc) (Mod (m', id));
- Hashtbl.add deftable m (Mod (m', id))
+ if Hashtbl.mem byidtable idx then ()
+ else Hashtbl.add byidtable idx (m', fullid, ty)
let find m l = Hashtbl.find reftable (m, l)
-let find_string m s = Hashtbl.find deftable s
+let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
(*s Manipulating path prefixes *)
@@ -238,18 +236,20 @@ let type_name = function
let prepare_entry s = function
| Notation ->
(* 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 +268,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;
@@ -290,11 +290,8 @@ let all_entries () =
let l = try Hashtbl.find bt t with Not_found -> [] in
Hashtbl.replace bt t ((s,m) :: l)
in
- let classify (m,_) e = match e with
- | Def (s,t) -> add_g s m t; add_bt t s m
- | Ref _ | Mod _ -> ()
- in
- Hashtbl.iter classify reftable;
+ let classify m (s,t) = (add_g s m t; add_bt t s m) in
+ Hashtbl.iter classify deftable;
Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
{ idx_name = "global";
idx_entries = sort_entries !gl;
@@ -324,8 +321,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
@@ -341,7 +357,16 @@ let read_glob f =
Scanf.sscanf s "R%d:%d %s %s %s %s"
(fun loc1 loc2 lib_dp sp id ty ->
for loc=loc1 to loc2 do
- add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
+ add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
+
+ (* Also add an entry for each module mentioned in [lib_dp],
+ * to use in interpolation. *)
+ ignore (List.fold_right (fun thisPiece priorPieces ->
+ let newPieces = match priorPieces with
+ | "" -> thisPiece
+ | _ -> thisPiece ^ "." ^ priorPieces in
+ add_ref !cur_mod loc "" "" newPieces Library;
+ newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
done)
with _ -> ())
| _ ->
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index a009e9dc..0f62a086 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Cdglobals
type loc = int
@@ -36,10 +34,11 @@ val type_name : entry_type -> string
type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
- | Mod of coq_module * string
+(* Find what symbol coqtop said is located at loc in the source file *)
val find : coq_module -> loc -> index_entry
+(* Find what data is referred to by some string in some coq module *)
val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit
@@ -54,7 +53,7 @@ val add_external_library : string -> 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..b33ec1f0 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> 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 <string> insert <string> in LaTeX preamble";
prerr_endline " --files-from <file> read file names to process in <file>";
prerr_endline " --glob-from <file> read globalization information from <file>";
+ 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 <string> call top level toc entries <string> 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..0dc86bc8 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Cdglobals
open Index
@@ -32,24 +29,27 @@ let build_table l =
let is_keyword =
build_table
- [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+ [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
"CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
- "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+ "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+ "Guarded"; "Goal"; "Hint"; "Debug"; "On";
"Hypothesis"; "Hypotheses";
- "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+ "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+ "Implicit"; "Import"; "Inductive";
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
- "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
- "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+ "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
+ "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
"Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+ "Search"; "SearchAbout"; "SearchRewrite";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
- "Delimit"; "Bind"; "Open"; "Scope";
- "Boxed"; "Unboxed"; "Inline";
+ "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
"Implicit Arguments"; "Add"; "Strict";
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
- "subgoal";
- "Opaque"; "Transparent";
+ "subgoal"; "subgoals"; "vm_compute";
+ "Opaque"; "Transparent"; "Time";
+ "Extraction"; "Extract";
(* Program *)
"Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -57,14 +57,20 @@ let is_keyword =
(*i (* coq terms *) *)
"forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+ "fix"; "cofix";
(* Ltac *)
- "before"; "after"
+ "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+ (* Notations *)
+ "level"; "associativity"; "no"
]
let is_tactic =
build_table
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
- "elimtype"; "progress"; "setoid_rewrite";
+ "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor";
+ "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+ "quote"; "eexact"; "autorewrite";
"destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
"f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
"set"; "assert"; "do"; "repeat";
@@ -73,8 +79,10 @@ let is_tactic =
"reflexivity"; "symmetry"; "transitivity";
"replace"; "setoid_replace"; "inversion"; "inversion_clear";
"pattern"; "intuition"; "congruence"; "fail"; "fresh";
- "trivial"; "exact"; "tauto"; "firstorder"; "ring";
- "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+ "trivial"; "tauto"; "firstorder"; "ring";
+ "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+ "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+ "eval"; "instantiate"; "until" ]
(*s Current Coq module *)
@@ -118,9 +126,12 @@ let initialize_texmacs () =
let token_tree_texmacs = ref (initialize_texmacs ())
+let token_tree_latex = ref Tokens.empty_ttree
+let token_tree_html = ref Tokens.empty_ttree
+
let initialize_tex_html () =
let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
- List.fold_right (fun (s,l,l') (tt,tt') ->
+ let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') ->
(Tokens.ttree_add tt s l,
match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
[ "*" , "\\ensuremath{\\times}", if_utf8 "×";
@@ -143,10 +154,9 @@ let initialize_tex_html () =
"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
(* "fun", "\\ensuremath{\\lambda}" ? *)
- ] (Tokens.empty_ttree,Tokens.empty_ttree)
-
-let token_tree_latex = ref (fst (initialize_tex_html ()))
-let token_tree_html = ref (snd (initialize_tex_html ()))
+ ] (Tokens.empty_ttree,Tokens.empty_ttree) in
+ token_tree_latex := tree_latex;
+ token_tree_html := tree_html
let add_printing_token s (t1,t2) =
(match t1 with None -> () | Some t1 ->
@@ -182,10 +192,20 @@ module Latex = struct
let push_in_preamble s = Queue.add s preamble
+ let utf8x_extra_support () =
+ printf "\n";
+ printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
+ printf "%%interpret utf8 characters but extra packages might have to be added\n";
+ printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
+ printf "%%Use coqdoc's option -p to add new packages.\n";
+ printf "\\usepackage{tipa}\n";
+ printf "\n"
+
let header () =
if !header_trailer then begin
printf "\\documentclass[12pt]{report}\n";
if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
+ if !inputenc = "utf8x" then utf8x_extra_support ();
printf "\\usepackage[T1]{fontenc}\n";
printf "\\usepackage{fullpage}\n";
printf "\\usepackage{coqdoc}\n";
@@ -255,6 +275,12 @@ module Latex = struct
| '^' | '~' as c ->
Buffer.add_char buff '\\'; Buffer.add_char buff c;
Buffer.add_string buff "{}"
+ | '\'' ->
+ if i < String.length s - 1 && s.[i+1] = '\'' then begin
+ Buffer.add_char buff '\''; Buffer.add_char buff '{';
+ Buffer.add_char buff '}'
+ end else
+ Buffer.add_char buff '\''
| c ->
Buffer.add_char buff c
done;
@@ -276,9 +302,23 @@ module Latex = struct
let stop_latex_math () = output_char '$'
- let start_verbatim () = printf "\\begin{verbatim}"
+ let start_quote () = output_char '`'; output_char '`'
+ let stop_quote () = output_char '\''; output_char '\''
+
+ let start_verbatim inline =
+ if inline then printf "\\texttt{"
+ else printf "\\begin{verbatim}"
- let stop_verbatim () = printf "\\end{verbatim}\n"
+ let stop_verbatim inline =
+ if inline then printf "}"
+ else printf "\\end{verbatim}\n"
+
+ let url addr name =
+ printf "%s\\footnote{\\url{%s}}"
+ (match name with
+ | None -> ""
+ | Some n -> n)
+ addr
let indentation n =
if n == 0 then
@@ -287,9 +327,6 @@ module Latex = struct
let space = 0.5 *. (float n) in
printf "\\coqdocindent{%2.2fem}\n" space
- let module_ref m s =
- printf "\\coqdocmodule{%s}{%s}" m (escaped s)
-
let ident_ref m fid typ s =
let id = if fid <> "" then (m ^ "." ^ fid) else m in
match find_module m with
@@ -306,18 +343,20 @@ module Latex = struct
printf "\\coqdoc%s{%s}" (type_name typ) s
let defref m id ty s =
- printf "\\coqdef{"; label_ident (m ^ "." ^ id);
- printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s
+ if ty <> 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) ->
defref (get_module false) fullid typ s
- | Mod (m,s') when s = s' ->
- module_ref m s
| Ref (m,fullid,typ) ->
ident_ref m fullid typ s
- | Mod _ ->
- printf "\\coqdocvar{%s}" (escaped s)
(*s The sublexer buffers symbol characters and attached
uninterpreted ident and try to apply special translation such as,
@@ -330,13 +369,22 @@ module Latex = struct
| Some ref -> reference s ref
| None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
+ let last_was_in = ref false
+
let sublexer c loc =
- let tag =
- try Some (Index.find (get_module false) loc) with Not_found -> None
- in
- Tokens.output_tagged_symbol_char tag c
+ if c = '*' && !last_was_in then begin
+ Tokens.flush_sublexer ();
+ output_char '*'
+ end else begin
+ let tag =
+ try Some (Index.find (get_module false) loc) with Not_found -> None
+ in
+ Tokens.output_tagged_symbol_char tag c
+ end;
+ last_was_in := false
let initialize () =
+ initialize_tex_html ();
Tokens.token_tree := token_tree_latex;
Tokens.outfun := output_sublexer_string
@@ -345,7 +393,11 @@ module Latex = struct
let translate s =
match Tokens.translate s with Some s -> s | None -> escaped s
+ let keyword s loc =
+ printf "\\coqdockw{%s}" (translate s)
+
let ident s loc =
+ last_was_in := s = "in";
try
let tag = Index.find (get_module false) loc in
reference (translate s) tag
@@ -478,8 +530,7 @@ module Html = struct
end
let trailer () =
- if !header_trailer then
- if !footer_file_spec then
+ if !header_trailer && !footer_file_spec then
let cin = Pervasives.open_in !footer_file in
try
while true do
@@ -487,14 +538,14 @@ module Html = struct
printf "%s\n" s
done
with End_of_file -> Pervasives.close_in cin
- else
- begin
- if !index && (get_module false) <> "Index" then
- printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
- printf "<hr/>This page has been generated by ";
- printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
- printf "</div>\n\n</div>\n\n</body>\n</html>"
- end
+ else
+ begin
+ if !index && (get_module false) <> "Index" then
+ printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+ printf "<hr/>This page has been generated by ";
+ printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+ printf "</div>\n\n</div>\n\n</body>\n</html>"
+ end
let start_module () =
let ln = !lib_name in
@@ -547,17 +598,22 @@ module Html = struct
let start_latex_math () = ()
let stop_latex_math () = ()
- let start_verbatim () = printf "<pre>"
- let stop_verbatim () = printf "</pre>\n"
+ let start_quote () = char '"'
+ let stop_quote () = start_quote ()
- let module_ref m s =
- match find_module m with
- | Local ->
- printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
- | External m when !externals ->
- printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s
- | External _ | Unknown ->
- output_string s
+ let start_verbatim inline =
+ if inline then printf "<tt>"
+ else printf "<pre>"
+
+ let stop_verbatim inline =
+ if inline then printf "</tt>"
+ else printf "</pre>\n"
+
+ let url addr name =
+ printf "<a href=\"%s\">%s</a>" addr
+ (match name with
+ | Some n -> n
+ | None -> addr)
let ident_ref m fid typ s =
match find_module m with
@@ -575,12 +631,8 @@ module Html = struct
| Def (fullid,ty) ->
printf "<a name=\"%s\">" fullid;
printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
- | Mod (m,s') when s = s' ->
- module_ref m s
| Ref (m,fullid,ty) ->
ident_ref m fullid (type_name ty) s
- | Mod _ ->
- printf "<span class=\"id\" type=\"mod\">%s</span>" s
let output_sublexer_string doescape issymbchar tag s =
let s = if doescape then escaped s else s in
@@ -597,12 +649,16 @@ module Html = struct
Tokens.output_tagged_symbol_char tag c
let initialize () =
+ initialize_tex_html();
Tokens.token_tree := token_tree_html;
Tokens.outfun := output_sublexer_string
let translate s =
match Tokens.translate s with Some s -> s | None -> escaped s
+ let keyword s loc =
+ printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+
let ident s loc =
if is_keyword s then begin
printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -624,7 +680,7 @@ module Html = struct
let rec reach_item_level n =
if !item_level < n then begin
- printf "<ul>\n<li>"; incr item_level;
+ printf "<ul class=\"doclist\">\n<li>"; incr item_level;
reach_item_level n
end else if !item_level > n then begin
printf "\n</li>\n</ul>\n"; decr item_level;
@@ -662,7 +718,9 @@ module Html = struct
let end_code () = end_coq (); start_doc ()
- let start_inline_coq () = printf "<span class=\"inlinecode\">"
+ let start_inline_coq () =
+ if !inline_notmono then printf "<span class=\"inlinecodenm\">"
+ else printf "<span class=\"inlinecode\">"
let end_inline_coq () = printf "</span>"
@@ -670,7 +728,50 @@ module Html = struct
let end_inline_coq_block () = end_inline_coq ()
- let paragraph () = printf "\n<br/> <br/>\n"
+ let paragraph () = printf "\n<div class=\"paragraph\"> </div>\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 "&nbsp;"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 "&nbsp;" (String.length s))
+ results
+ in
+ String.concat "" (List.concat strs)
+ in
+ let start_assumption line =
+ (printf "<tr class=\"infruleassumption\">\n";
+ printf " <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in
+ let end_assumption () =
+ (printf " <td></td>\n";
+ printf "</td>\n") in
+ let rec print_assumptions hyps =
+ match hyps with
+ | [] -> start_assumption "&nbsp;&nbsp;"
+ | [(_,hyp)] -> start_assumption hyp
+ | ((_,hyp) :: hyps') -> (start_assumption hyp;
+ end_assumption ();
+ print_assumptions hyps') in
+ printf "<center><table class=\"infrule\">\n";
+ print_assumptions assumptions;
+ printf " <td class=\"infrulenamecol\" rowspan=\"3\">\n";
+ (match midnm with
+ | None -> printf " &nbsp;\n </td>"
+ | Some s -> printf " %s &nbsp;\n </td>" s);
+ printf "</tr>\n";
+ printf "<tr class=\"infrulemiddle\">\n";
+ printf " <td class=\"infrule\"><hr /></td>\n";
+ printf "</tr>\n";
+ print_assumptions conclusions;
+ end_assumption ();
+ printf "</table></center>"
let section lev f =
let lab = new_label () in
@@ -858,19 +959,28 @@ module TeXmacs = struct
let stop_latex_math () = output_char '>'
- let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+ let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+ let stop_verbatim inline = in_doc := false; printf "</verbatim>"
+
+ let url addr name =
+ printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+ (match name with
+ | None -> ""
+ | Some n -> n)
- let stop_verbatim () = in_doc := false; printf "</verbatim>"
+ let start_quote () = output_char '`'; output_char '`'
+ let stop_quote () = output_char '\''; output_char '\''
let indentation n = ()
+ let keyword s =
+ printf "<kw|"; raw_ident s; printf ">"
+
let ident_true s =
- if is_keyword s then begin
- printf "<kw|"; raw_ident s; printf ">"
- end else begin
- raw_ident s
- end
+ if is_keyword s then keyword s
+ else raw_ident s
+ let keyword s loc = keyword s
let ident s _ = if !in_doc then ident_true s else raw_ident s
let output_sublexer_string doescape issymbchar tag s =
@@ -985,13 +1095,21 @@ module Raw = struct
let start_latex_math () = ()
let stop_latex_math () = ()
- let start_verbatim () = ()
+ let start_verbatim inline = ()
+ let stop_verbatim inline = ()
- let stop_verbatim () = ()
+ let url addr name =
+ match name with
+ | Some n -> printf "%s (%s)" n addr
+ | None -> printf "%s" addr
+
+ let start_quote () = printf "\""
+ let stop_quote () = printf "\""
let indentation n =
for i = 1 to n do printf " " done
+ let keyword s loc = raw_ident s
let ident s loc = raw_ident s
let sublexer c l = char c
@@ -1105,6 +1223,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
let char = select Latex.char Html.char TeXmacs.char Raw.char
+let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
@@ -1132,10 +1251,33 @@ let start_verbatim =
select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
let stop_verbatim =
select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
- select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+ select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
let hard_verbatim_char = output_char
+let url =
+ select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+ select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+ select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
+ start_verbatim false;
+ 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 false
+
+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..80f39011 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Cdglobals
open Index
@@ -62,6 +60,7 @@ val rule : unit -> unit
val nbsp : unit -> unit
val char : char -> unit
+val keyword : string -> loc -> unit
val ident : string -> loc -> unit
val sublexer : char -> loc -> unit
val initialize : unit -> unit
@@ -72,13 +71,34 @@ val latex_char : char -> unit
val latex_string : string -> unit
val html_char : char -> unit
val html_string : string -> unit
-val verbatim_char : char -> unit
+val verbatim_char : bool -> char -> unit
val hard_verbatim_char : char -> unit
val start_latex_math : unit -> unit
val stop_latex_math : unit -> unit
-val start_verbatim : unit -> unit
-val stop_verbatim : unit -> unit
+val start_verbatim : bool -> unit
+val stop_verbatim : bool -> unit
+val start_quote : unit -> unit
+val stop_quote : unit -> unit
+
+val url : string -> string option -> 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
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 9de39083..10a105f9 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 3b756e18..e9c74307 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 380448be..a5376ec4 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,8 +9,6 @@
(* coqwc - counts the lines of spec, proof and comments in Coq sources
* Copyright (C) 2003 Jean-Christophe Filliâtre *)
-(*i $Id: coqwc.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
It assumes the files to be lexically well-formed. *)
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
new file mode 100644
index 00000000..50e8faad
--- /dev/null
+++ b/tools/escape_string.ml
@@ -0,0 +1 @@
+print_string (String.escaped Sys.argv.(1))
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
new file mode 100644
index 00000000..22a36ede
--- /dev/null
+++ b/tools/fake_ide.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)
+
+exception Comment
+
+let coqtop = ref (stdin, stdout)
+
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
+let eval_call (call:'a Ide_intf.call) =
+ prerr_endline (Ide_intf.pr_call call);
+ let xml_query = Ide_intf.of_call call in
+ Xml_utils.print_xml (snd !coqtop) xml_query;
+ flush (snd !coqtop);
+ let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
+ let res = Ide_intf.to_answer xml_answer call in
+ prerr_endline (Ide_intf.pr_full_value call res);
+ match res with Interface.Fail _ -> 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 [<coqtop>]\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..7b051d1c 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gallina.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Gallina_lexer
let vfiles = ref ([] : string list)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 638d5936..cfbfac98 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gallina_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
-
{
open Lexing
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 00000000..f01b62cc
--- /dev/null
+++ b/tools/mingwpath.ml
@@ -0,0 +1,15 @@
+(** Mingwpath *)
+
+(** Converts mingw-encoded filenames such as:
+
+ /c/Program Files/Ocaml/bin
+
+ to a more windows-friendly form (but still with / instead of \) :
+
+ c:/Program Files/Ocaml/bin
+
+ This nice hack was suggested by Benjamin Monate (cf bug #2526)
+ to mimic the cygwin-specific tool cygpath
+*)
+
+print_string Sys.argv.(1)
diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib
new file mode 100644
index 00000000..42395f65
--- /dev/null
+++ b/tools/win32hack.mllib
@@ -0,0 +1 @@
+Win32hack_filename \ No newline at end of file
diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml
new file mode 100644
index 00000000..74f70686
--- /dev/null
+++ b/tools/win32hack_filename.ml
@@ -0,0 +1,4 @@
+(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
+ Let's tweak that... *)
+
+let _ = Filename.dir_sep.[0] <- '\\'