Emilio Jesús Gallego Arias

> @ejgallego What specifically do you see as so hard to revert that you'd rather prefer splitting the downstreams between `rocq-stdlib` and `coq-stdlib`? This PR , #19310, and more critically,...

One problem we seem to have is that the github interface doesn't scale for PRs like this. In the past that made discussion and review very hard, but I other...

> Reviewing by commits may help (I took great care of having meaningful self-contained plugins, on both branches, if only for all the rebase I have to do to remain...

I don't know a lot about Nix @Zimmi48 , how does the Nix setup work for the developer who breaks `coq-stdlib` and has to prepare N overlays, having to build...

Thanks @jpoiret , indeed the logic for goals and errors is different. I think here you may be witnessing 2 things: - over-execution: in 0.2.2 we detected some commands do...

Ping @jpoiret , I want to check that my understanding of this issue is correct: I guess you want a fully lazy mode, so that sentences are not executed while...

@jpoiret thanks for the example, I'm still not sure tho what the best fix for this issue is. As you note, requesting a goal will indeed force the execution of...

@kindaro , indeed that's the case today, however it is easy to have `rule` (you mean `rule` above I think, not `action`) to produce test targets.

Yes @rlepigre , I'm almost at the point I will resume work on Dune Rocq; thanks for your patience.

Looks pretty good to me, I have some minor comments, but I suggest to add a changelog and documentation, as I can fix the comments myself.