The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Thanks, Jean-Cristophe!  I should look more closely at that makefile.

It turns out there is a bug in creating this coqchk rule, as I have 
-impredicative-set in all of the coqc rules - it is in OTHERFLAGS - but 
that is not used in the coqchk rule.

-- Jonathan

On 05/17/2016 03:55 AM, Jean-Christophe Léchenet wrote:
> 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