Beta Ziliani (Jun 13 2020 at 16:04): Beta Ziliani (Jun 13 2020 at 16:04):I decided to rename Unicoq's Make file to _CoqProject, but that broke Mtac2's CI because it was using the instructions from "somewhere" in opam:
opam pin add unicoq https://github.com/unicoq/unicoq#master
Initially, the unicoq.opam file in the project was empty. So I decided to create it with the relevant information. However, when I try to pin add the project (locally), with
> opam pin add ~/my_path/to/unicoq
it fails to acknowledge there is a unicoq.opam file and fails.
Fatal error:
In /home/beta/.opam/4.06.1/.opam-switch/sources/unicoq/unicoq.opam:
unsupported or missing file format version
The opam doc says:
opam pin add PKG URL modifies package
PKG to fetch its source from URL. If a package definition is found in
the package's source tree, it will be used locally.
But it seems to not be doing this. Any clues? Thanks!
Karl Palmskog (Jun 13 2020 at 16:14):have you tried: opam pin add https://github.com/unicoq/unicoq#master -k git
for local pins, I strongly recommend: opam pin add ~/my_path/to/unicoq -k path
Karl Palmskog (Jun 13 2020 at 16:18):I see now that https://github.com/unicoq/unicoq/blob/master/unicoq.opam is empty, then pinning via git will obviously not work.
Beta Ziliani (Jun 13 2020 at 16:21):The idea is to upload the file, but I'm trying first locally
Karl Palmskog (Jun 13 2020 at 16:24):if you're not using -k path, I believe the default local behavior is -k git, so if you haven't checked in the unicoq.opam file into version control it won't work.
Beta Ziliani (Jun 13 2020 at 16:24):Thanks Karl! the missing -k path did the trick
Karl Palmskog (Jun 13 2020 at 16:28):it's not recommended to have url { ... } in an opam file that lives in a repo, this is typically inserted when uploading it into an opam repo like coq-released.
Last updated: May 28 2023 at 16:30 UTC