coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to use coqchk in a stand-alone folder?

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] how to use coqchk in a stand-alone folder?
Date: Fri, 13 May 2016 15:12:25 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f179.google.com
Ironport-phdr: 9a23:W+hraxw3tTS8RXvXCy+O+j09IxM/srCxBDY+r6Qd0e0SIJqq85mqBkHD//Il1AaPBtWKragdwLOM4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZ7unLnoqtX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjUSrY9RTSr6e9PRR72hSEbf2o792fWicF0ga9zrxeophg5yInRNtLGfMFid7/QKItJDVFKWdxcAmkYWtux

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

[Coq-Club] how to use coqchk in a stand-alone folder?, Jonathan Leivent, 05/13/2016
- Re: [Coq-Club] how to use coqchk in a stand-alone folder?, Jean-Christophe Léchenet, 05/17/2016
  - Re: [Coq-Club] how to use coqchk in a stand-alone folder?, Jonathan Leivent, 05/17/2016