Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Looking for a Coqhammer container

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Looking for a Coqhammer container


Chronological Thread 
  • From: Timothy Carstens <intoverflow AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Looking for a Coqhammer container
  • Date: Wed, 9 Feb 2022 12:21:59 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=intoverflow AT gmail.com; spf=Pass smtp.mailfrom=intoverflow AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f50.google.com
  • Ironport-data: A9a23:xEbQra0RHTo+qmyjF/bD5fp3kn2cJEfYwER7XKvMYLTBsI5bp2EGz DEfC2qFM6uJM2Hzcoh2Ot7n9UkCvcKDzNJlTgY63Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOH9IQMcacUsxLbVYMpBwJ1FQzy4bVvqYy2YLjW1nV6 IuoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt/9v4 c5h5azucywCOZbwneYjVhwELRgraMWq+JefSZS+mcmazkmDa3m1hvszVAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmez9F7EEascLdKEHOKsevG1n0zzDA/IhXrjMRqzL4ZlT2zJYasVmQKqOP 5FEOFKDajyYIBdpIEcnD6g8lcG4vnndXBMHlnma8P9fD2/7lVQtitABKuH9cduTAM5Rg0ywv XPD522/AxcANdXZxyDtz563rurGnCe+QIBLUbPlrrhlh1qcwmFVAxoTPbemnRWnomGgcslze 3xKwAEFqpMO8U6VS9yhYSTt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4othpOIxOWCgeFW1C6 7OZoz/6LWcw7+DNGBpx4p/R/GziY3FERYMXTXZcFVNt3jX1nG0kYvvyojtLFae0ipjtG2i1z W3S6ic5gLoXgIgA0KDTEbH7b9CE9sahou0dvF2/soeZAuVROtTNi2uAtwOz0Bq4BNzFJmRtR VBd8yRk0MgADIuWiAuGS/gXEbei6p6taWOA3QUzQsF5r2/2oxZPmLy8BhkudC+F1e5UKFfUj LP75Gu9GbcPZiLxNfYvC25PI55ykfS9fTgaahwkRoMWPsIZmP6v8yZpakqdt10BY2B9+ZzTz ayzKJ72ZV5DUfoP5GPvG481jOF2rghjmju7bc2ql3yPjOvFDFbIGOdtGAXVNYgRsvjUyDg5B v4FaKNmPT0EALOgCsQWmKZPRW03wY8TW8yo9ZwNK7Lrz8gPMDhJNsI9CIgJI+RN95m5XM+Rl p1kckMHmlf5m1PdLgCGNiJqZL/1DMRwqHs6OWonOlPxgyovZoOm7aE+cZorfOl/pLYzk6IsF /RVKd+dBvlvSyjc/2tPYJT4qrtkfkv5iA+LOR2jfzViLYVrQBbE+4O/cwa2rHsOAyO7uNEQu bql0g+HE5MPSx4zXsnTYfOriVi2uCFFyu51WkLJJPhVeVntoNA6cXyv0qdvLphVexvZxzac2 wKHOjsipLHA890v7d3EpaGYtIP2QeZzG0xtGWOEv7u7MC/t+HX6nd1NXeOOSjDqVG3u/ZKka +gIner3N+cKnQoTvodxT+RrwKY564e9rrNW1F4/TnDCblDuErE5Z3fbhY9AsapCwrIfsgyzA xrd9t5fMLSPGcXkDF9Be1Z/P7rbjakZymvI8PA4AETm/ysrrrCJZkNfYkuXgytHIbopbY4on bU7tMgN51DtgxYmKIzd3CVd9mDJNn5ZFqt67tcVB4jkjgdtwVZHOMSOBijz6ZCJStNNLkh6f WPO1fSa3+xRlhjYbn4+NXnRxu4B154AjxZHkQ0ZLFOTl9uZ2/I60XW9K9jsoti5E/mG7w5yB oSvH0h8JKHL5zUxwcYeByajHAZOABDf8Uv0o7fMeKs1UGHwPlEh7kVkUQpOwKzd221Zdzlfu rqfzQ4JlB70Kdrp0HJatVFN8pTeoB8YyuEGsM+iFsWBWZI9ZFIJR0NoiXUg83PaPC/6uKELS SSGMgq9hW0X+BP8e5EGNrQ=
  • Ironport-hdrordr: A9a23:gkOZm60Bh4xnE9LetOzJ5QqjBJ8kLtp133Aq2lEZdPUzSL37qy nOpoV56faQslwssR4b6La90cW7MBbhHNtOkPIs1MmZLXDbURqTXeVfBOLZqlWKexEWtNQtrZ uIG5IeNDSaNykcsS+V2njDLz/i+rW6GWKT6Ns2A00DcegTUdAc0+6xMGimLnE=
  • Ironport-phdr: A9a23:85+OkB/Pi6ak3/9uWeG2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Z gqCur401AKBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR 5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdq72/qy9pDRbAlEmSaxbLNvJ xiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4U KdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4 KdxUBLnlCgJOT42/2/KhMJ+j6xbrxC/qRJ42IPbeoOYNP9kc6PdYd8XR2xMVdtRWSxbBYO8a pMCAfQAPeZdqIn9u1sOrBujDgSyHuzv0CRIhmPo0q08yOQqDAbL3A0mH9ISt3TUssv6NL0cU eCxy6nJwy7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+duV eaihmEkpg9/oTWhyMcih5XNi48XxF3J9Ct3zYk6KNCkSEB2fdCqHYVfuS2GN4V7QN0vTW91t Sg117EItoK2cS4Xw5opwB7fbuaIc4mO4h/7W+aRICt4hHJ4eL2knRq97U+gyujkWsm11lZKt CtFncPWunADzRze7NWMRPhl/kq5xzqDywTe5vtHLE00j6bXNYMtz78qmpcTrUjPBi37lUvsg KOLakkp/vKk5/rpb7n6vJOQKpJ4hwfjOao0gMO/G/43Mg0WUmib5+u80Lrj8FX8QLpQj/02l rDVsIjYJcgGv6K5DQ9Y3po55xawCDem19sYnX0ZI15fZB2HiI3pN0nPIPD+E/i/n0yhnCl3y /3CJLHsAZXAImLdnLv8fLtx8U5RxBYrwdBa/Z1UC7UBIPzpWk/2sdzVFh45Mwqow+bgFtVyy JkeWWyLAq+ePqLfqlCI5uc1LOmNYI8ZoiryK/8g5/L2i382gkcSfbO10psPdHC4AvNmLl2Eb Xb0mNcODX8KvhYiTOztkFCNTTlTZ2+rU60g4jE7FZmpAJzYRoGthbyBxD20EodXZmBAEFCME G3ne5+KW/cWO2quJZpqlSVBXry8Qacg0wuvvUn00elJNO3RrxEZsJX/1Mk9zOTJjg0/8yc8W 8Wbz2aTQnt6mmQXbzAz1aF750d6zwHQguBDn/VEGIkLtLtyWQAgOMuEpwQbI9X7WwaaO8yMV E7jWdK+Rzc4UtM2xdYKJUd7AdSryB7ZjGKxG7FAsbuNCdQv977EmWDrLpN8zWrByqQ7gV0hX eNAMGSnguh08A2AT5XRnRChnr2xPb8ZwDaL8W6CyWSUu0QNUQhsVrvIR34bYVT+otHw50eER LirWvw8KgUU78mEJ+NRb8Hxy1VLQPC2INPFf2e4gHu9Hz6Nz7KIKZLoIiATgX2bB08DnAQeu 32BMGDSHw+HpGTTRHxrHFPrOAb39PVm7Wi8Vgkyxh2LaEto0/y0/AQUjLqSUaFb2LVMoyonp zhueTT1l9vLF9qNoRZgd6RAcJs85llAz2fQqw16ONSpMaljglcUdwk/sVnp0l17DYBJkM5iq 31PrkI6KKSE101MbT2c2o/YNbjeK2209xeqKubX1lzYzNeK6/IX8v1r417nvQyvCg8j6yA9i 4gTgybavMyUSldKAveTGg4t+hN3pq/XeHw47oLQjjh3NLWs9yTFw5QvDfckzRCpe5FeNrmFH Un8CZ5/ZYDmJeo0llyudh9BMvpV8ft+PsW6cOWLwqCvO/lIkzevjGAB64d4mBHplWI0WqvT0 pAJzuvNlAqBSzDigU2vtsfosY9BbDAWWGG4zGK3YewZLr03doENB2C0JsSxzdgrnJ/hVUlT8 1u7Dk8H0sukEfaLR2T0xhYYlUEeoHj83DC90yQxiDYx6KyWwC3Jxe3mMhsBIG9CAmd43x/gJ o29jtZSW0bNDUBhlR254lj33aZfo7tXIGzaQEMOdC/zZ21vSaq/sLOebtUHsst593UKFr7lP xbHEvb0uFMC3jnmHndCyTxeFXnioZj/kxFgySqcIHt1sHvFaJR1zBbb6sbbQK0Z1T4HSS9kz DjPUwLkbp/5oJPOzsmF77jtMgDpHodeeiTq046a4S6y5GkxRAa6g+j2gdr/Vw4zzS780dBuE yTOthf1JIfxhMHYeapqeFdlAFjk5o90AIZ7x8Exgo0Xx3UAiJGS4lIIlG7yNZNQ3qe0Px9vD XYbhsXY5gTowhgpL3SVwJz0THuZxdRJaNyzY2dQ0SU4pZMvau/c/PlPmi17pUC9pATabK1mn zsT/vAp7WYTn+ADvAd+hjXYGL0ZGlNUeDD9jxndpc7rt71ZPSz8FNr4nFo7h92qC6uO5x1RS GqsMIl3Bjd+t41+KA6eiyC1s9C8PoOMMpRL8UfI2xbY07oLdNRrzaFM3HQ/fzq65CxAqaZzj AQyj8/k+tHfcSM1uvr+WEYQNyWpNZ1NvGux3OAOxoDOmNr3VpR5RmdUBt2xEbTxQWhU7bO+Z 2PsWHU9sivJRuaZRFXCrh8g9zWWTdiqLy3FfSFJi4w9G1/NYhQY2llcXS1mzMdmTUbzlZCnK AEhoWlPgzyw4hpUlrAyb0i5AjqZ/V34LG9zEcfXLQIKvFsbuQGIYYrHv7g1R2YBr9WgtFDfc DXFIV4TXCdSAArcQAmyW9vmrc/J9+zSbganB93JZ7jG6elXVvPTgImqzpMj5DGUcMOGInhlC fQ/nEtFR3FwXcrDyX0JTGQMmiTBYtT+xl/08zBrrs257PXgWR7+rYqJBbxINNxz+hewya6dP u+UjSx9JH5WzJQJjXPPzbEe2hYVhUQMP3G1Fq8csCfWUK/KsqpeDhpecyEqccUVt+Qz2Q5CP cOdgdTwl/Z5gvMzF1ZZRAnhl8WuNqloaym2MFLKAlrONazTf2WahZGqJ/nlF/sN1LYx1VX4o zuQHk79My7WkjDoU0vqKuRQlGSAOwQYvoihcxFrAGylTdT8axT9PsUk6F9+ibAymH7OMnYRd DZmdEYY5LyW8SRGj+9xH2texnVgJOiA3S2e6qOLT/Re+esuGSlym+9AtT4izKBJ6ShfWPFvs C7br9oru1P/1+fSknxoVx1BrjsNj4WO9xYHW+2R5txLXnDK+wgI5GObBkERptdrPdbovrhZ1 tnFkK+bwNJq/Nfd/M9aDM/Reprv2JUJPh/gGTqSBwwAH2fD3YD3gkVclLSK9CTQoMVi7Jfrn 5UKR/lQU1lnTpsn
  • Ironport-sdr: np8UxUhpD/qIr7Sik2Lr+fLoJHzM0G58YffwF+P6Ktnc27NBvx8khjVPBfLh4SklsEQ0KCmHyp k/cSAbrFHv/peoGcrUAV2TWJpQ63mFj3sRYNllgS9mXgxkzzG70hI08pFzzCsHbk7fEZKrwTPo 7Ur5mjNIp617KWYpQqvv6oQG7HpDzBLdBI+VEt4D5yOYZLJ+t7ZHv82XAwZ5X5oRrCPC0+gnNp lKjuDhNO0AD1SjIWZAP2jL1UXawWTwPsvKmubZpbHFiMvfWzi89WxtQMmFCjSPh4jY8z44KpZM 6gRXJ+0NBCio7/aq8Dj8j55o

Unfortunately I don’t have any Docker images with Coq Hammer; however, you may find this repo useful, which contains examples of how to extend the docker-coq image with various additional packages.

https://github.com/appliedfm/docker-coq-vst

Kindly,
-t

Sent from my iPhone

On Feb 9, 2022, at 12:11 PM, Richard Dapoigny <richard.dapoigny AT univ-smb.fr> wrote:


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



Archive powered by MHonArc 2.6.19+.

Top of Page