aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/main.ml
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-19 15:30:49 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-12-19 15:30:49 +0000
commita81329a241ba18b8c8535576290a0ffa23739d27 (patch)
tree8075b8ab33e56b6610a3ae7ad58a8a47505d2487 /tools/coqdoc/main.ml
parent35709dcb82a88ff300c5bb62b7de4b18f5c2127f (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 'tools/coqdoc/main.ml')
-rw-r--r--tools/coqdoc/main.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index e6c3e5c07..864b2718e 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -57,6 +57,7 @@ let usage () =
prerr_endline " --no-externals no links to Coq standard library";
prerr_endline " --coqlib <url> set URL for Coq standard library";
prerr_endline " (default is http://coq.inria.fr/library/)";
+ prerr_endline " --boot run in boot mode";
prerr_endline " --coqlib_path <dir> set the path where Coq files are installed";
prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir";
prerr_endline " --latin1 set ISO-8859-1 input language";
@@ -318,6 +319,8 @@ let parse () =
Cdglobals.coqlib := u; parse_rec rem
| ("--coqlib" | "-coqlib") :: [] ->
usage ()
+ | ("--boot" | "-boot") :: rem ->
+ Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
| ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
Cdglobals.coqlib_path := d; parse_rec rem
| ("--coqlib_path" | "-coqlib_path") :: [] ->