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 /doc/stdlib | |
| 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 'doc/stdlib')
| -rwxr-xr-x | doc/stdlib/make-library-files | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index add14a13b..9516a19ff 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -1,6 +1,6 @@ #!/bin/sh -# Needs COQTOP and GALLINA set +# Needs COQSRC and GALLINA set # On garde la liste de tous les *.v avec dates dans library.files.ls # Si elle a change depuis la derniere fois ou library.files n'existe pas @@ -13,12 +13,12 @@ LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes" rm -f library.files.ls.tmp -(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp +(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then mv -f library.files.ls.tmp library.files.ls rm -f library.files; touch library.files ABSOLUTE=`pwd`/library.files - cd $COQTOP/theories + cd $COQSRC/theories echo $LIBDIRS for rep in $LIBDIRS ; do (cd $rep |