the issue (at least for me) with vos
-only is that then basically everything is down to the file layout in a project. The only way to skip/check a proof is to consciously have it be located in some file. In projects with many big files, using vos
/vok
is not really worth the effort based on checking times we saw in real-world projects.
Is there at least some ambition to enable official support for individually checking proofs independently of files in a batch/CI context in the future? To my knowledge, there isn't anything about it in the Roadmap
A message was moved here from #Coq devs & plugin devs > coq call by Emilio Jesús Gallego Arias.
Thanks for having a look into this @Karl Palmskog , IMHO we can see understand the problem as two different sub-problems:
At least for the general user that wants to check documents quickly, and later on verify them, the .vio solution works pretty poorly; moreover, it gets in the way of 2, even if minimally.
Is there at least some ambition to enable official support for individually checking proofs independently of files in a batch/CI context in the future? To my knowledge, there isn't anything about it in the Roadmap
I didn't contribute anything yet to the roadmap due to other motives, but indeed, coq-lsp
/fleche
are designed to do this (and in fact, even if very far, we'd like to enable fully per-definition incremental checking in the future).
As of today we are almost there to enable this feature, the design is completed, but we are missing a few bits in Coq and in coq-lsp implementation-wise (happy to detail what).
I much prefer the model we have designed for coq-lsp over the current model, as in it is sound, however a crucial point missing is to understand how effective this approach is when we require full soundness.
Still, we can recover the current unsound behavior easily, as we just change the eq function used in the cutoff.
vio
allows checking a specific proof inside a file in isolation, but one needs to build the .vio
first and use an awkward number identifier unrelated to the constant name.vio allows you to do that, however you need to build the vio file which is quadratic in space. Moreover you don't get soundness guarantees, so it is a kind of "weak" check.
For 2, the main question is what kind of semantics do you want? coq-lsp
could do that easily, however, you still don't get sound results in general, if you don't check the proofs before that definition.
How crucial is soundness in your case?
Let's assume we have a file with 3 lemmas in that order, a, b, c
.
Then the idea is coq-lsp
is a bit more subtle: check b
if the user is looking at that, without checking the proof of a
(we don't care about c
, as it is later in the file. The check for b
is "speculative", it assumes when we check a
, the stuff b
cares about (universe constraints), won't have changed.
Then, at some point, a
is checked; then the output of a
becomes the input for checking b
, however, if the dependency turns (universe graph) turns out to be the same, then Flèche will cutoff the check, and we done (in a sound way).
We can of course implement 2
now, ignoring universes (I have a branch for that, but needs careful testing and it is scheduled for 0.2.0), but still you don't get sound stuff, unless you are willing to forget about it.
can you qualify what the "soundness" concerns here? Obviously universe global checks are impossible, but is there something else?
my interest is only in some check completely divorced from GUI/interfaces, so "looking at" b
doesn't really make sense. Generally, we would like to check b
whenever something that b
depends on has changed (including b
itself), regardless of other factors
the individual check should ideally be completely divorced from any LSP or other session, so one doesn't have to feed in any specific Coq sentences just to do a check, e.g., the files should be pre-compiled in some way
the basic idea is very similar to "modular verification" in Hoare-style reasoning with procedures: we want establish that a procedure (term) fullfils a certain contract (has a type), assuming all other procedures (opaque constants) are represented only by their contract (type)
Karl Palmskog said:
can you qualify what the "soundness" concerns here? Obviously universe global checks are impossible, but is there something else?
That's already a pretty big hole, as shown many times, a missing universe check can make a tactic output true
or false
later on, changing everything. Universe global checks are not impossible, why do you say that? I just explained how to do them incrementally, whether that will be effective is a different matter.
"Looking at" in your case means your tool telling Flèche "check b", there is nothing UI dependent on that (you could actually almost implement that now with a very simple fcc
plugin as follows: check in lazy mode the document, then the plugin requests the check for b
only).
The issue is that wrote "checking b without checking was is before b", that's just not possible to do soundly in general.
Karl Palmskog said:
the basic idea is very similar to "modular verification" in Hoare-style reasoning with procedures: we want establish that a procedure (term) fullfils a certain contract (has a type), assuming all other procedures (opaque constants) are represented only by their contract (type). So we pick a procedure and its contract and check it.
There is a big problem with this assumption, Coq respect that contract by far. But indeed, you can just tell Fleche to work like that, but I'm unsure why this is useful given that you have abandoned guarantees. If the contract is true, IMHO you are still better with true incremental checking which should take similar time but produce sound results.
Anyways the answer to question 1. "is .vio currently usable / useful for your purposes" is not very clear to me. Can you clarify?
as I said, the big problem with .vio
is that there's no good (CLI) interface to them to run a check based on a kernel name. There is also the problem of having to annotate with Proof using
So the answer is "no"?
it's in the direction of being useful, but no, without significant engineering it can't be used for reliable batch/CI incremental checking
don't universe constraints leak through the opaqueness barrier? At least when I discussed it last, I got the impression it [universe constraint checking] could only be done with proof terms available
Yes, they do leak. This is why I'm trying to understand the model you need.
We can still do incremental in this sense:
b
, without the constraintsa
, b
is reeschuled for execution, however, if the constraint graph is equivalent, we will use the previous value in step 1The data we are missing is how many memoization "hits" we can achieve with this strategy.
Of course, if b
access the opaque table we don't even bother, that's why we need the patch declaring use of opaquetable in the vernac_type
note that the function that checks "the constraint graph is equivalent" is often tweaked, for example you can set the function to return true
always, then b
will never be re-checked when constraints are updated
but how we know or determine that we check a
? You're saying you can never avoid checking it for universe constraint soundness, only try to do it with as much memoization as possible?
if you want your check to be sound indeed I don't see any other way
but you can relax that restriction easily in this model, losing soundness
So you can get the current behavior if you want easily.
but vos
/vok
is unsound in this sense too, right?
It is a bit less unsound I understand, but I think it still suffers from that problem
a bit less in the sense I believe you only lose the constraints that come from other vos files
but you still keep the ones in-file
But indeed thanks for the feedback, I've added to the TODO list to implement the "check a single def in a file" plugin
@Emilio Jesús Gallego Arias did you ever do the measurement we talked about of how much universe leak there is in practice from Qed definitions?
@Gaëtan Gilbert I'm on it, code is almost ready (I want to implement the stats via a Fleche plugin, so I need to add the plugin callback for "Qed")
isn't there some sufficient condition for non-leaking universe constraints through Qed
? The whole thing with global memoization seems almost non-incremental to me, probably there won't be too much time savings in this way vs. just doing full .vo
and file-level incrementality
@Karl Palmskog I'd say depends a lot on what your workload is, as of today, with a much simpler strategy, for many developments time savings are already considerable for example in the case you are editing a proof, as we hit the cache very often for most changes.
We don't have data on the case of speculative execution.
My question was more in the lines of trying to understand what you want in terms of soundness.
We can do like .vio / .vos easily (have the cutoff function for the univ graph return true always), but I was wondering if that's OK for your case, or you would like stronger guarantees.
I'd like .vo
level soundness, of course. If soundness is dropped, there should be some big gain in performance. vos
/vok
seems to be a bad tradeoff to me, we get pretty much the same unsoundness as .vio
but no way to even exploit it at proof level
The main positive tradeoff .vos
bring when compared to .vio is that is much faster due to .vio file size being quadratic on the input file.
for the parts about memoization, I think benchmarks are needed to even show it can give something tangible vs. .vo
at file level
So indeed, it provides _usable_ "skip the proofs" at the file level, at the cost of indeed re-doing the whole file. But it turns out that is faster than .vio, see the origianl .vos PR for more info (IIRC)
if I remember correctly, there is also no path going from .vos
to .vo
- it's unsound forever
Karl Palmskog said:
for the parts about memoization, I think benchmarks are needed to even show it can give something tangible vs.
.vo
at file level
The Qed data will tell us indeed what the gains are, but I am more optimistic as once we understand the data I'm sure a sweet pragmatic spot can be found as to get closer to vos performance.
Karl Palmskog said:
if I remember correctly, there is also no path going from
.vos
to.vo
- it's unsound forever
Indeed, there is no path, but that's what we are tying to implement in Flèche
is it even possible to mix .vos
with .vo
?
In principle yes, with some caveats that are not often found (like extraction and print assumption needing bodies, etc...)
I thought there was some fundamental block against mixing them right now
Of course, we don't track what we did check with a .vos / .vo , so that's what Flèche does, tracks it, and will try to re-use if the new constraints are compatible with the previous check.
Karl Palmskog said:
I thought there was some fundamental block against mixing them right now
Not that I'm aware, in principle. For example in Flèche you case save .vo files even if some definitions are broken. In this case, it will be as if the user had typed Admitted
, I believe that's exactly what .vos does.
IIANM .vos files are similar to .vo files but replacing Proof. ... Qed.
with Admitted.
. coq-lsp
/ Flèche already do this dynamically, so hence we can easily implement this selectively.
So you can see the scheme I'm talking about like:
foo.v
file replacing all proofs with Admitted
b
with the real proof.a
, then we try to re-check the deps, if the universe graph changed in a meaningful way, we re-execute. In this case, what "meaningful" means is up to the userIndeed the above approach could not work very well, but not all hope is lost. Once we understand why the universe graph is changing where we would like it not to change, we can discuss how to implement some form of local universe constrains on the Coq side. But at this point, we are blocked on getting that data.
The above approach has a good property in that no special handling is required from the Kernel etc... at least in a first phase.
Emilio Jesús Gallego Arias said:
Of course, we don't track what we did check with a .vos / .vo , so that's what Flèche does, tracks it, and will try to re-use if the new constraints are compatible with the previous check.
I thought the whole point of .vok
was that when a .vo
file is present you can make a dummy .vos
or whatever?
I think most people have no idea about the universe issues, so I wonder if they will notice any difference with "Fleche+memoization" and vos/vok. So probably the main driver for aiming for "Fleche+memoization" is (a) benchmarking and (b) stepping stone to a universe sound version.
[minor note: Fleche already includes memoization, that's the whole point of it, so Fleche + memo = Fleche]
The drivers for Flèche are a bit more wide IMHO:
Admitted
So for example the moment we implement (soon) Isabelle-like "only check proofs in view", that's gonna be IMHO a very noticeable difference. There is a problem in having this to work better in batch mode, due to the way we Marshall stuff, that will take a bit more time tho, but for the purposes of simple "check single def" it should work.
Jason Gross said:
Emilio Jesús Gallego Arias said:
Of course, we don't track what we did check with a .vos / .vo , so that's what Flèche does, tracks it, and will try to re-use if the new constraints are compatible with the previous check.
I thought the whole point of
.vok
was that when a.vo
file is present you can make a dummy.vos
or whatever?
Yes, but IIUC the regular workflow can still check proofs in parallel, so that means that you can require some .vos
so in that sense the full check with .vok would be unsound.
But I may be wrong, we could check that; in the end you trade speed for soundness.
Once you can be a bit more fine grained (for example to handle a dep on just the universe graph or opaque proofs) you can reap big benefits (as pointed by Andrey Mokhov)
Last updated: Oct 13 2024 at 01:02 UTC