Stream: Coq users

Topic: Warning for `Admitted`?


view this post on Zulip Anton Trunov (Jan 07 2021 at 11:42):

Is it possible to have a warning for each Admitted lemma in a project? I can do something like

Lemma foo : False.
Proof.
Admitted.
Print Assumptions foo.

But it's not really a warning and I would need to do something like this for each admitted lemma as opposed to e.g. having a flag in my _CoqProject file. Also, grepping for warnings is a non-solution since the goal is to have a reminder for admits.

view this post on Zulip Stéphane Desarzens (Jan 07 2021 at 17:23):

I don’t know whether Coq has the feature you want.
You could run grep from your Makefile, then you’d get the results each time you run make.

view this post on Zulip Gaëtan Gilbert (Jan 07 2021 at 18:00):

do you want to warn on axiom/parameter/declare instance/declare module/etc too?

view this post on Zulip Anton Trunov (Jan 07 2021 at 18:43):

Gaëtan Gilbert said:

do you want to warn on axiom/parameter/declare instance/declare module/etc too?

I think a warning about axioms (if introduced at all) should be separate from the rest of the declared things.

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:46):

Is there a robust criterion for that?

view this post on Zulip Anton Trunov (Jan 07 2021 at 19:14):

I guess I would be happy with the syntactic approximation :)

view this post on Zulip Gaëtan Gilbert (Jan 07 2021 at 20:06):

declare instance and declare module produce axioms

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 22:48):

Yeah, I’d file a bug at anything that treats Axiom and Parameter as different. Coqchk doesn’t.

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 22:49):

It is a bit annoying that coqchk doesn’t treat “Declare Module M : I.” as a single axiom.


Last updated: Feb 08 2023 at 23:03 UTC