Stream: Coq devs & plugin devs

Topic: Checking individual theorems.


view this post on Zulip Karl Palmskog (Mar 20 2024 at 08:52):

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

view this post on Zulip Notification Bot (Mar 20 2024 at 08:59):

A message was moved here from #Coq devs & plugin devs > coq call by Emilio Jesús Gallego Arias.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 09:02):

Thanks for having a look into this @Karl Palmskog , IMHO we can see understand the problem as two different sub-problems:

  1. is the current way that .vio provides usable / or useful for your purposes ?
  2. what is the ideal way we would like to implement this feature.

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 09:05):

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.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 09:06):

  1. 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
  2. the ideal implementation is in my opinion a CLI tool that allows checking a specific proof based on its constant's kernel name, without having checked it (and any other proofs inside the file) before

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 13:34):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 13:38):

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.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 13:52):

can you qualify what the "soundness" concerns here? Obviously universe global checks are impossible, but is there something else?

view this post on Zulip Karl Palmskog (Mar 20 2024 at 13:54):

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

view this post on Zulip Karl Palmskog (Mar 20 2024 at 13:58):

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

view this post on Zulip Karl Palmskog (Mar 20 2024 at 14:01):

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)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:28):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:29):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:30):

Anyways the answer to question 1. "is .vio currently usable / useful for your purposes" is not very clear to me. Can you clarify?

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:32):

So the answer is "no"?

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:33):

it's in the direction of being useful, but no, without significant engineering it can't be used for reliable batch/CI incremental checking

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:35):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:42):

Yes, they do leak. This is why I'm trying to understand the model you need.

We can still do incremental in this sense:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:42):

The data we are missing is how many memoization "hits" we can achieve with this strategy.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:44):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:45):

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

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:45):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:46):

if you want your check to be sound indeed I don't see any other way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:46):

but you can relax that restriction easily in this model, losing soundness

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:47):

So you can get the current behavior if you want easily.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:47):

but vos/vok is unsound in this sense too, right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:48):

It is a bit less unsound I understand, but I think it still suffers from that problem

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:48):

a bit less in the sense I believe you only lose the constraints that come from other vos files

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:48):

but you still keep the ones in-file

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:49):

But indeed thanks for the feedback, I've added to the TODO list to implement the "check a single def in a file" plugin

view this post on Zulip Gaëtan Gilbert (Mar 20 2024 at 15:49):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:50):

@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")

view this post on Zulip Karl Palmskog (Mar 20 2024 at 15:53):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:55):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:57):

We don't have data on the case of speculative execution.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 15:58):

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.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 16:01):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:04):

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.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 16:05):

for the parts about memoization, I think benchmarks are needed to even show it can give something tangible vs. .vo at file level

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:05):

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)

view this post on Zulip Karl Palmskog (Mar 20 2024 at 16:06):

if I remember correctly, there is also no path going from .vos to .vo - it's unsound forever

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:06):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:06):

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

view this post on Zulip Karl Palmskog (Mar 20 2024 at 16:07):

is it even possible to mix .vos with .vo?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:07):

In principle yes, with some caveats that are not often found (like extraction and print assumption needing bodies, etc...)

view this post on Zulip Karl Palmskog (Mar 20 2024 at 16:08):

I thought there was some fundamental block against mixing them right now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:08):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:09):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:10):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:15):

So you can see the scheme I'm talking about like:

  1. check a foo.v file replacing all proofs with Admitted
  2. then, check a constant b with the real proof.
  3. if later we check 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 user

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

view this post on Zulip Jason Gross (Mar 21 2024 at 01:58):

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?

view this post on Zulip Karl Palmskog (Mar 21 2024 at 06:55):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 21 2024 at 11:48):

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

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 21 2024 at 11:49):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 21 2024 at 11:51):

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