The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Le jeudi 06 mars 2014 à 14:44 +0100, Julien Thierry a écrit :
> Is there a way to tell coq_makefile to map physical paths to logical paths
> without
> loosing my libraries when using make clean?
No, and that a serious problem !!!

Well OK don't put 
> -R /pathtowhy3install/lib/why3/coq Why3
in your Make file and then use
> make COQLIBS="-R /pathtowhy3install/lib/why3/coq Why3 -R . Mystuff -R
foo other__stuff_from_the_Makefile" all

and you might go somewhere but it is a pity ...

It would have been much easier if the Why3 lib could install itself in a
directory called Why3 that is 'included' by coq ... For example, by
doing
> mkdir /pathtowhy3install/lib/why3/coq/Why3 &&
mv /pathtowhy3install/lib/why3/coq/*.vo /pathtowhy3install/lib/why3/coq/Why3/
> export XDG_DATA_DIRS=$XDG_DATA_DIRS:/pathtowhy3install/lib/why3/
coq{top,dep,c} would be able to Require Why3.* ...

I didn't find yet any good idea for a
-R_for_coqtop_and_coqdep_but_not_coq_makefile option in coq_makefile.
Nevertheless, this question is postponed to "after the revolution about
what physical paths Coq includes by default". Revolution that is stuck
somehow somewhere (in its consequences about native_compute if I
understood well) and have to be brought back to life !

All the best,
Pierre B.

> 
> Regards,
>