Proposal to create coq-notation-examples in coq-community

[bcpierce00]

Project name:

coq-notation-examples

Initial author(s):

Benjamin Pierce (bcpierce00)

Current URL:

None.

Kind: pure Coq library / OCaml plugin / extractable program / formalization of a mathematical theorem / ...

Collection of single-file Coq developments

License: MIT license

Description:

It's been proposed that it would be helpful for the Coq community to have a repository of "worked examples" showing best practices for using notations and custom entries.

Status:

Still in discussion stage, but there is already material to include once the repo is created.

New maintainer: looking for a volunteer

I (Benjamin Pierce) can serve as initial maintainer if no one else wants to, but I would hope to involve a few more people over time.

[palmskog]

@bcpierce00 our standard recommendation for license here is the MIT license, is this OK with you?

[bcpierce00]

Yes, that's fine!

[bcpierce00]

P.S. Feel free to rename it just "notation-examples" instead of "coq-notation-examples" for brevity.

On Tue, Jan 30, 2024 at 9:33 AM Benjamin Pierce @.***> wrote:

Yes, that's fine!

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/coq-community/manifesto/issues/154*issuecomment-1917008415__;Iw!!IBzWLUs!RoB4SEM-gDg77q1y3VFlP9yoObVZa2ypVkDu5fZ4-jgcfBE8rEFfgVlBPBZa89pa0d9QDYLYRRNnar2U4s127RQ74kWi$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCZE5SLH4X3L57BBIETYREADRAVCNFSM6AAAAABCRIS5W2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMJXGAYDQNBRGU__;!!IBzWLUs!RoB4SEM-gDg77q1y3VFlP9yoObVZa2ypVkDu5fZ4-jgcfBE8rEFfgVlBPBZa89pa0d9QDYLYRRNnar2U4s127W8r29LP$ . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[palmskog]

@bcpierce00 OK, so I think all our prerequisites are met here (e.g., we have an initial maintainer and an approved license). Feel free to transfer the repository to the coq-community organization whenever convenient, see repository settings under "Danger Zone". We can add new maintainers over time as they volunteer.

[palmskog]

P.S. Feel free to rename it just "notation-examples" instead of "coq-notation-examples" for brevity.

You can either rename the repository yourself, e.g., before the transfer, or I can do it once the transfer has been made.

[bcpierce00]

OK, so I should create the repo and transfer it?

[palmskog]

Ah, I think I misunderstood. If the repo hasn't been created yet, easiest is if I create it and give you admin access

[palmskog]

The repo is up and running with admin permissions: https://github.com/coq-community/notation-examples

If you add some Coq files, I can help up with setting up some basic continuous integration to check that the code builds (this is a requirement for joining Coq's CI).

[bcpierce00]

OK, I've added Test.v and a Makefile that compiles it. Please feel free to adjust anything I've done, if there's a way to do it that's more convenient for you.

On Tue, Jan 30, 2024 at 9:51 AM Karl Palmskog @.***> wrote:

The repo is up and running with admin permissions: https://github.com/coq-community/notation-examples https://urldefense.com/v3/__https://github.com/coq-community/notation-examples__;!!IBzWLUs!RwH1hhO8T7y84XO1Y-RuniIeDtHKhJ41K2APZf-HKPNBv2G9-FiIzVUfoha8f3VnKL2o1eIYhAEaRv7kqcoKt7RqMtsR$

If you add some Coq files, I can help up with setting up some basic continuous integration to check that the code builds (this is a requirement for joining Coq's CI).

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/coq-community/manifesto/issues/154*issuecomment-1917062493__;Iw!!IBzWLUs!RwH1hhO8T7y84XO1Y-RuniIeDtHKhJ41K2APZf-HKPNBv2G9-FiIzVUfoha8f3VnKL2o1eIYhAEaRv7kqcoKt6V_biwH$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCYYVT73PGETQC4GZGLYRECHDAVCNFSM6AAAAABCRIS5W2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMJXGA3DENBZGM__;!!IBzWLUs!RwH1hhO8T7y84XO1Y-RuniIeDtHKhJ41K2APZf-HKPNBv2G9-FiIzVUfoha8f3VnKL2o1eIYhAEaRv7kqcoKt28T3wJ3$ . You are receiving this because you were mentioned.Message ID: @.***>