Stream: Elpi users & devs

Topic: elpi documentation

view this post on Zulip Mathis Bouverot-Dupuis (Sep 17 2024 at 14:34):

Hi all, is there any documentation for coq-elpi (other than the source code and excellent tutorials) ? I'm looking for something in the style of https://coq.inria.fr/doc/master/api/coq-core/index.html which allows me to browse the different modules/files online and follow links by clicking on the types and terms that are documented.

view this post on Zulip Enrico Tassi (Sep 17 2024 at 18:41):

Scroll to the end of the REAME in the github repo. You find a short DOC of the vernacular commands and pointers to the files with the APIs.

If you don't find what you are looking for, feel free to ask here.

view this post on Zulip Enrico Tassi (Sep 17 2024 at 18:42):

These files are well commented, but not an hypertext. Still APIs are named quite consistently, usually text search on these files is quite effective.

view this post on Zulip Mathis Bouverot-Dupuis (Sep 18 2024 at 10:16):

Thanks for the pointers. Is there a kind of LSP for Elpi which would allow me to follow "links" by looking at the source code in e.g. VSCode ?

view this post on Zulip Enrico Tassi (Sep 18 2024 at 10:57):

No, there is no language-server implementing intellisense. Maybe one day, @Romain Tetley ;-)

view this post on Zulip Enrico Tassi (Sep 18 2024 at 10:59):

The main reason is that the "compiler" and the "type checker" are a bit too much of a contraption. I hope to improve these components in the coming year. After that building an LSP server would be possible, but today it is not easy at all.

view this post on Zulip Enrico Tassi (Sep 18 2024 at 11:00):

Out of curiosity, which piece of software are you trying to understand or build?

view this post on Zulip Mathis Bouverot-Dupuis (Sep 18 2024 at 11:39):

Ok I see, future work ;-)

view this post on Zulip Mathis Bouverot-Dupuis (Sep 18 2024 at 11:41):

I'm currently learning Elpi so no serious piece of software yet. The goal will be to compare it to other metalanguages in the Coq ecosystem (Ltac2, MetaCoq, Ocaml Plugins, etc) by writing toy commands/tactics in each of the languages.

view this post on Zulip Mathis Bouverot-Dupuis (Sep 18 2024 at 11:41):

Working with Yannick Forster.

view this post on Zulip Enrico Tassi (Sep 18 2024 at 12:46):

Then I recommend you start by looking at the proof-of-concept section of the README: https://github.com/LPCIC/coq-elpi?tab=readme-ov-file#small-examples-proofs-of-concept
These are small, commented, Elpi programs.

Last updated: Oct 13 2024 at 01:02 UTC