Stream: coq-lsp

Topic: Configuration from _CoqProject


view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Nov 28 2022 at 14:53):

By default, it's not picking up the right imports

view this post on Zulip Ali Caglayan (Nov 28 2022 at 20:59):

AFAIK atm we are not reading any _CoqProject or dune files.

view this post on Zulip Ali Caglayan (Nov 28 2022 at 21:00):

We definitely could, we just haven't gotten round to doing it yet.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2022 at 12:43):

We are reading _CoqProject tho

view this post on Zulip Emilio Jesús Gallego Arias (Dec 06 2022 at 12:43):

I'll open an issue to track MetaCoq

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 08 2022 at 17:53):

That could be the cause of the problem

view this post on Zulip 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