The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

>  Has someone built something like it already?  (From your first message)

Not that I'm aware of, but OTOH I don't spend any time proving anything other than toy proofs, so I'm not the best person to comment on that.  Assuming that there isn't anything existing that addresses your needs, I suggest the following:

> I was not sure whether everyone who could help me is on Zulip.

Most of the main Coq developers are on Zulip.  I use it occasionally.  The quality of the responses vary.  Often you get only short comments.  And it can often be challenging to get help.  If I were you, I would write up a fairly complete, detailed description of how the tool should work for the user (with examples) and submit this as a GitHub issue (an enhancement).  And include what you can about what work may be needed to implement your proposal.

You could also do a CEP (Coq Enhancement Proposal), which has a bit more process and overhead attached to it.  Both of these will let others comment on your ideas and you can revise your proposal as needed.  IMO these are more likely to get useful feedback.

> 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 exist but belongs there (X.v imports Y.v), we often write/copy D right there in X.v. ...  Then, during cleanup, we do need to move it to Y.v.

If the definition exists, why can't you refer directly to the existing definition?  That would be simpler for users (no cleanup) but if it requires changes to Coq then it's probably more complex to implement than the tool you suggest.

A few specific thoughts:

- You may be able to do a lot of what you want by writing a Coq plugin with commands.  But some of it may mean enhancing Coq itself to make info accessible.  Perhaps you can write the needed commands to stdout rather than creating a file and an import command.

- ExportContextInfoRelevantToLastSentence works on X.v as you say above, or perhaps you meant on Y.v?  It may be easier to implement (and harder to use) if it's inserted after D in Y.v.  There should be internal data structures that tell what notations, sections, imports, etc. are available at that point.  If it's in X.v, all that information probably has to be saved in Y.vo--more complex.

- There's probably no code that will tell you exactly which notations are used for D.  A more brute force approach is just knowing and exporting all the available notations at that point.

- Wouldn't you potentially need to handle recursive definitions, e.g. D depends on E and so forth?  That makes it even trickier to get all the right data automatically.  But you could leave it to the user to add E in a separate step.  Or a variable V may depend on another variable W.

- The user may need to edit the generated output, e.g. to remove notations and imports that already exist in X.v.

It's probably best to think through everything you aspire to (identifying the easy/hard parts) and then for implementation, starting with the simplest parts.  Cut corners judiciously.  You could start with commands and then later migrate the tool to work through coq-lsp.

Others may give different advice.

Hope this helps,

Jim

On Wed, Oct 11, 2023 at 11:02 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/