X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fxmltheory%2FCoq_v2theoryxml%2Fcoq_v2theoryxml.ml;fp=helm%2Fxmltheory%2FCoq_v2theoryxml%2Fcoq_v2theoryxml.ml;h=0000000000000000000000000000000000000000;hp=b1e856e1ae35ec23f8508e7f7cf84802756840fa;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml b/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml deleted file mode 100644 index b1e856e1a..000000000 --- a/helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml +++ /dev/null @@ -1,176 +0,0 @@ -(* 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 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