Fabian Kunze (Dec 09 2021 at 21:44): Fabian Kunze (Dec 09 2021 at 21:44):https://github.com/fakusb/vscoq/releases/tag/0.3.6-alpha.0
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.
Fabian Kunze (Dec 09 2021 at 21:49):Just drop me a short message here if you tested it for a bit an it worked/didn't.
Karl Palmskog (Dec 09 2021 at 21:52):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)
Fabian Kunze (Dec 09 2021 at 21:53):master also gives the "version" coq-8.15-alpha, does it?
Fabian Kunze (Dec 09 2021 at 21:53):i think we just parse coqc -v, so master should also work
Karl Palmskog (Dec 09 2021 at 21:53):no, it switched to coq-8.16+alpha a while ago to my knowledge
Fabian Kunze (Dec 09 2021 at 21:53):ok, but i just check >=8.15, so this should be fine
Fabian Kunze (Dec 09 2021 at 21:54):(i was not sure whether it might be coq-master, did not use master for a while)
Karl Palmskog (Dec 09 2021 at 21:54):OK, then coq.devfrom the core-dev opam repo is fine as well, or if people install it directly from a git clone
Karl Palmskog (Dec 09 2021 at 21:56):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
or
opam install coq.8.15+rc1
thanks Karl!
Karl Palmskog (Dec 09 2021 at 21:59):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.
Fabian Kunze (Dec 09 2021 at 22:01):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 ^^'
Paolo Giarrusso (Jan 02 2022 at 15:24):Works for me, thanks! (both on 8.13.2 and 8.15+rc1)
Paolo Giarrusso (Jan 02 2022 at 15:28):and I'm going to assume the "alpha" labeling is overly cautious and keep using it
Paolo Giarrusso (Jan 02 2022 at 16:52):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 Display options...
Fabian Kunze (Jan 03 2022 at 10:51):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