Stream: Coq users

Topic: Warning for `Admitted`?

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.

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.

Gaëtan Gilbert (Jan 07 2021 at 18:00):

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

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.

Paolo Giarrusso (Jan 07 2021 at 18:46):

Is there a robust criterion for that?

Anton Trunov (Jan 07 2021 at 19:14):

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

Gaëtan Gilbert (Jan 07 2021 at 20:06):

declare instance and declare module produce axioms

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.

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: Oct 13 2024 at 01:02 UTC