Emilio Jesús Gallego Arias

Thanks @liyishuai , unfortunately that repos is too heavy for Dune's CI. In order to add a test case to Dune, we should do something self-contained (that can work with...

`simple.v`: any file that uses the prelude, for example `Definition a := 3.` Numbers before installing `memtrace_viewer`: ``` Fl_dynload.load_packages: coq-lsp.serlib.ltac , 0.028070 ms Fl_dynload.load_packages: coq-lsp.serlib.number_string_notation , 0.025253 ms Fl_dynload.load_packages: coq-lsp.serlib.tauto...

I'm not sure Rocq would be affected as we don't directly use `Fl_dynload`, but indeed, this problem is independent of `coq-lsp`: ``` Fl_dynload.load_packages: rocq-runtime.plugins.ltac , 0.364408 ms Fl_dynload.load_packages: rocq-runtime.plugins.number_string_notation ,...

The function that takes the large runtime is `Fl_package_base.requires_deeply` , Rocq calls`Findlib.package_deep_ancestors` in `Mltop.add_deps` which is basically an alias to this function. However this function is only called when compiling...

@ppedrot do your examples trigger `Mltop.add_deps` ? This is where the call to [`Findlib.package_deep_ancestors`](https://github.com/ocaml/ocamlfind/blob/bd9aad183f0d1c2caf3ec29e4f52bc69361f266d/src/findlib/fl_package_base.ml#L358) happens. Note that `fcc` does several calls to load the serlib plugins, so usually have the...

@SkySkimmer I think the algorithm in `Findlib.package_deep_ancestors` may be quadratic, but I need to look more into it. It could also be some other problems with findlib and the way...

> You mean you init twice? We init for each workspace, as these may have different `OCAMLPATH` settings, see `coq/workspace.ml:apply`. This is still buggy when resuming checking, but mostly works...

Actually I have a branch with support for code actions which could do this, however I'm not sure if getting this info from Rocq is possible. @SkySkimmer @ppedrot any idea?...

This is ready, but requires js_of_ocaml master, so I will wait until we have a new release.

Note that in `coq-lsp` I'm running Coq master + latest jsoo just fine. So that's a positive data point w.r.t. toolchain. But porting `jsCoq` legacy may be far from trivial,...