coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: John Sarracino <jsarracino AT cornell.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Pointing dune to external libraries (Equations)
- Date: Sat, 14 May 2022 16:39:51 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cornell.edu; dmarc=pass action=none header.from=cornell.edu; dkim=pass header.d=cornell.edu; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=//1g/ViSU6jExEcXpF+TnMT1YDI2Tf2vWTBtjD0d9OA=; b=mK5B0lXSe5p6JP2nWn2QqUgd/72FIkGXKgClCNN6pWgnRw2GWNtxgtyKJ71uYr3Bddu1F8dEvur50+oY0tD06WxuYEfvBYdTTvcdjoJ88hzVelX6+FLgOcbjl4WwQtKu34vpEfBmbasVPL6hzjfoMXZv4UUg+Ot2CRqXUms12uuhB4SoRUVe/A7zM8Wc2QhQVt9bjf9KojuylP8mz52J15rJ+PSURO4wTTmrlpByK7o0AyPZbGrHirMI3q4wByfSQ8cd9TLYf9HTLXQLzgOv+YRisuhurvvZYktCfZmwDJyLEx+B4hmaJZ3EIOpnYZ2oqA00JSZ34q7sNiCQBJXZiQ==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=MyMjmfFyhstTHSuiBoX3srKGT6V4XkUZmRSPbzzM5Yaejm45nHkuSD3iBszqtQ36EbClVNhfjTZaDEFHR2hrsX65hfzQtQtepKSqzHxH/cyWSavkyr/hb1GaMGV6+HsIrwe51TmpQlcoy3h6QzOBWcK3CXi4sAj7WtQ3mXxgnBHqmY8g6CLSZbbVFNljfIrr8liJVJha7MjRsFgJQuzNJxDF93EOiIhU6E4mn99hMqxMUswdaxXWb/SGcxM04zXM0kV63chD4oNXG8tnOyInl14b4EDunDPxtmP/ycNMe2Z+qTJpkafTHPxXX2Cw3bJyRvOzGJPByOVsFWnVQFutUQ==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jsarracino AT cornell.edu; spf=Pass smtp.mailfrom=jsarracino AT cornell.edu; spf=Pass smtp.helo=postmaster AT NAM10-MW2-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:Qs/Bma/ixM1Cmoculu97DrUD4XuTJUtcMsCJ2f8bNWPcYEJGY0x3y jZOWmmAaPmMMzHwcttyboyx9h4E75XUztVlSVM9+X1EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9g6mJUqYLhWVnV5 Iqu+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z2 ckRtIPhdwYVM7DKxcgXSR0DHzNOIvgTkFPHCSDXXc276WTjKiOp5so0SUY8MMsf5/p9BnxI+ boAMjcRYxufhuWwhrWmVu1rgcdlJ87uVG8dki04i2iBUrB3HdaaGPWiCdxwhF/cguhMBv/Ef cMSaDxoRB/HeRtCPlNRBZ4j9AutriKhKWII+AjLzUYxy0Px4CZ9y/vGDODYXduMSux1o2XJr X2TqgwVBTlBbYfEllJp6EmEjejW2Cj/RYg6D6y97vcsgVuJx2VVBgd+aLegifywi0r7Xs0FL UURo3Ipq/JrrxztScThVRqlpnLCpgQbR9dbD+w97keK17bQ5AGaQGMDS1atdeDKqucnWWAry Q63nu/kGDoynLePTSmR5IeL+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOP7r5jESMWGvq w1mvBTSlJ1P0pBTjPnTEUTvxmv2/MOVF1JdChD/Bzr9tmtEiJiZi5tEALQ3AAYpEWp0ZlyIv XxBntfE6ukLVMmKknbUG7VLG6y17fGYNjGamURoA5Qq6zWq/TikYJxU5zZ9YkxuN67omAMFg meM4mu9B7cKYBNGiJObharsU6zGKoC9TbzYugj8NIYmX3SIXFbvENtSTUCRxXvxt0MnjLsyP 5yWGe71UytAVfo5kmHtG7tAuVPO+szY7TODLXwc50T3uYdymFbOGN/pzXPSM7tpvfPe/G05D f4FZ5PXk0o3vBLCjtn/qtdIdg9iwYkTAJH9sctMceCfagFhAnkmEfbNwLQnE7GJbIwE/tokC kqVAxcCoHKm3SOvAVzTNhhLNe2zNb4i8yNTFXF9ZT6Ahil4Ca7yvfd3X8VtIdEPqrc5pdYqF KZtRil1Kq8SItgx029BNsaVQU0LXEjDuD9iyAL/O2hiI885HlGWkjImFyO2nBQz4uOMnZNWi 9WdOsnzGPLvnixuU5TbbuyB1VS0sSRPke5+RRKRcNJUYkPh9IwsJiDs16dlL8YJIBTF5z2by wfKUE9C/rKT+9c4oIvTmKSJj4a1CO8iTEBUKG/WsOStPi7A82v/nIJNCb7afT3UWG7u1r+lY OFZk6P1PPEdxQ8YuI1mFbtvyeQz68a2/+1WyQFtHXPqaVW3C+8xeiPdhpcX7qAUn+1Xowq7X E6L6+J2A7TRNZO3CkMVKSokcv+HiaMelA7U4KlnO079/iJ2oOeKXEgObRmBjCtRcOl8PI8/n bpznuczslT6ryVwd9GMg2ZT6niGKWEGX+M/rJYGDYT3iw0tjFZffZjbDSyw65aKMo0ePk4vK z6SpazDm7UDmRWbIyBvTSDAjbhHmJADmBFW11tddVmEn9zygPVojhBc9DIASBtYk0dc2OVpN 2k3bEB4efeU8zFziJQRVmygAVwYVhiQ+0i0zkRTkmTcFhGvUDaUdz17PvuR9kcE9W4aZiJc4 LyT1GfiV3DtYd312SwxH0VirqW7H9B28wTDnuGhHtiEQMZlOGq/3vf2aDpasQbjDOMwmFbD+ rtn8eN2Xqvxanwdrqg9PI+F2OlCUxuDPmFDHaps8a5h8bswo91uNeVi6nxde/+h49Ts2GrhU 4lLGZgKUB6zkiGTsjocGKgAZadum+Ik78YDfbWtInMat7yYrXxit5e4Gu3WmjowW9s3+SoiA tq5St5AOjX4abhod6vlp85ePGe8ZZ8JaBCUMCWd7rASD5xa2A1zWRha71Z31kl59CNs+AiSs QfHIaLa0oSODGiqc5TESs1+Oul/FT8/uClkPux+XxSioO4j6fvzij4=
- Ironport-hdrordr: A9a23:G7UT36+sJvMmyxWDNQluk+FRdb1zdoMgy1knxilNoENuH/Bwxv rFoB1E73TJYW4qKQkdcKO7SdK9qBLnhNZICOwqUYtKMzOW3FdAQLsC0WKm+UyYJ8SczJ8X6U 4DSdkYNDSYNzET4qjHCUuDYrAdKbK8gcOVbJLlvhJQpHZRGsNdBmlCajqzIwlTfk1rFJA5HJ 2T6o5svDy7Y0kaacy9Gz0sQ/XDj8ejruOqXTc2QzocrCWehzKh77D3VzKC2A0Fbj9JybA+tU DYjg3C4Lm5uf3T8G6R64aT1eUYpDLS8KoDOCW+sLlUFtwqsHfqWG1VYczNgNnympDs1L9lqq iIn/5qBbUI15qYRBDJnfKq4Xir7N9m0Q6f9XaIxXTkusD3XzQ8Fo5Igp9YaALQ7w46sMh7y7 8j5RPvi3N7N2K0oM3G3am9a/iqrDvFnVMy1eoIy3BPW4oXb7Fc6YQZ4UNOCZ8FWCb38pouHu ViBNzVoK8+SyLSU1nJ+m10hNC8VHU6GRmLBkAEp8yOyjBT2HR01VERysATlmoJsJg9V55H7e LZNbkArsA5cuYGKaZmQOsRS8q+DWLABRrKLWKJOFziULoKPnrcwqSHkondJNvaC6Dg4KFC5q gpCmkoylLaU3ieePGz4A==
- Ironport-phdr: A9a23:XYJkOBFlsgnyKG7NegY1Up1Gf6ZFhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmUBM6Cs6gMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9IiTagbr9+M Qm6oRvMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5wzJLbb4yOLvVyYqbdcMkGSWZdXMtcUTFKDIOmb 4sICuoMJeJWr479p1sIsBCwGBOjBPn1yjBSmnD23Ks60+M8GgzB3gwgBMgBsG7OrNrvKKgSU Oa1zK7TwDrfaPNWwzH955bMchAlu/2DQ69/cdfIxEQpCgjKgUmep5b/MDOJyuQCrXKb7+x4W O+rl2MqpR18rDahyMooloTEm58Zx03a+Ch7w4s4Id21RVNnbNOnDpdduS6XOo94TM88TWxlp Tg3xqEFtJKmciUHzoksyRDYa/yCaYeI4xTjWf6LIThmnn1qZa6/hxas/ke9ze3zStK03ExLr ipClNTHq3MD1wTL58WIVvdx5Fqt1SqN2gzJ7uxJLlo4mbfVJpMi2rI8iJsevVjNEyLzhUn6k LSZe0Qh9+ey9+jqbLDrqoGBO4BvjwzzN7kil8+5DO8lKAYBRXKb9v651LD7/U32XrFKjvoun 6fBrJ3UItkXqrKgDwFS0okv9Q+zDzC939sGh3UHK09FeA6cgIjuJlHOJu33Ae2ng1S2lzdr2 +7JMaH9ApXMKXjDlq3tfbFg605AzAozytdf55FOBr4dJ/LzX1f9tN3eDhAnLwy52+nqBMln2 o8DRW6CALWVPafdvFOS++4iLeqBaJcQuDnnKvgl4/DujWU+mV8YZaSp34AXZ2qiHvR8OUqWf XvsgtEGEWoRogU+S/bqiFucXj5XY3a+Rbwz6SwmCI6+C4fMXZiigKad0yejAp1WemdGB0iRH XvwbYWLR+8MaD6OIs9mijELSb+hS5Y42R6ysA/61qFoI/HP+iwYsJLjzMJ66/fSlRE07zx0D t6S33uDT2FuzSs0QGp816dm5Ed5112r0K5igvUeG8YZr6dCVR5/PprBxcR7DcrzU0TPZIHaZ kyhR4CEBjE3Buk42cUHaEd7HJ32jAvKxTCjCL4TkJSAA4Yy/6bYmXX9OpAumD79yKA9ggx+E YN0Pmq8i/snn+CyL4vAkkHD0r2vabxZxinGsmGK0WuJukhcFg92S6TMG34FNQPNtdqswETEQ ve1DKg/dBNbwJuAMaJQcNTijFNBbPzkItLTZ2b3lmutVl6T3r3ZVIPxYC0G2TnFTk0NkgQd5 3GDYAolDz27qmnfCjtGHlX1ZU7o9a9zpG7oBlQswVSyZlZ6n6Gw5gZThfGYTKYL2akYvS46t zhuNHCU+ouOTv+//U9mdqgaZs4h6lBa026frxZ6IpGrM6FlgBgZbhhzuETtkR5wD+2siOAMq 3UnhEp3IKOcihZaci+AmIr3MfvRI3Xz+xamb+jX3Evf2ZCY4PVH7vNwsFjlsAyzcyhqu3x6z 9lY1Wed7ZTWHUITV5z2SEM+6xl9ofnTfCA844re0XAkP7Ozt3fO3NcgBe1tzRjFHZ8XMriND hX7GMwcAOClL/YsllytKB8IIaEa9aI5Od+na+rTwLSib4MC1HqtiWVK5pw401rZq3I6E7aXm cdZhajDjljiNX+0llqqv8HplJoRYDgTGjD60i34HMtLYaY0e48XCGCoKsnxx9NkhperVWQLk TzrT14AxsKtfgKfKlLn2ggFn0YMqGa9kCC5yTtcmDYzqKeb2GrDz/moJ39lciZbAXJvi1vhO 93+jcsTRlKhZAkvkzOu4lz8yqxf4qlzMiOAJCUANzizJGZkXKyqs7OEaMMa85IkvxJcV+Gka EybQLrwy/cD+xvqBHAWhDUydjXw/478gwQ/kmWWanB6sHvef8h0gxbZ/t3VA/BLjHIKQyxxi D+fAVbZXZHh/86djY3KueG4UEqqUYdVfC3vi46MqWO36HZrDhu2g/2o0oG/V1Fijmmqi58zD nWApQ20eoTx0qWmLe9rGysgTETx7cZ3AMA2k4c9go0RxWlPg5yU+XQdlmKged5f2K/4cD8MX WtXm5iMuFejiREldynZlOebHj2Hz8BsZse3eDYT0yM5tYVRDbuMqaZDlm1zq0a5qgTYZb58m C0cwL0g8i1/4alBtQwzwyGaGr1XE1NfOHmmlQ+B9cq3p6RRY06kdqK22U56292tEfvRx2MUE Ga8YZokESJqu499K1vWynT464fjUNLXd9QeshnSnhvdxbswStp5hr8BgixpPnj4tHsuxrsgj BBg6pq9uZCON2Rn+K/qSg4dLDD+YNkfvy38lasL1NjDxJihR98yf1dDFIutV/+jFyge8OjqJ xrbWiNpsW+VQPLeBVPNtB8g/iiJS9bzcCjKbHgBkYc+HF/EfBMZ2EZMG2xk+/xxXgGymJ68K gEgvmhXvhig7UIQguNwa0umCjuZ+FjuMnFsD8HAZBtOsFMY7h+MY5XHt7B9Q3kArM/m8FzoS CTTZhwWXzsAAhXWXgm6bLfyvYKSoa/EVqK/KfDKfLmD+/dGWfvO3YiozoZt4zeLMIOII2VmC Po4nEFEWBUbU4yckjELAUT7jgr1ZtWA7Fe58yxz9IWk9ejzHRjo7s2JAqdTNtNm/1a3h72CP qiennQxJTFd35IKjXjGrdpXlEYVkD1rfiKxHK4okwfoFfqVv5ANShkRZmV0KddC6L860k9VI 8nHh9jp17l+yPkoF1NCUl+nkcasAK5Ca22wL1LIAk+XOa/OeWWNmpmoJ/LgD+QL3K1drFWot CyeElP/MzjLjDTvWx21cKlNgCydIB1CqdS9fxJqWg2BBJrtbhy2NsMyjCVjneVy3yuVcz9Ad 2EnIxAozPXY9y5Tj/RhFnYU63NkKbPBgCOF96zCLZ1Qt/J3AyNynuYc4XIgyrIT4jsXIZ490 CbUsNNqpEmr1+eVzT8yGhhVoyxRjYmKu0JKMqLD8JREXTDJ8A9HvgDyQ1wa4sBoDNHiofUa0 t/UiKf6MytP6fry1O5FX43xF5jCN3Asdx30BDTTEQ0JCyaxMn3SjFBcl/fU8WCJqp89qd7nn 59EGdo5HBQlU/gdDEpiBtkLJpx6CyglnbCsh8kN/XOirRPVSZYSrtXdW/mVG/mqNCeBgOwOe U4T2b2hZ9d2VMWzywl4Z1J9hoiPB0fAQYUHvHh6dgFt6ERVrCoiFitigQS9LFvquSJbFOboz EJuzFImPqJ1sm+ruglSRBKCpTNswhRr34y92XbJNma2dfv4XJkKWXOs6w5tbdWjBV4yNFL6n FQ6Zm3NH+sD1uI5J2430FeO69wTSZs+BeVFeEFCn/jPPqdxiA0OpHn/nh0VoreVQZpknw83f ZP+tGpO10R7dtkpKKfMJa1PiF9NmqaJuSzu3ec0pW1WbwME9GfYEMbnkEcPLL8rIy7u8+Bxu 1Xqc95rc28WUfcuprRn+l5vY4xoLgrG+psacgWUCLbaKKmU/W/dicSPX1U8kFsSkFVI9qR31 sFldFeIU0coz/2aEBFbbKL/
- Ironport-sdr: 4pZf/f6wnMDgklQTbYSnXdYEskukdb9XfYIyrCBa4HWlMXWqM3OhVf47eInzSwJAz8aImIJOfJ 87EKSY40VATmG88sabz0IxLxvUJEm7e8Omfxbt0YFGzYRv9uSlgsTa9Y09OB3C56LiJyVWCMPc GoJuRfdIlPEFgMaqJhzz/24r8zf4W7Jcmj2NhGAjAyPaoCzLJ2FIRNY+xslDjpUsIhqNiW7Wn1 4KahKstGrvrmFRI1aclEFfuGetL4IxTtknMtStZn1NfhrttfmxK9FhcgHUu9R+lWJGiQYEm1Jm zyr2VNepSH/sMSH4hfKUdUnO
Hi TJ (and others),
You can’t do everything in dune, but you can get most of the way by having dune-project generate the opam file for your project: https://dune.readthedocs.io/en/stable/opam.html#generating-opam-files
If you generate opam files from dune, then you just need to install local dependencies from the generated opam (e.g. by running "opam install -- deps-only .”).
I use this workflow a lot (in fact, with equations as well), along with different switches for different projects as needed.
Cheers,
John
On May 13, 2022, at 9:02 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
Hi.
IIUC you want dune to call opam and install things, like gradle would
do for a java project for instance. AFAIK this is not implemented in
dune. I think it goes the other way around: dune allows to build opam
packages, and then opam deals with its dependencies.
https://dune.readthedocs.io/en/stable/opam.html
best.
Pierre
Le ven. 13 mai 2022 à 08:02, Tj Barclay <tjbarclay AT ku.edu> a écrit :
Howdy,
I'm currently trying to convert my project to use dune as its build system. I'm wondering how to tell dune my project depends on the Equations plugin. Previously I installed Equations from source and just pointed to it in the _CoqProject file, but would like to instead use the package provided by opam. I've installed coq-equations via opam but using the (libraries) field in my dune file isn't working. It does however work for coq-core.foo. I've noticed that Equations doesn't appear in 'ocamlfind list' but coq-core does.
Is there a standard way of declaring these kinds of dependencies? If not, is there a hack that other people are using for now?
Best,
TJ
--
TJ Barclay
Electrcial Engineering & Computer Science, University of Kansas
tjbarclay AT ku.edu
+1 316 259 2250
- [Coq-Club] Pointing dune to external libraries (Equations), Tj Barclay, 05/12/2022
- Re: [Coq-Club] Pointing dune to external libraries (Equations), Pierre Courtieu, 05/13/2022
- Re: [Coq-Club] Pointing dune to external libraries (Equations), John Sarracino, 05/14/2022
- Re: [Coq-Club] Pointing dune to external libraries (Equations), Pierre Courtieu, 05/13/2022
Archive powered by MHonArc 2.6.19+.