coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] moving a definition to a different file
- Date: Wed, 11 Oct 2023 14:01:29 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f42.google.com
- Ironport-data: A9a23:yfLPFqOfMw56zrnvrR3RksFynXyQoLVcMsEvi/4bfWQNrUoj1T1Rz WFJD2rXMv6Iamr2KoxwbojioBsH78PVyt5iQHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYATNNwJcaDpOsPvb8Uo35pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXWfSC06OhPHHgfOLBBwMQpPH5g6 M4hfWVlghCr34pawZq+Q+how9smdYzlYNlZtXZnwjXUS/0hRPgvQY2QvY4ejGp235oeW6qED yYaQWIHgBDoahdPO0wXBZF4leGhgHW5cjxEp3qaoKM25y7YywkZPL3FaYGNJYfXFJ0M9qqej l3/0H/HKzdDCOKa2zy1wzWN2cLhoAquDer+E5X9rJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924QBjh5XDY5FgTXN1fF+B84waIokbJ3zuk6qE/ZmYpQLQbWAUeHFTGD 3fYxIu7Ni8lq7CPV3OW+5GdqD74a2BfLnYPaWVABUEJ6sXq6tN7xB/ebMdRIIjshP3MGBb03 2+rqgo6jO4tlsIl7fiw0m3GpDOOnaL3aDAJyD/ZZF/40TMhVrWZP9SpzXP58cd/KJ2oSwjdn XocxOmbwuM8LbCMsy2vRu8yMqmjzKuHOmeEgHpEPZooxxKy8VGNIKFS5zBfIh9yE8AmIDXGX m7aiTlz1rRyYkS4TPZQSJ2jLugX1o7cLMTBetGIS8tRc75zWRSi/iozVXWP3mvorlcgoZs/N bifb8yoK3QQUoZj8xabWMYf1q0N1Akl5GaOW63+8Qur4YCeaFGRV70BFlmENcI9zaGcpTTq4 8RtDNSLxzpfQd/BTHHuq6BLFm8zLF8/GZzSgO5UfLTaIgNZRUcQO8WIyrYlI4FYj6BZk9nTx U6EW2ha9gvbpWbGIgC0eHxceOvRfZJgn0kaYw0oH3iVgkYGX6j+zZ0xVZUNeZsfyNdC1t9xF vkMRNWBCK9ASxPB4DUsUqP+p41DKjWuiR6/AC6+RD0ZYZRbZhfo/+X8dVDF7xg+DSuQtOo/r Ya/1wjdf4ExegR6AOvSa9Ot11mUv0VBvM5XQG3zPYB1VGj31YplOQjdr6USGN4dDwfHyh+x9 RekMT1Bqcbj+4YKocT034aapIKXIs5CN0t9HUyAyJ2pNCPfr1GR8aUZXMmmJTniBX7JooO8b uBoztb5Av0NvHBOl6FeS79L76YP1+HDlo9g7DZPPSv0NgywK7ZaPHO589FFtfRNyp9nqAKGY B+z1ecAC4qZGvHOMQA3FFI+Y/WhxMMkvGDYzc4ILXXQ4A51+7u6UntuASSctRwFLJVJHdMk5 cwDpP8p7xeOj0t2E9Se0QFR2We+Dl0BdKQFqqAlBJTPugY372obZLrwKzLEusCRWY9cNm0vB CGev4vZprFm3kGZWWECJXvM+ut8hJo1pxFBymEZFWmJgtbogvwW3gVb1CYeFCB570xg/bpoG 25JM0ZVG/2/zw1wjpIeY1H2ShBzOhKJ32fQlX0LrTT9ZGu1XDXvKGYdB768zHoB+TgBQgkBr aCq80e7YzPEZ8qr4zATX3RioPndTdBc0A3OtcSkPsadFakBfjvXrf6yVFUMtifYL5s9tG/fq clu2dRAW6nxGCoTgq88UoekjOVaDFjOIWFZWvhu8Z8YBWyWKnn4xTGKLFv3Yc9XYeDD9UijE cF1O8ZTTFKE2T2TqiwAT7s5S1OucCXFOPJZEl8qGYIHj1dbhj9gsZaV6S2nwWF3GZNhlsEyL o6XfDWHeoBVab24hEeVxPSo+ELhCTXHWOE49O+w+eQNUZkEtYmAtGksh6CssSz93BRPpnqpU cCqW0MS5+NnwIVo2YDrF82vwulyxczbDIy1zex4jziCgR4j/ysDW8P5Z2QL5zhrAIY=
- Ironport-hdrordr: A9a23:Cpp7FKp+VFbNLhDmpCtj4LIaV5oaeYIsimQD101hICG9Ffbo9f xG/c5rtiMc7Qx6ZJhOo6HmBEDtewK4yXcK2/hpAV7SZniDhILAFugLhuvfKlXbehEWndQts5 uIHZIOcOEYzmIXsS852mSF+hobr+VviJrY/ts2Bk0CcT1X
- Ironport-phdr: A9a23:OBSOWRZD64pya+wi/3C2KmP/LTFU2YqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1g+PANWQsqsYw6qO6ua8AzJGuc7A+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohA c5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/I Au1oAnLtsQbgoRuJrssxhbGv3BEf/hayX5yKV+cgRrx59288IJ//yhVpvks69NOXaLmcqoiU LdWFi4mM2c75M3qsRnMUw6C7WYCX2sVjxRFHRHL4An1UZntvCT6sPF92DSBMs3tUb80QzWi4 Lx1RxLulSwKKiQ28GDTisx3kaJbvBesrAFxzoLIfI2YMud1c6XAdt0YWGVBRN5cWCNPAoy+b 4UBAekPM/tGoYbhvFYBtweyCBO2Ce/z1jNFhHn71rA63eQ7FgHG2RQtEs4Vv3TUrdX1L6cSX v62zKLV0TjDaelZ2THg54PVdR0uu+qDXbJxccrKyUkgCQDFgk+KpozjJTyV0PkCv3Ka7+phS eKvhHUqqw50oje1x8csjpPFiZ4SylDB7Ch0xps+KtKkRkBhe9GkDIdQuD+AN4twWs4sTH9lt SUnxrMJp5O1fCgHxZQ7yxDQd/CKboaG7BL+WeuSPzp1hnZodbOhihqu8Uat1PHwWteo3FpXo SdInNjBu3YQ3BLd7ciHT+Fy/kan2TuX0gDT8uBELVkvlavVMJ4t2LkwloAcsUjbAiD2n1/2j KmIeUUg/uik8frobaj7ppKaKoR6iRn+P7wwlsCjBek0KAsDUmiB9eihyrHu/lf1TbpUgvAwj 6LXqorVJd4Bqa68GwJV0pgs6xK4Dzq+1dQXh3gHLFZcdBOJiojlJkjCIP73APuhmVisnzBrx /fJPr3lHJrBNGTMkLDkfbpl6k5czhQ8zcxH6p5KFr0MJOj/V0zxudDCExM1LQ+5z/zoBdljz o8eXHiAAq6dMKPcq1+I4ecvLvGWa4AOuDb9KuMl5/7wgn86g1MSZ6+p0oERaH+lBPhmIkSZY WbjgtoaHmcKuxAxTO3uiFGYTTFTYHOyU7o65j4gEI2mF5vMRpixgLyd2ye2BoBaanhcCl+QC Xfoa5mEW/AUZS2OJc9hiyUIWqSlS488zh6jrxT6yrpiLurM4CIUr5Pj1N5v5+3Sjx4+7zJ0D 97Om12KGmpzhyYDQyI89KF5u010jFmZgoZihPkNPNZT5uhJXwRyHJjVyeAyX9n4WgPaftqKD l+gS9OqRzAwUt0ZzNoHYkI7ENKn2EOQlxG2CqMYwuTYTKc/9bjRiiCZz6dVzn/H0PNklFw6W o5VMmbggKdj9g/VDoqPkkODlq/se75PlDXV+jKlymyD9FpdTBY2Sb/MCHkVZkrNrdn6oErER rmiT7UmLgRpxsuLK68MYdrs3h1dXPm2AN3FeCqqnnuoQxOBx7eCdo3vLmwX3CTGCEUH1QkV9 HCKcwk/GiiJrGfXDTgoHlXqMAv36ecrjnS9Qwcvyh2SKU1s073g4hkOmfmVUO8exJoBsSYl7 ipxRROzg4iQBN2HqA5sOq5bZLvR+X9h0mTU/0x4N52kdeV5g0IGNh5wtAXo3gl2DYNJlY4rq mkrxUx8M/DQ1lQJbD6e0Z3qX9+fYmDv4BCibbLX0VDCwZ6X/KkI8vExt1TkukmgCEMj93xt1 9Qd3WGb493GCw8bUJS5VUhSlVAyrrvaYzI96oCS3HtlN6Xysz7e1PomAeIkzlCreNIeeKKIG QnuEtELUtC0Ib9P+RDhZRYFMeZOsa8sapn+Jr3WhejyZrYmwGj16AYPqJpw2U+N6SdmH+vB3 pJfhuqdwhPCTTD3ylGorsHwn4lAIzAUBGu2jyb+V+szLuV/e5gGDWC2Loi53NJ70tTkUX5Z7 16uBBUP3savdVyTbkDy9QJV3EUT53egnGHrql482yFstaeZ0CHUlq7rfhoGIW5GRy9ri17qL c61jswVdEetZgkt0hCi4AyposoT7LQ6JG7VT0BSeiHwJGw3Saq8uI2JZMtX4Y8puyFaOAilS WiTUaW14x4T0ie5WnBb2Ch+bTah/JPwgx19jmuZand1tnvQP89ql1/T49nVRPgZ2TRjJmEwg DPXB0O8Mtrv9NOdkZuFs+GiWEquU5RSdW/gyobIuCag5GJsCAGyhLjpwoyhQVV8iHWrkYUwH SzTyXS0KpHmzaG7Lf5qcgFzCVnw5tA7UoByn40shY0BjH0Th5Gb530Cwi/4NdRW3767bWJYH 2ZahY6IplG/iAs/dCHspcqxTHiWz8p/asPvZ2oX3nh49MVWEOKO67cCmyJpo12+pAaXYP5nn z5bx+F9jRxSy+wPpgcpyT2QR74IGkwNdyXmlxWT79296qxRbWCjN7mxyEVWktWoDbXEqQZZE iWcGN9qDWpr48NzPUiZmnT56oD/eNTTK9sVvxuY1RbBk+d9J5c4l/5Mji1iczGY3zVt26swi hpg2ou/tY6MJjB2/a63NRVfMyX8e8IZ/jy+xbYbhMud2JqjW4lwAjheFoW9VuqmSXhB0Javf xbLCjA3rW2XXKbSDRPKolkztGrBStiqLy3FfyRflIQ6AkPBewoHx1pIFDQiwsxnSkbwn5enK RkhoGhWvw+dyFMEy/o0ZUehFD6H/kHwLG9zEsDXLQIKvF8coR2JYIrOtqQrWHsAtpy58F7Sc CrCO0IRXDtPAgvdVzWBdvGv/YWSrLTeX7DjaaOIOfLX96RfT6vanMr/lNI5oHDccJ3IZCAqD uVniBMcBjYgSpifw3NXDHVJ8kCFJ8+D+EXmonwx/p35qa67HlqovNTHCqMOY482pVbr0eHaZ rTW3GEgeH5Zzs9enyaWjuJEjRhJ0Wc2MGD8dNZI/TjESKaa8kNOJzgcbS47dM5B7qZmmxJIJ daekNT+kLhxkv8yDV5BE13ngMCgI8IQcSm7MxvcCUCHOa7jR3WDytzrYa66VbxbjflF/xy2t zGBFkb/PzOF3zD3XhGrOOtIgWmVJhtb8I26dx9sDyDkQreEIlWjN8RriDQt3bAurnbDNGpZL j0lNk0R9Puf6iRXhvg5EGtErzJkIeSChyeF/rzYJ5IR4p4JSmx/k+NX5mh/yqMAtnkVAqwo3 nKI/pgy+QLD8KHH0DdsXRtQpywegYuKuR8nIqDF7txaXn2C+hsR7GKWAhBMpt1/C9SptboDr 7qH3K/1NjpG9MrZuMUGAM2BYsuNMHs6MRfqXjfSBQ0JCz+qKW73iElUkfXU/XqQ5MtfyNCki N8VR7lXWUZgXOsdEVhgFcceLY1fWzollfuEiZdN6ybk6hbWQ8pes9bMUffYUpCNYH6JyLJDY RUP27bxK48eY5b610JVYV5/hI3WGkDUULilQwVkZw4w5VpIqT1wEjd11EXiZQegpnQUEKzs9 vbZogR7aOUpsjzr5gVuTrIvjCQ1mUg1397ihGLJGAM=
- Ironport-sdr: 6526e327_Q15dFuB1xHZe0fhYoL6eOITyKcxH0NuBA0zkh9Xb36b2eFF 1se8cWDGS6Xv0wvUqRww+Ar44i6R/8+4TLdKtkA==
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.JimOn 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 missingsection 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.-- Abhishekhttp://www.cs.cornell.edu/~aa755/
- [Coq-Club] moving a definition to a different file, Abhishek Anand, 10/10/2023
- Re: [Coq-Club] moving a definition to a different file, Jim Fehrle, 10/11/2023
- Re: [Coq-Club] moving a definition to a different file, Abhishek Anand, 10/11/2023
- Re: [Coq-Club] moving a definition to a different file, Jim Fehrle, 10/11/2023
- Re: [Coq-Club] moving a definition to a different file, Abhishek Anand, 10/12/2023
- Re: [Coq-Club] moving a definition to a different file, Jim Fehrle, 10/12/2023
- Re: [Coq-Club] moving a definition to a different file, Abhishek Anand, 10/12/2023
- Re: [Coq-Club] moving a definition to a different file, Meven Lennon-Bertrand, 10/12/2023
- Re: [Coq-Club] moving a definition to a different file, Jim Fehrle, 10/11/2023
- Re: [Coq-Club] moving a definition to a different file, Abhishek Anand, 10/11/2023
- Re: [Coq-Club] moving a definition to a different file, Jim Fehrle, 10/11/2023
Archive powered by MHonArc 2.6.19+.