Stream: VsCoq devs & users

Topic: Beta testing VsCoq 0.3.6


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Fabian Kunze (Dec 09 2021 at 21:53):

master also gives the "version" coq-8.15-alpha, does it?

view this post on Zulip Fabian Kunze (Dec 09 2021 at 21:53):

i think we just parse coqc -v, so master should also work

view this post on Zulip Karl Palmskog (Dec 09 2021 at 21:53):

no, it switched to coq-8.16+alpha a while ago to my knowledge

view this post on Zulip Fabian Kunze (Dec 09 2021 at 21:53):

ok, but i just check >=8.15, so this should be fine

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Fabian Kunze (Dec 09 2021 at 21:57):

thanks Karl!

view this post on Zulip 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.

view this post on Zulip 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 ^^'

view this post on Zulip Paolo Giarrusso (Jan 02 2022 at 15:24):

Works for me, thanks! (both on 8.13.2 and 8.15+rc1)

view this post on Zulip Paolo Giarrusso (Jan 02 2022 at 15:28):

and I'm going to assume the "alpha" labeling is overly cautious and keep using it

view this post on Zulip 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...

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC