Problem when updating opam about aac-tactics HOT 6 CLOSED

Hi. I have tried to reproduce the problem, like this:

$ opam repo list
  30 [http]  coq-released     https://coq.inria.fr/opam/released
  20 [http]     default     https://opam.ocaml.org

$ opam install -v -j4 coq
$ opam install -v coq-aac-tactics.8.5.0
$ opam upgrade

but failed. For me, the above commands worked fine. So I am not sure what is wrong.

If you can, please post the output of the following commands:

$ opam repo list
$ cat ~/.opam/repo/coq-released/packages/coq-aac-tactics/coq-aac-tactics.8.5.0/opam
$ cat ~/.opam/repo/coq-released/packages/coq-aac-tactics/coq-aac-tactics.8.5.1/opam

from aac-tactics.

You should use opam lint to detect this kind of problems:

$ cd released/packages/coq-aac-tactics/coq-aac-tactics.8.5.1/
$ opam lint
[ERROR] At .../released/packages/coq-aac-tactics/coq-aac-tactics.8.5.1/opam:14:45:
  Not a recognised version-control URL
File format error

(opam 1.2.0)

from aac-tactics.

The errors you guys mention are produced by opam installed as a Debian package, or by something you compiled yourselves?

In my context:

• when I use opam 1.2 compiled from source, everything is fine (opam lint prints PASSES)
• when I use opam 1.3 compiled from source, everything is fine (opam lint print PASSES)
• when I use opam from master branch, I get a similar error that I can fix by replacing https by git+https.

That, however, does not fix your problem. When I try to use opam provided as a Debian package, I still get an error.

At the moment I am not sure what is the right thing to do.

from aac-tactics.

Ok. I think I've figured out what to do. I've pushed appropriate commit (coq/opam@ab6abd2)

Let me please know if everything works on your side.

Thank you.

from aac-tactics.

It is easy to fix, just use the actual address of the repository rather than using a webpage: https://github.com/coq-contribs/aac-tactics.git. opam is actually right to complain since there is no way it can use the address currently in the opam file to perform a checkout.

from aac-tactics.

Thanks. Done (coq/opam@408c36d).

from aac-tactics.