From fd106c270ac00994275898a77e48c311b554636a Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 3 Nov 2000 10:21:00 +0000 Subject: compilation des fichiers ml4 sans GNUseries git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7 --- scripts/.cvsignore | 1 - scripts/coqc.ml | 164 +++++++++++++++++++++++++++++++++++++++++++++++++++++ scripts/coqc.ml4 | 164 ----------------------------------------------------- 3 files changed, 164 insertions(+), 165 deletions(-) create mode 100644 scripts/coqc.ml delete mode 100644 scripts/coqc.ml4 (limited to 'scripts') diff --git a/scripts/.cvsignore b/scripts/.cvsignore index ee865a5683..b95eb1ba95 100644 --- a/scripts/.cvsignore +++ b/scripts/.cvsignore @@ -1,4 +1,3 @@ coqmktop tolink.ml coqc -coqc.ml diff --git a/scripts/coqc.ml b/scripts/coqc.ml new file mode 100644 index 0000000000..baf86982bd --- /dev/null +++ b/scripts/coqc.ml @@ -0,0 +1,164 @@ + +(* $Id$ *) + +(* Afin de rendre Coq plus portable, ce programme Caml remplace le script + coqc. + + Ici, on trie la ligne de commande pour en extraire les fichiers à compiler, + puis on les compile un par un en passant le reste de la ligne de commande + à un process "coqtop -batch -load-vernac-source ". + + On essaye au maximum d'utiliser les modules Sys et Filename pour que la + portabilité soit maximale, mais il reste encore des appels à des fonctions + du module Unix. Ceux-ci sont préfixés par "Unix." +*) + +(* environment *) + +let environment = Unix.environment () + +let bindir = ref Coq_config.bindir +let binary = ref "coqtop.byte" + +(* 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 -> () + +let specification = ref false + +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 ".v" then + Filename.chop_suffix basename ".v" + else + basename + in + check_module_name modulename; + let tmpfile = Filename.temp_file "coqc" ".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 filevo = Filename.concat dirname (modulename ^ ".vo") in + let oc = open_out tmpfile in + Printf.fprintf oc "Module %s.\n" modulename; + Printf.fprintf oc "Load \"%s\".\n" file; + Printf.fprintf oc "Write Module %s \"%s\".\n" modulename filevo; + 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_coqc () ; + flush stderr ; + exit 1 + +let parse_args () = + let rec parse (cfiles,args) = function + | [] -> + List.rev cfiles, List.rev args + | "-i" :: rem -> + specification := true ; parse (cfiles,args) rem + | "-t" :: rem -> + keep := true ; parse (cfiles,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 + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" + |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" + |"-require"|"-unsafe"|"-quiet"|"-silent"|"-v"|"--version" + |"-load-ml-object"|"-user"|"-init-file" as o) :: rem -> + begin + match rem with + | s :: rem' -> parse (cfiles,s::o::args) rem' + | [] -> usage () + end + | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> + parse (cfiles,o::args) rem + | f :: rem -> + if Sys.file_exists f then + parse (f::cfiles,args) rem + else + let fv = f ^ ".v" in + if Sys.file_exists fv then + parse (fv::cfiles,args) rem + else begin + prerr_endline ("coqc: "^f^": no such file or directory") ; + exit 1 + end + 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 "coqc: too few arguments" ; + usage () + end; + let coqtopname = Filename.concat !bindir !binary in + List.iter (compile coqtopname args) cfiles + +let _ = Printexc.print main (); exit 0 diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 deleted file mode 100644 index 5500903a9f..0000000000 --- a/scripts/coqc.ml4 +++ /dev/null @@ -1,164 +0,0 @@ - -(* $Id$ *) - -(* Afin de rendre Coq plus portable, ce programme Caml remplace le script - coqc. - - Ici, on trie la ligne de commande pour en extraire les fichiers à compiler, - puis on les compile un par un en passant le reste de la ligne de commande - à un process "coqtop -batch -load-vernac-source ". - - On essaye au maximum d'utiliser les modules Sys et Filename pour que la - portabilité soit maximale, mais il reste encore des appels à des fonctions - du module Unix. Ceux-ci sont préfixés par "Unix." -*) - -(* environment *) - -let environment = Unix.environment () - -let bindir = ref Coq_config.bindir -let binary = ref "coqtop.byte" - -(* 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 -> () - -let specification = ref false - -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 ".v" then - Filename.chop_suffix basename ".v" - else - basename - in - check_module_name modulename; - let tmpfile = Filename.temp_file "coqc" ".v" in - let args' = - command :: "-batch" :: "-silent" :: args - @ ["-load-vernac-source"; tmpfile] in - let devnull = - ifdef Unix then - Unix.openfile "/dev/null" [] 0o777 - else - Unix.stdin - in - let filevo = Filename.concat dirname (modulename ^ ".vo") in - let oc = open_out tmpfile in - Printf.fprintf oc "Module %s.\n" modulename; - Printf.fprintf oc "Load \"%s\".\n" file; - Printf.fprintf oc "Write Module %s \"%s\".\n" modulename filevo; - 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_coqc () ; - flush stderr ; - exit 1 - -let parse_args () = - let rec parse (cfiles,args) = function - | [] -> - List.rev cfiles, List.rev args - | "-i" :: rem -> - specification := true ; parse (cfiles,args) rem - | "-t" :: rem -> - keep := true ; parse (cfiles,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 - | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" - |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" - |"-require"|"-unsafe"|"-quiet"|"-silent"|"-v"|"--version" - |"-load-ml-object"|"-user"|"-init-file" as o) :: rem -> - begin - match rem with - | s :: rem' -> parse (cfiles,s::o::args) rem' - | [] -> usage () - end - | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" - |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> - parse (cfiles,o::args) rem - | f :: rem -> - if Sys.file_exists f then - parse (f::cfiles,args) rem - else - let fv = f ^ ".v" in - if Sys.file_exists fv then - parse (fv::cfiles,args) rem - else begin - prerr_endline ("coqc: "^f^": no such file or directory") ; - exit 1 - end - 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 "coqc: too few arguments" ; - usage () - end; - let coqtopname = Filename.concat !bindir !binary in - List.iter (compile coqtopname args) cfiles - -let _ = Printexc.print main (); exit 0 -- cgit v1.2.3