Emilio Jesús Gallego Arias

@rgrinberg it is because we've been told that depending on things in `_install` is not good practice. However I'm not sure that advice is correct.

I mean, why the rule for `pkg.install` can depend on things there but our Coq rules cannot?

@rgrinberg I'm fine not depending on `_install`, as long as we agree on a general method to provide runtime deps. For example, I'd be fine emulating `(env (bin ...))` and...

We could implement this feature as a new `(runtime-libraries ...)` field (which could just set a boolean), or we could unconditionally make them available, I don't know. This provides an...

> Are you dynlinking? Yes, we are dynlinking, and we use `Fl_dynload` because we need to be able to pull deps when dynlinking, and also we need to support quite...

This was discussed and a few points where made: - there are two ways to make `Fl_dynload` work for build `(run ...)` actions: + depend on the required files on...

In `src/coq/coq_rules.ml` we just depend on the `META` install location, that works, and IMHO should be better supported in the stanzas. When we generate `dune` files, we use a very...

Behavior with 0.1.9 should be much better suited for CoqTail, including a new `serverStatus` notification which you can use instead of `fileProgress`. Also set the checking to lazy mode, and...

> This looks like it makes the code more complex and I'm not sure what the benefit is supposed to be. I was thinking the same exact thing than @SkySkimmer...

Ah indeed sorry, I got confused by some other PR, the claim here is "This prevents loading in memory potentially useless data, especially the so-called "structured values" which are (potentially...