coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] moving a definition to a different file
- Date: Tue, 10 Oct 2023 12:21:38 -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-wr1-f42.google.com
- Ironport-data: A9a23:QY29I64P8yPObDk3KCZIYgxRtEzCchMFZxGqfqrLsTDasY5as4F+v mYXWWvXb6uOZDanedl3OoXno0IC6MSHmocwQAdk/C0wZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UoYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhXgsaQr414rZ8Ek05ayr4GtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/U1BlgYN7wxwcVMMz0Xy v8yIxktTQ/W0opawJrjIgVtrsEqLc2uI5lG/388l3fWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP ZNfNWAHgBfoO3WjPn8eApI/h+elhT/2dTRepBSUpLY4y2fWxQ11lrPqNbI5f/TTHp0JzxnC+ TquE2LRIhFKHoSC+Qi5+yirv8DvhAHcdLJCLejtnhJtqBjJroAJMzUdUkL+qv2kgGalStdHI goV/DAvpO487iSWosLVWhS5pDubpEdZVYYKVeI97w6Jx+zf5APx6nU4cwOtoecO7KceLQHGH HfQ9z8wLW006O+mWjiG+62KrDi/HyEQICVQLWUHVAYJqZ2r6o06khuFHJ4pHb+Xn+/FP2j64 wmLiywi2JQVr8oAjJug8X793jmDm5nuTywO3DvxYF6L1A1CSbCAW52J8nnetPZJE5aYRAKOv V8CgMmv09oNBpCsyg2IGeUEI661662kIBnjsAZKHsQn/W78/XSMQJ1humBiBUZ2M/QrfS3iT 1/TtDhwur5SHiqORo1mb72hD/8FyfDbKu3kcfTPfP9iU4NUdjLbzBpxZEWV4X/hoHIsnY47J 52fV8SmVlQeNohK0xu0QL07/YIw5yVj217We4/3/y6n3ZWaenSRb7UPa3mKT+Ih6ZK7sBfny MleO+SK2idgfrXHOAePyrEqLHcOMXQfLrL1oZYOdue8fyxXKFt4APrVmb4ca4hpmppOrdjx/ 1a/ZB586EH+jnj5Owm1eihdSLfwb61e81M/HwIRZGiN5VZyQLyBzqklc7kPQYIG781mlP59c OkEcZ6PA9NJUTX2xA4eZpjc8q1neAiaugaVGy+DfjIEXoVBQjbR8YTOZTrf9ygpDwu2u/Aho ram6BjpfJobSylmD+fUcPiKzW7tmVQ4h8RJQBLuDvRIXUfj4qxGCnbUteAmBdMIJTHo5Cqo5 yzPDTg2/eDy8pIIqv/XjqW6nqKVOupZHG8BOkLE7LyzZBLozkD6zaBuCO+3LC3gDkXq86CfZ MJQ/fH2ENsDuH1o64NcMbJa/ZgS1uvVhY1x71pbRS3QTlGRFLlfDGGM3pBPuo1z17Zpg1aKd XzVyOZKG4eiGZ3DIAYKKRsHf9az86geugPv4MQfJGT44y5K/4S7b3hCAinUtgtjKOpaDYB05 8Ygp88c1CKngDUILNutr35Z5kaMHFM6QoQlsZAoWtbrgzU012AYMID9CzD30r6Led5jIkknG R7Kpavg1pB35FvOTGo3LlfJhdFivJUpvAtb6mMNPHGbs4PhqsJv+SZO4BMbax9wzCRX985SY U9Vb1ZUI4eK9BdW3PlzZXimQVx9NUfI637PxEssv0yHalujSUjmDnA3YMSJ92Anq1NsRCBRp uyk+Ty0QATRXZ/D2wUpUhRYsN3ld9t68zPClO2BH8ioG5obYyLvspSxZFgn+gfWPscsuHLp/ eVa3v58SaneBx4ip6cWD4q717NJRi7ddSYGCbtk8bgSFG7RRCCq1HLcYwqtc8dKPLrR/VX+F 8VqIdlVWg+j0DqV6AoWHrMIP6Q+ictBCADuoV83DTVuX3qjQjtVXFb48yH/gCo0WYwrn5pnb IzWcD2GHyqbgn48d6ohaiVbEjLQXDXGTFSUMCOJHCEhGJcKseUqekY3uldxl2vAKxNppnp4o yuaD5I7DIVeJUBEkI7lE6EFDAKxQT82uCJk7yjr2+lzgRjz3Qsieu/bRpQL/+ibAFfJZ+lKq A==
- Ironport-hdrordr: A9a23:wFPOxKiOxgu1zqc4YexjsliP53BQXtcji2hC6mlwRA09TyX4rb HIoB1/73XJYVkqKRIdcLy7WJVoIkm8yXcW2/hyAV7KZmCP01dAR7sSiLcKrQeQfxEWNdQw6U 6jScVD4RHLYmSSRPyV3DWF
- Ironport-phdr: A9a23:6XNVuR3Qee6TVK2JsmDOzg0yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaPo6gwxw6XFcWDsrQY0bSQ6/ihEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCS+bL9oL Bi7rQrdu80XjIB/Lqo91gbFrmFHduhIxG5kP06fkwr56syt4JNt7iNctu47+cVdS6v6ZaM4T bJZDDQiLW844dDguAfAQwWS+HYSS30anRVUDQfL6hH6RYrxvTDhtuVhwimaPNb5Qq4yVD+/8 qpkUh7oiCMANz4k7GHaj9F7gaxHrB69oRF03ojZa5yXOvVjZKPQZdwVS2pPUMhSSiJPHJ+zY pAVAOYdJ+tVtZXxq0cMoBa4GAKiBPnvyjhNhnLuwaA1yOQhEQDd3AwgAd0Os2nfocnzNKgIV +C60bTDwDLZYPxN2Tf96ZPIchA/rvGPR75/a8zRxlMpFwzYlFmQqI3lPy+a1ukWvGib6vBvV eOri2I9tw5xpT2vy94qh4LUiY0b1krK+j9lwIYpO9K4Ukh7bMa6HZVQqSyXKoR7TMw/Tm12t is21L4LtIK1cSYK1pgqyBrSZv6af4WK/x/uVOafLDV7iX9nZL6zmQi+/Eujx+DyUMS/zVhEr i1AktbWt3AN0QTe5dSASvtn+EeuxzKP1wTJ5u5aPE80iKzWIIMizL4ojpcfr1jPEyvslEj1j KKabFso9va15+j9bbjquJmRPJJuhA7kKKQhgMm/DPw4MgcQW2ib/vyx1Lj58k34RLVGl/M3k rPEvJzDK8QWqbC1DxVa0oYk7Ba/ADOm38oCkXYbK1JFfQqLj4nvO17QPPD1Femzj0ionTtxx P3LPqftDovTInTeirvscqhx51ZZyAUpzNBf45xUCqsGIPL2QkL+rsfXDh84Mwyvw+boFtZ92 pkEVmKJGKCZNr7dvUWJ5uIuP+mMa5QYuDn4K/c/5v7uiWU1lkMafamsxZcXbmu3Eex8I0qFe XrsnssBEWASswYjVODqkkGNUSZPZ3auWKIx/i00CIW/DYvaWo+thKGB0zygE51NZmFGD0iMH m3ye4WFXfcMciOSLdV7njwKT7jyA7MmgBqprUrxz6dtZr7f/TRdvpb+3vB04ffSnFc872onI d6a1jSkRWF1hWMFRHcf2ql5rQQpw12D0LN4jv8eHNpa4f8PUwYmOrbTyuV7D5b5XQeXLYTBc 0qvXtjzWWJ5ddk22dJbOy6Vev2nhxHHhW+xBqMN0qaMD9oy+77d2H74I4B8zWzH3e8vlQpuW dNBYEuhgKM37A3PH8jRiUzMnqyqdL8c0S2L/WGKy2bIvUBEXyZ/VKzEWTYUYU6F5c/h6Bb6R qS1Qa8iLhMHzMeDLqVQbdi8hF9GRezjNdeYamS4nWv2BBeUyZuDaYPrfyMW2yCOQFMcnVU1+ nCLfRM7Gj/no2/aC2l2EknzZkr37eRkgHayT0tx0BvTKkM9jfy6/RkagfHaQPQWtl4dkAEmr Tg8XFO03taMTsGFuxIkZqJXJ9U0/FZA02vd8Q17JJ2paa541BYYdExsskXi2g8SaM0ImNU2r H4s0At5KL6JmFJHeTSC2JnsO7rRYmDs9RGrYqTS1xnQytGTsqsI7f05rR3ksmTLXgIr+XVmy NlY0D2V4JzMAEwTUI7+ekky/hl+4brdZ2h15o/Z02FtLbjhqiXLiLdLTKMuzhetecsaMbvRT lejVZ1HQZL0cap2wQvMDFpMJu1Z+a8qMtnzcvKH3PTuJ+N8hHe8im8B5olh00WK/i46S+jS3 p9DzevLu2nPHzr6klqltdj63I5eYjRHVGO1ySn/BINSIKR0dIAHT2avP8KfydB3hpqrUHldv g3GZRtOyIqydByeYkaolwRa1UUMoXGk3yK+xjp41TAosqW30ynHwuCkfx0CcD0uJiEqnRLnJ o66iMofVU6jYl0ylRer0k39wrBSuKV1K2S7rV5gRyHtNCkiV6KxsuDHeMtT8NYyti4RVu2gY FecQ7q7oh0A0iqlEXEMjDw8cjirvN3+kXkYwCqUJnZyt3rUeod5wx7Z6JrdROJe9jUDTSh8z zLQAxCwMsKo8tOdi5rY+rrmBiTxC9sJK3CtkdnIvTDehyUiGRClmvGvhtDrWRM31yP2zZgiV CnFqgr9fpi+0q27Nex9eUw7TFT46sd8BsR/it5q3MBWiSVc3M/MuyZdwgKReZ1B1KnzbWQAX 2sOyt/Ruk3+3VF7a2iOzMT/X2mcxc1oY5+7ZHkX02Qz9ZMvau/c4bpakC9yulf9oxjWZK03l z0dyOAu5X1ciucAvgZrzySBDZgdGEBZOWrnkBHCvLXc5O1HIX2id7S9zh80lNqhDaqCrwIaU XDwfJtkHC5s4e1wNVvN1Dv47YSuK7yyJZoD8xaTlRnHle1cLpk8w+ELiSRQMmX4pXQ5yuQ/g E8mzdSgsYOAMWko4LOhD0sSKGjuf81KsGKI7+4WjoOM0ouoBJkkBjgbQM6iU6ezCDxL/fX/a 1TVTXtl+y/dQ+aAW1fYshsurmqTQc73cSvMfz9Ak40kHF7EdSk9yEgVRGlowMB/T1jwgpSnK AAjvngQ/gKq9EUKkL45cUmnFD+Y/l/gay9oGsfFakMKqFgTvQGNdpXOi4A7VyBAos/+8ErUc DHdP0IQSjhXEk2cWwK6ZunovIaftbjeXq3kdrPPeenc8LMFEa7ZmdT3lNMhpmjpVI3HP2E+X adjiwwTADYgQZSfw3JWFGQWj36fNZfF4krsvHQm9Ibnt626EAP3udnVUuUUa44+vUvsx//Eb r/15m4xPz9c0tlkKWbg7r8Z0RZSjihvc2PoCrEcrWvXS6mWnKZLDhkdYic1Nc1S7qt60BMfc cjcwsj40LJ1lJtXQx9MSEDhl8e1ZMcLP3D1NVXJA1yOPaiHIjuDyt/+YKe1Q7ldxOtOsBj4t TGeGk7ldjON8luhHwioKv1JhTqHMQZ2vYi8dlNyEzGmQo68LBK8N9BzgHs9xrh1znLGOGgAM CRtJkNAqrrDiEEQyv57GmFH8j9kNbzew3ffv7SecMxP96cxUUEW36pA7X83yqVY9nRBTf1xw m7Jq8J25kuhma+JwyZmVxxHrnBKgpiKtANsI/a8lNEIVHDa8RYK9WjVBQ4Noo4vA9fvurtQx 9uJnaT6LjsE8tPI8uMTAsHVLISMN39rYn+LUHbESRAISzKmLzSVn0tGjPSb7WGYtLA/o5no3 YUUE/pVCAZzGfQdBUBoWtcFJd0kO1Fs2a7eh8kO632kqRDXT8gPpZHLWMWZBvD3ISqYh71JD /Pt6bz9JIUXcIb83h46ArGVtIvPEkvUG9tKp384BufViEBE8Xw7UXdqnky5MEWi53gcEfPyl Rkz2FMWXA==
- Ironport-sdr: 65257a3f_att/BOvJVnjBuG5XV7mAucAGI8jbN6sOClgII6Qek3Ym60V nRPdamq0aBeGPFFCBvhc1GweQmjcUi1m2AO4MvQ==
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/- [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+.