diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-19 15:30:49 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-19 15:30:49 +0000 |
commit | a81329a241ba18b8c8535576290a0ffa23739d27 (patch) | |
tree | 8075b8ab33e56b6610a3ae7ad58a8a47505d2487 /lib/envars.ml | |
parent | 35709dcb82a88ff300c5bb62b7de4b18f5c2127f (diff) |
Nettoyage des variables Coq et amélioration de coqmktop. Les
principaux changements sont:
- coqtop (et coqc) maintenant insensible aux variables
d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
librairies Coq peut être spécifié par l'option -coqlib
- coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
-camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
chemins des exécutables OCaml; en dehors du mode boot, coqmktop
cherche les exécutables OCaml dans PATH
- installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
étant installé en copiant l'architecture des sources (ie lib.cmxa
est installé dans COQLIB/lib/lib.cmxa)
- coq_makefile prend maintenant 3 paramètres sous forme de variables
d'environnement: COQBIN pour dire où trouver les exécutables Coq,
CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
chemins vers les librairies sont déduits en utilisant -where
Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/envars.ml')
-rw-r--r-- | lib/envars.ml | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/lib/envars.ml b/lib/envars.ml new file mode 100644 index 000000000..82e0d3162 --- /dev/null +++ b/lib/envars.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This file gathers environment variables needed by Coq to run (such + as coqlib) *) + +let coqbin () = + if !Flags.boot || Coq_config.local + then Filename.concat Coq_config.coqsrc "bin" + else Filename.dirname Sys.executable_name + +let guess_coqlib () = + let file = "states/initial.coq" in + if Sys.file_exists (Filename.concat Coq_config.coqlib file) + then Coq_config.coqlib + else + let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in + let coqlib = if Coq_config.local then prefix else + List.fold_left Filename.concat prefix ["lib";"coq"] in + if Sys.file_exists (Filename.concat coqlib file) then coqlib else + Util.error "cannot guess a path for Coq libraries; please use -coqlib option" + +let coqlib () = + if !Flags.coqlib_spec then !Flags.coqlib else + (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) + +let path_to_list p = + let sep = Str.regexp_string (if Sys.os_type = "Win32" then ";" else ":") in + Str.split sep p + +let rec which l f = + match l with + | [] -> raise Not_found + | p :: tl -> + if Sys.file_exists (Filename.concat p f) + then p + else which tl f + +let guess_camlbin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath "ocamlc" + +let guess_camlp4bin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath Coq_config.camlp4 + +let camlbin () = + if !Flags.camlbin_spec then !Flags.camlbin else + if !Flags.boot then Coq_config.camlbin else + try guess_camlbin () with _ -> Coq_config.camlbin + +let camllib () = + if !Flags.boot + then Coq_config.camllib + else + let camlbin = camlbin () in + let com = (Filename.concat camlbin "ocamlc") ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + res + +(* TODO : essayer aussi camlbin *) +let camlp4bin () = + if !Flags.camlp4bin_spec then !Flags.camlp4bin else + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () with _ -> Coq_config.camlp4bin + +let camlp4lib () = + if !Flags.boot + then Coq_config.camlp4lib + else + let camlp4bin = camlp4bin () in + let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + res + + |