Emilio Jesús Gallego Arias

That's interesting, maybe work reporting upstream? Allow me some questions because I don't know this stuff very well, what's the typical workflow for this case? 1. you do the rewrite...

Mmm, how do you propose to implement that, I'm unsure we can do something like this and still remain LSP compliant? Note that once #49 and #24 are implemented memory...

memprof limits are geared more towards limiting single sentences, I think here, as we handle everything under one instance, it is really about #348 + better cache eviction.

Note that once I get the require from memory PR Coq upstream memory consumption for things like HoTT and multiple documents should be reduced dramatically (as requires may be shared)!...

That's a great idea, I can try to automate that. Maybe every file is too much? What is a set of files where you start to have pain?

Maybe we should make this issue broader and include errors too? Actually this is not hard to implement, see #29 , the difficult part is to get a maintainable architecture....

There was a recent PR in Coq proposing to add this information to the warnings; if that PR is accepted, we can implement quickfixes quite easily following the standard.

I think it is 19147

Hi @SnarkBoojum , I think this is fixed in `master`, sorry for the trouble.

Will close the issue when we release the 0.20 version, so we can check.