coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo AT irif.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Looking for a Coqhammer container
- Date: Wed, 9 Feb 2022 21:20:33 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
- Ironport-data: A9a23:zehQ6KqkKt7qShgATd6PIOorXXVeBmLfYxIvgKrLsJaIsI4StFCzt garIBmFaPbYajHxf94iaIXg9hkFvZWAyII1SgJtri5hHyIboOPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHkZqTZMEE/Nszo68wICqtMu0YjR7z+l4 4uo+ZWFYA79gVaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSVcCIiPLWcl9g5eDVKOSByfrJG8bL+dC3XXcy7lyUqclPvxO9pCEwoe5Ae+/gyGWhU9 OdHbj4XBvyBr7vnnPThF7Uq2J1ldZK7VG8ckikIITXxEfYrRrjCWaTEo9FCtNs1rpoWQKiCO ZRFAdZpRD/meTl/IE1UMqtkzN6tqX3lXxYGomvA8MLb5ECKkF0gj+iyWDbPQfSBQtwQlUKFr Erd7mHhC1cbMsaewHyL6BqRavTnniThX4YfCvul8P90xUWa3G0IV1sYTzNXvMVVlGabYvdUK VRE9RYKhoQg3k2nDcb9VhCB9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVsctKnQIB63CPRbWBwv mJlj+8FFhQz4O3OEyj1GqO892/qZnV9wXoqP3dcJTbp9eUPt6kdtHojpP5bGbS0lbUZ8hmvn mjT90DSa524a8oGkqm2uH7dijSnq/D0ou8JCuf/AD/NAuBRPd7Ni2mUBb7zsa0owGGxEgDpg ZT8s5LChN3i9LnU/MB3fM0DHauy+9GOOyDGjFhkEvEJrmrxpyX/INgIuGoudC+F1/ronxe3O Cc/XisPvvdu0IeCNvYtC25MI5lykfmwSIqNug78PosTOvCdizNrDAk3OR/BgDCy+KTdubsyP 56HfNzEMJrpIfoP8dZCfM9EieVD7nlmmwv7HMmrpzz6j+b2TCPLGN8tbQvfBshkvfjsiFiEo 753aZHXoz0BC7eWSneMruYuwaUidiVT6Wbe8JAMKYZu42NORAkcNhMm6e19JdI1xfkJ/goKl 1nkMnJlJJPErSWvAW23hrpLMdsDhL5z8iA2OzICJ1Gt1yRxaIqj9vhNdoE2c/8p7rU7n/JzS vAEfeSGA+hOE2icomlHPcWk/YEyJg62gQ+uPja+ZGRtdZBXQQGUqMTveRHi9XVTAyfu7Zk+r rSs2xn1W50GQwg+Xs/aZOjwnVKrvHZblvgrBxnEJdxaeUPN9ol2KnWt1aZqeZFQcETOn2LI2 RyXDBEUofj2j7U0qNSZ17qZq4qJEvdlGhYIFWfs67vrZzLR+XCuwNMdXeuFIWLdWWfz9Pnwb OlZ1aumYv4AhlFOvpQ6DrBq0+cm7sHuvOAcwB49RCfHaFGiC7VBJHia3JAX7/cdmOQH4VO7C hCV591XGbSVI8e7QlQfEwoScbjR3/8jnDSPv+8+J1/35XIp8ePfA1lSJRSFlAdUMKBxbNE+2 e4ktcNKuRazjAEmboSPgixOrT7eLXsaVKEqqNcHBo71zxIi0FBZPtrSEHausp2IbtxNNGgsI yOV3fKb3eQCnRSaK3djR2LQ2ed9hIgVvE4YxlE1J2OWxojPiMgx0UAD6j8wVAlUk0tKirohJ mhxOkRpDqyS5DM01tNbVmWhFgwp6Md1IaAtJ4/lVVE1TnVEkkTOK3c6PeuTul0f8nwZZjFB/ arHjmj/OdovkAcdwQNqMXOJadS6JTCyyuEGsMG9HsrDEYNSjf/NnPq1fWRRw/f4KZpZuaAEz NWGOM5xc6z1cyAKy0H+5092ypxIIC25yKd+rT2NMU/H8awwuN1/5NRWF32MRw==
- Ironport-hdrordr: A9a23:B52eUKGFIEokzFokpLqER8eALOsnbusQ8zAXPidKOGNom62j5r yTdZsgpGbJYVoqKRcdcJW7Sc69qBDnhPtICOsqTMyftWDd0QPCRuwMg+rfKn/baknDH4VmpN 1dmsZFeaDN5JtB7frS0U2XF94hxZ2g66CnheDXyjNIQRtxY69tqydVYzzranGeiDM2ZqbQm/ enl7Q31gaISDAybsGnCmIIUoH41q27564OqCR2ZSLPNzPjsRqYrL2/GRmb2h8fVndixqgv9G 7digCR3NTQwoSG4y6Z1CvY7pZTkNvljuFIAteB4/JlXkSati+YIIckUbyBuDg0paWU9V42jM OkmWZXTo1O108=
- Ironport-phdr: A9a23:sdhAShDffYBHh/nTffyRUyQUYEgY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua83ygKWFtyDtrptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys5ZHfeQVFiTiybb9vM Bm7rRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3T bpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58 axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJWCNBDIGzY YsBAeQCIOhWsZXyqVQVoBuiHAmhHv/jxiNUinL026AxzuQvERvB3AwlB98ArnTUq8/yNKgKU u+1zazIzTDdYPNM3Dfy8o7IchY8qvyLQbJwcdTeyU40GgPElFWQqILlMymb1uQXqmWW6fdrW u2zhWA9sQ5xviSvydk2ionPno8Y1l7K+Dh3zYopK9C2SFB3b9G4HZdMtCyWKoR7T90/Tm10u ys21r4LtJ6lcCYK1Zkq2RHSZviEfoWK4h/tWvicLDFlj3xrf7K/ggy98UmmyuDkWcm00UpKr ipYktbXrHwCyxvT6s2fRvt8+EehwzeP2BrJ5uFKO0A5k7fQJZ05wrMoi5YetUvOEjXolEj2g 6KabEQp9vWy5+j6bLjrpYeQO5Fohgz6KKgjmcyyDf4mPgQTW2WX4+ux2bLl8EbkWrtFlOc2n bPcsJ3CJcQUuKq5AwhN34Yg7Ba/FTCm0NAGknkZNl5FZRSHj4n3O13XOPD3F+2/g1W3kDpp3 fzGMKfhDo3MLnjFjrjhYa5w51NYxQc819xT+ZJZB74bLP/yR0P9rsHUAxE6PgCsxuboEtR91 ocQWWKVBa+ZNbvfsUOI5u0xJOmBf44VuCz8K/gr/fLug2U5lUcbfaayxZQXcmy3Hux6I0WFZ nrhmsoNHX8QvgUiVOzqlEGCUTlLanmuWKI8/yg3B56iDYfeXY+gm6eB3Se+Hp1OfG9KEFGME XHyd4WFQfgAciySItUy2gADAJOmUscK0Qyk/FvxzKMiJe7J8AUZs4ji3Z57/buAuws18GlID 0Wa5FOMSmR5hGYBQTl+iLx/rEtVy02C3+52maoLRpRo+/pVX1JiZtbnxOtgBoW3A1qZFj/oY FOvQ9H8RCo0Usp02dgFJUB0B9SliBnHmSusGb4c0bKRV9Qv6qyJ+X/3Ko5mzmrekrE7hgw6Q sZIHWy8h6A5+RKAT5XRnRChnr2xPb8ZwDaL8W6CyWSUu0QNTA59Vo3ER3ERIEXM/pzi/k2Xa bioBPw8NxdZj86PLqwfctrykVBPX+vuIvzdZHi2n2quQwuOx63JdIPwen5CmivHYKQduyYU+ 3vOdQ03ByP75nnbECQrD1XkJUXl7eh5rnq/CE4y1QCDKUN7hfKz/VYOiPqQRul2vPpMsTo9q zhyAFe23s7HQ9uGqQ17eaxAYNQ7qF5Z3GPdvgZ5M9SuNadnzlIZdg12uQvp2XAVQs1ckcUth HIwzQQ0J7jZmFJNejWE3Izhb6XNIzq69xSuZqjKn1DGhY/HpuFVtah+9Qyl5Vr5RS9Auz193 tJY0mWR/MDPBQsWC9fqV1ovsgJ9rPfcazU84IXd0TttN7O1u3nMwYFMZqNtxxC+ctNYKK7BG hX1FphQG8ijL8QrgVmnKBwedrMa5OsvMsWqeuHTkrKrMeFInSingyJJ+soutyDEvzo5QenO0 ZEfxvie1QbSTDbwgmCqtcXvkJxFbzUfdoam4RDtH5UZJqh7fIJRTHyrP9Xy3NJ1wZjkR39f8 lenQVIAws6gPxSIPRTx2ghZ1EJfpnLC+2Pw0zx5lBkotKuRmiLUi+jvbxsIPGdXSXIq1AawZ 9Lp05ZEBQ7xNFhhnQDt/UvgwqlHuKlzZ3LeR0tFZWmTTSkqU6e9sKaDf98a7ZoptStNV+HvK VueS7P7v14by3a6TjcYnm1nMW/z/Myiz08f6irVNnt4oXvHdNslwB7e4IaZXvtNxn8cQyI+j zDLB1+6Nt3v/NOOlp6FvPrtMgDpHpBVbyTvypuN8SWh4mg/SwG/kvebm8fmH040y2Won8kvT ijOoBvmN8P316m9GeN9f0cuCkW2uK8YUslu14A3gp8Xw30TgJ6YqGEGnWnEOtJewavibXAJS G1D05vP7QPiwkEmMmORytezSCCG2sU4LYrfACteymcn4stNEqvR8LFUgX4/vA+jtQyIKf1t1 mAUzf9kgJIDq8cOvgdljiCUA7RIWFJdITSpjRODqda3sKRQYm+rN7m2zkt32967XvmEpUlHV XD1d41Hf2c459hjMF/KzHz46531MNjWY9UJsxSIkhDGx+FLIZM1n/AOiGJpI2X49XEizuc6i 1Rp0/TY9MCfLH5x+auiHhNCHj7yfcQX9y+rkKBfgIOO1pquBconFC9KFJrkQPS0ES4D4PTqM wHddV904nyfGLfZAUqe8BI//i6JSc33cS/OYiBCnYYHJlHVPkFUjQEKUS9vm5c4Elrv38n9a AJj4TtX4FfkqxxKw+YuNh/lU26Zqh37D1V8AJWZMhdS6RlPoknPNsnLpP5zEiZw/4egokqDM CbIAmYARXFMQUGCC135a/O24sLc9uGDGuekB/jJe7KKpPIYSvGJ29e325Fn5GnKON/FbRwAR 7Urn0FEW35+AcHQnT4CHjcWmyz6ZMmevB6g+ydzo6hXH9zqQgPho4WVWeI62TBH+gq3j+GNL bzI7M6YATVfzJQIyGGO1b4ewhsKgjtvbGbrH65S7Ubw
- Ironport-sdr: p0emZU9ny9s5uv5dcLt5PdK4HQkpC7J96c8qB7StYDLJwLkBgJMJP7V56WOAu2VnLjonV9jH5b /SPVnj9396pi340y8GrHterWV+/4YQCpIAHOK6EQ9SnvHMjPh6bYpAR7wuI0fHTe6xeFytcCi/ FkUZo+qkzpEd8oAkFZ1YAMJ0pDvvEvTFekr/GgX6CjGXC7hXt3FLh8LABgPayScrnZXPfSRT+u XeKjbYVbG88CgJ6ZnUOXKfLB93fVmm1HC2R0LypwzfASqpwnvKDl4bZWXk5EDxYvJ52mlC5R+a O+cK9EYhIbxBt8MRNP7Edgkn
Dear Richard,
The best way to get an installation of CoqHammer ready to run is to
rely on the Coq Platform. The last release
(https://github.com/coq/platform/releases/tag/2022.01.0) contains
CoqHammer with several SMT solvers.
It is indeed planned in the future for the Coq Platform to be
available as a Docker container.
Best,
Théo
Le mer. 9 févr. 2022 à 21:10, Richard Dapoigny
<richard.dapoigny AT univ-smb.fr> a écrit :
>
> Dear coq users,
> I have found some docker containers for applications working with Coq
> (e.g., https://gitlab.inria.fr/bertot/coq-docker).
> While there exists containers with smtcoq, i have not been able to found
> any container with CoqHammer.
>
> Is there exists such a container or is it planned in a close future?
> Thanks in advance,
> Richard
- [Coq-Club] Looking for a Coqhammer container, Richard Dapoigny, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Patrick Barlatier, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Richard Dapoigny, 02/11/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Théo Zimmermann, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Richard Dapoigny, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Timothy Carstens, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Richard Dapoigny, 02/09/2022
- Re: [Coq-Club] Looking for a Coqhammer container, Patrick Barlatier, 02/09/2022
Archive powered by MHonArc 2.6.19+.