Emilio Jesús Gallego Arias

> It seems Undo only counts tactics (even though the manual says "commands or tactics". For instance > > ```coq > Goal True -> True. > intros. > Set Printing...

> Looks like something went wrong in test-suite:base+async Why don't we just remove `async` ? Unless I am mistaken it is essentially quadratic so I'd be surprised if it makes...

> @ejgallego I've found that most of the time my cores are saturated on file-level parallelism, and haven't tried async-proofs much, alas. @andres-erbsen do you know if it speeds up...

> `par:` is crippled by its inability to share a jobserver with `make` (#14203), which means that we can't really take full advantage of it. Its also so memory-heavy/duplicative that...

I confirm that this example displays both the error and the warning in coq-lsp. Tho indeed, the whole setup is IMHO a bit confusing usability wise.

On the other hand the quickfix codeaction works, so IMHO that makes the situation much better.

@Alizter thanks a lot for the debug info, what's the non-local plugin file here tho? A quick inspection doesn't reveal any out-of-tree file there. Do you have the backtrace?

Thanks for the feedback @mjambon , indeed location tracking can decrease efficiently greatly, good point. I guess it makes sense to keep this issue open to see if a solution...

I guess more than seeing the improvement as "small", it is more in the category of "critical for some users" vs "non important for others", for example if you need...

Indeed! While I'm not expert on parsing, it seems to me that a parser geared towards user input is very different than a parser geared towards de-serialization. In particular locations...