Stream: VsCoq devs & users

Topic: Support for older versions of Coq


view this post on Zulip Théo Winterhalter (Jun 05 2020 at 15:32):

I saw @Maxime Dénès comment on github that at some point the older Coq versions would no longer be supported. I guess it might be also relation to the new document model. What is the policy regarding this?

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:33):

Indeed, the new document manager will introduce some fundamental incompatibilities, so I plan to drop support for old Coq versions as part of https://github.com/coq-community/vscoq/pull/140

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:33):

To compensate, I think we should package the current version of VsCoq as a legacy, minimally maintained extension

view this post on Zulip Théo Winterhalter (Jun 05 2020 at 15:34):

I see, that's great!

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:34):

What would be ideal for users is if we can make the two coexist, so that they can be installed simultaneously, but activate only when they detect the corresponding Coq version

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:34):

I haven't explored whether that's easy to do or not yet

view this post on Zulip Théo Winterhalter (Jun 05 2020 at 15:35):

So it will not be a progressive drop, but at some point there will be a different VSCoq.

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:35):

Yes, at least that's what I have in mind for now. The reason is that we effectively drop half of the code (the "server" part)

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:36):

Actually, more like 2/3 of the code :)

view this post on Zulip Théo Winterhalter (Jun 05 2020 at 15:37):

I'm really looking forward to it.

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:37):

I already have a working prototype (as a Coq branch), but it lacks delegation of proofs (for parallel execution)

view this post on Zulip Maxime Dénès (Jun 05 2020 at 15:38):

@Enrico Tassi is working on it too

view this post on Zulip Ramkumar Ramachandra (Jun 05 2020 at 16:07):

Exciting!


Last updated: Jan 30 2023 at 17:03 UTC