Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 21 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,17 +1,28 @@
<!---
This file was generated from `meta.yml`, please do not edit manually.
Follow the instructions on https://github.com/coq-community/templates to regenerate.
--->
# Rosetta stone of metaprogramming in Coq

[![Contributing][contributing-shield]][contributing-link]
[![Code of Conduct][conduct-shield]][conduct-link]
[![Zulip][zulip-shield]][zulip-link]


[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md

[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md

[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
[zulip-link]: https://coq.zulipchat.com/#narrow/stream/373964-CUDW-2023/topic/Rosetta.20stone.20of.20extension.20languages
[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users



A rosetta stone for metaprogramming in Coq, with different examples
of tactics, plugins, etc., implemented in different metaprogramming
languages such as OCaml and Elpi.

## Meta

Expand All @@ -28,4 +39,12 @@
- Yannick Forster ([**@yforster**](https://github.com/yforster))
- License: [MIT License](LICENSE)
- Compatible Coq versions: 8.17
- Additional dependencies: multiple, see READMEs in directories
- Additional dependencies: none
- Related publication(s): none

## Building

See the README in each subdirectory for information about dependencies
and building instructions.


41 changes: 41 additions & 0 deletions meta.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
---
fullname: Rosetta stone of metaprogramming in Coq
shortname: metaprogramming-rosetta-stone
organization: coq-community
community: true

synopsis: Examples of Coq tactics, plugins, etc., implemented in different metaprogramming languages

description: |-
A rosetta stone for metaprogramming in Coq, with different examples
of tactics, plugins, etc., implemented in different metaprogramming
languages such as OCaml and Elpi.

authors:
- name: Enzo Crance
- name: Davide Fissore
- name: Yannick Forster
- name: Gaëtan Gilbert
- name: Talia Ringer
- name: Michael Soegtrop
- name: Enrico Tassi
- name: Tomas Vallejos

maintainers:
- name: Yannick Forster
nickname: yforster

license:
fullname: MIT License
identifier: MIT

supported_coq_versions:
text: 8.17
opam: '{>= "8.17" & < "8.18~"}'

build: |-
## Building

See the README in each subdirectory for information about dependencies
and building instructions.
---