coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
- To: anoun AT labri.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] dependance entre fichiers Coq+ compilation
- Date: Tue, 4 Nov 2003 17:51:17 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Houda Anoun writes:
> Bonjour tt le monde,
> Je suis en train de réaliser un développement qui comprend plusieurs
> répertoires contenant différents fichiers Coq...
> Je voulais savoir comment résoudre le probleme qui se pose à cause de la
> dependance entre des fichiers Coq se trouvant ds des repertoires
> differents...dans ce cas, la commande Require rep/fichier ne marche pas ?!
> Une solution pas tres elegante est d'inclure la commande 'Add LoadPath
> rep' au début de chaque fichier qui utilise des fichiers se trouvant ds
> 'rep'...
> Je me demande s'il y'a pas une autre solution plus élégante?!
> Le second probleme, est celui de la compilation, en effet, pour chaque
> repertoire il y'a un makefile qui permet de compiler ses fichiers ....
> bien evidemment il y'aura un certain ordre qu'il faut respecter lors de
> la compilation 'compiler les fichiers de rep1 avant ceux de rep2 etc...'...
> je veux savoir s'il y'a pas un outil génerique qui permet de compiler
> tous les fichiers se trouvant ds des repertoires differents?
Oui, un tel outil existe : make. Une bonne solution est d'avoir un
unique Makefile à la racine. Cela convient parfaitement à coqc et
coqdep. Plus précisément on aura une commande de compilation de la
forme :
%.vo: %.v
coqc -I rep1 -I rep2 ... $^
et une commande de calcul de dépendances de la forme :
.depend:
coqdep -I rep1 -I rep2 ... rep1/*.v rep2/*.v ...
include .depend
Remarque : il n'y a même plus lieu de respecter un certain ordre entre
les répertoires. Seul l'ordre entre les fichiers, calculé par coqdep,
est pris en compte par make.
--
Jean-Christophe
- [Coq-Club] dependance entre fichiers Coq+ compilation, Houda Anoun
- Re: [Coq-Club] dependance entre fichiers Coq+ compilation, Jean-Christophe Filliatre
Archive powered by MhonArc 2.6.16.