The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Thank you for the quick reply. Good to know that there is a script which automates the process.

I got this error, though.

On Sun, Sep 27, 2020 at 12:35 PM Andrew Appel <appel AT princeton.edu> wrote:

Agnishom:

Two or three days ago, I wrote an updated and detailed explanation of how to install VST, on this page:

https://vst.cs.princeton.edu/download/

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 Toolchain

I am not sure what the issue is, and how to fix it. Any help would be appreciated.

--Agnishom