Stream: Coq devs & plugin devs

Topic: 4.14


view this post on Zulip Ali Caglayan (May 23 2022 at 12:08):

Hi, can we reach a consensus on https://github.com/coq/coq/pull/15867 ?

@Emilio Jesús Gallego Arias

view this post on Zulip Ali Caglayan (May 23 2022 at 12:08):

To update, PMP says he is happy to take responsibility in maintaining our (substantial) modification of camlp-streams.

view this post on Zulip Ali Caglayan (May 23 2022 at 12:13):

On the other hand, 4.14 causes alerts in older versions of Coq too. So if we decide to go down the route of adding camlp-streams as a dep we might need to add it for all older versions or at least cap before 4.14.

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:15):

(FTR you can still remove half of that ml file. We don't use debug and the Sapp node is dead code.)

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:35):

You could do many things indeed, but still I fail to see why adding a dependency as everyone else has done (thus following upstream rec) is not the least effort.

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:35):

Pierre-Marie claims that there is a lot of cost on adding the dep

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:35):

but I fail to see that

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

on the other side adding this crap to clib has a cost

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

many cost for Coq devs

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

it increases the surface of our API, which impacts everybody

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

so it's not only about maintaining it

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

moreover, something in clib is supposed to be of general use

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 12:36):

whereas this thing is private to gramlib?

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:51):

many cost for Coq devs

(doubt)

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:51):

the fact this is private to gramlib is even a stronger argument for forking

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:51):

half of the library implemented in that PR is actually dead

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:52):

we could make the attack surface even smaller by tweaking gramlib

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 12:52):

adding coupling to a legacy, unmaintained library for a private one does seem like pretty bad practice to me

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:16):

Pierre-Marie Pédrot said:

adding coupling to a legacy, unmaintained library for a private one does seem like pretty bad practice to me

Ok if you think forking is better, then we can fork it, but I'd suggest to put in gramlib not in clib, and use (private_module )

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:16):

Note that the coupling was there, so the dep is what upstream suggested, and I think we should try to follow upstream.

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:17):

Note that the coupling was already there, in the same way we are coupled to OCaml's stdlib

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:17):

Forking has still a cost, but using private modules alleviates quite a bit of the pain

view this post on Zulip Ali Caglayan (May 23 2022 at 13:18):

OK we are settled then? Remove from clib, put in gramlib and make private?

view this post on Zulip Ali Caglayan (May 23 2022 at 13:18):

cc @Gaëtan Gilbert did you try putting it in gramlib before?

view this post on Zulip Gaëtan Gilbert (May 23 2022 at 13:20):

I tried putting it in gramlib but it's also used by coqproject_file
there's a comment in my PR about this

view this post on Zulip Gaëtan Gilbert (May 23 2022 at 13:21):

is https://github.com/ocaml/dune/issues/4892 fixed yet? looks still open

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:22):

Gaëtan Gilbert said:

is https://github.com/ocaml/dune/issues/4892 fixed yet? looks still open

No idea, but if we can put in gramlib then it is not critical to make it private (we can put a comment)

view this post on Zulip Emilio Jesús Gallego Arias (May 23 2022 at 13:23):

if that's a Coq-wide dependency then I still think that the same way we don't fork OCaml's stdlib (oh wait, we actually do!) we shouldn't fork that.

Indeed, it is unfortunate that the discussion is really about the mess clib is, and in particular our hideous fork of the already not very good OCaml stdlib, and my desire not to continue with the trend "death by a thousand paper cuts" that we are doing, but indeed, that's a discussion way deeper than what this PR requires.

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 13:33):

It's trivial to fix coqproject not to use the Stream library. I'm not even sure why it uses it in the first place. (By imitation of legacy code that was around at the time maybe?)

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 13:34):

I can open a PR if nobody wishes to do it.

view this post on Zulip Ali Caglayan (May 23 2022 at 14:00):

Why are we using streams to read a file?

view this post on Zulip Pierre-Marie Pédrot (May 23 2022 at 14:02):

https://github.com/coq/coq/pull/16058


Last updated: Feb 05 2023 at 22:03 UTC