GitLab

I have a little Why3 program as an example of a Coq library. When my library is installed, why3 replay works fine.

Now I would like to check the why3 example within the build of my library but this time replay can't locate my library files (fair enough they are not yet installed), I get :

goal 'prime'vc.32.1.0.1', prover 'Coq 8.12.0': Unknown (Unable to locate library)

In order to indicate where the vo files can be found, I have added a config file :

[prover_modifiers]
name="Coq"
option="-R path_to_my_vofiles name_of_my_library"

still when I do

why3 replay --extra-config config.file

I get the same error message

When I pass the option "-debug call_prover" it seems that the extra config is actually not added to the Coq command

cmd=[coqtop, -batch, -R, /home/thery/opam-coq.8.12.0/4.07.1+flambda/lib/why3/coq, Why3, -l, /tmp/why_5aab7e_zilch_T_h.v]

Is there a way to make this work?