Hi, 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 is there a way to get the exact coqc command that is issued so I can figure out what is going wrong ? Thanks -- Laurent _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
