aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tools/coq_makefile.ml4113
-rw-r--r--tools/coqdep.ml80
-rwxr-xr-xtools/coqdep_lexer.mll2
-rw-r--r--tools/coqdoc/pretty.mll12
4 files changed, 101 insertions, 106 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index d641f8744..0599c4982 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -145,25 +145,9 @@ let implicit () =
print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
print "%.v.d: %.v\n";
print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-
- and ml_suffixes =
- if !some_mlfile then
- [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ]
- else
- []
- and v_suffixes =
- if !some_vfile then
- [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ]
- else
- []
in
- let suffixes = ml_suffixes @ v_suffixes in
- if suffixes <> [] then begin
- print ".SUFFIXES: "; print_list " " suffixes;
- print "\n\n"
- end;
- if !some_mlfile then ml_rules ();
- if !some_vfile then v_rule ()
+ if !some_mlfile then ml_rules ();
+ if !some_vfile then v_rule ()
let variables l =
let rec var_aux = function
@@ -171,10 +155,10 @@ let variables l =
| Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r
| _ :: r -> var_aux r
in
- section "Variables definitions.";
- print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
- print "CAMLP4:=$(notdir $(CAMLP4LIB))\n";
- print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+ section "Variables definitions.";
+ print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+ print "CAMLP4:=$(notdir $(CAMLP4LIB))\n";
+ print "COQSRC:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-I $(COQTOP)/library -I $(COQTOP)/parsing \\
-I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
-I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
@@ -185,28 +169,28 @@ let variables l =
-I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\
-I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
-I $(CAMLP4LIB)\n";
- print "ZFLAGS:=$(OCAMLLIBS) $(COQSRC)\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 "COQC:=$(COQBIN)coqc\n";
- print "COQDEP:=$(COQBIN)coqdep -c\n";
- print "GALLINA:=$(COQBIN)gallina\n";
- print "COQDOC:=$(COQBIN)coqdoc\n";
- (* Caml executables and relative variables *)
- printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
- printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -c\n";
- printf "CAMLLINK:=$(CAMLBIN)ocamlc\n";
- printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n";
- print "GRAMMARS:=grammar.cma\n";
- print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
- print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
- var_aux l;
- print "\n"
+ print "ZFLAGS:=$(OCAMLLIBS) $(COQSRC)\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 "COQC:=$(COQBIN)coqc\n";
+ print "COQDEP:=$(COQBIN)coqdep -c\n";
+ print "GALLINA:=$(COQBIN)gallina\n";
+ print "COQDOC:=$(COQBIN)coqdoc\n";
+ (* Caml executables and relative variables *)
+ printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
+ printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -c\n";
+ printf "CAMLLINK:=$(CAMLBIN)ocamlc\n";
+ printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt\n";
+ print "GRAMMARS:=grammar.cma\n";
+ print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+ print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+ var_aux l;
+ print "\n"
let absolute_dir dir =
let current = Sys.getcwd () in
@@ -239,9 +223,10 @@ let include_dirs l =
in
let l' = if List.exists (is_included ".") l then l else Include "." :: l in
let inc_i, inc_r = parse_includes l' in
+ let inc_i' = List.filter (fun d -> List.exists (fun d' -> is_prefix d' d) inc_r) inc_i in
section "Libraries definition.";
print "OCAMLLIBS:="; print_list "\\\n " inc_i; print "\n";
- print "COQLIBS:="; print_list "\\\n " inc_i; print " "; print_list "\\\n " inc_r; print "\n";
+ print "COQLIBS:="; print_list "\\\n " inc_i'; print " "; print_list "\\\n " inc_r; print "\n";
print "COQDOCLIBS:="; print_list "\\\n " inc_r; print "\n\n"
let rec special = function
@@ -281,9 +266,9 @@ let all_target l =
let rec parse_arguments l =
match l with
| ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o)
- | Subdir n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
+ | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
| V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
- | Special (n,_,_) :: r -> let v,m,o = (parse_arguments r) in (v,m,n::o)
+ | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
| Include _ :: r -> parse_arguments r
| RInclude _ :: r -> parse_arguments r
| Def _ :: r -> parse_arguments r
@@ -293,19 +278,27 @@ let all_target l =
vfiles, mlfiles, other_targets = parse_arguments l
in
section "Definition of the \"all\" target.";
- print "VFILES:="; print_list "\\\n " vfiles; print "\n";
- print "VOFILES:=$(VFILES:.v=.vo)\n";
- 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";
- print "MLFILES:="; print_list "\\\n " mlfiles; print "\n";
- print "CMOFILES:=$(MLFILES:.ml=.cmo)";
- print "\n";
- print "all: $(VOFILES) $(CMOFILES) "; print_list "\\\n " other_targets;
- print "\n\n";
- if !some_vfile then begin
+ if !some_vfile then
+ begin
+ print "VFILES:="; print_list "\\\n " vfiles; print "\n";
+ print "VOFILES:=$(VFILES:.v=.vo)\n";
+ 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";
+ end;
+ print "\nall: ";
+ if !some_vfile then print "$(VOFILES) ";
+ if !some_mlfile then print "$(CMOFILES) ";
+ 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";
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 097e19fe2..f188ebfa6 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -41,6 +41,11 @@ let file_concat l =
if l=[] then "<empty>" else
List.fold_left (//) (List.hd l) (List.tl l)
+let make_ml_module_name filename =
+ (* Computes a ML Module name from its physical name *)
+ let basename = Filename.chop_extension filename in
+ String.capitalize basename
+
(* Files specified on the command line *)
let mlAccu = ref ([] : (string * string * dir) list)
and mliAccu = ref ([] : (string * string * dir) list)
@@ -234,12 +239,13 @@ let traite_fichier_Coq verbose f =
| Declare sl ->
List.iter
(fun str ->
- if not (List.mem str !deja_vu_ml) then begin
- addQueue deja_vu_ml str;
- try
- let mldir = Hashtbl.find mlKnown str in
- printf " %s.cmo" (file_name ([String.uncapitalize str],mldir))
- with Not_found -> ()
+ let s = String.capitalize str in
+ if not (List.mem s !deja_vu_ml) then begin
+ addQueue deja_vu_ml s;
+ try
+ let mldir = Hashtbl.find mlKnown s in
+ printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+ with Not_found -> ()
end)
sl
| Load str ->
@@ -304,36 +310,37 @@ let traite_Declare f =
let decl_list = ref ([] : string list) in
let rec treat = function
| s :: ll ->
- if (Hashtbl.mem mlKnown s) & not (List.mem s !decl_list) then begin
- let mldir = Hashtbl.find mlKnown s in
- let fullname = file_name ([(String.uncapitalize s)],mldir) in
- let depl = mL_dep_list s (fullname ^ ".ml") in
- treat depl;
- decl_list := s :: !decl_list
- end;
- treat ll
+ let s' = String.capitalize s in
+ if (Hashtbl.mem mlKnown s') & not (List.mem s' !decl_list) then begin
+ let mldir = Hashtbl.find mlKnown s in
+ let fullname = file_name ([(String.uncapitalize s')],mldir) in
+ let depl = mL_dep_list s (fullname ^ ".ml") in
+ treat depl;
+ decl_list := s :: !decl_list
+ end;
+ treat ll
| [] -> ()
in
- try
- let chan = open_in f in
- let buf = Lexing.from_channel chan in
- begin try
- while true do
- let tok = coq_action buf in
- (match tok with
- | Declare sl ->
- decl_list := [];
- treat sl;
- decl_list := List.rev !decl_list;
- if !option_D then
- affiche_Declare f !decl_list
- else if !decl_list <> sl then
- warning_Declare f !decl_list
- | _ -> ())
- done
- with Fin_fichier -> () end;
- close_in chan
- with Sys_error _ -> ()
+ try
+ let chan = open_in f in
+ let buf = Lexing.from_channel chan in
+ begin try
+ while true do
+ let tok = coq_action buf in
+ (match tok with
+ | Declare sl ->
+ decl_list := [];
+ treat sl;
+ decl_list := List.rev !decl_list;
+ if !option_D then
+ affiche_Declare f !decl_list
+ else if !decl_list <> sl then
+ warning_Declare f !decl_list
+ | _ -> ())
+ done
+ with Fin_fichier -> () end;
+ close_in chan
+ with Sys_error _ -> ()
let file_mem (f,_,d) =
let rec loop = function
@@ -407,11 +414,6 @@ let usage () =
flush stderr;
exit 1
-let make_ml_module_name filename =
- (* Computes a ML Module name from its physical name *)
- let basename = Filename.chop_extension filename in
- String.capitalize basename
-
let add_coqlib_known phys_dir log_dir f =
if Filename.check_suffix f ".vo" then
let basename = Filename.chop_suffix f ".vo" in
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index ffb35c528..32ad4bdc5 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -215,7 +215,7 @@ and modules = parse
| '"' [^'"']* '"'
{ let lex = (Lexing.lexeme lexbuf) in
let str = String.sub lex 1 (String.length lex - 2) in
- mllist := str :: !mllist; modules lexbuf }
+ mllist := str :: !mllist; modules lexbuf}
| _ { (Declare (List.rev !mllist)) }
and qual_id = parse
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index db1caaeee..8774d9d2e 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -189,7 +189,7 @@ let symbolchar_no_brackets =
'\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
let symbolchar = symbolchar_no_brackets | '[' | ']'
let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
-
+let printing_token = (token | id)+
let thm_token =
"Theorem"
@@ -370,9 +370,9 @@ rule coq_bol = parse
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space* "(**" space+ "printing" space+ (identifier | token) space+
+ | space* "(**" space+ "printing" space+ printing_token space+
{ let tok = lexeme lexbuf in
- let s = printing_token lexbuf in
+ let s = printing_token_body lexbuf in
add_printing_token tok s;
coq_bol lexbuf }
| space* "(**" space+ "printing" space+
@@ -617,7 +617,7 @@ and body = parse
{ let s = lexeme lexbuf in
Output.ident s (lexeme_start lexbuf);
body lexbuf }
- | token
+ | printing_token
{ let s = lexeme lexbuf in
Output.symbol s; body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
@@ -645,13 +645,13 @@ and skip_hide = parse
(*s Reading token pretty-print *)
-and printing_token = parse
+and printing_token_body = parse
| "*)" | eof
{ let s = Buffer.contents token_buffer in
Buffer.clear token_buffer;
s }
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
- printing_token lexbuf }
+ printing_token_body lexbuf }
(*s Applying the scanners to files *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 04:27:08 +0000