Is there a tool we can use to insert `Proof using`

in every file of a project automatically, based on the suggestions by `Set Suggest Proof Using`

? There is the `proof-using-helper.py`

from here`, but I think it is broken for ~4 years since Coq does not print the module names anymore (https://github.com/coq/coq/issues/7877). @Emilio Jesús Gallego Arias, you suggest in the issue that maybe an approach via SerAPI would be more feasible, do you know whether somebody tried?

the automatic insertions are likely to be extremely noisy (`Proof using X Y Z ... `

) everywhere. I think it would be a much better idea to first do `Set Default Proof Using "Type".`

on top of every file, and then fill in automatically just enough to compile.

see the commit here: https://github.com/coq-community/reglang/commit/5bfb0318820c893ff159f4d982bcf194d9ce8a9e

My problem with `Set Default Proof Using "Type."`

is that it can generate too many dependencies, so the porting process requires two actions: (1) add more dependencies if `"Type"`

is not sufficient, (2) go back to a proof to remove dependencies. Especially (2) is annoying, because it can involve lots of recompilation

`Type`

should be the minimum dependencies, how can it generate too many?

I don't get why you would have to go back to a proof to remove dependencies. Sometimes you have to add stuff to `Proof using`

, sure, but for a development of 5000+ lines, it was only like 30-40 times.

The script by Jason is trying to do too many smart things.

If you `ls -a`

you will find many `.aux`

files. In there you find stuff like: `7321 7340 context_used ""`

where the numbers are cthe characters at which one finds Qed, and `""`

is a string containing all section variables used by the proof. The only thing one has to do is to crawl back up to `Proof`

and add `using ....`

.

@Yannick Forster using SerAPI or PyCoq you could get an API to do that, I would not do it tho. Caching this kind of transient information in the proofs themselves seems like a bad idea to me.

Emilio Jesús Gallego Arias said:

Yannick Forster using SerAPI or PyCoq you could get an API to do that, I would not do it tho. Caching this kind of transient information in the proofs themselves seems like a bad idea to me.

Is there another way to get parallel compilation with sections apart from `Proof using`

?

I don't know @Yannick Forster , what kind of speedups you see from Proof using?

@Yannick Forster if you want to skip proofs or asynchronously prove a bunch of proofs, `Proof using`

is the only way with sections. But in many cases, file-level parallelism gets you a long way compared to skipped proofs and asynchrony. It depends on the structure of the project.

Karl Palmskog said:

I don't get why you would have to go back to a proof to remove dependencies. Sometimes you have to add stuff to

`Proof using`

, sure, but for a development of 5000+ lines, it was only like 30-40 times.

Right, indeed, this *shouldn't* happen. In principle, `Set Proof Using "Type".`

should break exactly at the `Qed`

of the lemma, if I understand correctly. I can observe though that the MetaCoq codebase breaks: We have things defined in sections where `using Type`

results in dependencies not actually mentioned in the type, so later files break. I suppose this is a bug, possibly due to the interaction of several features

Karl Palmskog said:

Yannick Forster if you want to skip proofs or asynchronously prove a bunch of proofs,

`Proof using`

is the only way with sections. But in many cases, file-level parallelism gets you a long way compared to skipped proofs and asynchrony. It depends on the structure of the project.

Thank you! My understanding also was that skipping asynchronously a section requires `Proof using`

, which is exactly what I'd like to do

Enrico Tassi said:

The script by Jason is trying to do too many smart things.

If you`ls -a`

you will find many`.aux`

files. In there you find stuff like:`7321 7340 context_used ""`

where the numbers are cthe characters at which one finds Qed, and`""`

is a string containing all section variables used by the proof. The only thing one has to do is to crawl back up to`Proof`

and add`using ....`

.

Thank you, this sounds like the right way to go :) Lacking the scripting skills to do this quickly, I ended up using Proof General's auto-insertion of suggested variables :see_no_evil:

Karl Palmskog said:

Sometimes you have to add stuff to

`Proof using`

, sure, but for a development of 5000+ lines, it was only like 30-40 times.

Maybe I should have done it manually, but MetaCoq has around 150k lines, and my quick naive assessment yielded that that would be too much work manually

@Gaëtan Gilbert I believe `Proof using Type`

includes all `Let`

s in the context?

the main payoff with `Proof using`

these days is probably the `vos`

/`vok`

toolchain, I think the speedup was 10-15% on a small project, so big projects could potentially see a lot more

The script I had was doing many things because, IIRC, the info wasn't in the .aux file back when I first wrote it. @Enrico Tassi I don't think your suggested algorithm will work perfectly, because sometimes there is no `Proof.`

line after `Theorem`

or `Definition`

. (Also, is `Proof with tac`

still supported?)

Karl Palmskog said:

the main payoff with

`Proof using`

these days is probably the`vos`

/`vok`

toolchain, I think the speedup was 10-15% on a small project, so big projects could potentially see a lot more

I can report the payoff for MetaCoq in about one hour :)

Also, ProofGeneral has a mode where if you run through a file with `Set Suggest Proof Using`

turned on (I do it in my `~/.coqrc`

file), it will automatically insert the `Proof using`

for you

yes, exactly, one has to have `Proof.`

everywhere for this stuff to work, and I don't think there is automation for inserting missing `Proof.`

We could add a warning to complain about no Proof. and get a tool to use that.

but how do you decide where to raise that warning? Some people don't want `Proof`

if the thing lives in `Set`

/`Type`

or if it's an `Instance`

, etc.

Right, I am not suggesting it becomes default. We could have it opt-in.

Someone proposed `Body`

as a synonym of `Proof`

I think that was Karl lol

Karl Palmskog said:

the main payoff with

`Proof using`

these days is probably the`vos`

/`vok`

toolchain, I think the speedup was 10-15% on a small project, so big projects could potentially see a lot more

On a first view, the performance of `make vos`

profited by something like 30% from including `Proof using`

everywhere. Some files had such directives already however, and GitHub CI worker performance might play a role, but still I feel confident to say that we're getting even more than 15%

Addendum: I was comparing the CI times with a global `Unset Universe Checking`

together with `make vs`

- don't know whether this benefits the performance gain or not

Enrico Tassi said:

Someone proposed

`Body`

as a synonym of`Proof`

Yes, that was me, I still have a branch working on this, will likely submit when things calm down at end of spring semester

but how do you decide where to raise that warning? Some people don't want

`Proof`

if the thing lives in`Set`

/`Type`

or if it's an`Instance`

, etc.

just raise the warning everywhere where enabled

Last updated: Oct 03 2023 at 04:02 UTC