Stream: Coq users

Topic: How to use `_CoqProject` with coqchk


view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:53):

Is there a recommended way to run coqchk in a project with a _CoqProject in it? I'm thinking about metacoq more specifically (but I think other projects are similar), in that it has a makefile which runs coqc but if you want to run any other tool it seems like you are out of luck unless the tool has _CoqProject support? (Let's assume I don't want to copy and paste 20 lines from the _CoqProject directly into my command line invocation)

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 16:07):

coq_makefile generated makefiles have a validate target
metacoq however is split into multiple coq_makefile invocations so not so easy to get it all

view this post on Zulip Mario Carneiro (Dec 20 2023 at 16:09):

hm, I was hoping to find such a target in e.g. pcuic/Makefile but it seems to be a hand-written (or hand-written-configure-written) makefile

view this post on Zulip Mario Carneiro (Dec 20 2023 at 16:11):

oh but there is Makefile.coq which looks like it was written by coq_makefile

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 16:11):

yes


Last updated: Jun 13 2024 at 21:01 UTC