Matthieu Sozeau (Nov 28 2022 at 14:53): Matthieu Sozeau (Nov 28 2022 at 14:53):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
Matthieu Sozeau (Nov 28 2022 at 14:53):By default, it's not picking up the right imports
Ali Caglayan (Nov 28 2022 at 20:59):AFAIK atm we are not reading any _CoqProject or dune files.
Ali Caglayan (Nov 28 2022 at 21:00):We definitely could, we just haven't gotten round to doing it yet.
Emilio Jesús Gallego Arias (Dec 06 2022 at 12:43):We are reading _CoqProject tho
Emilio Jesús Gallego Arias (Dec 06 2022 at 12:43):I'll open an issue to track MetaCoq
Emilio Jesús Gallego Arias (Dec 08 2022 at 17:52):I have added some additional logging and fixed a bug, where coq-lsp did ignore -I settings from _CoqProject
Emilio Jesús Gallego Arias (Dec 08 2022 at 17:53):That could be the cause of the problem
Emilio Jesús Gallego Arias (Dec 08 2022 at 20:08):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: Feb 06 2023 at 06:29 UTC