flèche as a library

[Lysxia]

I'm very interested in using flèche for building LSPs, so I'm wondering what the working status is. It seems that its code is currently tied to Rocq-specific things. Is there a functor hidden somewhere, or would you recommend waiting for it?

[ejgallego]

Hi @Lysxia , thanks for opening this issue. There is indeed a roadmap to make Flèche more flexible! We are actually working on it with @Alidra , for porting Flèche back to Lambdapi. I'm very happy to expand this effort and try to improve things in this regard.

The key idea is to reach a state where we can replace the Coq module for a different language with the same interface, and things work. We are still far from it, mainly due to two reasons:

• I wanted to experiment with Rocq in-depth before committing to a generic design. Abstracting the language as a functoris a bit heavy for a rapidly evolving prototype. There is still quite a few things to do, for example, I just recently started to experiment with multi-threading support, which is a must, and will require some non-trivial changes. Also, we need to improve the way we handle changes in the file system and across multiple files. On the other hand, I think that it is before a 1.0!
• the Coq library is too specific to Rocq, in particular to a) the way Rocq parses commands; b) the number of phases Rocq has. This is a bit harder to overcome without meta-programming; c) the way Rocq commands depend on each other.

Let me write a few TODOs that are already in the roadmap:

• move Loc and Pp to Coq, I have already a tree.
• remove direct access to Rocq libraries, for this we want to set (implicit_transitive_deps false) in the build config.

I'd say these two items would allow us to reach the first milestone of having Coq as a functor to a more generic Flèche setup.

Note that an old PR / branch exists for that, but it is not in a shape where it can be rebased, cc #66