The Coq mailing list

[Julien Thierry <thierry AT adacore.com>]

On 2014-03-06 16:20, Pierre Boutillier wrote:
> 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.* ...

Thanks for the workarounds.

> 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 !

Such an option would be really useful indeed.
Good luck with the revolution ;)

Best regards,

-- 
Julien Thierry