Emilio Jesús Gallego Arias

Indeed this can be improved, as of today the code that detects coqlib is still in bad shape, despite our attempts to fix it. If it doesn't find coqlib it...

Yes, it is not an easy fix. Not worth opening an issue IMO, some ideas are: - forbid calling `Env.init` more than once per execution, once you get the env,...

> This is in effect, how it works today. If you call Env.Init after it has already been initialized, it detects the reference being set and just passes the already...

That's good, but indeed we build stdlib with -boot (which is actually our goal medium term), so it is normal Env.init is never called. I'm more curious about regular developments,...

The right way to run `coq_makefile` is indeed to use `dune exec` , however, we are still missing a feature in dune that allows us to specify runtime deps, so...

For diffing I really recommend using `patdiff` , https://github.com/janestreet/patdiff , tho a tree diff algorithm could also be interesting, but much more effort. Another thing that would be cool would...

Another interesting exploration for diffs is to see if the algorithms used by vue/react for virtual dom update would work well in this context, IMHO they should.

> * the info should be in a dedicated libobject/summary entry (I guess in vernac, of type `Loc.t Names.Cmap.t ref`) and not recomputed from libobject What does a "dedicated libobject"...

> Libobject _is_ the API to store data in the vo files and load it ar require/import time. I am aware of that, how does this relate to your comment...

I guess I'm missing something very obvious @gares but I don't understand what you mean.