helm/xmltheory/Coq_v2theoryxml/coq_v2theoryxml.ml

   1 (* environment *)
   2
   3 let environment = Unix.environment ()
   4
   5 let bindir = ref Coq_config.bindir
   6 let binary = "coqtop.byte"
   7 let image = ref ""
   8 let xml_theory_library_root = ref (
   9  try
  10   Sys.getenv "XML_THEORY_LIBRARY_ROOT"
  11  with Not_found -> ""
  12 )
  13
  14 (* the $COQBIN environment variable has priority over the Coq_config value *)
  15 let _ =
  16   try
  17     let c = Sys.getenv "COQBIN" in
  18     if c <> "" then bindir := c
  19   with Not_found -> ()
  20
  21 (* coq_v2theoryxml options *)
  22
  23 let keep = ref false
  24
  25 (* Verifies that a string do not contains others caracters than letters,
  26    digits, or `_` *)
  27
  28 let check_module_name s =
  29   let err () =
  30     output_string stderr
  31       "Modules names must only contain letters, digits, or underscores\n";
  32     output_string stderr
  33       "and must begin with a letter\n";
  34     exit 1
  35   in
  36   match String.get s 0 with
  37     | 'a' .. 'z' | 'A' .. 'Z' ->
  38         for i = 1 to (String.length s)-1 do
  39           match String.get s i with
  40             | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
  41             | _ -> err ()
  42         done
  43     | _ -> err ()
  44
  45  (* compilation of a file [file] with command [command] and args [args] *)
  46
  47 let compile command args file =
  48   let dirname = Filename.dirname file in
  49   let basename = Filename.basename file in
  50   let modulename =
  51     if Filename.check_suffix basename ".vo" then
  52       Filename.chop_suffix basename ".vo"
  53     else
  54       basename
  55   in
  56   check_module_name modulename;
  57   let tmpfile = Filename.temp_file "coq_v2theoryxml" ".v" in
  58   let args' =
  59     command :: "-batch" :: "-silent" :: "-is" :: "barestate" :: args
  60     @ ["-load-vernac-source"; tmpfile] in
  61   let devnull =
  62     if Sys.os_type = "Unix" then
  63       Unix.openfile "/dev/null" [] 0o777
  64     else
  65       Unix.stdin
  66   in
  67   let oc = open_out tmpfile in
  68   Printf.fprintf oc "Require XmlTheory.\n" ;
  69   Printf.fprintf oc "XmlTheory Begin %s \"%s\".\n" modulename
  70    !xml_theory_library_root ;
  71   Printf.fprintf oc "Load %s.\n" modulename;
  72   Printf.fprintf oc "XmlTheory End.\n" ;
  73   flush oc;
  74   close_out oc;
  75   try
  76     let pid =
  77       Unix.create_process_env command
  78         (Array.of_list args') environment devnull Unix.stdout Unix.stderr in
  79     let status = Unix.waitpid [] pid in
  80     if not !keep then Sys.remove tmpfile ;
  81     match status with
  82       | _, Unix.WEXITED 0 -> ()
  83       | _, Unix.WEXITED 127 ->
  84           Printf.printf "Cannot execute %s\n" command;
  85           exit 1
  86       | _, Unix.WEXITED c -> exit c
  87       | _                 -> exit 1
  88   with _ ->
  89     if not !keep then Sys.remove tmpfile; exit 1
  90
  91 (* parsing of the command line
  92  *
  93  * special treatment for -bindir and -i.
  94  * other options are passed to coqtop *)
  95
  96 let usage () =
  97   Usage.print_usage
  98    "Usage: coq_v2theoryxml <options> <Coq options> module...\n
  99 options are:
 100   -xml-theory-library-root d   specify the path to the root of the XML library
 101                                (overrides $XML_THEORY_LIBRARY_ROOT)
 102   -image f                     specify an alternative executable for Coq
 103   -t                           keep temporary files\n\n" ;
 104   flush stderr ;
 105   exit 1
 106
 107 let parse_args () =
 108   let rec parse (cfiles,args) = function
 109     | [] ->
 110         List.rev cfiles, List.rev args
 111     | "-xml-theory-library-root" :: v :: rem ->
 112         xml_theory_library_root := v ; parse (cfiles,args) rem
 113     | "-t" :: rem ->
 114         keep := true ; parse (cfiles,args) rem
 115     | "-boot" :: rem ->
 116         bindir:= Filename.concat Coq_config.coqtop "bin";
 117         parse (cfiles, "-boot"::args) rem
 118     | "-bindir" :: d :: rem ->
 119         bindir := d ; parse (cfiles,args) rem
 120     | "-bindir" :: []       ->
 121         usage ()
 122     | "-byte" :: rem ->
 123         parse (cfiles,args) rem
 124     | "-opt" :: rem ->
 125         raise (Failure "To load ML modules, only -byte is allowed")
 126     | "-image" :: f :: rem ->
 127         image := f; parse (cfiles,args) rem
 128     | "-image" :: [] ->
 129         usage ()
 130     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 131     | ("-libdir"|"-outputstate"|"-I"|"-include"
 132       |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object"
 133       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
 134       |"-init-file" as o) :: rem ->
 135         begin
 136           match rem with
 137             | s :: rem' -> parse (cfiles,s::o::args) rem'
 138             | []        -> usage ()
 139         end
 140     | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
 141     | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois"
 142       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
 143       |"-silent"|"-m" as o) :: rem ->
 144         parse (cfiles,o::args) rem
 145     | ("-v"|"--version") :: _ ->
 146         Usage.version ()
 147     | "-where" :: _ ->
 148         print_endline Coq_config.coqlib; exit 0
 149     | f :: rem -> parse (f::cfiles,args) rem
 150   in
 151   parse ([],[]) (List.tl (Array.to_list Sys.argv))
 152
 153 (* main: we parse the command line, define the command to compile files
 154  * and then call the compilation on each file *)
 155
 156 let main () =
 157   let cfiles, args = parse_args () in
 158   if cfiles = [] then begin
 159     prerr_endline "coq_v2theoryxml: too few arguments" ;
 160     usage ()
 161   end;
 162   let coqtopname =
 163     if !image <> "" then !image else Filename.concat !bindir (binary ^ Coq_config.exec_extension)
 164   in
 165   if !xml_theory_library_root = "" then
 166    begin
 167     prerr_endline "coq_v2theoryxml: you must either set $XML_THEORY_LIBRARY_ROOT or use -xml-theory-library-root";
 168     usage ()
 169    end
 170   else
 171    List.iter (compile coqtopname args) cfiles ;
 172    prerr_endline
 173     ("\nWARNING: all the URIs in the generated XML files are broken." ^
 174      "\n         See the README in the XML contrib to learn how to fix them.\n")
 175
 176 let _ = Printexc.print main (); exit 0