coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Facing Strange Error Trying to install VST

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] Facing Strange Error Trying to install VST
Date: Sun, 27 Sep 2020 11:49:30 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:eSNY+xKnBMN9QN+21NmcpTZWNBhigK39O0sv0rFitYgeL/rxwZ3uMQTl6Ol3ixeRBMOHsq0C0bad4vGocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalsIBi5ogncss0bipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhcN+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIdMOZXqYn9pkAOrRu5BQmpGeji1D9IiWXq3a0m1OQhCRvJ0xEgH9MOqnvVrMj+OaAIXuC6yqnIzC7Db/NR2Tf484XHbhUhofCWUb1qbcXd00gvFwXcg1iWtIfqMC+b2P4XvGiH8+pvS/ivi2g/pgxvojWi2tkgh4bGiI8WxF3J6yV0zZsoKNC7VkJ2fcCoHZRfui2EK4Z6XM0sTmB2tCs0xLMLupG1ciYUxJknxRPSbeGMfYaP4hLmTumRIDF4iWp4eLKnmRmy906gxvfiWcapzVZHqDdOnNrUtn0VyhDf98iKRuFj8kqu2juDzR7f5vxeLUwplqfXN4YtzqAsmpcXq0jOHS/7lF/rgKKXd0go4Oel5uvhb777vJGTLZV0hRv7Mqk2msywH+A4Mg8WUmie4+u81bnj8VflT7VPj/06iLPWv4zAKcQaoK61Gw5V0oA95BajFzqqzckUkHkdIF5bdx+KjJLlN0/TLPziEPuygEignC9ux//cP73hBpvNLmLEkLfkZbty8UFcyAwyzdBE55JUDbQBLenvVU/0tdzUFAU2PBCuz+bmDtVxzpkeVn6XAq+FLKPStkeF6f4oI+mVfYMapDL9K+U+6PP1ln84mVodfbGz0pcNaXC4GO5mI0SDbnb2jNcBCzRCgg1rR+vzzVaGTDR7ZnCoXqt66CtoJpihCNLqSYasm7yG2W+QHpRKemdeA1yMAH75P9GNVPENcyKVJ+dqlz1CXLPnSol3hkLmjxPz17cydrmcwSYfr5+2jIEktd2Wrgk78HlPN+rY1miMS29umWZRHm092aE5qEc7y1HRiPEl0cwdLsRa4rZyail/NZPYyLUkWdX7WwaHddKIDl+tBNSgU2loEoABhuQWakM4IO2MywjZ1nPzUbQQlvqCD9o19PCE0g==

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

[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