I'm wondering what coq-lsp is doing regarding auto-config, which _CoqProject is it picking? MetaCoq is slightly non-standard so I'm wondering if it can be made to fit in coq-lsp's model
By default, it's not picking up the right imports
AFAIK atm we are not reading any _CoqProject or dune files.
We definitely could, we just haven't gotten round to doing it yet.
We are reading
I'll open an issue to track MetaCoq
I have added some additional logging and fixed a bug, where coq-lsp did ignore
-I settings from _CoqProject
That could be the cause of the problem
I had some success with metacoq testing now, but indeed for a project of this size, lack of parsing resumption and problems due to multi-file state become a bit annoying. But quite a few files feel right to use tho.
Last updated: Mar 02 2024 at 17:02 UTC