The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

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