Ali Caglayan (May 23 2022 at 12:08): 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
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.
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.
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.)
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.
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
Emilio Jesús Gallego Arias (May 23 2022 at 12:35):but I fail to see that
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):on the other side adding this crap to clib has a cost
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):many cost for Coq devs
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):it increases the surface of our API, which impacts everybody
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):so it's not only about maintaining it
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):moreover, something in clib is supposed to be of general use
Emilio Jesús Gallego Arias (May 23 2022 at 12:36):whereas this thing is private to gramlib?
Pierre-Marie Pédrot (May 23 2022 at 12:51):many cost for Coq devs
(doubt)
Pierre-Marie Pédrot (May 23 2022 at 12:51):the fact this is private to gramlib is even a stronger argument for forking
Pierre-Marie Pédrot (May 23 2022 at 12:51):half of the library implemented in that PR is actually dead
Pierre-Marie Pédrot (May 23 2022 at 12:52):we could make the attack surface even smaller by tweaking gramlib
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
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 )
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.
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
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
Ali Caglayan (May 23 2022 at 13:18):OK we are settled then? Remove from clib, put in gramlib and make private?
Ali Caglayan (May 23 2022 at 13:18):cc @Gaëtan Gilbert did you try putting it in gramlib before?
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
Gaëtan Gilbert (May 23 2022 at 13:21):is https://github.com/ocaml/dune/issues/4892 fixed yet? looks still open
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)
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.
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?)
Pierre-Marie Pédrot (May 23 2022 at 13:34):I can open a PR if nobody wishes to do it.
Ali Caglayan (May 23 2022 at 14:00):Why are we using streams to read a file?
Pierre-Marie Pédrot (May 23 2022 at 14:02):https://github.com/coq/coq/pull/16058
Last updated: Jun 08 2023 at 04:01 UTC