The Coq mailing list

[Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>]

    I support the fact that this is a common need. MetaCoq suffers quite
    a bit from lemmas that were not moved to their "right" place when
    proven, and now untangling the whole thing has become rather tricky
    (if I remember correctly, one of us tried such a large-scale
    reorganisation and got lost in it). Having a way to automate this
    task would make the cost of these reorganisations much lower, and
    hopefully with a lower access threshold we would have less of these
    ill-placed lemmas in further development.
Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 11/10/2023 19:01, Abhishek Anand wrote:

CAB44C3ksfCf8zyN6QUsUvx+Cj7ODac4mm48uBxxXnK3Mu94VEQ AT mail.gmail.com">

My use case is quite common I think.

When working in a proof in X.v, if we need to edit a definition D which either already exists in Y.v or doesn't exists but belongs there (X.v imports Y.v), we often write/copy D right there in X.v (often with Set Nested Proofs On). Then, during cleanup, we do need to move it to Y.v. Sometimes, the Y.v does not even actually exist.

(For example, in our work, we follow a convention of having the specs functions defined in Y.cpp in Y_cpp_spec.v and the location of the latter is precisely determined by the location of the former.)

With lots of imports and section variables and notations, it often takes even 20 minutes to upstream D to Y.v

Most of the time is spent in figuring out the missing imports, which should be completely automatable, at least for most usecases: we can look into the fully elaborated definition of D in X.v (I hope Set Printing All always prints fully qualified names of all the referred-to constants). company-coq's jump to definition does a good job of splitting the fully qualified name into the logical path of the .vo file and the rest, although there are some corner cases.

Set Printing All will miss the imports of files containing the notations used in D. But I think .glob files record where the notations were defined (I guess that's what coqdoc html uses to hyperlink notations to their definition sites, e.g. in this page, click at any reference of ≼ https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html)

Our build system can tell the logical path of a .v file. Some parsing may be needed to figure out which notation scopes to open and which modules to open if the notations are hidden under a module. This is where some help from coqtop/coq-lsp would be nice.

Then, often some time is spent adding the missing section variables. Figuring out the "missing" section variables in Y may be tricky (especially if Y.v already exists and has some section variables) but under some common discipline, this should be doable. I do not yet have a formal characterization of this discipline but given that when I do it manually, it is never hard (it is often tedious), I expect there exists one that covers majority of use-cases. The IDE could try to instantiate the full definition of D X.v (after closing sections) with the existing section variables in Y.v to figure out which ones already exist and which ones need to be added. Typically, there are not more than 10 section variables so even some bruteforce approaches may be feasible.

It would be nice to offload this computation to coqtop/coq-lsp as much as possible instead of my GPT-generated elisps for company-coq, so that other IDEs can benefit more easily as well.  One API could be to add the following to commands coqtop (I know coqtop well so I am using that as an example, but something similar may make sense for coq-lsp as well)

1) ExportContextInfoRelevantToLastSentence: when this command is sent just after a Definition/Inductive, e.g. D in X.v, it records all the contextual info relevant for the body of D to typecheck *exactly as written by the user*. the output could be in a file, say /tmp/D

2) ImportContextInfo /tmp/D: when this command is sent at the destination point in Y.v, it will suggest all the missing imports, context variables, notation scope commands so that if the next command is D, it will typecheck exactly as written during the export.

(Please let me know if I should post these questions on the Coq zulip. I was not sure whether everyone who could help me is on Zulip. I myself tend to forget to open Zulip for years, but emails are harder to miss)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Oct 11, 2023 at 11:17 AM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

What is your use case?  It sounds like this would be useful to extract a definition to a simpler (minimal) environment for study or debugging.  Or is it meant as a refactoring (inserting the definition into an existing file)?

I'm not aware of a command that outputs the information you need.  It shouldn't be conceptually that difficult to add for someone who knows the internals.  Doing your own parsing is likely fragile because parsing Coq input is complex (eg interpreting notations).

It would be good if tools like this could be integrated as plugins in Coq GUIs.  However, I'm not aware of any plans to support that.

Jim

On Tue, Oct 10, 2023, 9:22 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I have been planning to build a tool to move a definition/inductive/fixpoint (no proof script, for now)

from one file to another file. Has someone built something like it already?

The objective is to change the environment at the destination so that the exact text of the definition type checks at the destination (vs elaborating the definition e.g. using Set Printing All).

It seems possible for the tool to automatically add the missing imports and missing 

section typeclass variables (under certain discipline assumptions). Obtaining the body of the definition at the source location after closing sections doing "Set Printing All" seems to be very helpful here, as is "Locate" and "Locate Library" at the destination, though I haven't yet figured out all the details.

What I have less clue about is notations: how to recreate the same notation environment at the destination?

Is there a coqtop query to print the state of open notation scopes at a point?

Maybe I can read the .glob files to figure out where the notations are defined and import those files. But I would also need to parse the notation declarations to figure out which scopes to open. Some coqtop support would make things much easier.

Also, if people have some corner cases in mind, please let me know.

-- Abhishek

http://www.cs.cornell.edu/~aa755/