Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] moving a definition to a different file

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] moving a definition to a different file


Chronological Thread 
  • From: Jim Fehrle <jim.fehrle AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] moving a definition to a different file
  • Date: Wed, 11 Oct 2023 08:16:51 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f41.google.com
  • Ironport-data: A9a23:I6lNJa7fwFeT8z4mHKIklAxRtPbDchMFZxGqfqrLsTDasY5as4F+v jRKCGuPMvbZMGSjeNx3aN+29k1X7ZKExoMyGVdlpCs8Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsaQr414rZ8Ek05ayr4WtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj695hLUsvOs4owfgtC2IX5 6UxETERfh/W0opawJrjIgVtrsEqLc2uMYFG/388lHfWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP ppfNWMHgBfoO3WjPn8VCZd4kuqonH3yWzJdoVOR46Ew5gA/ySQvgOS3b4ePJrRmQ+1Oul6hg W7I0FjTAzUTGfa16BS4ziiF07qncSTTAdpOTtVU7MVCi1qKg2cXFRc+Tkq+ufD/i0ikWtsZJ VZ8x8Y1ha079UjuQ9ukGhPk+TiLuRkTX9cWGOo/gO2Q9kbKyy2WJ2IdSX1xU8J8vsxvV2UD7 16Vj9y8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0ts4mLTGYb3kKnczpzLEKmpoaqRmyok lhmuAB71upD15dav0mu1Qmf22rEm3TfcuIiCuzqso+N6wp4YMuoZdXt5wSCq/lHK4mdQx+Ku 31sdymiAAImXMvleM+lGr1l8FSVCxCtbmO0bblHQcRJythV0yT/Fb28GRknTKuTDu4KeCXyf GjYsh5L6ZlYMROCNPEmPdPvUZpxk/GwTLwJs8w4iPIeMvCdkyfXrElTibK4gggBbWB1zvBjZ MjLGSpSJSxHUvg5pNZJewvt+eZzmnpWKZL7Spf8wBCquYdyl1bEIYrpxGCmN7hjhIvd+Fu92 48Ga6OilU8DOMWgOXK/2dBIfTg3wY0TX8+eRzp/Lb7dfGKL2QgJV5fs/F/WU9c6z/8Jx72Wo CvVt40x4AOXuEAr4D6iMhhLAI4Dl74m8BrX5AR9Zg766Gtpeou18qYUer0+eLRtpqQpzud5Q 7NBM4+MC+hGAGaPsTkMT4jPnKo7fjSShCWKI3WEZho7dMVeXADnwILvUTbu0ygsNRCJk/UCj Yeu7D6GfqpbdT9eVJ7XTNmN02KOuWMsnbMufknQffhWVkbe0KlrDC3TiPUIDdkGAkjBzGHC1 iK9IxQRlc/SqaAbrfjLgqGlqd+yMu1cR0B1IUjS3YyUBwL7oFWx4NZne/maWBzgT0XIwbWGS cQJ6uDjIdsFsU1vsYEhI410zKk72cTjl4VawitgAn/PSVahUZFkHVWrwuhNsb9r1JZCmA7rR H+KxMZWCY+JNOzhDlQVAggvNcaH9PMMnwjt/eYHG1r76AB37Yi4fx1rZTfUsxNkLZxxLI8B6 sUispRP6wWA1zwbAuzfhSVQr2mxPngMVps8ja4jAajptFsP6kpDapniGCPJ8MmxS9FTAHILf B6QpoT/3op5+GSTUkAOBUDs3PVcj6sgoBpl7kEPDHXXl8vnhs0Y5gxw8zM2RDt71h9siuZ6O EV3BU9MNYGL8yli3sRYbVvxGQsbXBy90W7ywmsvi2f2YRSJVGvMDWtlIseL3hkT3Fx9dwhh3 oOz6TjaQxP1WsDuzw0OWUJBgN7yf+xbrwHttpiuIJWYIsMcfzHgvJ6LWUMJjBnWWeUKm0zNo LhRztZaMKHUG3YZnPwmNtO8y78VdRGjIV5CS9FH+IciPznVWBO26Ai0B3GBQOF/DN2UzhbgE O1rHNxFaDqm3iXXrjw7O78FE4UpoNEXvug9apHZDk9YlYvHtTd4koPixg6njk8Rftheu8IcK ITQSjG8LlKtlUZkw2/gkc0VFVe7MP8lZRL91t+b6O8mNYwOm8AyfFAQ0ombhWS0MgxmzUjNv Ar8eLLnlb1+6IVznrnDFrdIKBW0JOjSCsWJ0lGXmPZfYezfNfzhs1sulWDmGABNLJ0tVM9Sh 53UlPLKhGb+o6cRf0XCvpuwB41lxJ6VYrJME8TVKHJ6o3OzaPX06UFex1HieI17rtxNw+KGG S6qY9SUXvwIUY5/wHZ1VXBvIywFAf6qUpa69DKPlNXSOB0zygedEciG80XuZmRldiMlHZ3yJ wv3mvS27OBjs4V+K04YNs5iHqNHDgfvaYk+e/31kAuoPG2ir1eBm7nlzBQesGCBTjHOFcvh+ pvKSyTvbBn46umC0NhdtJc0pRENSmp0he4rZE8G5tpqkHaAAXUbKfgGe4AzYn2OfvceCLmjD N0MUIcjNck5dTFNcBG57da6GwnDX6oBPdD2IjFv9ESRA8tz6EVsH5M5nhqMIV8vEtcg8A1jA d4b83z0eBO2x/mFgM4Ns+ejj74PKuzynxo1FIOUryA2KxkbCLQOkndmGWKhkMAB/97lzC32G IT+eYyIrIxXh6I8/QaMtkO5wC0kgQ4=
  • Ironport-hdrordr: A9a23:/pc8HKmHd6hO4snvPswPhSXB/9DpDfIV3DAbv31ZSRFFG/Fw9v re5cjzsCWftN9/YgBEpTntAtjjfZqYz+8X3WBzB9aftWvdyQ+VxehZhOOI/9SjIU3DH4VmpM BdmsZFebvN5JtB4foSIjPULz/t+ra6GWmT69vj8w==
  • Ironport-phdr: A9a23:zAohURPHbV0w2CuhvPYl6nbCBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6Ur0Q+CDd2Tq6odzbaM7ea4AS1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7B/I A+2oAjSucUbgpduIbs1xhfVv3dEYetbyX1pKF6Jgxrw+sK894N//ipNvP4s69ROWrjgcaQiS rxYAjUmM2Qr68DuqBLOUwiB6GYCX2sPihZHDBTL4x/8Xpfqryv1rfF91zWAPc33Vr87RzKv5 Lp2RRDyiScHMzk58HzLisF1kalWrg6tqwB5zoXJe4yeKuZwcb3BctMbXWpBX9heVypdAoOnc oADC/MNMftEo4XholcDqwa1CwuxC+P10jJHiXH20q863eovEg/IwRIuEM4VvXvOsNn4Lr0fX fypwKTKyzjIcvNY2S366IjNah0vpfCMXbdtesTR10YvFxnFjlGOpof4OD6V1OUNs22B4+puS +2vi3QnqwVvrTW0yccsj5PGhoMRylze6Sp5x4M1KMS+RUVmbtGqDIFeuDuGN4tqXMwiWWdot T4mx7MGpZO3YCYHxZc7yhLBdfGKbZaF7w/9WeuVPDt1h3Boda+wiRuv7ESuxeLyW82q3VhKs idIjNfBuH4O2hDP7MWMV/Vz/kCk2TmV1gDT7PlJLlwzlarBLZ4u3Lowlp4JvUvdAyD2hUP7h 7KVeEU84uWk9fjrb7H8qpKfN4J4kB/yPrktl8ClDuk0Lw4DVHWB9+umzr3s50j5Ta1KjvIol qnZt4jXJcEBqa64Bw9Zy5gs6xSiAzu/3tQVkmQLIEhKeBKAiIjpNFXOL+7iAfijhFSslS9nx /HAPrL/HpXANmbPnKvlcLpn6ENRyBA/wc5C659XEL0ML+//Vlf0tNPCDx85NwK0w/zgCNV4z o4eW2OPAqqDPKPcr1CI5vgvI+2Sa4IOtzb9LuIq5//qjXMjhVAdeqyp0YMRaH+jBvtmOVmWY WLwgtcdFmcHphcyQPTwiFKeST5Te2qyX6Uk6z4nD4KmFJ7PSZypgLycxyi2BYZWZ2BDClCUC 3jkbYSEW/EWaCKTOMBtiDIEVaLyA7MmgDqprUfRz6dtZr7f/TRdvpb+3vB04ffSnFc872onI d6a1jSvTmQ8sG4IXTs7lPR9oEk7xFqDy6x1q/NdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTR QPjG43+adlQZtc4wttVJl14B83nlRfbmSyjH74SkbWPQp0y6KPVmXbrdI5m03iT8q4nghE9R 9dXc3W8j/t99g2VCYPJiUGUv6mvfKUYmiXK8TTL1nKA6XlRSxU4SqDZRTYab0rSo87+4xbAT rroB7knKA9M4cGHI6pOLNbuiAYOX+/tbfLZZW/5gGKsHVCIy7eLOZLtYHkY1T7BBVIslgkS+ TOLN1F7CHv45W3ZCzNqGBTkZEaEHfBWjnS9Qwd0ygiLaxYkzL+p4lsOguTaTfoP37UCsSNnq jNuHV/70ciEQ9yH7xFseqlRe7ZfqB9OyH7ZugphP5ehM7Eqh1gQdB5ytl/v0BM/A5tJkMwjp ncnhARoLqfQ3FREfjKelZf+X9+fYmvz+VahZq7M3lz239Of+6NJ4/M96h3isAyvCks+4iB/y dAGm3CY55jMEE8TScerChdxp0U8/eiKJHVktOa2nTV2PKK5syHPwYcsDeohkVO7estHdbiDD En0GtEbAM6nLKornUKoZ1QKJrM3luZ8MsW4ev+BwKPuMvxnmWfsj2VCpo5w0liI+gJzT+fJ2 9AOxPTSjW7lH3/syUystMz6g9UOZzAXWGSyyTLgCaZeY6RzecAADmLkcKjVjp1uwpXqXXBf7 luqAVgLjdSodRSlZFv4xQRM1E4TrBRLgAOAxidv23Esp6ubh2nVxvj6MQEAIihNTXVjilHlJ c61icobVQ6mdVphmByg7Ef8j69VwcY3Z2vSRAFGcijsK2xKXa65t77EaMlKoJ8lqiRYVu2gb EvSEOas5UtHlXm6Ty0CnXgybHmyt4/8ngBmhW74Tj47t3ffdcxqhF/e6NHaWf9Nz28DTSh8h yPQAwv0NN2o8NOI0pbb57rmBiTxC9sJKHmtkdrT0UnzrXdnChC+gf2pz9juEAxhlDT+y8EvT iLQ6hD1fojs0a2+d+NhZEhhQlHmuK8YUslzlJU9gJYI1D0UnJKQqDAFkGK1P9hbw6bzRHUIT D8PhdXS5UK2vS8rZmLM3I//WniHl4FjZtz8bG4WwCYwx89PAaaQqrdDmGEmxzjw5RKUav97k DAHzPIo43NPmOAFtj0mySCFC6wTF01VbmT80g6F5NekoOBLdX6iJPKugVFmk4nrX9Tg6klMH Wz0cZA4EWps49VjZRjShWbr5NisecGMP4lO8ETFy1Ga07cTcNVryrILnXY1Zz675yZ+jbdl1 Vo2msjr2erPY2R1oPDnXFgBbmezP4VLvWu1xadGwpTIgcb1QsQnSm1NBNyyFbqpCG5A6q6hb lrISWxm7C/cQOq6f0fX6V86/S2TVcnxajfPYiFelIsqRQHBdhUH0EZNA2p8zthhUVrzjM35L BUguWtXvw+k7EMKkqUxaXydGi/evFv6MG9lDsjCakMMvkcaoB6Kec2GsrApRn8eo83n9V3Xb DTcPlUADHlVCBbdWRa5ZejovoOGq6/BV4/cZ7PYaLGK44SyTt+uwpSimstj9jeIbYCUO2V6S uY8wgxFVGx4HMLQn3MOTTYWnmTDdZzTohD04SBxos2llZajEAvy+YuCDadTOtRz6li3h6mEL euZmCd+L35RyJoNwXbCzLVX0kQVjmlicDykELJIsiCoLuqYgqhMExsScD9+LuNN5qM4mwRPY IvV1oqz2bl/gfo4TVxCUB2pm82kY9ALP3DoNF7DAxXuVvzOLjnKzsfrJKKkHOcI3aME6lvq4 GbdTxawW1bL3yPkXB2uL+xW2SSSPRgF/Zq4bg4oEm/7CtTvdhy8NtZzyzww27w9wH3QZgt+e XBxdV1AqrqI4GZWmPJ6TiZD738jI+SEgSKUx+bdI5cS9/BsB24n8oASqGR/0LZT4CxeEbZtn zDOq9d1v1y8uuyGyz4iXRgX7zgX3cSEukJtPaif/Z5FEyWhnlpF/SCbDBIEoMFgA9vktvVLy 9TBo6n0LS9L79Pe+cZ07y38J8eOMX5nOh3sSma85OotSDeqMSTShRUYnq3LsHKSqZc+p97nn 59cEtezu3Q6E/obDgJuG9lQef9K
  • Ironport-sdr: 6526bc6f_Z5NH774hMBXTAEAf/dQHmpKlJdOXKnrpxOtrF4VSEyefSoO UhZt5lse+siKA4N2s26UzXz2D2Kl0JW2LVAbcag==

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.







Archive powered by MHonArc 2.6.19+.

Top of Page