How to use with a _CoqProject

[JoJoDeveloping]

Hello,

when I naively try to execute find . -name '*.v' -exec alectryon.py --frontend coqdoc --backend webpage {} \; in a project using a _CoqProject, I get errors like this:

./Instance/Coq/Dist.v:(7:16)-(7:28): (ERROR/3) Coq raised an exception:
     > Cannot find a physical path bound to logical path matching suffix Category.
   The offending chunk is delimited by >>>…<<< below:
     > Require Import Coq.Sets.Ensembles.
     >
     > Require Import >>>Category.Lib<<<.
     > Require Import Category.Lib.Same_set.
     > Require Export Category.Theory.Functor.
   Results past this point may be unreliable.

The _CoqProject starts with -R . Category.

Is there a general way for generating alectryon files for a project like this? I have wondered about this a few times now, but never really figured it out.

Thanks!

[ana-borges]

This is not really an answer, but it should work in a pinch. You can pass -R . Category to Alectryon, as well as several different files. So:

alectryon -R . Category --frontend coqdoc --backend webpage *.v

should accomplish what you want. Still, it won't take into consideration other things in your _CoqProject, such as any annotations disabling warnings, for example.