Théo Winterhalter (Jun 05 2020 at 15:32): 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?
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
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
Théo Winterhalter (Jun 05 2020 at 15:34):I see, that's great!
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
Maxime Dénès (Jun 05 2020 at 15:34):I haven't explored whether that's easy to do or not yet
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.
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)
Maxime Dénès (Jun 05 2020 at 15:36):Actually, more like 2/3 of the code :)
Théo Winterhalter (Jun 05 2020 at 15:37):I'm really looking forward to it.
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)
Maxime Dénès (Jun 05 2020 at 15:38):@Enrico Tassi is working on it too
Ramkumar Ramachandra (Jun 05 2020 at 16:07):Exciting!
Last updated: Jun 04 2023 at 23:30 UTC