Check commands

[yforster]

Andrej's investigation into performance yielded that we shouldn't use Print Assumptions, because it is too slow.

Now an open question is whether we want Check commands after important theorems or not. Previously we wanted them to out Print Assumptions into context, nut now they might be unnecessary as well. Leaving them out might make the compile logs easier to read.

An alternative (that I don't find necessarily good) is to have a summary.v file which contains lots of Check commands, but is not in the Coq project.

I could also look into implementing a MetaCoq Run Check command which only prints its results in interactive mode and not in compilation mode.

[DmxLarchey]

Yes indeed Print Assumptions can be slow. On the other hand, Check is usually not slow.

There are two issues indeed:

• slow compilation;
• too verbose output of compilation.

So concerning summary.v, we could for instance have a file that collect all the main results of the paper under Checks but w/o Print Assumptions and the make all would be make summary.vo instead, hopefully compiling everything via dependencies.

We could also have a sanity_check.v file with Check followed by Print Assumptions but that one would not be compiled by make unless explicitly asked for? May be it would only be run into an interactive proof assistant.

Both summary.v and sanity_check.v could be auto-generated from a list of files/theorems (perhaps I am not sure).

That way, both summary.v and sanity_check.v could appear in _CoqProject w/o implying they would be automatically compiled by CI.

[mrhaandi]

I suggest keep it simple. I like to insert Check after the mathematically most important theorems, e.g. Problem_undec : undecidable Problem. If the overall project is uniformly well-structured (and documented via comments), then specification, reductions and the main undecidability results should be easy to survey without additional summary.v or sanity_check.v.

[DmxLarchey]

I am ok with inplace Check commands for the main theorems.

But I still think that we should provide a way for extrernal reviewers to control the claims about axiom free-ness. Of course, it is up to them to do so but we can explain how to do it in case the reviewer is not very knowledgeable in Coq.

[mrhaandi]

Of course, it is up to them to do so but we can explain how to do it in case the reviewer is not very knowledgeable in Coq.

In my work I refer to the actual Print Assumptions Coq documentation. If anyone is knowledgeable enough to compile the library in order to inspect the theorems, then this is only a small step (or, of similar size compared to argument passing for different compilation targets).

[fakusb]

For the record: Print assumption can be tricked: https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users/topic/impredicative.20set/near/216492018