coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrew Appel <appel AT princeton.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Facing Strange Error Trying to install VST
- Date: Sun, 27 Sep 2020 13:35:02 -0400 (EDT)
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT princeton.edu; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT yellowcard.cs.princeton.edu
- Ironport-phdr: 9a23:FgVgzh0YgXXWm9LQsmDT+DRfVm0co7zxezQtwd8ZseMQI/ad9pjvdHbS+e9qxAeQG9mCtLQe16GP6vmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBi5ogndq9QajZZ/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF+gqJVrgyiqRN9zY7afY6aO+Z/fq3aYdMXXnBOUtpNWCFbGI6wc4kCAuwcNuhYtYn9oF4OoAOiCAmqGezv0CFHh3Hr1qAmy+QhCR/J3Ag9FN8JqnvUtM31O7kWUe2u1KnI1zTDb/VK1jjj9IjIdRYhreuSUr1tbMrc0E8iHB7KgVuMs4LqJS+V1vgTvGiB6eptTf6ihmE6pg1soDWhycgih4bUio8UxF7J9jt1zYIrKNC4R0N2YMOoHZ9MuyyVOIZ4Qs0sTmJ2tSs0ybAKpYO2cSoMxZ86yRDfbPmHfJKJ4hLlTOuROS14hHNjeL2jmRmy7U+gyuvmWsaqzVlKszJJktbNtnAR1xzT99OIRuFh8Uem3DaDzx3T6vlaLkAyk6rXMYAuzaMtlpcVrE/NHTf2lV3rgKOIdUgo4PWk5/n5brn8u5OROY55hhv/P6kvgsCyBeU1PhIQU2WV+emwzqDv8E73TblQkPE6jK3UvIjHKcgFpaO1GRJZ3ps95xqlEjur3tUVkWMHIV9Hfh+MkpLnNEvUIP/iCPeym1Ssnylvx/DBJrDgAovCLnzHkLfmc7dy91RTyBAuwtxF+51UEasNIOrpWk/wstzXEgE2MxCzw+bhEtlyyJ4RWX+XDq+YNqPdr0OI6/oyL+WSZ4IZoivxJ+U76/L0kHM0l14QcbOo0JYWcHy4G+5pI0SdYXrimNcBFmIKsxIkQ+zykF2NTzpTam2uUKIn/D07EJimDYbFRo+xnrOBwCC7HptMam9YF1+MDG/kd5+YVPcUdCKSPshhnyQYWrimUo8tzA2htAvny7V8NefU4S0ZtZf71Ndv/eHTlBcy9SZ1D8uHyW2NQXt0zSs0QGo927k6qkhgwB/X2q9hxvdcCNZ75vVTUw58O4SKnMJgDNWncwTNZNqWAH++WtiiSWU4Vso8x/cWeUd7ENi+iRaF0ia3VexG34eXDYA5p/qPl0P6INxwni6fiPsRymI+S84KDlWIw7Zl/lGOVZbTkkOSmrqtc+IR0DOfrD7en1rLh1lRVUtLaYuAXX0bYRGH/8X04kfFULSnE7hhORAH0dSDLKBHdtrvy1hKWaW6YYWMUyeKg261QC2w6PaJZYvudX8a2XyNWkMf1RgJ/HCNOBQ5AGGsr3+MVTE=
Agnishom:
Two or three days ago, I wrote an updated and detailed explanation of how to install VST, on this page:
The basic point, as you'll see there, is that there is enough system-dependency in opam-installing any package for Coq, not only VST, that the recommended way to do it is via the "Coq Platform" shell scripts. These do an opam-install of whatever packages (including VST) you choose, but they are more likely to get the dependencies right than doing it yourself via opam.
(Personally I find this a bit mysterious, as I would have thought that this is exactly the purpose of opam itself, but apparently opam needs some help.)
-- Andrew Appel
From: "Agnishom Chattopadhyay" <agnishom AT cmi.ac.in>
To: "coq-club" <coq-club AT inria.fr>
Sent: Sunday, September 27, 2020 12:49:30 PM
Subject: [Coq-Club] Facing Strange Error Trying to install VST
Hi;I am trying to follow this and install VST.However, I am facing some problem, even though I seem to have the correct repositories and an updated opam.agnishom@agnishomDuncan:~$ coqtop -v
The Coq Proof Assistant, version 8.12.0 (September 2020)
compiled on Sep 24 2020 22:43:53 with OCaml 4.10.0
agnishom@agnishomDuncan:~$ opam switch
# switch compiler description
4.07.0 ocaml-base-compiler.4.07.0 base-bigarray.base base-threads.base base-unix.base ocaml-base-compiler.4.07.0
→ 4.10.0 ocaml-base-compiler.4.10.0 4.10.0
system ocaml-system.4.05.0
agnishom@agnishomDuncan:~$ opam install coq-vst
Sorry, no solution found: there seems to be a problem with your request.
No solution found, exiting
agnishom@agnishomDuncan:~$ opam search coq | grep vst
coq-vst -- Verified Software ToolchainI am not sure what the issue is, and how to fix it. Any help would be appreciated.--Agnishom
- [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/27/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Andrew Appel, 09/27/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/27/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Michael Soegtrop, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Michael Soegtrop, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Michael Soegtrop, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Agnishom Chattopadhyay, 09/28/2020
- Re: [Coq-Club] Facing Strange Error Trying to install VST, Andrew Appel, 09/27/2020
Archive powered by MHonArc 2.6.19+.