--- /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