Alex Sanchez-Stern (Apr 10 2023 at 18:36): Alex Sanchez-Stern (Apr 10 2023 at 18:36):Hey all,
I noticed that when I try to install ocamlformat to format my ocaml code, opam insists on downgrading me to Coq 8.15 instead of more recent Coq like 8.16. So, if I want to contribute ocaml code to coq 8.16, I have to write my code, switch to an opam switch which has Coq 8.15 and ocamlformat, run dune fmt, and then go back to the coq 8.16 switch for any testing. Is ocamlformat supposed to be compatible with Coq 8.16 or later? If so, how do I get it set up?
Gaëtan Gilbert (Apr 10 2023 at 18:40):does opam say anything interesting if you tell it eg opam install ocamlformat coq.8.16.1?
also I think we disabled ocamlformat so I don't think dune fmt will do anything?
Alex Sanchez-Stern (Apr 10 2023 at 18:46):Oh, it might be a coq-lsp and coq issue, I guess the ocaml-format install just triggered it. When I tried that command (well, 8.16.1 instead of 8.16), it asked to remove coq-lsp. If I try adding coq-lsp to the command, it says
[ERROR] Package conflict!
* No agreement on the version of coq:
- coq >= 8.16.1
- coq-lsp = 0.1.2+v8.16 → coq < 8.16
Re ocamlformat being disabled, maybe this issue is more coq-lsp specific than I thought then. coq-lsp dune fmt still does ocamlformat things, and the CI fails if you haven't formatted.
Gaëtan Gilbert (Apr 10 2023 at 18:58):that's interesting, the coq-lsp package for that version says "coq" { >= "8.16.0" & < "8.17" }
https://github.com/ocaml/opam-repository/blob/master/packages/coq-lsp/coq-lsp.0.1.2%2Bv8.16/opam#L22
and if I ask my opam to install coq.8.16.1, that version of coq-lsp and ocamlformat it has no complaints
Alex Sanchez-Stern (Apr 10 2023 at 19:06):Oooh actually I found the issue, it was a problem on my end. I forgot that when you opam install . a local coq-lsp build, it misreports the version of coq-lsp as being from the repo. So while my opam was claiming I had coq-lsp.0.1.2+v8.16, I actually had pinned a local copy of coq-lsp on the v8.15 branch, so it didn't like Coq 8.16.
Paolo Giarrusso (Apr 10 2023 at 19:23):I forget the conditions but I've also seen opam use unhelpful versions for local packages. And without prompting!
Last updated: Nov 29 2023 at 22:01 UTC