+++ /dev/null
-(* environment *)
-
-let environment = Unix.environment ()
-
-let bindir = ref Coq_config.bindir
-let binary = "coqtop.byte"
-let image = ref ""
-let xml_theory_library_root = ref (
- try
- Sys.getenv "XML_THEORY_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_v2theoryxml 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_v2theoryxml" ".v" in
- let args' =
- command :: "-batch" :: "-silent" :: "-is" :: "barestate" :: 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 XmlTheory.\n" ;
- Printf.fprintf oc "XmlTheory Begin %s \"%s\".\n" modulename
- !xml_theory_library_root ;
- Printf.fprintf oc "Load %s.\n" modulename;
- Printf.fprintf oc "XmlTheory End.\n" ;
- 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_v2theoryxml <options> <Coq options> module...\n
-options are:
- -xml-theory-library-root d specify the path to the root of the XML library
- (overrides $XML_THEORY_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-theory-library-root" :: v :: rem ->
- xml_theory_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 ->
- parse (cfiles,args) rem
- | "-opt" :: rem ->
- raise (Failure "To load ML modules, only -byte is allowed")
- | "-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_v2theoryxml: too few arguments" ;
- usage ()
- end;
- let coqtopname =
- if !image <> "" then !image else Filename.concat !bindir (binary ^ Coq_config.exec_extension)
- in
- if !xml_theory_library_root = "" then
- begin
- prerr_endline "coq_v2theoryxml: you must either set $XML_THEORY_LIBRARY_ROOT or use -xml-theory-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
projects / helm.git / blobdiff