Bug minimizer

[Alizter]

coq-lsp should have a functionality to create a minimal test case for a particular error similarly to the bug minimiser in coq-tools.

The basic functionality would be to inline Requires. Remove any unnecessary vernac.

coq-tools does this by checking a regexp of the error and rerunning coqc for each attempt. coq-lsp could do this without ever rerunning and instead of regexp we could simply check the hash of the object we are comparing.

cc @JasonGross who I believe considered working on something like this. Did the idea ever come to fruition?

[ejgallego]

It seems to me that program slicing as done in minimization do belong as a separate tool from coq-lsp/Flèche.

But indeed, coq-lsp / Flèche can provide much better support for the bug minimizer than what is actually done. For example, we can provide a structured document view, error resilience, more info about commands and their effects and dependencies. Moreover incremental checking should provide large performance gains in some cases.

Also as coq-lsp can work over multiple documents, inlining requires is not often needed. For example, you could have a .lv file that is something like:

:file foo/bar.v
:contents
Definition foo := 3.
:end
:file foo/moo.v
:contents
Require bar.
...
:end

When coq-lsp opens this file, it can split it server-side and work as if many files were found.

[Alizter]

@ejgallego The reason we inline requires however is so that we get a minimal .v file at the end. I'm not sure I understand your point with multiple documents?

[Alizter]

The feature I am envisioning here is we literally have a button: "Help, Coq is giving me an unexpected behaviour". We minimize and help the user produce an issue upstream.

Of course none of this would be needed if Coq didn't have bugs, but that is not the reality. i think coq-lsp can save a lot of users a lot of time in this regard.

[JasonGross]

See also JasonGross/coq-tools#56

The short answer is that I don't have time to work on this, alas.

---

The basic functionality would be to inline Requires. Remove any unnecessary vernac.

The other big important pass is admitting the proofs of unneeded lemmas and definitions.

---

Is there a reason to bundle this feature with coq-lsp rather than have it as a separate package built on top?

I think minimization would go faster if we avoided inlining requires until after minimizing the file being required, both because the current implementation tries to remove things it's already tried to remove after inlining, which is only rarely useful, and because sometimes files cannot be inlined, but would be inlinable if some constructs were removed. See also JasonGross/coq-tools#102

---

A more minimal version of this feature could just aggregate the current file and its recursive dependencies in order into a .lv file and prompt the user to upload the file to a GitHub issue with @coqbot coq.version minimize uploaded file. We'll have to tweak the bot to recognize this format of request, and tweak the minimizer runner to split the .lv file, build a _CoqProject + dune file or coq_makefile, and run make or dune, but I expect the server side on all this to be only an hour's work or so, which I could probably find time for at some point.

This has the benefit of not making the user wait for hours without touching their project while the bug is minimized locally.

[ejgallego]

.lv files are mainly helpful for two reasons:

• they help avoid inlining, which is often brittle and hard to implement.
• the provide an atomic and incremental protocol for the minimizer to work on several files, so the minimizer doesn't have to worry about make dune or whather other stuff is needed, and moreover, coq-lsp will check the whole thing incrementally.

So the minimizer doesn't need to do any split for .lv (except maybe internally?) just slice, send, wait for results, and re-slice.

Is there a reason to bundle this feature with coq-lsp rather than have it as a separate package built on top?

