Stream: Coq devs & plugin devs

Topic: Minisys and coqdep


view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:26):

@Emilio Jesús Gallego Arias I don't quite understand why we need to get rid of minisys from coqdep? Are you suggesting to rely on System? Whats the point of that if System includes Minisys?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:28):

We don't need to, what I mean is that it is redundant now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:28):

we can just merge minisys into system

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:28):

before, due to bootstrapping, system couldn't be used

view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:29):

OK merging is what you had in mind

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:29):

actually we have a lot of weird stuff in these modules that would be great to replace with stdlib / more standard stuff, but that's orthogonal

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:29):

yup, merging, and actually reducing the surface api there

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:29):

well I guess merging makes sense, but we can keep both if we want

view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:31):

OK I will merge for now

view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:35):

OK https://github.com/coq/coq/pull/15765


Last updated: Feb 02 2023 at 13:03 UTC