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

1 files changed, 4 insertions, 8 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 1ed094cf27..9c1802cab0 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -43,7 +43,7 @@ let (/) = Filename.concat
 
 let get_version_date () =
   try
-    let ch = open_in (Coq_config.coqlib^"/revision") in
+    let ch = open_in (Coq_config.coqsrc ^ "/revision") in
     let ver = input_line ch in
     let rev = input_line ch in
       (ver,rev)
@@ -108,13 +108,9 @@ let set_rec_include d p =
   check_coq_overwriting p;
   push_rec_include(d,p)
 
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib =
-    (* variable COQLIB overrides the default library *)
-    getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-	else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let contrib = coqlib/"contrib" in
   (* first user-contrib *)
@@ -323,7 +319,7 @@ let parse_args() =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
+        print_endline (Envars.coqlib ()); exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()