Skip to Content.
Sympa Menu

coq-club - [Coq-Club] produce _CoqProject from dune

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] produce _CoqProject from dune


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] produce _CoqProject from dune
  • Date: Mon, 16 Dec 2024 14:59:54 -0500
  • 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-ed1-f46.google.com
  • Ironport-data: A9a23:KkOXlKvEn+/M9FUOGc5RpfCNIufnVP1aMUV32f8akzHdYApBsoF/q tZmKT/QMvvYMDb8Ld11PI2+9EkDsZbRyddlGVFsqys9FC1HgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRNscpvlDs15K6u4WlB4ARkDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJEEOBtc7oMRTPSYN6 fUbKWspVzDAq8vjldpXSsE07igiBMziPYdat305iD+FU7ApRpfMR6iM7thdtNsyrpoWTLCOO oxDMWopMEqojx5nYj/7DLo3luepnXnycHtRrluTqew24nTc5AN02bnpdtHSf7RmQO0MzxfE9 ziWozqR7hcyCdewyT7asX2X3P7duDH+Sa4cSeyU36s/6LGU7jdOUUVJBAXTTeOCokW5QpdUL 1Ee0jE/qLA7sk2tVNj0GROiyENopTYZUttUVuA2sUSDlvSS7AGeCWwJCDVGbbTKqfPaWxQq7 mTTvInLIQAo86GcSnPG0o607h+bbH19wXA5WQcISg4M4t/GqY41jw7SQtsLLEJTpo2qcd0X6 2DaxBXSl4kuYdg3O7JXFG0rbhqpr5nNCwM5v0DZAjzj4QR+a4qoIYev7DA3DMqszq7IEzFtX 1BdxKByCdzi67nTz0Rhp81TQNmUCw6tamG0vLKWN8BJG86R03CiZ5tMxzp1OV1kNM0JERewP xSP41MOuM4PZiX3BUOSX25XI5R1pUQHPYS0Ps04kvIXM/CdiSfeo3E+OxHKhwgBbmB3wfhhY szznTmQ4YYyUvk+lGXnGY/xIJckwScxwW6bRJbwiXyaPUm2NRaopUM+GALWNIgRtfvayC2Mq oo3H5XQl313DralCgGJqt57ELz/BSJnbXwAg5YKLrbbSuencUl9Y8LsLUQJItY4wvkLyLySl px/M2cBoGfCabT8AV3iQhhehHnHBP6TdFpiZXdwb2W7kWMue5iu56o5fp46N+tvvu96wPI+C 7FPd8ycC74dAn7K6hYMX6nb9YZCTRWMgR7RHiyHZDNkQYVsaTaU8fDZfyzu1hI0MAyJieUEr YedizzrGag4e1w6DeL9Su6e8FeqjH1MxMNwRxTpJ/dQSmXN8a9rCSr7sdEvKepRKx+Znjq+/ CSVCCc+uuPijdIU8t7IpKbctKavMbJ0MXR7Flnhz4SdFHfl7Ev65qRfQsOkQCv7aFrk3ImDO cBE0ODaMtAcuVRB7rpHDLdgyJwh6+vVp7N1yhpuGFPJZQ+JDoxMD2an385dkL9k3Z5c5BWLX 3yQ9ulgObmmPN3vFHgTLlEHasWBzfQlpSnA388qIUnV5D5Fw5TfaB98ZyKzsS16KKd5FKgHw u174c4f1FGZuyoQa92DinhZynSIInk+SJ4Yj5A9ArLwqw8V21pHMI39CCj33cm1UO9yEHIWe x2auKmToI5n5BvmU2EyHn3zz+ZilcwwmBRV/mQjeXWNuPT438ES4jMA0A4ZbApvyjd/79lSI Ulubk18GrWP9Wxnhe9FRGGdJDtCDxy4pG30x0c4q2nCa0yOSGb2DXYcPNyV9xsz6FNsfTl8/ ZCZxl36UD3sQtrD4ysqVWNhqN3hVdZU9DCevOyCAOK+AMAcTRf+p62hd04kikHCOtwgol/Dq c1B3vdCWYeiOQE++6QEWpSnj5IOQxW6FUl+aPBG/oZSOErDeTu3iAO8G2roduxjf/X1oFKFU epwLcdyVjO75iaEjhYfIYUue7ZUvvoY1OAuS4PRB1wtkuWg92JykZfq6CLBqnchQIxuneYDO 4rhTW++PVLKt0REuV3mjZdiAXW5U+kmdQen/eGS8cc1LbwhntxoU3kP1uqTgy3IHiphpwmZr SHSVZ/wluZC87lhr6HoM6dEBji3F+/NafS1wFiznehjPdLrGuXShjwRsWjiblh3P6NOetFZl oatkd/Q3WHZjYkySETmpZqkLPBMw+mDQdgNY9zFdmleuS6kRsXXwgAi/lqgIsdji+Jt5ciAR iq5ZvCvdNUTZcxv+X1NZwVaEDcfE67SfI66gQ+M9NG3FQk77QzLCPiF5E3ZRzhXWQFQMqKvF zKuneil4+5pibhlBTgGNqlAOIB5KlqyYpkWXYT9mhfAB1b5n27YnKXpkCchzjT5CnOkNsLey rCdTzjccCWCgo35/Ot7gadT4CJOVG1chNMudH0z49R10jC2LFAXJNQnbKkpNMtmrTzQ5rrZO hf2c2oQOQfsV29lcDL9wujZcCWxO+gsAur9dxsVpx66SiHvCI25Ve4rsm8q5nptYTLswd22M dxUqDW6IhG1xYovXuoJoOCyheB83P7B23YU4gbHntfvBwoFS6A/vJC78NGhiQScey0MqKnKG YTxbWVNQUX+REKoVMg8JThaHxYWuD6pxDItBctKLBAzpK3DpNCsCtWmUw0w7lHHRMsPLb8KA 3jwQgNhJkiIj2cLt/JBV80B2MdJ5DHiIiR+BKDmTAwW2aq37wzL+i/EcTUnFKkfxeKUL78Re vRALZTz6IRp5X29AIGr9Dg=
  • Ironport-hdrordr: A9a23:EYSJdKnwAwJChtt+P3gI2vA1j4zpDfIW3DAbv31ZSRFFG/Fw9v re+sjzsCWftN9/YgBDpTntAtjifZq+z/5ICOsqTNKftWDd0QPCEGgI1/qH/9SPIVyYysdtkY llN4ZxYeeeMbG4t6rHCcuDfurIDOPozElgv4bj80s=
  • Ironport-phdr: A9a23:m6897RQ8Z3RJ9IshWcDoz105P9psorWWAWYlg6HPa5pwe6iut67vI FbYra00ygOSBMOKsLkd0LCe8/i5HzBbudDZ6DFKWacPfiFGoP1VpTBoONSCB0z/IayiRA0BN +MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55I AmroQnLucQbj5ZuJrw1xxbHrXdEZupbyX11Ll6Xgxrw+9288ZFt/ihMof4t69JMXaDndKkkU LJUCygrPG8y6MD3rxfPSheB6GUBWWsMiBpIBAbF7BD+Xpjvtybxq/Rw1iqHM8DoVL44QTut4 btlRx/ukycHKiU28HrLhcxqjaJUuwyuqhpiyIPJeo6VNf5+fqTAfdMGQGdKQ8hcWzBdDo66c oACCfcKM+RFoInnv1YBohuwCwevCu3y1DFHmmT70rcm3+k7CwzKwBAsEtAIvX/JrNv1LqASU eWtwaTU1jrDb/JW2Sz96IfWcRAqvO2BXbRqfsrX1EYkCgTIgU+LpozlPjOVzeQNvHaY7+Z6T +2vjXQoqwdsrTS1x8csi5XJho0Ox1DL8CV22oc1JdmiREFnZt6kFYJduieHPIR5Xs0sWXtnu DomyrIYo567ejAHxIonyRPdafGJfJWF7xHtWuqNPzt1imxpdbO9ihqv7UStyO3yW8m33VtKs iZIk9rBu24R2hHO5caKVOdw80S/1DuJygvd5OZEIUUumqraLZ4s2rEwlpsPsUTDAy/5g1/6g 7ORdkUh4uSo5OXnYqnmpp+BLIB4kBvyPbgpmsy6Geg3Lg8OX3Kd+eui0L3j+Vf1T6tXgf0rl KTSrZPUJdwDq6KnHwNY1pwv5hW/Aju8ztgUgXoKIEhKdR+GiYXiJk/DIPTlDfekn1Sjji1ry e3HPrzgHJrANmTPnbH8drhn8UFc0hA8zdVH6pJUFL4BJPXzV1f0tNPCDx85NxW4zPj6B9lgz 48eV22CD66DPKPdtl+I4e0vI+2Sa4MPpDn9LP0l6+bvjX8/h1AdYbGk0YULZH28BPhrIEWUb WDyjtsdEmoGpAUzQe3yhF2HSzFTZnKyX6wm5jE8DYKrFZ3MSZutgLyAxye7HoNZZmNcBl+WF 3fnbYOEVOoWZCKTI89hjjMEWKOuS48kzx6utQv6x6B7IerT/y0UrZTj28Nt6O3JiR4y7SB0D 9ia02yVUm14hnkISCMu3KBjvUx9zU+O3rR/g/xBDNBc+/dJUhohOpPH1Ox7C9XyWhrbcduTS VamRM+mATArQd4rzd8OeRU1J9L3hRfamiGuHrVdw7eMHdk/9r/W93n3Pcd0jXjcgvoPlV4jF +JFNWy9hqN8vyHVDojF2xGQnaarbqQR32jE8m6FwSyPvV1XeAF1WKTBG3sYYx2F/pzC+kreQ ur2WvwcOQxbxJvaQkMrQtjgjFEcAezmJMybeWW63WG5GRePwLqIKovsYWQUmivHWwAfiw5G2 3GAOEAlAzu55XrEBWlnH1LueEPh8q93rnq9Qgk1zh2FR0Jk3ruxvBUSgK/UUOsdi4oNozxps DBoBBC41tPSBcCHol9odqVdetMw4xFO02vfu0p8P4CvB69nj18aNQ9wuhCmzA15X6NHl8Vit 3Y21ExyJKafhUtGbC+d1IvsN6f/L2Dz+FWiZ/eT1A2AltmR/agL5bIzrFCLUBiBME0k/j0n1 tBU1yHZ/ZDWFE8IVpm3VE8r9h98rrWcYy8n5oqS22c+ea+z+iTP3d4kHo5Hgl6pYstfPaWYF QTzD9xSBs6gL/YvkkSoaRRMNf5b9ao9NcerP/Wc36vjMOFllTOgxWNJheI1mkuG9ytnSuPLm Z8DyveUmAqGSzjUg1Kos8SxkodBJHkTEme51Sn4FdtJfKQhGORDQWyqIsCx2pB/n8u3Ay8ep APlXQtWnpP3Kn/wJxTn0AZd1FoauymikCq8lXlvli0x67CY12rIyvjjcxwOPihKQnNjhBHiO 9vR7ZhSUU62YgwujBbg61z9wv0Rra5/LnLTTEQOdi7/KW0kU6qsuZKNZsdO7NUjtiAdA4HeK RiKD6XwpRcXyXapFmFexSs7ejLss5PwmRA8iWOBI158qXPYfYd7whKVt7m+DbZBmzEBQid/k zzeAFOxasKo8dujnJDGqumiVmilW/W/aAHTxJib/Gu+7GxuW1ikmuyr38fgGk482DP60N9jU WPJqgz9a8/lzfbyPeVid0huTFjyjqgyUoh0koorhJwTn3Ecj5OZu3sGjWjbPtBS2Ka4Z30ID TIG2N/a5gH51VYrdCrYgdKkEC/Fko09OZGzeQZ0kmol4tpPCbuI4bAMhiZzrlei7ErQbfV7g jYB2K4r4X8ejfsOvVllxSGcD7YOWEhAaHa0xlLYspbk9PURODj8FNr4nFBzlt2gEryY9wRVW XKjP4wnATc19MJ0dlTFzHz07IjgPtjWd9Ma8BOOwHKix6BYLow8kv0SiG9pI2X46Dcswe46l hxj3tezuoGBJyNs/b62KhFdPzzxIcgU/3u+6MQW1tbTxI2pEph7T38CVpvpVvKlE3Qbs/3hO 0CPESEzgnieELvbWwSY7Q01yhCHW4DuPHaRKn4DyNxkTxTIP01TjjcfWzAil4I4HASnl4TxN V107TcL6hvkuwNBn6h2YgLnXD6V92LKIn8kDYKSJx1M4kRe6lfJZIaAu/lrEXgQ/4X9/lfQb DXKP0ISUT5PAgveWxjiJuX8u4WGqbPDQLPgd72WJuzfzI4WH/aQmcDxjM0/p2zKboPXeSM6R /wjhhgdAzYjR5Wfy21JE2tNz2rMd5LJ+036o3Ex95HltqysAVKKh8PHCqMOY4ozvUns3OHbc bbX3XgxKC4EhMpUlTmRl+dZjBhKzHs3Pzi1TeZZ6nWLFfOM3PcRV1lCNUYRfINJ9/5uhFEcf 56GzIqvhvggyadqQ1ZdCQ67w5/vOJxMejDncguAXRfDNazad2eSnYetOvL6EucW1KIN5njS8 X6NGkvndFxvjhHPUBaieaFJhSCfZllFvZ2lNwxqAi7lRc7nbRuyNJl2iyc3yPs6nCGCM2lUK jV6f05Xy9/YpSpFnvVyHXBA5Xt5PKGFnSie9ezRNpcRt7NiHC11k+tQ5HlyxaFS6WlIQ/l8m S2aqdALwRnuiu6U1j9uSwZDsB5OjYOP+EhuYODXqscGVnHD8xYAq26XDlVCptdoDMHup7EFy tXLk/GWSn8K+NbV8M0AQsnMfZjfYTxxbFyzQG6SUFVWKFzjfXvSjEFcjvyIo3icr5xg74Pph IJLULhQElo8CvIdDE1hWt0EOpZ+GD0+wtv5xIYF42SzqB7JSYBUpJfCA7ibC/XuMzaUjv9NY RIOzfX5LJgcHoL+0k1mLFJ9mc6ZfiiYFcAIuSBnYgIu9Q9V92NiS2Qox0//Qgak4XtWGPLt2 xBq1E1xZuMi8Dqq6FAybAmvxmN4gAw6ntPrhiqUeTj6IfKrXI1YPCHzslA4LpLxRwsdheKak kltNTOCTLVU3eIInYFDjQbdvd5CFacZQ/EaJhAXwv6TarMj1lEO8k1PIGdI4OLEDd1pkw54K faR
  • Ironport-sdr: 676086e0_DxoyKQxDBWW6eEhwUpzBRCAdMwCP27iSIQSeu1mxLx7Qt2i jWNW8vc9eMia6lLG5mMsg91E5yb+v51G81HOPGA==

Has anyone developed some tooling to automatically produce _CoqProject files capturing the -Q/-R flags needed to interactively edit a file, based on a successful dune build? If not, does someone (especially dune internals experts)  have thoughts/suggestions on how to implement such a tool?
The -Q should not just map the physical paths in _build/default to logical paths but also the original source locations, as done here: https://github.com/bluerock-io/BRiCk/blob/master/_CoqProject.template#L14

(I understand that the long-term solution is to use dune coq top, but having the above tool would be useful until then)




  • [Coq-Club] produce _CoqProject from dune, Abhishek Anand, 12/16/2024

Archive powered by MHonArc 2.6.19+.

Top of Page