The Coq mailing list

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

>  I suggested a file because I think the output would be huge. In case someone wants to use this feature without an IDE, manually copying and pasting may be an unnecessary burden. with IDE support, stdout would be fine too.

Yeah.  In an IDE it may be possible to put it directly into the clipboard.  FWIW, we no longer consider coqtop as a realistic development environment for Coq.  But no plans for it to go away, either.

> I am not asking any change what gets stored in .vo files. this tool does not need any change in coqc.

It's certainly simpler if that's not necessary.

> .glob file/coqdoc hyperlinks all notations to their definitions, right? what would we miss?

I think you'd want to filter the universe of all notations rather than add every single one to your output.  I don't recall whether redefining an existing notation gives an error message or not.  In either case, it leaves a good bit of cleanup work for the user.  Identifying all the notations used in D from its string is not trivial.  I'm pretty sure the notation use info is not preserved in the .vo file.  You may also need to include notation scopes which can turn notations on and off.  OTOH, users may want to import more than just the items that are referenced by D.  If they're going to edit D, they may prefer all the relevant items that are in scope where D was defined.

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

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.

Because it may take 10 minutes to rebuild Y.v and all the deps between X.v and Y.v . .vok builds may help a bit but the context switch overhead may still be large. 

 

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.

I suggested a file because I think the output would be huge. In case someone wants to use this feature without an IDE, manually copying and pasting may be an unnecessary burden. with IDE support, stdout would be fine too.

 

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

No, I meant X.v, where the (new) definition of D is already known to type-check correctly. if we want the context in Y.v to match that point in X.v, we need to know what the (relevant) context was just before (or just after) D in X.v. The Export is to be done at the source of the definition, the Import at the destination. I am not asking any change what gets stored in .vo files. this tool does not need any change in coqc.

 

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

 

.glob file/coqdoc hyperlinks all notations to their definitions, right? what would we miss?

 

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

This is a great point I had not thought about but it does show up in practice: I move D from X.v to Y.v and then realize that D also depends on F in X.v so that has to be moved as well. Perhaps the ExportContextInfoRelevantToLastSentence  command should warn/fail if D depends on some definition, say F,  in the same file. The user or IDE will then first move F

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

a goal is to not add redundant imports. the Import command is supposed to look at the existing context in Y.v at the insertion spot and match with the export from X.v  and only add the missing bits