I am not sure if you are talking about error recovery or .lv files, but indeed, there are many good reasons for both to be in coq-lsp instead of externally. For .lv files mainly the main benefit is atomic and incremental, for error recovery, many heuristics are too dynamic so they need to be programmed (they don't have to be programmed in OCaml tho, we could use Pyml for that), handling error recovery synchronously has a lot of advantages, and is critical for incremental processing to work well.

The other big important pass is admitting the proofs of unneeded lemmas and definitions.

This step should not be really needed, note that coq-lsp has pretty good error recovery, and moreover can indeed skip proofs, but what to do depends on the slicing algoritm used.

fleche has already built-in support for replacing proofs by arbitrary stuff (used for example to replace all proofs by by hammer. and compute baselines, so indeed you can just replace proofs by Qed., or just tell coq-lsp to be lazy and not check these proofs (they will be auto-admitted)

The way I would approach the problem is to define an abstract interface for the slicing algorithm, and then see if coq-lsp can provide the needed information for the algorithm to run. Info we have now (or would be easy to add) is:

• file dependencies
• lemmas dependencies
• timing info
• structure (interactive proofs, sections, modules)

Then we can provide quite custom diagnostics in terms of errors.

[Alizter]

Can we compute dependencies on hints and instances?

[ejgallego]

Can we compute dependencies on hints and instances?

I don't know, what are those?

[ejgallego]

The part they depend as CIC terms, yes we can, using the same device than for lemmas.

[JasonGross]

Is there a reason to bundle this feature with coq-lsp rather than have it as a separate package built on top?

I am not sure if you are talking about error recovery or .lv files,

I was talking about @Alizter 's (apparent?) request to have bug minimization as part of coq-lsp.

[Alizter]

I think I misunderstood some of the earlier discussion.

It seems to me that program slicing as done in minimization do belong as a separate tool from coq-lsp/Flèche.

I read that as "the minimisation stuff should live outside of coq-lsp". But really I see that the dependency analysis etc. will be something lsp can offer and the bug minimiser ought to use these features of coq-lsp to do its work.

I guess this issue shoud rather be: Which features should we support in coq-lsp to make the job of the bug minimiser easy? I think what @ejgallego suggested above with the abstract interface is the direction we should go.

[JasonGross]

The other big important pass is admitting the proofs of unneeded lemmas and definitions.

This step should not be really needed, note that coq-lsp has pretty good error recovery, and moreover can indeed skip proofs, but what to do depends on the slicing algoritm used.

We want to skip not just opaque proofs, but also transparent proofs that don't matter. (Otherwise minimization would not work well for, e.g., HoTT and UniMath.)

The slicing algorithm is not very interesting, you just remove one block at a time sequentially in reverse order. A block is either a vernacular command (such as Require) or a definition/theorem with it's associated proof. The interesting case is when you have Program, you want to remove all the obligations simultaneously.

I guess with coq-lsp you want to do a tree-like removal: first try to remove everything in a file before removing it's contents; try removing sections and modules before removing their contents.

---

In order for dependency information to be useful, you need to operate on statements, not CIC terms. A lemma depends on all tactics used to prove it, auto introduces a dependency on all hints used (or at least all the successful ones + any term that is used in Hint Cut + all the failed ones if there's a timeout around the call to auto), a tactic depends not just on successful cases but on all terms mentioned in the tactic, etc. In the bug minimizer, it turned out not to be useful to try removing recursive dependencies all at once at any level more fine grained than "file". It was faster to just try removing lines one by one. (It was useful to first try skipping all proofs though, and only if that fails to reproduce the error to try skipping proofs one by one.)

[JasonGross]

Which features should we support in coq-lsp to make the job of the bug minimiser easy?

Ah, okay. The features are:

• tree structure presentation (lv file -> individual files -> module tree -> sections -> list of vernac + definition/lemma & associated proof -> individual sentences) (it is essential to group proofs with their definitions; it's nice but not essential to group obligations with their Program)
• ability to replace proofs with admitted on a per-definition basis
• ability to split Require Import/Export into Require & Import/Export, and then to split & absolutize these so each Require is for one file and each Import/Export is for one module (note that absolutizing is required for robust splitting of Import/Export)
• caching, so that if I change a bit in the middle of an lv file, recompilation is the minimal necessary (but it must not ever be the case that a bug shows up only when there's no cache)
• ability to remove all lines that occur after an error in a file
• access to error message text so we can check if the error message has changed in meaningful ways (changing universe numbers, for example, don't count as meaningful)

Nice to have:

• splitting a Definition := into Definition. exact. Defined
• tree structure for tactics to attempt removing, e.g., cases of a match
• ability to fetch the goal and context at a particular point so we can try replacing Lemma ... Some long script leading to the error with Goal ... final tactic invocation only