diff options
-rw-r--r-- | Makefile | 30 | ||||
-rw-r--r-- | bin/.cvsignore | 1 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 19 | ||||
-rw-r--r-- | man/coq_vo2xml.1 | 69 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 26 | ||||
-rw-r--r-- | tools/coq_vo2xml.ml | 175 | ||||
-rw-r--r-- | toplevel/usage.mli | 4 |
7 files changed, 302 insertions, 22 deletions
@@ -489,7 +489,8 @@ $(CONTRIBVO): states/initial.coq contrib: $(CONTRIBVO) omega: $(OMEGAVO) ring: $(RINGVO) -xml: $(XMLVO) +# xml_ instead of xml to avoid conflict with "make xml" +xml_: $(XMLVO) extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO) field: $(FIELDVO) @@ -509,8 +510,10 @@ COQDEP=bin/coqdep$(EXE) COQMAKEFILE=bin/coq_makefile$(EXE) GALLINA=bin/gallina$(EXE) COQTEX=bin/coq-tex$(EXE) +COQVO2XML=bin/coq_vo2xml$(EXE) +RUNCOQVO2XML=coq_vo2xml$(EXE) # Uses the one in PATH and not the one in bin -tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) dev/top_printers.cmo +tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) dev/top_printers.cmo COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo @@ -532,11 +535,16 @@ $(COQMAKEFILE): tools/coq_makefile.ml $(COQTEX): tools/coq-tex.ml $(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.ml +COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo + +$(COQVO2XML): $(COQVO2XMLCMO) + $(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQVO2XMLCMO) + clean:: rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml archclean:: - rm -f $(COQDEP) $(GALLINA) $(COQTEX) $(COQMAKEFILE) + rm -f $(COQDEP) $(GALLINA) $(COQTEX) $(COQMAKEFILE) $(COQVO2XML) ########################################################################### # minicoq @@ -555,6 +563,18 @@ archclean:: rm -f $(MINICOQ) ########################################################################### +# XML +########################################################################### + +# Warning: coq_vo2xml in PATH and not the one in bin is used + +.PHONY: xml +xml: .xml_time_stamp +.xml_time_stamp: $(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) + $(RUNCOQVO2XML) -boot -byte $(COQINCLUDES) $(?:%.o=%) + touch .xml_time_stamp + +########################################################################### # Installation ########################################################################### @@ -581,7 +601,7 @@ install-opt: install-binaries: $(MKDIR) $(FULLBINDIR) - cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(FULLBINDIR) + cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(COQINTERFACE) $(COQVO2XML) $(FULLBINDIR) LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) @@ -599,7 +619,7 @@ install-library: MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coq_makefile.1 man/coqmktop.1 \ - man/coq-interface.1 man/parser.1 + man/coq-interface.1 man/parser.1 man/coq_vo2xml.1 install-manpages: $(MKDIR) $(FULLMANDIR)/man1 diff --git a/bin/.cvsignore b/bin/.cvsignore index 51c25a5f3..39760ace8 100644 --- a/bin/.cvsignore +++ b/bin/.cvsignore @@ -10,3 +10,4 @@ coq-tex coq-extraction coq-interface parser +coq_vo2xml diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 573f4319b..5f23c1d64 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -305,15 +305,16 @@ let print_term inner_types l env csr = (* coq coding of terms (the one of the logical framework) *) match T.kind_of_term cstr with T.IsRel n -> - (match List.nth l (n - 1) with - N.Name id -> - X.xml_empty "REL" - (add_sort_attribute false - ["value",(string_of_int n) ; - "binder",(N.string_of_id id) ; - "id", next_id]) - | N.Anonymous -> assert false - ) + let id = + match List.nth l (n - 1) with + N.Name id -> id + | N.Anonymous -> N.make_ident "_" None + in + X.xml_empty "REL" + (add_sort_attribute false + ["value",(string_of_int n) ; + "binder",(N.string_of_id id) ; + "id", next_id]) | T.IsVar id -> let depth = match get_depth_of_var (N.string_of_id id) with diff --git a/man/coq_vo2xml.1 b/man/coq_vo2xml.1 new file mode 100644 index 000000000..21be67b77 --- /dev/null +++ b/man/coq_vo2xml.1 @@ -0,0 +1,69 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq_vo2xml \- Exports the content of a Coq module to XML + + +.SH SYNOPSIS +.B coq_vo2xml +[ +.B general \ Coq \ options +] +[ +.B -image +.I f +] +[ +.B -t +] +[ +.B -xml-library-root +.I d +] +.IR module " .\|.\|." + + +.SH DESCRIPTION + +.B coq_vo2xml +is a tool to export the content of a Coq module to XML. +Because it executes coqtop(1), it recognizes a superset of its options. +ones: +.PP +.B -image +.IR f +overrides the coqtop(1) executable with +.IR f "." +.PP +.B -t +does not remove the temporary file fed to coqtop(1). +.PP +.B -xml-library-root +.IR d +sets the path to the root of the XML library to +.IR d "," +overriding the value of $XML_ROOT_LIBRARY. The root of the XML library +must be specified, either using the flag or setting the variable. +.PP +.IR module \& +is the name of the module to export. The file module.vo will be searched in the +Coq path by coqtop(1). +The compiler produces a whole tree of XML files and directories rooted in the +specified XML root library. + +.SH OPTIONS + +.TP +.BI \-h +Will give you a description of the whole list of options of coq_vo2xml, +including the ones of coqtop(1). + +.SH SEE ALSO + +.BR coqtop (1), +.BR coq_makefile (1), +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ead690e50..ce220b54f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -93,6 +93,11 @@ let standard sds = (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n") sds; print "\n"; + print "xml::\n"; + List.iter + (fun x -> print "\t(cd "; print x; print " ; $(MAKE) xml)\n") + sds; + print "\n"; print "install:\n"; print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n"; if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n"; @@ -131,7 +136,7 @@ let implicit () = print ".v.tex:\n\t$(COQ2LATEX) $< -latex -o $@\n\n" ; print ".v.g.html:\n\t$(GALLINA) -stdout $< | $(COQ2HTML) -f > $@\n\n" ; print - ".v.g.tex:\n\t$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@\n\n" + ".v.g.tex:\n\t$(GALLINA) -stdout $< | $(COQ2LATEX) - -latex -o $@\n\n" ; and ml_suffixes = if !some_mlfile then [ ".mli" ; ".ml" ; ".cmo" ; ".cmi"; ".cmx" ] @@ -183,6 +188,7 @@ let variables l = print "CAMLLINK=ocamlc\n"; print "CAMLOPTLINK=ocamlopt\n"; print "COQDEP=$(COQBIN)coqdep -c\n"; + print "COQVO2XML=coq_vo2xml\n"; var_aux l; print "\n" @@ -234,7 +240,7 @@ let subdirs l = section "Special targets."; print ".PHONY: " ; print_list " " - ("all"::"opt"::"byte"::"archclean"::"clean"::"install"::"depend"::sds); + ("all"::"opt"::"byte"::"archclean"::"clean"::"install"::"depend"::"xml"::sds); print "\n\n"; sds @@ -242,17 +248,18 @@ let subdirs l = let rec other_files suff = function | V n :: r -> - let f = (Filename.chop_suffix n "vo") ^ suff in + let f = (Filename.chop_suffix n ".vo") ^ suff in f :: (other_files suff r) | _ :: r -> other_files suff r | [] -> [] -let gfiles = other_files "g" -let hfiles = other_files "html" -let tfiles = other_files "tex" -let vifiles = other_files "vi" +let gfiles = other_files ".g" +let hfiles = other_files ".html" +let tfiles = other_files ".tex" +let vifiles = other_files ".vi" let gtfiles l = List.map (fun f -> f^".tex") (gfiles l) let ghfiles l = List.map (fun f -> f^".html") (gfiles l) +let vofiles = other_files ".vo" let all_target l = let rec fnames = function @@ -281,6 +288,11 @@ let all_target l = print "\n\n"; print "gallinahtml: "; print_list "\\\n " (ghfiles l) ; print "\n\n"; + print "xml:: .xml_time_stamp\n" ; + print ".xml_time_stamp: "; print_list "\\\n " (vofiles l) ; + print "\n\t$(COQVO2XML) $(COQFLAGS) $(?:%.o=%)\n" ; + print "\ttouch .xml_time_stamp" ; + print "\n\n" end let parse f = diff --git a/tools/coq_vo2xml.ml b/tools/coq_vo2xml.ml new file mode 100644 index 000000000..9b47fed03 --- /dev/null +++ b/tools/coq_vo2xml.ml @@ -0,0 +1,175 @@ +(* environment *) + +let environment = Unix.environment () + +let bindir = ref Coq_config.bindir +let binary = ref ("coqtop." ^ Coq_config.best) +let image = ref "" +let xml_library_root = ref ( + try + Sys.getenv "XML_LIBRARY_ROOT" + with Not_found -> "" +) + +(* the $COQBIN environment variable has priority over the Coq_config value *) +let _ = + try + let c = Sys.getenv "COQBIN" in + if c <> "" then bindir := c + with Not_found -> () + +(* coq_vo2xml options *) + +let keep = ref false + +(* Verifies that a string do not contains others caracters than letters, + digits, or `_` *) + +let check_module_name s = + let err () = + output_string stderr + "Modules names must only contain letters, digits, or underscores\n"; + output_string stderr + "and must begin with a letter\n"; + exit 1 + in + match String.get s 0 with + | 'a' .. 'z' | 'A' .. 'Z' -> + for i = 1 to (String.length s)-1 do + match String.get s i with + | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' -> () + | _ -> err () + done + | _ -> err () + + (* compilation of a file [file] with command [command] and args [args] *) + +let compile command args file = + let dirname = Filename.dirname file in + let basename = Filename.basename file in + let modulename = + if Filename.check_suffix basename ".vo" then + Filename.chop_suffix basename ".vo" + else + basename + in + check_module_name modulename; + let tmpfile = Filename.temp_file "coq_vo2xml" ".v" in + let args' = + command :: "-batch" :: "-silent" :: args + @ ["-load-vernac-source"; tmpfile] in + let devnull = + if Sys.os_type = "Unix" then + Unix.openfile "/dev/null" [] 0o777 + else + Unix.stdin + in + let oc = open_out tmpfile in + Printf.fprintf oc "Require Xml.\n" ; + Printf.fprintf oc "Require %s.\n" modulename; + Printf.fprintf oc "Print XML Module Disk \"%s\" %s.\n" !xml_library_root + modulename; + flush oc; + close_out oc; + try + let pid = + Unix.create_process_env command + (Array.of_list args') environment devnull Unix.stdout Unix.stderr in + let status = Unix.waitpid [] pid in + if not !keep then Sys.remove tmpfile ; + match status with + | _, Unix.WEXITED 0 -> () + | _, Unix.WEXITED 127 -> + Printf.printf "Cannot execute %s\n" command; + exit 1 + | _, Unix.WEXITED c -> exit c + | _ -> exit 1 + with _ -> + if not !keep then Sys.remove tmpfile; exit 1 + +(* parsing of the command line + * + * special treatment for -bindir and -i. + * other options are passed to coqtop *) + +let usage () = + Usage.print_usage + "Usage: coq_vo2xml <options> <Coq options> module...\n +options are: + -xml-library-root d specify the path to the root of the XML library + (overrides $XML_LIBRARY_ROOT) + -image f specify an alternative executable for Coq + -t keep temporary files\n\n" ; + flush stderr ; + exit 1 + +let parse_args () = + let rec parse (cfiles,args) = function + | [] -> + List.rev cfiles, List.rev args + | "-xml-library-root" :: v :: rem -> + xml_library_root := v ; parse (cfiles,args) rem + | "-t" :: rem -> + keep := true ; parse (cfiles,args) rem + | "-boot" :: rem -> + bindir:= Filename.concat Coq_config.coqtop "bin"; + parse (cfiles, "-boot"::args) rem + | "-bindir" :: d :: rem -> + bindir := d ; parse (cfiles,args) rem + | "-bindir" :: [] -> + usage () + | "-byte" :: rem -> + binary := "coqtop.byte"; parse (cfiles,args) rem + | "-opt" :: rem -> + binary := "coqtop.opt"; parse (cfiles,args) rem + | "-image" :: f :: rem -> + image := f; parse (cfiles,args) rem + | "-image" :: [] -> + usage () + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + | ("-libdir"|"-outputstate"|"-I"|"-include" + |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object" + |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" + |"-init-file" as o) :: rem -> + begin + match rem with + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem + | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" + |"-silent"|"-m" as o) :: rem -> + parse (cfiles,o::args) rem + | ("-v"|"--version") :: _ -> + Usage.version () + | "-where" :: _ -> + print_endline Coq_config.coqlib; exit 0 + | f :: rem -> parse (f::cfiles,args) rem + in + parse ([],[]) (List.tl (Array.to_list Sys.argv)) + +(* main: we parse the command line, define the command to compile files + * and then call the compilation on each file *) + +let main () = + let cfiles, args = parse_args () in + if cfiles = [] then begin + prerr_endline "coq_vo2xml: too few arguments" ; + usage () + end; + let coqtopname = + if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension) + in + if !xml_library_root = "" then + begin + prerr_endline "coq_vo2xml: you must either set $XML_LIBRARY_ROOT or use -xml-library-root"; + usage () + end + else + List.iter (compile coqtopname args) cfiles ; + prerr_endline + ("\nWARNING: all the URIs in the generated XML files are broken." ^ + "\n See the README in the XML contrib to learn how to fix them.\n") + +let _ = Printexc.print main (); exit 0 diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 4322b0c9b..c24ae331a 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -12,7 +12,9 @@ val version : unit -> 'a -(*s Prints the usage on the error output. *) +(*s Prints the usage on the error output, preceeded by a user-provided message. *) +val print_usage : string -> unit +(*s Prints the usage on the error output. *) val print_usage_coqtop : unit -> unit val print_usage_coqc : unit -> unit |