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:
opam repo say
[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?
Using opam to install Coq packages
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.
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?
@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.
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)
@Enrico Tassi : thanks for the pointer - I indeed need to continue to work on this.
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 03 2023 at 20:01 UTC