Stream: MetaCoq

Topic: Call for help: Rosetta stone for Metaprogramming in Coq


view this post on Zulip Yannick Forster (Jun 28 2023 at 11:45):

Dear experts in writing MetaCoq plugins (@Marcel Ullrich @Tomas Vallejos @Adrian Dapprich @Johannes Hostert @Kenji Maillard @Bohdan Liesnikov @Christian Hagemeier, CC @Kathrin Stark), at this year's CUDW we have started the rosetta stone for metaprogramming, a project implementing different tactics, plugins, etc. in different metaprogramming languages such as MetaCoq, Coq-Elpi, Ltac2, etc. The idea is to use this to document these languages for Coq in the long run and make their features comparable. I am looking for people who are willing to help to implement some of the examples in MetaCoq, both because I don't have a lot of time and because it is interesting to see different people's approaches to it. I would expect this to take order of magnitude of a day of work, depending what exactly you want to do. Ping me if you're interested :) More info here: https://github.com/coq-community/metaprogramming-rosetta-stone

view this post on Zulip Yannick Forster (Jun 28 2023 at 11:45):

And here: https://coq.zulipchat.com/#narrow/stream/373964-CUDW-2023/topic/Rosetta.20stone.20of.20extension.20languages

view this post on Zulip Yannick Forster (Jun 28 2023 at 11:45):

Also @Jason Gross @Théo Winterhalter @Yann Leray

view this post on Zulip Yannick Forster (Jun 28 2023 at 12:16):

Also, to anybody reading this: We don't have enough documentation in MetaCoq, but all MetaCoq developers are very willing to help :) So even if you have little MetaCoq experience and I didn't tag you, feel free to say hi here and take this up as your first ever MetaCoq project

view this post on Zulip Yannick Forster (Jun 28 2023 at 18:28):

@Tomas Vallejos is having a look at autoinduct step 2. @Marcel Ullrich has indicated interest, probably a good thing to look at is either derive show or the reflection (both should be implemented in Elpi already)


Last updated: Jul 23 2024 at 21:01 UTC