The Coq mailing list

[Jean-Christophe Léchenet <jean-christophe.lechenet AT cea.fr>]

Hi Jonathan,

If the Makefile is produced using coq_makefile, there must be a target 
"validate" that runs coqchk on all the files.

Hope this helps,

Jean-Christophe

Le 13/05/2016 21:12, Jonathan Leivent a écrit :
> I am having difficulty getting coqchk to find all .vo files in a 
> folder.  The folder has its own _Coq_project file and generated 
> makefile.  The folder is stand-alone - it doesn't produce a library 
> used outside of itself, but produces many .vo files used within 
> itself.  If I run coqchk in that folder with the args present in 
> _Coq_project, it apparently finds nothing to do, as shown by:
>
> Ordered list:
>
> Modules were successfully checked
>
> CONTEXT SUMMARY
> ===============
>
> * Theory: Set is impredicative
>   Theory: Stratified type hierarchy
>
> * Axioms: <none>
>
> There are .vo modules in that folder, and some use axioms.  So I know 
> coqchk isn't doing anything.  However, because the folder is 
> stand-alone, there really isn't a library path to give coqchk.  Is 
> this just a case where coqchk can't be used?
>
> -- Jonathan