Mario Carneiro (Dec 20 2023 at 15:53): 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)
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
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
Mario Carneiro (Dec 20 2023 at 16:11):oh but there is Makefile.coq which looks like it was written by coq_makefile
Gaëtan Gilbert (Dec 20 2023 at 16:11):yes
Last updated: Oct 13 2024 at 01:02 UTC