Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Tj Barclay <tjbarclay AT ku.edu>
  • To: <coq-club AT inria.fr>
  • Subject: [Coq-Club] Pointing dune to external libraries (Equations)
  • Date: Thu, 12 May 2022 16:12:40 -0500
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 129.237.34.14) smtp.rcpttodomain=inria.fr smtp.mailfrom=ku.edu; dmarc=pass (p=none sp=none pct=100) action=none header.from=ku.edu; dkim=none (message not signed); 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=Fva+so1k4nB9ZG25mR6yW9V5gZnlOYfUUOdGL/7jwMU=; b=dimcReoW3HRrkW7DGBH8m9wTD2YjabqLO/SARQmLmr/mUHrYiY5r0TJDhhkryVmk6O+5xdcIpGl3H3AUBE/tWygmN7MFZput16jEdr33pznRdT5wJsFm7+Qjof8RZ3fiJY35gomLysYBCmuYOX5rk1szf2Yd9Y0ZhAB3URVgN6cOk+czF9TBFbIC2rFfiTEYpFbd0f6JB/k3NtKHdx5PuKatu+VP83HkDR1HhB7133cKBzZ6MeMG5yaTQA3ReFQsFnS0sXTPMKCsfQnOsIRzI+RGVQHos3s6hZnqHgiVedMFpdPV4S0foSBV8eI/p19e5n1OqZZijlh9YCjyjraD6Q==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=EZ56XVLjbuUNE6zuO+8P7+mZdc29EV+czZ5zyuMloWc+ACsUurltVFpD3+hWWEtUeC1x6rR12Q3LHai2cL2MqSrz1fERvMFZA+hl68HxWFJadMe/8UV7g1glO4mxwH5nj5qISJQO9gIDJJxBa0QKi8dF+viSm/RsMFDkLTMefQu/Qc6FGcjUOrVJt//Nx6XPUzK1Jdh7lSJVi0e8HlrGvnBH0UCxWMO+zrUgD8J7zFnwflyPpNciextD7dDYfsAd43MAmWV55Xh18sWqblwXi6Pml7OSiEpuCLn2r4av4tu3dyfHbbXfwk7Ya+vczx3yvQEiYKMTqxR4kUDRJsFVMw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tjbarclay AT ku.edu; spf=Pass smtp.mailfrom=tjbarclay AT ku.edu; spf=Pass smtp.helo=postmaster AT NAM02-DM3-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:eHYH7KlThIfF1zVFBKPpW+jo5gzfI0RdPkR7XQ2eYbSJt1+Wr1Gzt xJMWm3Xa/qKYzP0fth2b9i28hgG7ZfQx983Tgc4pC4wQVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvykTrSs1hlZHWeIcg944f5Ys7N/09cAbeSRWVvX4 4uv+peHYzdJ5hYtWo4qw/LbwP9QlK+q0N8olgRWiSdj4TcyP1FMZH4uDfnZw0nQGuG4LcbmL wr394xVy0uCl/sb5nxJpZ6gGqECaua60QFjERO6UYD66vRJjnRaPqrWqJPwZG8P4whlkeydx /1kmMycTi13JpHDu/YwajBUTzgmMpJZreqvzXiX6aR/zmXgWl60mbBCKRpzOocVvOFqHWtJ6 PoUbigXaQyOjP63x7T9TfRwgsMkL4/gO4Z3VnNIkWmfVK55B8GeBfySvLe03x9o7ixKNercb cMDYj5mfTzDfltCNkp/5JcWx7nw3SagKWwwRFS9ro0ywEv/8QhK4oPTE/PlXMLbRdgIkRPNz o7B1z+gWUpFXDCF8hKO9WvpjevSlwvgSYcKHfu58ORriRud3AQu5AY+UFK6pby1jxW4UtcHd EsSoHN29O416VChScT7U1ugunmYsxUAWt1WVeon9AWKzamS6AGcboQZctJfQPUL5OMxb2Iy6 lCqjf7QLDAzqeWadm3Io994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHokL/Emd3oOdJN3g/ 9yZhHRn2e1J1Kbnw43+rAuZ2mj3znTcZlRtjjg7SF5J+e+QiGSNS4GzoX3c7PBNN+51pXHc5 CNcxKByAA0eZKxheQSISeQJWb2svPCMNWWDhlg1RsF4sTOw53SkYIZcpilkI1tkOdoFfjmvZ 1LPvQRW59lYO37CgU5Lj2CZVJxCIUvITIiNuhXogjxmPscZmOivoH8GWKJo9zqx+HXAaIlmU XthTe6iDGwBFYNsxyesSuEW3NcDn35jnziDHcqhkUv9iNJygUJ5r59VYDNiichpvMu5TPn9r 4832zail0gEAbWlOXe/HXA7dw9afCdqbXwJlyCnXrXaeVE5cI3QI/rQyqkmYItrg+xekf3Q+ Wu0Rk5fzjLCaY7veG23hoRYQOq3B/5X9CplVQR1ZArA8yV9Pe6HsflOH7NqLOFP3LEylpZcE qhVE+3eWKgnYmqcoVw1M8KixLGOgTzw2GpiyQL+PGNgF3OhLiSVkuLZkvzHrndRVHbn7ptuy 1BivyuCKac+q81ZJJ6+QJqSI5mZ5xDxQcp+ABnFJMd9YkLp/NQ4IiD9lKFlINxKJBnen2PI2 wGTCBYehO/Mv45lrYCT1PHe99+kQ7lkA05XP2jH9rLqZyPUyWyunN1bW+GScDGBCW75of3wZ ehcw/zmHucAmVJG79h1H7pxk/A9+p3iq6IDllZoG3DCblKKDLJ8IynbhJMe5/cVnrIA4Fm4Q EOC/NVeKI6lAsK9HQ5DPhchY8SCyeoQxmvY48MzLRio/yRw5reGDRhfMhTQ2ixQKLx5bNEsz es75JNEzSWa0kBvHvPdyyde+iKLM2AKVLghutcCGoj3hwE3y1ZEJ5vBFivx55LJYNJJaxF4L jiRjavEprJd2kudLCVqRSKRhbJQ1cYUpRRH7F4ePFDWyNfIg/kA2hcOozk6SwJiyApKjrBoM W9xOkwpfqiDo2VyiM5YUzz+Eg1NHkDAqEn4yl9MmGiCSUCtDjPKKjdkYb/L+10F+WVBeDQd5 Kuf1GvuTTfteof2wzc2Xklm7ffkSIUppAHFncmmGeWDHoU7PmW62//0OTJQpku1G941iW3Gu fJuo7R9ZKj9Aiga/P82Boyc4rIPRU3WP2dFW/xgoPgEEGy0lOteAtRSx51du/+hJsAmNWeeI uk2fIdjck/70yyD6DcGGaQLPrl42uYz48YPca/qImhAtKaDqj1us9Tb8S2WaKoDXYB1ichkQ m/OX2vqL4BSrSI8d6zxQA1sOXf+bNUZDOE59P7g6/0HTvrvr8k1GXzfEdKIU7G9MxYh8h6J1 O8Gi2k60MQ6oblRc0DQ/mmvyul6xR4flAhFzexrj+lzUA==
  • Ironport-hdrordr: A9a23:kzhyAqxg5ffwv5+tWVffKrPxCuskLtp133Aq2lEZdPULSKGlfp GV9sjziyWetN9xYgBfpTnkAsW9qBznhOVICOUqTM+ftWrdyRKVxeNZnPbfKlTbckWQmJ8/pM UQFpSSEOeRMbETt7eK3ODSKadd/DDoytHWuQ+IpE0dPj2CX5sQnTuRRzzrX3GehzM2YaYRJd 6z4sJGon6HYnQYbsOyAz0gU/LYr9PG0LLKCCR2fSLPJDP+6g+A2frfKVy1zx0eWzRAzfML9n XEqRXw4uGZv/Sy2nbnpifuB8A9orrc4+oGIPbJptkeKz3qhArtTp9mQae+sDc8p/zqwEo2kf HXyi1Qffhb2jf0RCWYsBHt0w7v3HIF8Hn502KVhnPlvIjQWC86McxcnohUGyGpqHbIhOsMlZ 6j4ljp9qa/TCmw0hgV3uK4GC2CQ3DE4UbLkoYo/jViuMUlGftsRLckjTdo+ac7bVfHAb8cYZ 5T5eHnlb1rmAChHjrkVlcG+q3bYp1lJGb3fqFFgL3Y79GepgEe83cl
  • Ironport-phdr: A9a23:A/lG+RAbY4T3SUGKR3NSUyQUMkoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua82ygOWFtyHsLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys9ZDfeQpFiTiybb9vI xi7oxjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3T bpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8 qxlSgLniD0fOjE28G/ZhM9+gr9Frh29phxy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8Y pMRAeoDIO1VspPyp0ESohu6HwatBP7kxzhUhn/0xqI1yf4hHh3C3AM6H9MDq3fUrMjvOKgMT O+10bDFwDPeZPxZxTnz8pLHcgw9of6SR7Jwd9LcxEogGQ7Lj1idqpHpMT2R2+kJvGWW6/dsW +KxhmMkpAx/rSajy9koh4TVgo8YxVDK+yplzYs0JdC1R1J2bcKqHpZWqiqUNJN2T9stTm10o io216EKtJyhcCUOyJkr3QPTZ+Caf4SQ/x7vSuKcLS1miH9rer+znQu+/Eagx+HmVcS4yEtGo jRBn9XWqHwA2R7e5tKJR/Zy5EutxDmC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfulkjqi 6Gaalso9vGm5ergbLjqv5icOJRqhQ3kNaQuh9C/Dv8/MggTWWiU5P6w1KX5/U3+XLVFkOE5k rXYsJDdI8QXvKm5AxJJ0oYn7Ba/CDSm3M4EknkAKVJJYBOHj473NFHSOP31Auuzj06xnDt3x f3KJLnsD5XXInTejLvtYK5x60tGxwoyydBf6YhUCrYEIP/rRk/xtsfXAQUjMwOox+boEtV82 5gdWWKSGKOWLr7dsUKQ6uIpOOaDfJUVtyrlK/g5+/7uimc0lUIFcamzwZQXcGy4HuhhI0iBf XXshc4BHX4WsQo6Uezlk0aPUSVTZna3R6Iz/Cs3CIOgDYfZR4CimqaN3CmhHs4eWmcTXluLC DLjc5iOc/YKciObZMF7xG8qT7+kHrMjnTunrgT+wqsvevbW8CQCvpbqxfB2+qvemQxkpm88N NiUz2zYFzI8pWgPXTJjhMiXwGR4w1aHi+1jhuBAUMZU7LVPWxs7MpjVy6p7DcrzU0TPZITBU 06oF/OhBzx5Vdct25kWeU8oB9eohwrI2yO7K7wI0bGHGc986brSikD4PN010HPazO8khlgiT NFIMDi6hKR27QPXDp/hkFjfmqq3JuwHxCCYzG6Y1iKVuV1AFg59VaKQRXcEek7ftsj0/GvkZ pr2U/ELF1AEzsSPbKxXdtfukFNKAu/5P8jTaH6wnGH2AguUwrSLb8zhfGB1MDz1Lk8CnkhT+ H+HMVJ7HSK9uyfECzcoE1vzYkTq+O04qXWhT0ZywRvYJ0tmn6G4/BIYn5n+A7saw64EtSE9q j51AEf13tTYDMCFrhZge6MUaM004VNO32bU/wJnOZnoI6dnj18YOwN52iGmnwl1AIxamswjv Vsp0Ux/Jb/ZmFJNejWE3Izhb6XNIzq69xSuZqjKn1DGhYrOvP5Xt7Jp9hO65Fj6cyhqu29q2 NRUzXaGs5DDDQ5IFIn0Tl5y7R9x4bfTfig64YrQk3xqK6i99DHYiLdLTKMozAite9BHPeaKD gj3RocGBcKnMucukkmBbQ9CMexPvv1RXYvuZ76d1ainMfw11i6kh21d64R0w2qP6mxxRvOCj N4Vhvqf2AWATTL1ilys59v2lY5zbjYXBmOjyCLgCea9f4VKdJ0QQSerKsyznJBlgoL1HmRf/ xilDk8H38mgfVyTaUb81EtezxZfrXuikCq+hzt69lNh5rad1iXUyODrZTIEJyhGSHQqgVr3I IeyhswXRwD0N05wzETjtBu8nvAC7K1kZ3HeW0JJYzT7IwQAGuOru7yObtQOoJIkvCNLUfitN FWTS7rzuRwfgGvoG2pTwix+din/5s2/xkQlzjPAai8r9Sm8G4k43xrU6d3CSOQE2zMHQHM9k jzLHh2mONLv+9yIlpDFu+T4VmS7V5QVfzO4qOHI/Ca9+2BuBgWy2v6pndiyWxQ42ybh3N1jR A3LsVDxbpShhMHYeap3O1JlAlPx8Z8wBoN0m5E7gJgB8XsHwJiZ4DBU2Xe2OtJd16XkaXMLT jNe2N/Z7j/u30h7J26IzYb0BRD/ioNxIsO3aWQM1mch/thHXe2Kuadck3I/8RKo6Bjcav9nk nIBxOsyvTQE1voRtlNIrG3VA6hOTxUAe3220UzOt5fn8e1WfDr9LeD2jRIh24jnVPbb/EldQ CqrJ81kRHcoqJ05aBWVjBiRosnlYIWCNIpP8EHL1U+G168Md9owjqRY3yM/YDCk5CR3xbJj1 U48ms3q2erPY2R1ovDjC0YBZGSsPpEdpmm23/QZwpbe3oakGohtF2cQRJXkC+qyFy4fvujmM ADIFyAgrnCcGvzUGgr6ig8u6nvLF9rD22i/HHAC1p0iQRCcIBYamwUIRHAgmZV/EAm2xcvne UM/5zYL51e+pAEegu5vMhD+VC/YqmLKIn8sT4ODKRNN8gxYz2H8FJTEq85WRGRf9JDnqxGRI GuGYQgOFXsORkGPG1HkOP+p+MXE9O+bQOG5Kp6sKf2CpPdfWPGB2Z+0mtc+uW/UaYPeYz87V 6Rz01ELRX1jHsXFhzgDAzcakS7AdY/TpRux/DF2stHq8PnvX1GKh8PHAL9TPNNzvhGu1Pvbc bfI22AodHABjspfoB2AgKIS11MTlSx0IjykELBa8DXIULqVgKhcSRgSdyJ0MsJMqaM6xAhEf 8DB2baXnvZ1iOA4D1BdWBnvgMasMIYWIWu0LljDDVejN6nAKDHWiZKSA+v0WfhLgeNYugfl8 y6cCFPmNy+fmiPBcTmKabsJoATAeRtUtce6bwpnDnXlQJT+cBqnPdRrjDowh7opmnfNMm1aO j95ORAozPXY/WZThfNxHHZE53xuILyfmiqX2OLfL44frfphBikn3/If+nkxzKFZqT1VXPEg0 jWHtcZg+hv194vHgioiShdFrSxHwZ6GrVk3c7uM7YFOAD7F5E5fsT3WWk5M/509TYSy86FIl oqTzOSqcGgEq5SMupJCYqqcYMOfbCh8a1ywQGaSVE1dCmf3fWDH2x4EyK3UqiLT9t5i7cGz0 JsWFO0BXQRsRKpDUxZrQIRacsUwAmNB8/bTjdZWtyC39ECDHZwD7J6bDqnAU7KzeH6Yi7JAe hcFk6jgI4hVLpf8x0Fpdlh9msLNBlbUWtdO5CZma2pW6A0I+Xx6BAXbPmrmd0Wg7GJBTZZcf zYQoy4mO6EB0Wyp5F06YF3XuCE3jU89383/hiyceyLwK6H2WpxKDy3ztA46NZapGm6dgiWxg AppOCqWHtps
  • Ironport-sdr: gILny3PHg7/0Duipsvguee4mAO5dokZOzKYnQCO9U4AxPpYc8cPyN0h4XjuVRMnOmXDBI0SZIM VRTnXBDKdfLPmiiQRQfQH9s7iJ5FKCWQNR6Dg8ckXGFdr2oJmyiR0gp7+qi1CKQdbGB/du9z0A nRSKIz4bBFwA6gQBkCEuZN8RVRIrmtxF/lgfKtkPrGAgUEK9XEv+JUvu6I6SPhoaZd3gEVkmmA 1lOP+qjzIxq+SwTe5UVnlQPeVlr2b84810sdKSG7ZDTqp9CTsPWkAnDz2AOgVeCKI5s03JOu/e QQD98cDnpI4e9hctvgBiHrU0

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
+1 316 259 2250



Archive powered by MHonArc 2.6.19+.

Top of Page