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 youls -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 toProof
and addusing ....
.
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 thevos
/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 thevos
/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 ofProof
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 inSet
/Type
or if it's anInstance
, etc.
just raise the warning everywhere where enabled
Last updated: Oct 13 2024 at 01:02 UTC