I have a version of vscoq that should be backwards compatible, and work for >=8.15
I would appreciate beta-testers: People using 8.15-rc1 (or master, or coq.dev), and people using older versions, to check those two scenarios.
Just drop me a short message here if you tested it for a bit an it worked/didn't.
we only have 8.15-rc1 in the
core-dev opam repo (
coq.8.15+rc1). So it requires a bit of sophistication to install it (and few packages are compatible with it currently)
master also gives the "version" coq-8.15-alpha, does it?
i think we just parse coqc -v, so master should also work
no, it switched to
coq-8.16+alpha a while ago to my knowledge
ok, but i just check >=8.15, so this should be fine
(i was not sure whether it might be coq-master, did not use master for a while)
core-dev opam repo is fine as well, or if people install it directly from a git clone
so for willing beta testers that want to use Coq 8.15+rc1 or Coq master, please do:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
and then either:
opam install coq.dev
opam install coq.8.15+rc1
I'll try to watch here if someone has opam or other Coq installation trouble as well. We need more IDE testing overall for sure.
Yes, it's a bit unfortunate that the rc1 is out and the topmost IDE on https://coq.inria.fr/user-interfaces.html does not work with it ^^'
Works for me, thanks! (both on 8.13.2 and 8.15+rc1)
and I'm going to assume the "alpha" labeling is overly cautious and keep using it
BTW, starting from 8.14, VsCoq might benefit from support for
Set Printing Raw Literals.... confusingly, using
Set directly seems to work fine, unlike the other
Yep, that's the case, the alpha was just because i only tested it for 5 minutes at this point
Last updated: Jun 04 2023 at 23:30 UTC