diff options
| -rw-r--r-- | Makefile | 27 | ||||
| -rw-r--r-- | man/coq_vo2xml.1 | 69 | ||||
| -rw-r--r-- | tools/coq_vo2xml.ml | 174 |
3 files changed, 3 insertions, 267 deletions
@@ -943,8 +943,7 @@ $(CONTRIBVO): states/initial.coq contrib: $(CONTRIBVO) $(CONTRIBCMO) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) ring: $(RINGVO) $(RINGCMO) -# xml_ instead of xml to avoid conflict with "make xml" -xml_: $(XMLVO) $(XMLCMO) +xml: $(XMLVO) $(XMLCMO) extraction: $(EXTRACTIONCMO) field: $(FIELDVO) $(FIELDCMO) fourier: $(FOURIERVO) $(FOURIERCMO) @@ -1050,10 +1049,8 @@ GALLINA=bin/gallina$(EXE) COQTEX=bin/coq-tex$(EXE) COQWC=bin/coqwc$(EXE) COQDOC=bin/coqdoc$(EXE) -COQVO2XML=bin/coq_vo2xml$(EXE) -RUNCOQVO2XML=coq_vo2xml$(EXE) # Uses the one in PATH and not the one in bin -TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) \ +TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \ $(COQWC) $(COQDOC) tools:: $(TOOLS) dev/top_printers.cmo @@ -1098,12 +1095,6 @@ $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO) -COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo - -$(COQVO2XML): $(COQVO2XMLCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQVO2XMLCMO) - clean:: rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml rm -f tools/coqwc.ml @@ -1130,18 +1121,6 @@ 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) $(THEORIESVO) $(CONTRIBVO) - $(RUNCOQVO2XML) -boot -byte $(COQINCLUDES) $(?:%.o=%) - touch .xml_time_stamp - -########################################################################### # Installation ########################################################################### @@ -1224,7 +1203,7 @@ install-coq-info: install-coq-manpages install-emacs install-latex MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 \ - man/coq_makefile.1 man/coqmktop.1 man/coq_vo2xml.1 + man/coq_makefile.1 man/coqmktop.1 install-coq-manpages: $(MKDIR) $(FULLMANDIR)/man1 diff --git a/man/coq_vo2xml.1 b/man/coq_vo2xml.1 deleted file mode 100644 index 21be67b77..000000000 --- a/man/coq_vo2xml.1 +++ /dev/null @@ -1,69 +0,0 @@ -.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_vo2xml.ml b/tools/coq_vo2xml.ml deleted file mode 100644 index 5f71fca39..000000000 --- a/tools/coq_vo2xml.ml +++ /dev/null @@ -1,174 +0,0 @@ -(* 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 %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 |