Stream: Coq users

Topic: How to insert `Proof using` in all files automatically?


view this post on Zulip Yannick Forster (May 09 2022 at 09:32):

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?

view this post on Zulip Karl Palmskog (May 09 2022 at 09:35):

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.

view this post on Zulip Karl Palmskog (May 09 2022 at 09:36):

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

view this post on Zulip Yannick Forster (May 09 2022 at 11:02):

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

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 11:03):

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

view this post on Zulip Karl Palmskog (May 09 2022 at 12:16):

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.

view this post on Zulip Enrico Tassi (May 09 2022 at 12:22):

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 .....

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2022 at 14:53):

@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.

view this post on Zulip Yannick Forster (May 09 2022 at 15:20):

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?

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2022 at 15:21):

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

view this post on Zulip Karl Palmskog (May 09 2022 at 15:22):

@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.

view this post on Zulip Yannick Forster (May 09 2022 at 15:24):

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

view this post on Zulip Yannick Forster (May 09 2022 at 15:24):

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

view this post on Zulip Yannick Forster (May 09 2022 at 15:26):

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:

view this post on Zulip Yannick Forster (May 09 2022 at 15:27):

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

view this post on Zulip Jason Gross (May 09 2022 at 15:28):

@Gaëtan Gilbert I believe Proof using Type includes all Lets in the context?

view this post on Zulip Karl Palmskog (May 09 2022 at 15:29):

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

view this post on Zulip Jason Gross (May 09 2022 at 15:30):

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?)

view this post on Zulip Yannick Forster (May 09 2022 at 15:30):

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 :)

view this post on Zulip Jason Gross (May 09 2022 at 15:30):

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

view this post on Zulip Karl Palmskog (May 09 2022 at 15:31):

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.

view this post on Zulip Ali Caglayan (May 09 2022 at 15:36):

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

view this post on Zulip Karl Palmskog (May 09 2022 at 15:37):

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.

view this post on Zulip Ali Caglayan (May 09 2022 at 15:39):

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

view this post on Zulip Enrico Tassi (May 09 2022 at 16:27):

Someone proposed Body as a synonym of Proof

view this post on Zulip Ali Caglayan (May 09 2022 at 16:29):

I think that was Karl lol

view this post on Zulip Yannick Forster (May 09 2022 at 16:31):

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%

view this post on Zulip Yannick Forster (May 09 2022 at 16:43):

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

view this post on Zulip Karl Palmskog (May 09 2022 at 17:19):

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

view this post on Zulip Paolo Giarrusso (May 09 2022 at 18:05):

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.

view this post on Zulip Paolo Giarrusso (May 09 2022 at 18:06):

just raise the warning everywhere where enabled


Last updated: Jan 29 2023 at 06:02 UTC