Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Pointing dune to external libraries (Equations)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pointing dune to external libraries (Equations)


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Pointing dune to external libraries (Equations)
  • Date: Fri, 13 May 2022 15:02:39 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f179.google.com
  • Ironport-data: A9a23:WJp1sKvEO20tEfoWHNC7W1fLIOfnVG1YMUV32f8akzHdYApBsoF/q tZmKWnVaKvcZmSmLoxwPtu2/EtUvsTTnYNqSQNsrXgyQioUgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52LBVPyvX4 Ymo+5CGYwf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCncWCdgAVHoPyocIEAkEDNz1mYoBM8YaSdBBTseTLp6HHW37lwvErFV1veINBpbcxDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq35p7apC0bevzuVk4pd3dJe4nTIrZTuPB4sJCwDY9m+hBGP/fY 4wSbj8HgBHoOEMWZwhPUMxWcOGA3WDRSw0GpUiv5okQ7S/p0DJj4oPJGY+AEjCNbZwNwhzwS nj912/+G1QRMMGV4SGU92qlwO7JhyLyHowIfIBU7dZviVyXg3UPUVgYDATq5/a+jUG6VpRUL El8FjcSQbYarX6USeXdcSOBhmfV5kU4R8IPPucz0VTYokbL2DqxCm8BRz9HTdUpss4qWDAnv mNlefu5VVSDV5XFGRqgGqeoQSCaYndKcDdTDcMQZU5UvIm5+dBbYgfnF447SMaIYsvJ9SYcK g1mQQA7jrQXyNcXjuC1pA+WxT2roZfNQ0g+4QC/soOZAuFRNNLNi2+AswKzARN8wGCxEAHpU J8sxZD20Qz2JcvR/BFhuc1UdF1T296LMSfHnXlkFIQ7+jKm9haLJN4NumoufB0zbJleJVcFh XM/XysBtPe/21P6PcdKj36ZVqzGMIC7SIu9CaiKBjawSsEoLlTblM2RWaJg9zm1zBJEfVAXN pCcfsKhZUv2+ow2pAdas9w1iOdxrghnnT27bcmik3yPjOTDDFbIFu9tGAbfNogRsfLfyC2Io oY3H5XQl313DralCgGJqt57ELz/BSJkbXwAg5cHKLDrz8sPMD1JNsI9Npt7JdM/w/QOxregE 7PUchYw9WcTTEbvcW2iAk2Popu2NXqmhX5kbyEqI3iy3H0vPdSm4KsFJsk4eLAm8KpoyvstF 6sJfMCJA/JuTDXb+mRFPcOt8tA6LBn71xiTOyeFYSQke8EySgHM/OjidFS9+SQLCB2xqsZj8 aar0RnWQMZYSgk7VJTWZfujwkmfp38YnO4uDULELsMCKkrp+YlubSf2i6Zvcc0LLBzCwBqc1 hqXUU9I/7mT/9dt/YCQ166eroqvH+9vJWZgHjHWveSsKC3X3mu/2osfAuuFeDbqUmmrqqivY ONiye6lbK8KkVNMhIpLE7hxyJU46day9aRRyR5pHSmSYlmmVuFgL32B0ZUdv6FB3OUF6w6/W 0bK48UDfLvQZ5KjH1kWKw4oKO+E0KhMyDXV6P00JmT85TN2rOXbCxQMZ0HUhXwPNqZxPaMk3 fwl5Jwc5Tu5h0d4Kd2BlC1VqzmBIyBSSakhrZ1GUobnhhBxlgNHaJ3YTzbqudSBMooddEYtJ TCQiezJgLEFnhjOdH86FH7s2+tBhMRR5Eobkgdaf1nZyMDYgvIX3QFK9WhlRApiyBgagfl4P XJmNhEoKKiDl9uyaBOvg4xx98B96BylFojZzlIIkCjAUxDtWDWSfSsyPuGC+E1f+GVZFtSeE Hd01069OQsGvumotsfxZaKhg/PmRN11sAbFnahL2uybSoIib2ONbrCGPAI1RtiOPS/1rELCr Ohuuu13bMUX8MLWT7ITU+Gn6FjbdPxIyKGujx2sEGPl0FwwoA2P5AU=
  • Ironport-hdrordr: A9a23:/qDhd6m4AdmZ7FLE6AbLF/lxgxbpDfIT3DAbv31ZSRFFG/Fw8P re5MjztCWE8Qr5PUtLpTnuAtjkfZqxz+8W3WBVB8bAYOCEggqVxeNZnO/fKlTbckWUygce78 ddmsNFebrN5DZB/KDHCcqDf+rIAuPrzEllv4jjJr5WIz1XVw==
  • Ironport-phdr: A9a23:GRMvcBAIXwmfDJG3cAIqUyQU+kkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua82ygOYFtiGo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJbAhFgDWxbLNyI R6rsQjfq84ajJd4JK0s0BXJuHxIe+pXxWNsO12emgv369mz8pB+7Sleouot+MFcX6r0eaQ4V qFYAy89M28p/s3rtALMQhWJ63ABT2gZiBtIAwzC7BHnQpf8tzbxu+Rh1CWGO8D9UKs5Uiq+4 ah1VBDoiT8HNz8n/2HRlsxwl79QrBa4qxBi34LYfISZOfxjda3fYNwaX3JMUclfVyNDAo2yY YgBAfcfM+lEoIfwvEcOrQKkCAWwGO/j1j1Fi3nr1qM6yeQhFgTG0RQ6EdIPrnvUts/1O7kPW u2ry6nI0C/Db+9X2Tjj9YjDbxcsoemNXb1ua8rR01cgGxnZgVWXtIzlJS+V1uUTvGiG9OdgW uevhHQmqwF1uDSg2sAsiozQi48T11vL+jl3zpwvKt2kVE50f8SkEJ1IuiyHK4Z6X80sTnx1t Ssk1rALp522cSkIxZonxxPSZOCKfoeK7x//VOucPCt0inJkdbyxhhu/70itx+PzWMe701tHq DdOnNfLtnAIzRPT686HR+Nn/ki/wzmAyhzT6uFaLk8pkqrUN4UhzqQxlpoUt0nIAyz4mF3ug aOIakkp/vKk5ufnb7n8u5ORNpN4hhvjPqksnsGyB/kzPBIUUGiB4+u80aXu/U3nT7VOif07i qzZv4rbJcQfv6K5GhNV3ps65xaxEjur0tAVkWMILFJCfxKHgIzpNE/ULP/kCve/hkygkDZtx //YIr3sGovBImTHnbv7frtw61RQxBcywNxD/Z5YF7MMLfbrVk/0rtPYDxs5MwKuw+bgDdVwz pseWWORDa+DKqPdr0WE6f4oI+mRfo8VpDf9JOY45/P1gn85nEUSfait3ZcNdH+4GfFmL12fY XX3mtgBC3sFvhIiTOz2j12PSSNfa26oX60g/jE7FJ6mDYDbS4+xh7yBxT63EYFSZmBbEV+BC mzodoWBW/cUci2eOM5hkjoeVbigUYAtzx+utBWpg4Zge8HT42UzsY/pnIx+4PSWnhUv/xR1C d6c2ieDVTcnsHkPQmoO3a1lu0E14VCey7R5juEQQcRS6ulTX0ExMoPG0+13Fvj9XwvAepGCT 1PwEYbuOi04Ut9km4xGWE16Adj3y0mbh0JCYpcQnr2PXtkv977EmmL2LIB7wmrH068oix8nR NFOPCuonP037BDdUqjOlUjRjKO2beIExieY7GaO13CD+kpfTRRsUKjYdX8ab0rS69/+4xCKV KegXIwuKRAJ0sueMu1PY9ztg09BQaL7OdnEeW/3kGCtHwqJy66kY4/jemFb1yLYWwAfiw5G2 3GAOEAlAzu55WLTCDs7DVX0f0bl6vVzslu+R04wihiWNghvjuXkvBESgvOYRrUY2bdsVD4Jj TJyER792tvXD4DFvA99ZOBGZth75l5b1GXfvgg7P5q6LqkkiERMOwJw91jj0Rl6EOAi2YAjs W8qwQxuKKmZzEIJdjWW2or1M6HWLW+69Q6maqrf0FXTmNiM/aJH5PM9olTl9Aancyhqu21m3 sNP3j2X4YjQEAsfTLr+V082815xoLSbKigx6oXI1GF9ZLGuu2ynuZphD+8kxxC8OtZHZfncR UmiTotDWZDocbN7yD3LJloeMetf9bA5JZajfvqCguuwOfp42SihhiJB6Zx81USF82x9TPTJ1 tAL2aL9vEPPWjHigVOmqs2yl5pDYGRYBmuy0zLpQoVWe7dufIsWIWirKsyzgN55gtS+PhwQv E7mHF4A1MKzLFCKblHnxwAW3kMKu2CmlDaQwDl9kjVvpa2aln+roayqZF8MPWhFQ3NnhFHnL N2vjtwUa0OvahAgiBqv4UuSK7FznK1kNCGTRE5Je3KzNGR+Su6qsbHEZcdT6ZQuuCERUeKmY FncRKSv6xcd1iriGSNZylVZP3myu5jjhRE8g2WANmpyoWfxdsR5xBOZ79vZDfJcxTsJQiBkh CKfXADteYn0u4zKz9Ga7bH2XnnENNUbaSTxyIKcqCa3rXZnBxGyhbH7m9HqFxQ7zT6u0tBrU SvSqxOvB+ujn6++MO9hYgxpHAqms5s8Stw4y9VowshPiCt/5N3d53cMnGbtPM8O3Kv/aCBIX jsX25vP5wOj3kR/L3WPzoa/V3OHw8InacPpBwFeki878c1OD7+ZqbJemi4g6EK5oBjLbL52m SoH1foj9VYVhugIvEwmySDXUdVwVQFIeDfhkRiF9YX0tKRafnyiN7O3yVBinN28JL6HqwBYH n3+f91xeE04ptU6O1XK3nrp74jic9SFdtMfuCqflBLYhvRUIpY8xbIawDBqMmXnsTg52vY22 FZwiIqistHNeAAPtOqpRwRVPTrva4YP9yHx2OxAy92O0dnnH409SG5WGsK5FbTyTG1U7bO9a 06PCGFu9CvdQ+GEW1bBsAE+6CuedvLjf3CPeCtHk5M7HEPbfAoHx1pMFDQiwsxnSEbwmJ2nI B8/vndLvhb5skcelbgubkW5CzaF4l/vM2dRKtDXLQIKvF4eoR6PbIrGqLo0Rn8Q/4X9/lXVe irCOFsOXSdRHRbdT1H7Yuv3uoKGqrnEQLL4d7yXP9Ds4aRfT6van8r+lNs7uW/WZoPXeSA9R /wjhhgZBC4/RpSfwmRVDXRQznOFbtbH9k3lpGst9ZH5q66tAEW2tO7tQ/NEONFrsXhamI+lM OidzGZ8IDdcjNYXwGPQjaIY1xgUgj1vcD+kFfIBszTMReTegP0fCRlTcC51OMZSisB0lgBQJ c7WjM/03b9kn7Y0DVlCT1nohsCuY4QDPWi8MFrNAEvDOq6BIHXHxMT+YKX0TrM17q0crxqrp TOSCFPuJByGnjjtEgmzaKRC1X7KehNZv465f1BmDm2iBNPqZxunMcNm2D07xbpn4xGCfWUYM DV6bwZMtujKtXIe0qg5QjIZqCM6fLrh+W7R9eTTJ5cIvOE+By11k7gf+3Em0/5P6yoCQvVpm SzUp9ooole8k+DJxCA0NXgG4jtNmo+Pul1vfKvD8ZwVE27F8QgX4CObDAkQu9poF/XgvqlRz p7Ek6e5e1Igu5rEuNARAcTZMpfNKH06LR/gAyLZFiMARD+vcHjD3glTya7DsHKSqZc+p97nn 59EGdo5HBQlU/gdDEpiBtkLJpx6CyglnbCsh8kN/XOirRPVSa2yW7jIU/uTBbPkLzPL1dGsh jMNyLL8aJ0Pb8j1ghMzLFZ9m4vOFgzbWtUf+kWJgSc7pUxM9D51SWhhgirY
  • Ironport-sdr: owuh3fw74DomHJmqchtzdlXfoLHtfRAVE9xiOoeaKQ580aE6szDQHSgSp05oijx0qHFxQhewDE VkMaOPHxf86gJ2rlrzxEot0Zy636eRqDLScGKIjy0kIV8xR1MY3RoxZ9FZoRRtE55iYrOwYAxB PQXIZrwxBE4iQixrmhe5aDYGFM27J6ovn6JADRaj5sah/jhAzDgWToYS9yHmkIqtdrxgHepEJE 0mt0I8VZhbLt9S2zb04zZ3V9Bm5eb55wG0bdcMzELvN3tq/b2HG+y/nQXlG+kKBelodWcXBJZm 9d7jSyIaYXgAgWg0D5EWXHeK

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



Archive powered by MHonArc 2.6.19+.

Top of Page