Stream: Coq users

Topic: coq-vst not found using opam

view this post on Zulip Donald Sebastian Leung (May 31 2021 at 12:13):

So I decided to install Coq manually on Linux (Ubuntu 20.04 LTS) using opam since I need to use clightgen to generate ASTs for my own C programs for VST (currently starting volume 5 of SF) which cannot (easily) be done by using the Snap package + other packages included within the distribution.

My version of:

Now when I do opam list coq-vst (same for coq-vst-64), I get an error message saying that the package cannot be found:

# Packages matching: (installed | available) & name-match(coq-vst)
# No matches found

I'm probably missing something obvious here so any pointers are much appreciated :smile:

view this post on Zulip Gaëtan Gilbert (May 31 2021 at 12:18):

what does opam repo say

view this post on Zulip Donald Sebastian Leung (May 31 2021 at 12:20):

[NOTE] These are the repositories in use by the current switch. Use '--all' to
       see all configured repositories.

<><> Repository configuration for switch default ><><><><><><><><><><><><><><><>
 1 default https://opam.ocaml.org

Oh, I need to include the correct repository, thanks for the hint :+1:

EDIT: May I be informed of which repo to add?

view this post on Zulip Gaëtan Gilbert (May 31 2021 at 12:23):

https://coq.inria.fr/opam-using.html

Using opam to install Coq packages

view this post on Zulip Donald Sebastian Leung (May 31 2021 at 12:24):

Thanks!

view this post on Zulip Michael Soegtrop (May 31 2021 at 17:00):

The Coq Platform snap package does include VST and clightgen. See (https://github.com/coq/platform/releases/tag/2021.02.1). I would say this is the recommended method to install this. Alternatively you might want to use the Coq platform "compile from sources" scripts, which create a new opam switch and compile Coq, CompCert and VST from sources via opam.

view this post on Zulip Donald Sebastian Leung (Jun 01 2021 at 02:26):

Querying snap info coq-prover shows the following available commands:

coq-prover.clightgen does not seem to be present. Or can clightgen be invoked through some other alias or method I'm not aware of?

view this post on Zulip Michael Soegtrop (Jun 01 2021 at 07:00):

@Enrico Tassi is the expert for the snap package - I guess it is an omission to have an abbreviated named but I would expect that the executables are still there, buried in the folder hierarchy.

view this post on Zulip Enrico Tassi (Jun 02 2021 at 10:44):

it's a bug, the code to clean up unnecessary files in the snap is too aggressive. I think there is already a plan to share this code with the other installers, but it is not there yet. @Michael Soegtrop if you need a quick fix, the problem is here: https://github.com/coq/platform/blob/cd9e106fcf34cad31192337234ee15056dc510b2/linux/snap/snapcraft.yaml.in#L27 (I'm on VAC)

view this post on Zulip Michael Soegtrop (Jun 02 2021 at 14:58):

@Enrico Tassi : thanks for the pointer - I indeed need to continue to work on this.

view this post on Zulip Enrico Tassi (Jun 02 2021 at 15:00):

Once the file is not erased, one has to add a section down in the file, like the one for coqc, in order to have coq-prover.clightgen. Having the binary without the coq-prover. prefix is more involved, since it's an operation that needs the approval from the snap store admins.

I'm sorry I did not know that compcert ships this binary, my cleanup line was to purge ocamlc & co.

Last updated: Oct 13 2024 at 01:02 UTC