Stream: coq-community devs & users

Topic: Manifesto Notifications


view this post on Zulip Coq Github Bot (May 31 2020 at 17:27):

GitHub webhook has been successfully configured by Zimmi48.

view this post on Zulip Coq Github Bot (Jun 02 2020 at 14:03):

palmskog closed Issue #104 Change maintainer of project Stalmarck:

Project name and URL: https://github.com/coq-community/stalmarck

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

@herbelin is currently maintaining this project (and also qarith-stern-brocot and bertrand), but because he's also the one taking care of all the remaining coq-contribs, he'd gladly accept if someone else wanted to take over this package (or one of the other two I suppose). Cf. https://github.com/coq-community/stalmarck/pull/12#issuecomment-636029984.

view this post on Zulip Coq Github Bot (Jun 07 2020 at 23:40):

palmskog unlabeled Issue #16 proviola:

Move a project to coq-community

Project name: proviola

Initial author(s): Carst Tankink @Carst-Tankink

Current URL: https://bitbucket.org/Carst/proviola-source

Kind: tool

License: GPL v3

Description: A tool to be able to replay the proofs when browsing a coqdoc-generated HTML file.

Status: Not maintained.

New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer -->

cc @JasonGross @mgrabovsky @yforster who have shown interest by having a fork on GitHub and @spitters @aa755 @siddharthist who have shown interest otherwise.

For those of you that do not already know about coq-community, have a look at the README at https://github.com/coq-community/manifesto. And sorry for the noise if you do not feel concerned (you can easily unsubscribe from this issue).

view this post on Zulip Coq Github Bot (Jun 07 2020 at 23:45):

palmskog closed Issue #16 proviola:

Move a project to coq-community

Project name: proviola

Initial author(s): Carst Tankink @Carst-Tankink

Current URL: https://bitbucket.org/Carst/proviola-source

Kind: tool

License: GPL v3

Description: A tool to be able to replay the proofs when browsing a coqdoc-generated HTML file.

Status: Not maintained.

New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer -->

cc @JasonGross @mgrabovsky @yforster who have shown interest by having a fork on GitHub and @spitters @aa755 @siddharthist who have shown interest otherwise.

For those of you that do not already know about coq-community, have a look at the README at https://github.com/coq-community/manifesto. And sorry for the noise if you do not feel concerned (you can easily unsubscribe from this issue).

view this post on Zulip Coq Github Bot (Jun 10 2020 at 22:32):

palmskog unlabeled Issue #86 Proposal to move JMLCoq to coq-community:

Project name: JMLCoq

Initial author(s): Hermann Lehner (http://people.inf.ethz.ch/lehnerh/ http://www.hermann-lehner.com)

Current URL: http://jmlcoq.info (http://jmlcoq.info/index_files/JMLCoq.tar.gz)

Kind: pure Coq library

License: MIT

Description: Coq formalization of the Java Modeling Language.

Status: unmaintained since 2011

New maintainer: looking for a volunteer

There are many Coq formalizations of fragments of Java floating around, but this one is quite well documented (a whole thesis) and has applications in runtime checking, and thus may be interesting to maintain for the long term. It seems likely the author should agree to license this work under an open source license, since the final thesis paragraph reads:

We hope that our work will be of good use in the research community and help to motivate others to choose a more formal approach to software verification.

view this post on Zulip Coq Github Bot (Jun 12 2020 at 10:42):

palmskog closed Issue #86 Proposal to move JMLCoq to coq-community:

Project name: JMLCoq

Initial author(s): Hermann Lehner (http://people.inf.ethz.ch/lehnerh/ http://www.hermann-lehner.com)

Current URL: http://jmlcoq.info (http://jmlcoq.info/index_files/JMLCoq.tar.gz)

Kind: pure Coq library

License: MIT

Description: Coq formalization of the Java Modeling Language.

Status: unmaintained since 2011

New maintainer: looking for a volunteer

There are many Coq formalizations of fragments of Java floating around, but this one is quite well documented (a whole thesis) and has applications in runtime checking, and thus may be interesting to maintain for the long term. It seems likely the author should agree to license this work under an open source license, since the final thesis paragraph reads:

We hope that our work will be of good use in the research community and help to motivate others to choose a more formal approach to software verification.

view this post on Zulip Coq Github Bot (Jun 15 2020 at 15:19):

Zimmi48 opened PR #105 Remove remaining references to Gitter. from fix-remaining-gitter to master.

view this post on Zulip Coq Github Bot (Jun 15 2020 at 15:19):

Zimmi48 requested palmskog for a review on PR #105 Remove remaining references to Gitter..

view this post on Zulip Coq Github Bot (Jun 15 2020 at 16:16):

Zimmi48 merged PR #105 Remove remaining references to Gitter.

view this post on Zulip Coq Github Bot (Jun 19 2020 at 15:04):

palmskog opened PR #106 Refine code of conduct from refine-code-of-conduct to master:

I want to ensure that coq-community members are not attacked or reported for code-of-conduct violations based on (possibly politically-charged) statements or behavior that occur outside of coq-community, e.g., on Twitter, in personal blogs, and in issues in other GitHub organizations.

Here are two refinements of the code of conduct which I believe are conducive to this goal.

Note that the explicit mention of political views as an aspect of personal identity also exist in the Julia community standards, which the current code is based on.

view this post on Zulip Coq Github Bot (Jun 19 2020 at 15:06):

palmskog requested Zimmi48 for a review on PR #106 Refine code of conduct.

view this post on Zulip Coq Github Bot (Jun 19 2020 at 15:25):

palmskog merged PR #106 Refine code of conduct.

view this post on Zulip Coq Github Bot (Jun 19 2020 at 19:37):

palmskog opened PR #107 fix dead link to Idris community standards from fix-idris-standards-url to master.

view this post on Zulip Coq Github Bot (Jun 20 2020 at 18:46):

palmskog edited Issue #97 Proposal to move Almost Full to coq-community:

Project name: Almost Full

Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt

Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)

Kind: pure Coq library & formalization of a mathematical theorem

License: Unknown

Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).

There is also an Agda translation from 2014.

Status: Unmaintained since 2012

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Jun 20 2020 at 20:18):

palmskog merged PR #107 fix dead link to Idris community standards.

view this post on Zulip Coq Github Bot (Jun 23 2020 at 07:52):

Zimmi48 opened Issue #108 Proposal to move Hydra battles in Coq to coq-community:

Project name: Hydra battles in Coq

Initial author(s): Pierre Castéran @Casteran

Current URL: https://framagit.org/casteran/hydra-battles-in-coq

Kind: documentation project composed of Coq scripts + LaTeX sources

License: CeCILL-B

Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).

Status: draft stage (complete but needs reviewing)

New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48

When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.

view this post on Zulip Coq Github Bot (Jun 23 2020 at 07:52):

Zimmi48 labeled Issue #108 Proposal to move Hydra battles in Coq to coq-community:

Project name: Hydra battles in Coq

Initial author(s): Pierre Castéran @Casteran

Current URL: https://framagit.org/casteran/hydra-battles-in-coq

Kind: documentation project composed of Coq scripts + LaTeX sources

License: CeCILL-B

Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).

Status: draft stage (complete but needs reviewing)

New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48

When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.

view this post on Zulip Coq Github Bot (Jun 23 2020 at 10:03):

palmskog unlabeled Issue #97 Proposal to move Almost Full to coq-community:

Project name: Almost Full

Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt

Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)

Kind: pure Coq library & formalization of a mathematical theorem

License: Unknown

Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).

There is also an Agda translation from 2014.

Status: Unmaintained since 2012

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Jun 23 2020 at 10:04):

palmskog edited Issue #97 Proposal to move Almost Full to coq-community:

Project name: Almost Full

Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt

Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)

Kind: pure Coq library & formalization of a mathematical theorem

License: MIT License

Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).

There is also an Agda translation from 2014.

Status: Unmaintained since 2012

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Jun 23 2020 at 10:04):

palmskog edited Issue #97 Proposal to move Almost Full to coq-community:

Project name: Almost Full

Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt

Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)

Kind: pure Coq library & formalization of a mathematical theorem

License: MIT License

Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).

There is also an Agda translation from 2014.

Status: Unmaintained since 2012

New maintainer: @palmskog

view this post on Zulip Coq Github Bot (Jun 23 2020 at 10:57):

palmskog closed Issue #97 Proposal to move Almost Full to coq-community:

Project name: Almost Full

Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt

Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)

Kind: pure Coq library & formalization of a mathematical theorem

License: MIT License

Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).

There is also an Agda translation from 2014.

Status: Unmaintained since 2012

New maintainer: @palmskog

view this post on Zulip Coq Github Bot (Jul 02 2020 at 20:13):

palmskog opened Issue #109 Proposal to move High School Geometry to coq-community:

Project name: High School Geometry

Initial author(s): Frédérique Guilhot

Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry

Kind: pure Coq library / formalization of mathematical theorems

License: LGPL-2.1-or-later

Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.

Status: Unmaintained since 2019

New maintainer: @thery

This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.

@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the coq-community organization on GitHub. Please let us know here if there are any issues.

view this post on Zulip Coq Github Bot (Jul 02 2020 at 20:13):

palmskog labeled Issue #109 Proposal to move High School Geometry to coq-community:

Project name: High School Geometry

Initial author(s): Frédérique Guilhot

Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry

Kind: pure Coq library / formalization of mathematical theorems

License: LGPL-2.1-or-later

Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.

Status: Unmaintained since 2019

New maintainer: @thery

This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.

@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the coq-community organization on GitHub. Please let us know here if there are any issues.

view this post on Zulip Coq Github Bot (Jul 02 2020 at 20:15):

palmskog labeled Issue #109 Proposal to move High School Geometry to coq-community:

Project name: High School Geometry

Initial author(s): Frédérique Guilhot

Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry

Kind: pure Coq library / formalization of mathematical theorems

License: LGPL-2.1-or-later

Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.

Status: Unmaintained since 2019

New maintainer: @thery

This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.

@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the coq-community organization on GitHub. Please let us know here if there are any issues.

view this post on Zulip Coq Github Bot (Jul 02 2020 at 23:30):

palmskog closed Issue #109 Proposal to move High School Geometry to coq-community:

Project name: High School Geometry

Initial author(s): Frédérique Guilhot

Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry

Kind: pure Coq library / formalization of mathematical theorems

License: LGPL-2.1-or-later

Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.

Status: Unmaintained since 2019

New maintainer: @thery

This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.

@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the coq-community organization on GitHub. Please let us know here if there are any issues.

view this post on Zulip Coq Github Bot (Jul 13 2020 at 09:10):

Zimmi48 transferred Issue #37 State of CI testing with Nix:

It's been a long time since I said I would write this summary issue (cc @siddharthist who was interested in particular).

Overall, the current state of CI testing with Nix is documented in the wiki. It is one of the two newly established and officially supported ways of testing projects depending on Coq, the other being opam + Docker (see comparison here). Both setups avoid to rebuild Coq at every test or depend on an outdated opam cache.

Both setups should allow in theory to reuse build artifacts to build reverse-dependencies (e.g. corn which depends on math-classes) or the various packages depending on math-comp. In the case of Docker, it is a matter of generating a Dockerfile and pushing the new image to a Docker registry (either dockerhub when building the master branch, or GitLab's registry when building any branch, see discussion at https://github.com/math-comp/math-comp/pull/256).

In the case of Nix, it requires pushing to a cache on Cachix. This should be very easy to setup as soon as this is tested and documented. However, my initial tests did not work. The main difficulty is to make sure that the exact same derivation is built on the CI that is going to push to Cachix as is required in the depending builds. The problem is that the derivation depends in turn on the source derivation. Depending how it is built, it may be sensible to the name of the directory which contains it.

For instance, the default.nix file of Coq takes it source from the current directory, and this is also the case for the proposed template default.nix in this repository. When building with nix build, the source will be copied to the nix store in a repository like /nix/store/l14sddwdd8lrji8qp900jcd12h4w1sgq-name where name is the name of the directory that contained the sources in the filesystem. This is highly unstable. That's why in Coq's .gitlab-ci.yml, we do not run nix build on the sources but we do nix build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}". The fetchTarball operation will always copy the sources to a location in the Nix store that only depends on the content of the tarball. Then our template default.nix for projects depending on Coq will load the Coq dependency in the same way (using fetchTarball again).

A similar trick will be needed to be able to make the build artifacts that we upload to Cachix reusable, unless another way of fixing this instability is found (cc @vbgl to which I talked about these issues already).

view this post on Zulip Coq Github Bot (Aug 03 2020 at 12:55):

Zimmi48 opened PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:

For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.

view this post on Zulip Coq Github Bot (Aug 04 2020 at 11:23):

Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:

For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.

view this post on Zulip Coq Github Bot (Aug 04 2020 at 13:08):

Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:

For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.

view this post on Zulip Coq Github Bot (Aug 04 2020 at 14:22):

Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:

For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.

view this post on Zulip Coq Github Bot (Aug 04 2020 at 20:17):

palmskog merged PR #110 Add an FAQ on choice of licenses.

view this post on Zulip Coq Github Bot (Aug 14 2020 at 18:29):

palmskog labeled Issue #111 Listing and preserving formalized mathematical results in Coq:

This is a meta issue asking the general question:

How can coq-community work towards better listing and preservation of formalized mathematics in Coq?

A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.

As one example, consider Wiedijk's list of 100 theorems as formalized Coq, where the code for most entries are currently inaccessible or obsolete.

coq-community members can address this situation in at least two ways:

  1. Organize and maintain a curated list of mathematical results that are available for the latest stable Coq version (an inverse of a list of projects formalizing mathematics such as this one)
  2. Actively locate and port old code with noteworthy math results to the latest stable Coq version, and maintain it on GitHub.

One source of inspiration is what the Lean community is doing:

view this post on Zulip Coq Github Bot (Aug 14 2020 at 18:29):

palmskog opened Issue #111 Listing and preserving formalized mathematical results in Coq:

This is a meta issue asking the general question:

How can coq-community work towards better listing and preservation of formalized mathematics in Coq?

A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.

As one example, consider Wiedijk's list of 100 theorems as formalized Coq, where the code for most entries are currently inaccessible or obsolete.

coq-community members can address this situation in at least two ways:

  1. Organize and maintain a curated list of mathematical results that are available for the latest stable Coq version (an inverse of a list of projects formalizing mathematics such as this one)
  2. Actively locate and port old code with noteworthy math results to the latest stable Coq version, and maintain it on GitHub.

One source of inspiration is what the Lean community is doing:

view this post on Zulip Coq Github Bot (Aug 14 2020 at 19:34):

liyishuai closed Issue #70 Add Coq to Travis CI:

Meta-issue

Our current template builds everything in Docker, which is less flexible than what Travis can do with other languages. It'll be nice if we could have language: coq and run scripts conveniently.
Travis allows [community-supported languages](//docs.travis-ci.com/user/languages/community-supported-languages), and our community seems the right people to do that.
Similar issue in OCaml world: ocaml/ocaml-ci-scripts#53

view this post on Zulip Coq Github Bot (Aug 15 2020 at 20:15):

palmskog edited Issue #111 Listing and preserving formalized mathematical results in Coq:

This is a meta issue asking the general question:

How can coq-community work towards better listing and preservation of formalized mathematics in Coq?

A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.

As one example, consider Madiot's list of Coq theorems from Wiedijk's general list. Quite a few of the links in Madiot's list point to Coq code that does not build with the current stable version of Coq.

coq-community members can address this situation in at least two ways:

  1. Organize and maintain a curated list of mathematical results that are available for the latest stable Coq version (an inverse of a list of projects formalizing mathematics such as this one)
  2. Actively locate and port old code with noteworthy math results to the latest stable Coq version, and maintain it on GitHub.

One source of inspiration is what the Lean community is doing:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:18):

palmskog opened Issue #112 Change maintainer of project Binary Rational Numbers :

Project name and URL: https://github.com/coq-community/qarith-stern-brocot

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:18):

palmskog labeled Issue #112 Change maintainer of project Binary Rational Numbers :

Project name and URL: https://github.com/coq-community/qarith-stern-brocot

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:20):

palmskog opened Issue #113 Change maintainer of project Bertrand:

Project name and URL: https://github.com/coq-community/bertrand

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:20):

palmskog labeled Issue #113 Change maintainer of project Bertrand:

Project name and URL: https://github.com/coq-community/bertrand

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:24):

Zimmi48 labeled Issue #113 Change maintainer of project Bertrand:

Project name and URL: https://github.com/coq-community/bertrand

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 10:25):

Zimmi48 labeled Issue #112 Change maintainer of project Binary Rational Numbers :

Project name and URL: https://github.com/coq-community/qarith-stern-brocot

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Aug 19 2020 at 11:32):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 11:42):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 11:46):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 11:51):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 12:04):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 12:10):

palmskog:

view this post on Zulip Coq Github Bot (Aug 19 2020 at 13:10):

palmskog:

view this post on Zulip Coq Github Bot (Aug 25 2020 at 11:29):

lthms opened Issue #114 Proposal to publish project coqffi to coq-community:

Project name: coqffi

Initial author(s): Thomas Letan (@lthms), with contributions from Li-yao Xia (@lysxia), Yann Régis-Gianas (@yurug), and Yannick Zakowski (@YaZko)

Current URL: None, it would be an initial publication

Kind: extractable program, Coq tooling

License: GPLv3

Description: coqffi automatically generates FFI binding (i.e., extraction primitives) to OCaml libraries for Coq.

Status: Maintained, not yet publlished.

New maintainer: @lthms

view this post on Zulip Coq Github Bot (Aug 25 2020 at 14:21):

lthms edited Issue #114 Proposal to publish project coqffi to coq-community:

Project name: coqffi

Initial author(s): Thomas Letan (@lthms), with contributions from Li-yao Xia (@lysxia), Yann Régis-Gianas (@yurug), and Yannick Zakowski (@YaZko)

Current URL: None, it would be an initial publication

Kind: extractable program, Coq tooling

License: GPLv3

Description: coqffi automatically generates FFI binding to OCaml libraries for Coq. For instance, given the following .mli file

type fd

val fd_equal : fd -> fd -> bool

val openfile : string -> fd [@@impure]
val read_all : fd -> string [@@impure]
val write : fd -> string -> unit [@@impure]
val closefile : fd -> unit [@@impure]

coqffi generates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity to coq-simple-io.

(* This file has been generated by coqffi. *)

Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.

From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.

(** * Types *)

Axiom (fd : Type).

Extract Constant fd => "Examples.File.fd".

(** * Pure Functions *)

Axiom (std_out : fd).

Extract Constant std_out => "Examples.File.std_out".

(** * Impure Primitives *)

(** ** Monad *)

Class MonadFile (m : Type -> Type) : Type :=
  { openfile : string -> m fd
  ; closefile : fd -> m unit
  ; read_all : fd -> m string
  ; write : fd -> string -> m unit
  }.

(** ** [IO] Instance *)

Axiom (io_openfile : string -> IO fd).
Axiom (io_closefile : fd -> IO unit).
Axiom (io_read_all : fd -> IO string).
Axiom (io_write : fd -> string -> IO unit).

Extract Constant io_openfile =>
  "(fun x0 k__ -> k__ (Examples.File.openfile x0))".
Extract Constant io_closefile =>
  "(fun x0 k__ -> k__ (Examples.File.closefile x0))".
Extract Constant io_read_all =>
  "(fun x0 k__ -> k__ (Examples.File.read_all x0))".
Extract Constant io_write =>
  "(fun x0 x1 k__ -> k__ (Examples.File.write x0 x1))".

Instance MonadFile_IO : MonadFile IO :=
  { openfile := io_openfile
  ; closefile := io_closefile
  ; read_all := io_read_all
  ; write := io_write
  }.

Status: Maintained, not yet publlished.

New maintainer: @lthms

view this post on Zulip Thomas Letan (Aug 25 2020 at 14:31):

thanks for your feedback @Bas Spitters and sorry for the previous unhelpful description of the project

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:14):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:29):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:32):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:34):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:35):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 10:45):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 11:00):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 11:15):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 11:31):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 11:38):

palmskog:

view this post on Zulip Coq Github Bot (Aug 30 2020 at 11:38):

palmskog:

view this post on Zulip Coq Github Bot (Aug 31 2020 at 12:27):

chdoc opened Issue #115 Proposal to move project comp-dec-modal to coq-community:

Project name: Completeness and Decidability of Modal-Logic Calculi

Initial author(s): Christian Doczkal (me)

Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B

Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).

Status: maintained

New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.

Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current recursive make build infrastructure to a single centralized Makefile.

view this post on Zulip Coq Github Bot (Aug 31 2020 at 12:27):

chdoc labeled Issue #115 Proposal to move project comp-dec-modal to coq-community:

Project name: Completeness and Decidability of Modal-Logic Calculi

Initial author(s): Christian Doczkal (me)

Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B

Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).

Status: maintained

New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.

Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current recursive make build infrastructure to a single centralized Makefile.

view this post on Zulip Coq Github Bot (Aug 31 2020 at 12:29):

palmskog labeled Issue #115 Proposal to move project comp-dec-modal to coq-community:

Project name: Completeness and Decidability of Modal-Logic Calculi

Initial author(s): Christian Doczkal (me)

Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B

Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).

Status: maintained

New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.

Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current recursive make build infrastructure to a single centralized Makefile.

view this post on Zulip Coq Github Bot (Aug 31 2020 at 17:03):

jmadiot opened Issue #116 Proposal to move project coq100 to coq-community:

Project name: coq-100-theorems

Initial author(s): Jean-Marie Madiot

Current URL: https://madiot.fr/coq100/

Kind: web page + formalizations of a few mathematical theorems

License: MIT

Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.

Status: maintained

New maintainer: I wish to continue to maintain if that's possible

view this post on Zulip Coq Github Bot (Aug 31 2020 at 17:03):

jmadiot labeled Issue #116 Proposal to move project coq100 to coq-community:

Project name: coq-100-theorems

Initial author(s): Jean-Marie Madiot

Current URL: https://madiot.fr/coq100/

Kind: web page + formalizations of a few mathematical theorems

License: MIT

Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.

Status: maintained

New maintainer: I wish to continue to maintain if that's possible

view this post on Zulip Coq Github Bot (Aug 31 2020 at 17:05):

jmadiot edited Issue #116 Proposal to move project coq100 to coq-community:

Project name: coq-100-theorems

Initial author(s): Jean-Marie Madiot

Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100

Kind: web page + formalizations of a few mathematical theorems

License: MIT

Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.

Status: maintained

New maintainer: I wish to continue to maintain if that's possible

view this post on Zulip Coq Github Bot (Aug 31 2020 at 18:22):

palmskog labeled Issue #116 Proposal to move project coq100 to coq-community:

Project name: coq-100-theorems

Initial author(s): Jean-Marie Madiot

Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100

Kind: web page + formalizations of a few mathematical theorems

License: MIT

Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.

Status: maintained

New maintainer: I wish to continue to maintain if that's possible

view this post on Zulip Coq Github Bot (Aug 31 2020 at 19:37):

palmskog closed Issue #116 Proposal to move project coq100 to coq-community:

Project name: coq-100-theorems

Initial author(s): Jean-Marie Madiot

Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100

Kind: web page + formalizations of a few mathematical theorems

License: MIT

Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.

Status: maintained

New maintainer: I wish to continue to maintain if that's possible

view this post on Zulip Coq Github Bot (Sep 07 2020 at 15:57):

chdoc closed Issue #115 Proposal to move project comp-dec-modal to coq-community:

Project name: Completeness and Decidability of Modal-Logic Calculi

Initial author(s): Christian Doczkal (me)

Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl

Kind: pure Coq library / formalization of mathematical theorems

License: CeCILL-B

Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).

Status: maintained

New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.

Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current recursive make build infrastructure to a single centralized Makefile.

view this post on Zulip Coq Github Bot (Sep 08 2020 at 15:43):

palmskog opened Issue #117 Proposal to move project Gaia to coq-community:

Project name: Gaia (Geometry, Algebra, Informatics and Applications)

Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson

Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/

Kind: pure Coq library and formalization of a mathematical theorems

License: MIT

Status: unmaintained since José Grimm passed away in 2019

Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).

New maintainer: Laurent Théry (@thery)

Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).

I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.

view this post on Zulip Coq Github Bot (Sep 08 2020 at 15:43):

palmskog labeled Issue #117 Proposal to move project Gaia to coq-community:

Project name: Gaia (Geometry, Algebra, Informatics and Applications)

Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson

Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/

Kind: pure Coq library and formalization of a mathematical theorems

License: MIT

Status: unmaintained since José Grimm passed away in 2019

Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).

New maintainer: Laurent Théry (@thery)

Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).

I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.

view this post on Zulip Coq Github Bot (Sep 08 2020 at 15:44):

palmskog labeled Issue #117 Proposal to move project Gaia to coq-community:

Project name: Gaia (Geometry, Algebra, Informatics and Applications)

Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson

Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/

Kind: pure Coq library and formalization of a mathematical theorems

License: MIT

Status: unmaintained since José Grimm passed away in 2019

Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).

New maintainer: Laurent Théry (@thery)

Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).

I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.

view this post on Zulip Coq Github Bot (Sep 08 2020 at 16:15):

anton-trunov:

view this post on Zulip Coq Github Bot (Sep 08 2020 at 16:21):

Zimmi48:

view this post on Zulip Coq Github Bot (Sep 08 2020 at 16:37):

Zimmi48:

view this post on Zulip Coq Github Bot (Sep 08 2020 at 16:42):

anton-trunov:

view this post on Zulip Coq Github Bot (Sep 08 2020 at 18:22):

anton-trunov:

view this post on Zulip Coq Github Bot (Sep 09 2020 at 08:20):

palmskog closed Issue #117 Proposal to move project Gaia to coq-community:

Project name: Gaia (Geometry, Algebra, Informatics and Applications)

Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson

Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/

Kind: pure Coq library and formalization of a mathematical theorems

License: MIT

Status: unmaintained since José Grimm passed away in 2019

Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).

New maintainer: Laurent Théry (@thery)

Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).

I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.

view this post on Zulip Coq Github Bot (Sep 11 2020 at 17:07):

anton-trunov labeled Issue #118 Automated deployment of coqdoc HTML documentation for each new release:

Looks like the instructions in the wiki can be used in conjunction with Github Actions to do this, provided the build system has the coqdoc goal.

view this post on Zulip Coq Github Bot (Sep 11 2020 at 17:07):

anton-trunov opened Issue #118 Automated deployment of coqdoc HTML documentation for each new release:

Looks like the instructions in the wiki can be used in conjunction with Github Actions to do this, provided the build system has the coqdoc goal.

view this post on Zulip Coq Github Bot (Sep 14 2020 at 12:38):

palmskog edited Issue #111 Listing and preserving formalized mathematical results in Coq:

This is a meta issue asking the general question:

How can coq-community work towards better listing and preservation of formalized mathematics in Coq?

A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.

As one example, consider Madiot's list of Coq theorems from Wiedijk's general list. Quite a few of the links in Madiot's list point to Coq code that does not build with the current stable version of Coq.

coq-community members can address this situation in at least two ways:

  1. Organize and maintain a curated list of mathematical results that are available for the latest stable Coq version (an inverse of a list of projects formalizing mathematics such as this one)
  2. Actively locate and port old code with noteworthy math results to the latest stable Coq version, and maintain it on GitHub.

One source of inspiration is what the Lean community is doing:

view this post on Zulip Coq Github Bot (Sep 16 2020 at 13:02):

lthms edited Issue #114 Proposal to publish project coqffi to coq-community:

Project name: coqffi

Initial author(s): Thomas Letan (@lthms), with contributions from Li-yao Xia (@lysxia), Yann Régis-Gianas (@yurug), and Yannick Zakowski (@YaZko)

Current URL: None, it would be an initial publication

Kind: extractable program, Coq tooling

License: MIT

Description: coqffi automatically generates FFI binding to OCaml libraries for Coq. For instance, given the following .mli file

type fd

val fd_equal : fd -> fd -> bool

val openfile : string -> fd [@@impure]
val read_all : fd -> string [@@impure]
val write : fd -> string -> unit [@@impure]
val closefile : fd -> unit [@@impure]

coqffi generates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity to coq-simple-io.

(* This file has been generated by coqffi. *)

Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.

From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.

(** * Types *)

Axiom (fd : Type).

Extract Constant fd => "Examples.File.fd".

(** * Pure Functions *)

Axiom (std_out : fd).

Extract Constant std_out => "Examples.File.std_out".

(** * Impure Primitives *)

(** ** Monad *)

Class MonadFile (m : Type -> Type) : Type :=
  { openfile : string -> m fd
  ; closefile : fd -> m unit
  ; read_all : fd -> m string
  ; write : fd -> string -> m unit
  }.

(** ** [IO] Instance *)

Axiom (io_openfile : string -> IO fd).
Axiom (io_closefile : fd -> IO unit).
Axiom (io_read_all : fd -> IO string).
Axiom (io_write : fd -> string -> IO unit).

Extract Constant io_openfile =>
  "(fun x0 k__ -> k__ (Examples.File.openfile x0))".
Extract Constant io_closefile =>
  "(fun x0 k__ -> k__ (Examples.File.closefile x0))".
Extract Constant io_read_all =>
  "(fun x0 k__ -> k__ (Examples.File.read_all x0))".
Extract Constant io_write =>
  "(fun x0 x1 k__ -> k__ (Examples.File.write x0 x1))".

Instance MonadFile_IO : MonadFile IO :=
  { openfile := io_openfile
  ; closefile := io_closefile
  ; read_all := io_read_all
  ; write := io_write
  }.

Status: Maintained, not yet publlished.

New maintainer: @lthms

view this post on Zulip Coq Github Bot (Oct 08 2020 at 16:53):

palmskog closed Issue #114 Proposal to publish project coqffi to coq-community:

Project name: coqffi

Initial author(s): Thomas Letan (@lthms), with contributions from Li-yao Xia (@lysxia), Yann Régis-Gianas (@yurug), and Yannick Zakowski (@YaZko)

Current URL: None, it would be an initial publication

Kind: extractable program, Coq tooling

License: MIT

Description: coqffi automatically generates FFI binding to OCaml libraries for Coq. For instance, given the following .mli file

type fd

val fd_equal : fd -> fd -> bool

val openfile : string -> fd [@@impure]
val read_all : fd -> string [@@impure]
val write : fd -> string -> unit [@@impure]
val closefile : fd -> unit [@@impure]

coqffi generates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity to coq-simple-io.

(* This file has been generated by coqffi. *)

Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.

From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.

(** * Types *)

Axiom (fd : Type).

Extract Constant fd => "Examples.File.fd".

(** * Pure Functions *)

Axiom (std_out : fd).

Extract Constant std_out => "Examples.File.std_out".

(** * Impure Primitives *)

(** ** Monad *)

Class MonadFile (m : Type -> Type) : Type :=
  { openfile : string -> m fd
  ; closefile : fd -> m unit
  ; read_all : fd -> m string
  ; write : fd -> string -> m unit
  }.

(** ** [IO] Instance *)

Axiom (io_openfile : string -> IO fd).
Axiom (io_closefile : fd -> IO unit).
Axiom (io_read_all : fd -> IO string).
Axiom (io_write : fd -> string -> IO unit).

Extract Constant io_openfile =>
  "(fun x0 k__ -> k__ (Examples.File.openfile x0))".
Extract Constant io_closefile =>
  "(fun x0 k__ -> k__ (Examples.File.closefile x0))".
Extract Constant io_read_all =>
  "(fun x0 k__ -> k__ (Examples.File.read_all x0))".
Extract Constant io_write =>
  "(fun x0 x1 k__ -> k__ (Examples.File.write x0 x1))".

Instance MonadFile_IO : MonadFile IO :=
  { openfile := io_openfile
  ; closefile := io_closefile
  ; read_all := io_read_all
  ; write := io_write
  }.

Status: Maintained, not yet publlished.

New maintainer: @lthms

view this post on Zulip Coq Github Bot (Oct 12 2020 at 10:31):

jmadiot opened Issue #119 Proposal to move project Coqtail to coq-community:

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

view this post on Zulip Coq Github Bot (Oct 12 2020 at 10:31):

jmadiot labeled Issue #119 Proposal to move project Coqtail to coq-community:

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

view this post on Zulip Coq Github Bot (Oct 12 2020 at 12:36):

palmskog labeled Issue #119 Proposal to move project Coqtail to coq-community:

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

view this post on Zulip Coq Github Bot (Oct 12 2020 at 15:14):

jmadiot edited Issue #119 Proposal to move project Coqtail to coq-community:

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, Amaury Pouly

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

view this post on Zulip Coq Github Bot (Oct 13 2020 at 08:26):

Zimmi48 edited Issue #108 Proposal to move Hydra battles in Coq to coq-community / to create a documented-examples project.

Project name: Hydra battles in Coq

Initial author(s): Pierre Castéran @Casteran

Current URL: https://framagit.org/casteran/hydra-battles-in-coq

Kind: documentation project composed of Coq scripts + LaTeX sources

License: CeCILL-B

Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).

Status: draft stage (complete but needs reviewing)

New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48

When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.

view this post on Zulip Coq Github Bot (Oct 17 2020 at 12:04):

palmskog edited Issue #25 Proposal to add RelationExtraction:

Move a project to coq-community

Project name: RelationExtraction

Initial author(s): Catherine Dubois, David Delahaye, and Pierre-Nicolas Tollitte

Current URLs: https://github.com/coq-contribs/relation-extraction https://github.com/picnic/RelationExtraction

Kind: OCaml plugin

License: GPL3

Description: A plugin for generating functions from inductive types which make this possible. The functions can either be functions inside Coq or functions in an extraction language, such as OCaml. The underlying theory and implementation of the plugin is described in the paper Producing Certified Functional Code from Inductive Specifications.

Status: Currently maintained by Coq devs in Coq-contribs

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Oct 17 2020 at 13:46):

palmskog edited Issue #25 Proposal to add RelationExtraction:

Move a project to coq-community

Project name: RelationExtraction

Initial author(s): Catherine Dubois, David Delahaye, and Pierre-Nicolas Tollitte

Current URLs: https://github.com/coq-contribs/relation-extraction https://github.com/picnic/RelationExtraction https://github.com/herbelin/RelationExtraction

Kind: OCaml plugin

License: GPL3

Description: A plugin for generating functions from inductive types which make this possible. The functions can either be functions inside Coq or functions in an extraction language, such as OCaml. The underlying theory and implementation of the plugin is described in the paper Producing Certified Functional Code from Inductive Specifications.

Status: Currently maintained by Coq devs in Coq-contribs

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Oct 19 2020 at 13:25):

anton-trunov opened Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 19 2020 at 13:25):

anton-trunov labeled Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 19 2020 at 13:25):

anton-trunov labeled Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 19 2020 at 13:26):

anton-trunov edited Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT (GPL v3 at the time of publication)

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 19 2020 at 14:14):

anton-trunov edited Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT (GPL v3 at the time of publication)

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 20 2020 at 07:18):

palmskog closed Issue #119 Proposal to move project Coqtail to coq-community:

Project name: Coqtail

Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, Amaury Pouly

Current URL: https://coqtail.github.io/

Kind: formalization of mathematical theorems

License: LGPL 3.0

Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.

Status: maintained

New maintainer: I (@jmadiot ) am volunteering to maintain

view this post on Zulip Coq Github Bot (Oct 20 2020 at 08:19):

aerabi opened Issue #121 Proposal to move project generic-environments to coq-community:

Project name: Generic Environments

Initial author(s): Emmanuel Polonowski

Current URL: https://github.com/coq-contribs/generic-environments

Kind: pure Coq library

License: LGPL

Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.

Status: Not maintained recently. The last available version works with Coq 8.10.

New maintainer: I volunteer: @aerabi

view this post on Zulip Coq Github Bot (Oct 20 2020 at 08:19):

aerabi labeled Issue #121 Proposal to move project generic-environments to coq-community:

Project name: Generic Environments

Initial author(s): Emmanuel Polonowski

Current URL: https://github.com/coq-contribs/generic-environments

Kind: pure Coq library

License: LGPL

Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.

Status: Not maintained recently. The last available version works with Coq 8.10.

New maintainer: I volunteer: @aerabi

view this post on Zulip Coq Github Bot (Oct 20 2020 at 08:20):

anton-trunov labeled Issue #121 Proposal to move project generic-environments to coq-community:

Project name: Generic Environments

Initial author(s): Emmanuel Polonowski

Current URL: https://github.com/coq-contribs/generic-environments

Kind: pure Coq library

License: LGPL

Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.

Status: Not maintained recently. The last available version works with Coq 8.10.

New maintainer: I volunteer: @aerabi

view this post on Zulip Coq Github Bot (Oct 20 2020 at 15:27):

palmskog closed Issue #113 Change maintainer of project Bertrand:

Project name and URL: https://github.com/coq-community/bertrand

Current maintainer: @herbelin

Status: maintained

New maintainer: looking for a volunteer

As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

view this post on Zulip Coq Github Bot (Oct 21 2020 at 08:52):

anton-trunov closed Issue #120 Proposal to move project regexp-Brzozowski to coq-community:

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT (GPL v3 at the time of publication)

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.

view this post on Zulip Coq Github Bot (Oct 29 2020 at 11:54):

palmskog closed Issue #121 Proposal to move project generic-environments to coq-community:

Project name: Generic Environments

Initial author(s): Emmanuel Polonowski

Current URL: https://github.com/coq-contribs/generic-environments

Kind: pure Coq library

License: LGPL

Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.

Status: Not maintained recently. The last available version works with Coq 8.10.

New maintainer: I volunteer: @aerabi

view this post on Zulip Coq Github Bot (Nov 04 2020 at 21:02):

KevOrr:

view this post on Zulip Coq Github Bot (Nov 06 2020 at 17:08):

anton-trunov:

view this post on Zulip Coq Github Bot (Nov 13 2020 at 00:55):

palmskog closed Issue #108 Proposal to move Hydra battles in Coq to coq-community / to create a documented-examples project.

Project name: Hydra battles in Coq

Initial author(s): Pierre Castéran @Casteran

Current URL: https://framagit.org/casteran/hydra-battles-in-coq

Kind: documentation project composed of Coq scripts + LaTeX sources

License: CeCILL-B

Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).

Status: draft stage (complete but needs reviewing)

New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48

When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.

view this post on Zulip Coq Github Bot (Nov 13 2020 at 02:04):

palmskog opened Issue #122 Proposal to move Autosubst version 1 to coq-community:

Project name: Autosubst (version 1)

Initial author(s): Steven Schäfer and Tobias Tebbi

Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)

Kind: pure Coq library

License: MIT

Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.

Status: unmaintained

New maintainers: @RalfJung and @co-dan

This is based on a discussion on Zulip.

The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.

view this post on Zulip Coq Github Bot (Nov 13 2020 at 02:04):

palmskog labeled Issue #122 Proposal to move Autosubst version 1 to coq-community:

Project name: Autosubst (version 1)

Initial author(s): Steven Schäfer and Tobias Tebbi

Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)

Kind: pure Coq library

License: MIT

Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.

Status: unmaintained

New maintainers: @RalfJung and @co-dan

This is based on a discussion on Zulip.

The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.

view this post on Zulip Coq Github Bot (Nov 13 2020 at 02:04):

palmskog labeled Issue #122 Proposal to move Autosubst version 1 to coq-community:

Project name: Autosubst (version 1)

Initial author(s): Steven Schäfer and Tobias Tebbi

Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)

Kind: pure Coq library

License: MIT

Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.

Status: unmaintained

New maintainers: @RalfJung and @co-dan

This is based on a discussion on Zulip.

The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.

view this post on Zulip Coq Github Bot (Nov 13 2020 at 06:03):

palmskog edited Issue #122 Proposal to move Autosubst version 1 to coq-community:

Project name: Autosubst (version 1)

Initial author(s): Steven Schäfer and Tobias Tebbi

Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)

Kind: pure Coq library

License: MIT

Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.

Status: unmaintained

New maintainers: @RalfJung and @co-dan

This is based on a discussion on Zulip.

The current proposal is that someone with access rights in the uds-psl organization transfers the above repo to the coq-community organization. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.

view this post on Zulip Coq Github Bot (Nov 27 2020 at 07:44):

palmskog closed Issue #122 Proposal to move Autosubst version 1 to coq-community:

Project name: Autosubst (version 1)

Initial author(s): Steven Schäfer and Tobias Tebbi

Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)

Kind: pure Coq library

License: MIT

Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.

Status: unmaintained

New maintainers: @RalfJung and @co-dan

This is based on a discussion on Zulip.

The current proposal is that someone with access rights in the uds-psl organization transfers the above repo to the coq-community organization. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.

view this post on Zulip Coq Github Bot (Dec 10 2020 at 16:25):

anton-trunov:

view this post on Zulip Coq Github Bot (Dec 12 2020 at 00:04):

erikmd:

view this post on Zulip Coq Github Bot (Dec 12 2020 at 00:06):

erikmd:

view this post on Zulip Coq Github Bot (Dec 15 2020 at 08:43):

palmskog opened Issue #123 Change maintainer of ATBR:

Project name and URL: https://github.com/coq-community/atbr

Current maintainer: @tchajed

Status: unmaintained

New maintainer: looking for a volunteer

@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.

view this post on Zulip Coq Github Bot (Dec 15 2020 at 08:43):

palmskog labeled Issue #123 Change maintainer of ATBR:

Project name and URL: https://github.com/coq-community/atbr

Current maintainer: @tchajed

Status: unmaintained

New maintainer: looking for a volunteer

@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.

view this post on Zulip Coq Github Bot (Dec 15 2020 at 08:44):

palmskog labeled Issue #123 Change maintainer of ATBR:

Project name and URL: https://github.com/coq-community/atbr

Current maintainer: @tchajed

Status: unmaintained

New maintainer: looking for a volunteer

@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.

view this post on Zulip Coq Github Bot (Dec 15 2020 at 08:44):

palmskog labeled Issue #123 Change maintainer of ATBR:

Project name and URL: https://github.com/coq-community/atbr

Current maintainer: @tchajed

Status: unmaintained

New maintainer: looking for a volunteer

@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.

view this post on Zulip Coq Github Bot (Dec 15 2020 at 08:44):

palmskog labeled Issue #123 Change maintainer of ATBR:

Project name and URL: https://github.com/coq-community/atbr

Current maintainer: @tchajed

Status: unmaintained

New maintainer: looking for a volunteer

@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.

view this post on Zulip Coq Github Bot (Dec 20 2020 at 18:03):

palmskog:

view this post on Zulip Coq Github Bot (Dec 20 2020 at 18:04):

palmskog:

view this post on Zulip Coq Github Bot (Dec 20 2020 at 18:05):

palmskog:

view this post on Zulip Coq Github Bot (Dec 21 2020 at 08:16):

palmskog:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 13:29):

palmskog opened Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: looking for a volunteer

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 13:29):

palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: looking for a volunteer

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 13:29):

palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: looking for a volunteer

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 13:29):

palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: looking for a volunteer

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 15:29):

palmskog unlabeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: looking for a volunteer

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 15:35):

palmskog edited Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: @Casteran

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 01 2021 at 18:02):

palmskog closed Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:

Project names: Goedel and Pocklington

Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)

Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington

Kind: pure Coq libraries

License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)

Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.

Status: unmaintained

New maintainer: @Casteran

The last version of Coq known to work is 8.10:

view this post on Zulip Coq Github Bot (Jan 05 2021 at 15:50):

palmskog:

view this post on Zulip Coq Github Bot (Feb 15 2021 at 16:51):

Zimmi48 opened PR #125 Update manifesto with current state of affairs. from update-manifesto to master:

view this post on Zulip Coq Github Bot (Feb 15 2021 at 16:51):

Zimmi48 requested palmskog for a review on PR #125 Update manifesto with current state of affairs..

view this post on Zulip Coq Github Bot (Mar 10 2021 at 13:58):

Zimmi48 updated PR #125 Update manifesto with current state of affairs. from update-manifesto to master.

view this post on Zulip Coq Github Bot (Mar 10 2021 at 14:01):

Zimmi48 updated PR #125 Update manifesto with current state of affairs. from update-manifesto to master.

view this post on Zulip Coq Github Bot (Mar 10 2021 at 14:03):

Zimmi48 edited PR #125 Update manifesto with current state of affairs. from update-manifesto to master:

view this post on Zulip Coq Github Bot (Mar 10 2021 at 14:16):

Zimmi48 merged PR #125 Update manifesto with current state of affairs.

view this post on Zulip Coq Github Bot (May 05 2021 at 17:22):

siraben opened Issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): @ notin (not on GitHub) @herbelin

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (May 05 2021 at 17:22):

siraben labeled Issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): @ notin (not on GitHub) @herbelin

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (May 05 2021 at 18:18):

Zimmi48 edited Issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): Laurent Théry @thery

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (Jul 03 2021 at 03:28):

siraben closed issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): Laurent Théry @thery

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (Jul 27 2021 at 18:03):

Zimmi48 opened issue #127 Proposal to move project CoqEAL to coq-community:

Project name: CoqEAL

Initial author(s): according to the README, the authors are

- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)

Current URL: https://github.com/CoqEAL/CoqEAL

Kind: pure Coq library, which depends on the parmcoq plugin.

License: MIT

Description:

This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:

Status: maintained

New maintainer: the current maintainers would stay in place.

This move was already proposed by one of the CoqEAL author (@CohenCyril) and approved by the others (@maximedenes @mortberg @drouhling) earlier this year (https://github.com/CoqEAL/CoqEAL/issues/33). I just discovered about this proposal and I think this is a good idea, given that the repository is quite significant but not very actively developed, is currently alone in its organization, already uses the coq-community templates, and could probably benefit from help from other coq-community members.

@CohenCyril If this is still something that you want to do, you should be able to proceed with the transfer.

view this post on Zulip Coq Github Bot (Jul 27 2021 at 18:03):

Zimmi48 labeled issue #127 Proposal to move project CoqEAL to coq-community:

Project name: CoqEAL

Initial author(s): according to the README, the authors are

- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)

Current URL: https://github.com/CoqEAL/CoqEAL

Kind: pure Coq library, which depends on the parmcoq plugin.

License: MIT

Description:

This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:

Status: maintained

New maintainer: the current maintainers would stay in place.

This move was already proposed by one of the CoqEAL author (@CohenCyril) and approved by the others (@maximedenes @mortberg @drouhling) earlier this year (https://github.com/CoqEAL/CoqEAL/issues/33). I just discovered about this proposal and I think this is a good idea, given that the repository is quite significant but not very actively developed, is currently alone in its organization, already uses the coq-community templates, and could probably benefit from help from other coq-community members.

@CohenCyril If this is still something that you want to do, you should be able to proceed with the transfer.

view this post on Zulip Coq Github Bot (Jul 27 2021 at 19:09):

palmskog labeled issue #127 Proposal to move project CoqEAL to coq-community:

Project name: CoqEAL

Initial author(s): according to the README, the authors are

- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)

Current URL: https://github.com/CoqEAL/CoqEAL

Kind: pure Coq library, which depends on the parmcoq plugin.

License: MIT

Description:

This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:

Status: maintained

New maintainer: the current maintainers would stay in place.

This move was already proposed by one of the CoqEAL author (@CohenCyril) and approved by the others (@maximedenes @mortberg @drouhling) earlier this year (https://github.com/CoqEAL/CoqEAL/issues/33). I just discovered about this proposal and I think this is a good idea, given that the repository is quite significant but not very actively developed, is currently alone in its organization, already uses the coq-community templates, and could probably benefit from help from other coq-community members.

@CohenCyril If this is still something that you want to do, you should be able to proceed with the transfer.

view this post on Zulip Coq Github Bot (Aug 08 2021 at 11:16):

Zimmi48:

view this post on Zulip Coq Github Bot (Aug 08 2021 at 13:09):

Zimmi48:

view this post on Zulip Coq Github Bot (Aug 08 2021 at 13:21):

Zimmi48:

view this post on Zulip Coq Github Bot (Aug 08 2021 at 15:41):

Zimmi48:

view this post on Zulip Coq Github Bot (Aug 16 2021 at 13:14):

ybertot opened issue #128 Proposal to move project X to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Aug 16 2021 at 13:14):

ybertot labeled issue #128 Proposal to move project X to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Aug 16 2021 at 13:16):

palmskog edited issue #128 Proposal to move project matric-canonical-forms to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Aug 16 2021 at 13:17):

palmskog labeled issue #128 Proposal to move project matric-canonical-forms to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Aug 16 2021 at 13:17):

palmskog edited issue #128 Proposal to move project matrix-canonical-forms to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Aug 17 2021 at 13:39):

thery reopened issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): Laurent Théry @thery

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (Aug 18 2021 at 04:27):

palmskog closed issue #126 Proposal to move sudoku to coq-community:

Project name: https://github.com/coq-contribs/sudoku

Initial author(s): Laurent Théry @thery

Current URL: https://github.com/coq-contribs/sudoku/

Kind: certified Sudoku solver

License: LGPL-2.1

Description: This is a project that implements a certified Sudoku solver in Coq

Status: Hasn't seen commits in over two years, except recently by @siraben

New maintainer: @siraben

view this post on Zulip Coq Github Bot (Aug 31 2021 at 19:58):

Zimmi48:

view this post on Zulip Coq Github Bot (Sep 01 2021 at 09:52):

palmskog closed issue #127 Proposal to move project CoqEAL to coq-community:

Project name: CoqEAL

Initial author(s): according to the README, the authors are

- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)

Current URL: https://github.com/CoqEAL/CoqEAL

Kind: pure Coq library, which depends on the parmcoq plugin.

License: MIT

Description:

This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:

Status: maintained

New maintainer: the current maintainers would stay in place.

This move was already proposed by one of the CoqEAL author (@CohenCyril) and approved by the others (@maximedenes @mortberg @drouhling) earlier this year (https://github.com/CoqEAL/CoqEAL/issues/33). I just discovered about this proposal and I think this is a good idea, given that the repository is quite significant but not very actively developed, is currently alone in its organization, already uses the coq-community templates, and could probably benefit from help from other coq-community members.

@CohenCyril If this is still something that you want to do, you should be able to proceed with the transfer.

view this post on Zulip Coq Github Bot (Sep 07 2021 at 08:47):

palmskog closed issue #128 Proposal to move project matrix-canonical-forms to coq-community:

Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.

Initial author(s):
Guillaume Cano

Current URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)

Kind: pure Coq library / formalization of a mathematical theorem / ...

License: MIT

Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.

Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.

New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->

view this post on Zulip Coq Github Bot (Sep 14 2021 at 07:18):

ejgallego opened issue #129 Current setup vs full repository project templates?

Hi folks,

this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.

Moreover, we have the current alternative Coq project templates in the wild:

How should we organize things? Should we move all the templates to coq-template-foo and have this repository just be an index to all the existing templates, as suggested in the thread?

view this post on Zulip Coq Github Bot (Sep 14 2021 at 07:19):

palmskog labeled issue #129 Current setup vs full repository project templates?

Hi folks,

this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.

Moreover, we have the current alternative Coq project templates in the wild:

How should we organize things? Should we move all the templates to coq-template-foo and have this repository just be an index to all the existing templates, as suggested in the thread?

view this post on Zulip Coq Github Bot (Sep 14 2021 at 07:20):

palmskog labeled issue #129 Current setup vs full repository project templates?

Hi folks,

this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.

Moreover, we have the current alternative Coq project templates in the wild:

How should we organize things? Should we move all the templates to coq-template-foo and have this repository just be an index to all the existing templates, as suggested in the thread?

view this post on Zulip Coq Github Bot (Sep 14 2021 at 07:25):

Zimmi48 edited issue #129 Hosting project templates in coq-community?

Hi folks,

this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.

Moreover, we have the current alternative Coq project templates in the wild:

How should we organize things? Should we move all the templates to coq-template-foo and have this repository just be an index to all the existing templates, as suggested in the thread?

view this post on Zulip Coq Github Bot (Sep 23 2021 at 06:00):

mycroft92 opened issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:

Project name: vcs-prettify-symbols-mode

Initial author(s): Seige Bell

Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode

Kind: Visual Studio Code Plugin

License: MIT License

Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.

Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)

New maintainer: Looking for a volunteer.

view this post on Zulip Coq Github Bot (Sep 23 2021 at 06:00):

mycroft92 labeled issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:

Project name: vcs-prettify-symbols-mode

Initial author(s): Seige Bell

Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode

Kind: Visual Studio Code Plugin

License: MIT License

Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.

Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)

New maintainer: Looking for a volunteer.

view this post on Zulip Coq Github Bot (Sep 23 2021 at 06:59):

Zimmi48 labeled issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:

Project name: vcs-prettify-symbols-mode

Initial author(s): Seige Bell

Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode

Kind: Visual Studio Code Plugin

License: MIT License

Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.

Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)

New maintainer: Looking for a volunteer.

view this post on Zulip Coq Github Bot (Sep 23 2021 at 06:59):

Zimmi48 edited issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:

Project name: vcs-prettify-symbols-mode

Initial author(s): CJ Bell

Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode

Kind: Visual Studio Code Plugin

License: MIT License

Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.

Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)

New maintainer: Looking for a volunteer.

view this post on Zulip Coq Github Bot (Sep 27 2021 at 12:18):

ybertot labeled issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> Yves Bertot Volunteers, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Sep 27 2021 at 12:18):

ybertot opened issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> Yves Bertot Volunteers, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Sep 27 2021 at 14:04):

Zimmi48 edited issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: Yves Bertot, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Sep 27 2021 at 14:11):

Zimmi48 edited issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: Yves Bertot, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Sep 27 2021 at 14:12):

palmskog labeled issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: Yves Bertot, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Sep 28 2021 at 09:21):

palmskog closed issue #131 Proposal to move project coq-dpdgraph to coq-community:

Project name: coq-dpdgraph

Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons

Current URL: https://github.com/karmaki/coq-dpdgraph

Kind: OCaml plugin

License: GNU LGPL 2.1

Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.

Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.

New maintainer: Yves Bertot, will be happy to onboard any other volunteer.

view this post on Zulip Coq Github Bot (Oct 02 2021 at 10:57):

BinderDavid opened issue #132 Proposal to move project Autosubst2 to coq-community:

Project name: Autosubst2

Initial author(s): Kathrin Stark

Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/

Kind: Automatic boilerplate generation for substitutions.

License: Unclear at the moment, the website is down and not archived with the wayback machine :(

Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101

Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the Coq a la carte project: https://dl.acm.org/doi/10.1145/3372885.3373817 ?

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Oct 02 2021 at 10:57):

BinderDavid labeled issue #132 Proposal to move project Autosubst2 to coq-community:

Project name: Autosubst2

Initial author(s): Kathrin Stark

Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/

Kind: Automatic boilerplate generation for substitutions.

License: Unclear at the moment, the website is down and not archived with the wayback machine :(

Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101

Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the Coq a la carte project: https://dl.acm.org/doi/10.1145/3372885.3373817 ?

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Oct 02 2021 at 11:12):

palmskog closed issue #132 Proposal to move project Autosubst2 to coq-community:

Project name: Autosubst2

Initial author(s): Kathrin Stark

Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/

Kind: Automatic boilerplate generation for substitutions.

License: Unclear at the moment, the website is down and not archived with the wayback machine :(

Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101

Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the Coq a la carte project: https://dl.acm.org/doi/10.1145/3372885.3373817 ?

New maintainer: looking for a volunteer

view this post on Zulip Coq Github Bot (Oct 30 2021 at 15:45):

kbrummert opened PR #133 Update README.md from master to master.

view this post on Zulip Coq Github Bot (Oct 30 2021 at 16:02):

Zimmi48 merged PR #133 Update README.md.

view this post on Zulip Coq Github Bot (Nov 03 2021 at 11:05):

palmskog:

view this post on Zulip Coq Github Bot (Nov 05 2021 at 11:14):

palmskog:

view this post on Zulip Coq Github Bot (Nov 06 2021 at 17:05):

palmskog opened PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master:

We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.

I change from "choose" to "use", since these are in many requirements that restrict choice rather than mere recommendations on top of free choice.

view this post on Zulip Coq Github Bot (Nov 06 2021 at 17:06):

palmskog requested Zimmi48 for a review on PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI.

view this post on Zulip Coq Github Bot (Nov 06 2021 at 17:20):

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.

view this post on Zulip Coq Github Bot (Nov 06 2021 at 18:57):

palmskog edited PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master:

We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.

I change from "choose" to "use", since these are requirements that restrict choice rather than mere recommendations on top of free choice.

view this post on Zulip Coq Github Bot (Nov 08 2021 at 07:55):

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.

view this post on Zulip Coq Github Bot (Nov 09 2021 at 09:09):

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.

view this post on Zulip Coq Github Bot (Nov 09 2021 at 09:16):

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.

view this post on Zulip Coq Github Bot (Nov 09 2021 at 09:40):

palmskog edited PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI-FSF intersection from osi-fsf-license to master:

We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.

I change from "choose" to "use", since these are requirements that restrict choice rather than mere recommendations on top of free choice.

view this post on Zulip Coq Github Bot (Nov 09 2021 at 09:41):

palmskog merged PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI-FSF intersection.

view this post on Zulip Coq Github Bot (Nov 14 2021 at 02:14):

palmskog opened PR #135 new name and description for hydra-battles repo project from hydras-update to master.

view this post on Zulip Coq Github Bot (Nov 14 2021 at 02:14):

palmskog requested Zimmi48 for a review on PR #135 new name and description for hydra-battles repo project.

view this post on Zulip Coq Github Bot (Nov 14 2021 at 16:03):

Zimmi48 merged PR #135 new name and description for hydra-battles repo project.

view this post on Zulip Coq Github Bot (Dec 08 2021 at 17:55):

palmskog opened issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 08 2021 at 17:55):

palmskog labeled issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 08 2021 at 17:55):

palmskog labeled issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 08 2021 at 17:56):

palmskog labeled issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 08 2021 at 17:56):

palmskog labeled issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 09 2021 at 10:23):

proux01 unlabeled issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: looking for a volunteer

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 09 2021 at 10:23):

proux01 edited issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: @proux01 (and others?)

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Dec 09 2021 at 15:08):

palmskog closed issue #136 Proposal to move bignums to coq-community:

Project name: Bignums

Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey

Current URL: https://github.com/coq/bignums

Kind: Coq library and OCaml plugin

License: LGPL-2.1-only ("same as Coq")

Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.

Status: part of Coq's CI and sometimes changed by Coq team members

New maintainer: @proux01 (and others?)

Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.

@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.

@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:13):

amahboubi opened issue #137 Proposal to move project Apery to coq-community:

Project name: Apery

Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote

Current URL: https://github.com/math-comp/apery

Kind: pure Coq library, formalization of a mathematical theorem

License: CeCiLL-C

Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Status: Maintained, part of MathComp CI

New maintainer: @amahboubi

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:13):

amahboubi labeled issue #137 Proposal to move project Apery to coq-community:

Project name: Apery

Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote

Current URL: https://github.com/math-comp/apery

Kind: pure Coq library, formalization of a mathematical theorem

License: CeCiLL-C

Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Status: Maintained, part of MathComp CI

New maintainer: @amahboubi

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:15):

palmskog labeled issue #137 Proposal to move project Apery to coq-community:

Project name: Apery

Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote

Current URL: https://github.com/math-comp/apery

Kind: pure Coq library, formalization of a mathematical theorem

License: CeCiLL-C

Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Status: Maintained, part of MathComp CI

New maintainer: @amahboubi

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:48):

Zimmi48 requested palmskog for a review on PR #138 Update info on editorial work..

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:48):

Zimmi48 opened PR #138 Update info on editorial work. from editorial-work-update to master:

To reflect what has been done. See https://github.com/coq-community/coq-community.github.io/issues/2.

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:58):

Zimmi48 updated PR #138 Update info on editorial work. from editorial-work-update to master.

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:58):

Zimmi48 updated PR #138 Update info on editorial work. from editorial-work-update to master.

view this post on Zulip Coq Github Bot (Feb 02 2022 at 10:59):

Zimmi48 merged PR #138 Update info on editorial work.

view this post on Zulip Coq Github Bot (Feb 03 2022 at 10:27):

palmskog closed issue #137 Proposal to move project Apery to coq-community:

Project name: Apery

Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote

Current URL: https://github.com/math-comp/apery

Kind: pure Coq library, formalization of a mathematical theorem

License: CeCiLL-C

Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Status: Maintained, part of MathComp CI

New maintainer: @amahboubi

view this post on Zulip Coq Github Bot (Mar 09 2022 at 10:29):

ybertot opened issue #139 Proposal to move project fourcolor to coq-community:

Project name: fourcolor

Initial author(s): Georges Gonthier

Current URL: https://github.com/math-comp/fourcolor

Kind: formalization of a mathematical theorem

License: CeCILL-B

Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Status: <!-- is it maintained or not? if not, since when? --> maintained

New maintainer: @ybertot

view this post on Zulip Coq Github Bot (Mar 09 2022 at 10:29):

ybertot labeled issue #139 Proposal to move project fourcolor to coq-community:

Project name: fourcolor

Initial author(s): Georges Gonthier

Current URL: https://github.com/math-comp/fourcolor

Kind: formalization of a mathematical theorem

License: CeCILL-B

Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Status: <!-- is it maintained or not? if not, since when? --> maintained

New maintainer: @ybertot

view this post on Zulip Coq Github Bot (Mar 09 2022 at 10:31):

palmskog labeled issue #139 Proposal to move project fourcolor to coq-community:

Project name: fourcolor

Initial author(s): Georges Gonthier

Current URL: https://github.com/math-comp/fourcolor

Kind: formalization of a mathematical theorem

License: CeCILL-B

Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Status: <!-- is it maintained or not? if not, since when? --> maintained

New maintainer: @ybertot

view this post on Zulip Coq Github Bot (Mar 10 2022 at 14:29):

palmskog closed issue #139 Proposal to move project fourcolor to coq-community:

Project name: fourcolor

Initial author(s): Georges Gonthier

Current URL: https://github.com/math-comp/fourcolor

Kind: formalization of a mathematical theorem

License: CeCILL-B

Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

Status: <!-- is it maintained or not? if not, since when? --> maintained

New maintainer: @ybertot

view this post on Zulip Coq Github Bot (Sep 27 2022 at 18:45):

palmskog labeled issue #140 Volunteer interim maintainers needed for VsCoq:

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.

VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.

An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.

During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).

view this post on Zulip Coq Github Bot (Sep 27 2022 at 18:45):

palmskog opened issue #140 Volunteer interim maintainers needed for VsCoq:

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.

VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.

An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.

During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).

view this post on Zulip Coq Github Bot (Sep 27 2022 at 19:50):

palmskog labeled issue #140 Volunteer interim maintainers needed for VsCoq:

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.

VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.

An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.

During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).

view this post on Zulip Coq Github Bot (Sep 30 2022 at 13:47):

Zimmi48 labeled issue #141 CI feedback from the Coq Community Survey 2022:

We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.

cc @erikmd @CohenCyril

CI usage

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-use-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/not-ci-reasons-barplot.png)

The other answers were:

  1. Insufficient project maturity (somewhat like don't need it)
  2. Waste of energy (save the planet)
  3. I only have small Coq projects at this date
  4. Don't know advantages of doing so
  5. Time to set it up
  6. low priority
  7. I didn't think about it yet
  8. I'm not sure how my small projects would benefit from it
  9. Laziness :-)
  10. Just too small projects so far
  11. All of the above
  12. I didn't get around to it yet.
  13. I'm not sure how CI looks for coq, didn't think about it
  14. My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
  15. not needed for mostly exercise problems
  16. It was not necessary for my doctoral work.
  17. I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
  18. lazyness
  19. I'm too lazy / busy with other things to set it up.
  20. Waste of cycles. Nightly or weekly automated build runs are more than sufficient.

CI platforms

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-upset.png)

The other answers were:

We can also see that Travis CI has not been used by a lot of newcomers:

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-multiple-barplot.png)

CI tools

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-barplot.png)

The other answers were:

  1. UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
  2. can't remember
  3. I don't know, a team member set this up
  4. https://github.com/ocaml/setup-ocaml
  5. Opam
  6. Someone else set up CI
  7. ubuntu packages at https://launchpad.net/~jgross-h

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-barplot.png)

The other answers were:

  1. the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
  2. I don't know what we did, a team member set this up
  3. I reused & adapted scripts made by a colleague
  4. Learning how to use them might pay off in the future, but it is hard to give it a try with limited time when something else is already working.
  5. at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
  6. I had trouble making it work together with a Haskell environment in the past

General CI feedback

  1. I think that CI support is good. I wish that the docker images were released more tightly since that is the main bottleneck in updating coq projects to a newer version of coq.

  2. I am not at all aware about the CI tools that the Coq ecosystem provides.

    In UniMath, we have somewhat struggled with setting up CI, and we would love to learn more about the available CI tools.

  3. I feel hobbled using CI because I'm not an expert in the use of opam. And opam seems quite complex to me, so I am not well motivated to become expert in opam.

  4. Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

  5. I only started using it recently and it’s insanely helpful!

  6. I love Coq :D keep on the good work !

  7. A bit of delay with the coq/ocaml most recent versions

  8. A coq/setup-coq repo is what people will look for/expect when it comes to github-actions.
    That repo would install coq using the tool cache at the desired version.

    Getting coq into the actions/virtual-environments images will make everyone's CI jobs faster and make it simpler for people to get started. They are pretty generous with including niche software in their base images.

  9. For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

  10. I would love to see well-supported binary tarballs of Coq and ocaml and etc instead of special solutions for each platform of the day.

  11. I love it!

  12. Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

  13. I have used NixOS ages ago and I'm not an expert. With my basic knowledge I find the documentation on the nix solutions hard to follow, in particular when it comes to adding dependencies and having them cached with cachix. I didn't do a lot of digging because it was not too important, but overall I would very much like to switch from our custom docker images to a nix-based solution.

view this post on Zulip Coq Github Bot (Sep 30 2022 at 13:47):

Zimmi48 opened issue #141 CI feedback from the Coq Community Survey 2022:

We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.

cc @erikmd @CohenCyril

CI usage

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-use-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/not-ci-reasons-barplot.png)

The other answers were:

  1. Insufficient project maturity (somewhat like don't need it)
  2. Waste of energy (save the planet)
  3. I only have small Coq projects at this date
  4. Don't know advantages of doing so
  5. Time to set it up
  6. low priority
  7. I didn't think about it yet
  8. I'm not sure how my small projects would benefit from it
  9. Laziness :-)
  10. Just too small projects so far
  11. All of the above
  12. I didn't get around to it yet.
  13. I'm not sure how CI looks for coq, didn't think about it
  14. My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
  15. not needed for mostly exercise problems
  16. It was not necessary for my doctoral work.
  17. I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
  18. lazyness
  19. I'm too lazy / busy with other things to set it up.
  20. Waste of cycles. Nightly or weekly automated build runs are more than sufficient.

CI platforms

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-upset.png)

The other answers were:

We can also see that Travis CI has not been used by a lot of newcomers:

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-multiple-barplot.png)

CI tools

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-barplot.png)

The other answers were:

  1. UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
  2. can't remember
  3. I don't know, a team member set this up
  4. https://github.com/ocaml/setup-ocaml
  5. Opam
  6. Someone else set up CI
  7. ubuntu packages at https://launchpad.net/~jgross-h

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-barplot.png)

The other answers were:

  1. the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
  2. I don't know what we did, a team member set this up
  3. I reused & adapted scripts made by a colleague
  4. Learning how to use them might pay off in the future, but it is hard to give it a try with limited time when something else is already working.
  5. at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
  6. I had trouble making it work together with a Haskell environment in the past

General CI feedback

  1. I think that CI support is good. I wish that the docker images were released more tightly since that is the main bottleneck in updating coq projects to a newer version of coq.

  2. I am not at all aware about the CI tools that the Coq ecosystem provides.

    In UniMath, we have somewhat struggled with setting up CI, and we would love to learn more about the available CI tools.

  3. I feel hobbled using CI because I'm not an expert in the use of opam. And opam seems quite complex to me, so I am not well motivated to become expert in opam.

  4. Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

  5. I only started using it recently and it’s insanely helpful!

  6. I love Coq :D keep on the good work !

  7. A bit of delay with the coq/ocaml most recent versions

  8. A coq/setup-coq repo is what people will look for/expect when it comes to github-actions.
    That repo would install coq using the tool cache at the desired version.

    Getting coq into the actions/virtual-environments images will make everyone's CI jobs faster and make it simpler for people to get started. They are pretty generous with including niche software in their base images.

  9. For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

  10. I would love to see well-supported binary tarballs of Coq and ocaml and etc instead of special solutions for each platform of the day.

  11. I love it!

  12. Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

  13. I have used NixOS ages ago and I'm not an expert. With my basic knowledge I find the documentation on the nix solutions hard to follow, in particular when it comes to adding dependencies and having them cached with cachix. I didn't do a lot of digging because it was not too important, but overall I would very much like to switch from our custom docker images to a nix-based solution.

view this post on Zulip Coq Github Bot (Sep 30 2022 at 14:20):

Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:

We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.

cc @erikmd @CohenCyril

CI usage

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-use-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/not-ci-reasons-barplot.png)

The other answers were:

  1. Insufficient project maturity (somewhat like don't need it)
  2. Waste of energy (save the planet)
  3. I only have small Coq projects at this date
  4. Don't know advantages of doing so
  5. Time to set it up
  6. low priority
  7. I didn't think about it yet
  8. I'm not sure how my small projects would benefit from it
  9. Laziness :-)
  10. Just too small projects so far
  11. All of the above
  12. I didn't get around to it yet.
  13. I'm not sure how CI looks for coq, didn't think about it
  14. My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
  15. not needed for mostly exercise problems
  16. It was not necessary for my doctoral work.
  17. I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
  18. lazyness
  19. I'm too lazy / busy with other things to set it up.
  20. Waste of cycles. Nightly or weekly automated build runs are more than sufficient.

CI platforms

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-upset.png)

The other answers were:

We can also see that Travis CI has not been used by a lot of newcomers:

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-multiple-barplot.png)

CI tools

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-barplot.png)

The other answers were:

  1. UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
  2. can't remember
  3. I don't know, a team member set this up
  4. https://github.com/ocaml/setup-ocaml
  5. Opam
  6. Someone else set up CI
  7. ubuntu packages at https://launchpad.net/~jgross-h

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-barplot.png)

The other answers were:

  1. the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
  2. I don't know what we did, a team member set this up
  3. I reused & adapted scripts made by a colleague
  4. Learning how to use them might pay off in the future, but it is hard to give it a try with limited time when something else is already working.
  5. at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
  6. I had trouble making it work together with a Haskell environment in the past

General CI feedback

  1. I think that CI support is good. I wish that the docker images were released more tightly since that is the main bottleneck in updating coq projects to a newer version of coq.

  2. I am not at all aware about the CI tools that the Coq ecosystem provides.

    In UniMath, we have somewhat struggled with setting up CI, and we would love to learn more about the available CI tools.

  3. I feel hobbled using CI because I'm not an expert in the use of opam. And opam seems quite complex to me, so I am not well motivated to become expert in opam.

  4. Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

  5. I only started using it recently and it’s insanely helpful!

  6. I love Coq :D keep on the good work !

  7. A bit of delay with the coq/ocaml most recent versions

  8. A coq/setup-coq repo is what people will look for/expect when it comes to github-actions.
    That repo would install coq using the tool cache at the desired version.

    Getting coq into the actions/virtual-environments images will make everyone's CI jobs faster and make it simpler for people to get started. They are pretty generous with including niche software in their base images.

  9. For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

  10. I would love to see well-supported binary tarballs of Coq and ocaml and etc instead of special solutions for each platform of the day.

  11. I love it!

  12. Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

  13. I have used NixOS ages ago and I'm not an expert. With my basic knowledge I find the documentation on the nix solutions hard to follow, in particular when it comes to adding dependencies and having them cached with cachix. I didn't do a lot of digging because it was not too important, but overall I would very much like to switch from our custom docker images to a nix-based solution.

view this post on Zulip Coq Github Bot (Sep 30 2022 at 16:29):

Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:

We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.

cc @erikmd @CohenCyril

CI usage

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-use-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/not-ci-reasons-barplot.png)

The other answers were:

  1. Insufficient project maturity (somewhat like don't need it)
  2. Waste of energy (save the planet)
  3. I only have small Coq projects at this date
  4. Don't know advantages of doing so
  5. Time to set it up
  6. low priority
  7. I didn't think about it yet
  8. I'm not sure how my small projects would benefit from it
  9. Laziness :-)
  10. Just too small projects so far
  11. All of the above
  12. I didn't get around to it yet.
  13. I'm not sure how CI looks for coq, didn't think about it
  14. My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
  15. not needed for mostly exercise problems
  16. It was not necessary for my doctoral work.
  17. I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
  18. lazyness
  19. I'm too lazy / busy with other things to set it up.
  20. Waste of cycles. Nightly or weekly automated build runs are more than sufficient.

CI platforms

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-upset.png)

The other answers were:

We can also see that Travis CI has not been used by a lot of newcomers:

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-multiple-barplot.png)

CI tools

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-barplot.png)

The other answers were:

  1. UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
  2. can't remember
  3. I don't know, a team member set this up
  4. https://github.com/ocaml/setup-ocaml
  5. Opam
  6. Someone else set up CI
  7. ubuntu packages at https://launchpad.net/~jgross-h

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-upset.png)

The other answers were:

  1. the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
  2. I don't know what we did, a team member set this up
  3. I reused & adapted scripts made by a colleague
  4. Learning how to use them might pay off in the future, but it is hard to give it a try with limited time when something else is already working.
  5. at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
  6. I had trouble making it work together with a Haskell environment in the past

General CI feedback

  1. I think that CI support is good. I wish that the docker images were released more tightly since that is the main bottleneck in updating coq projects to a newer version of coq.

  2. I am not at all aware about the CI tools that the Coq ecosystem provides.

    In UniMath, we have somewhat struggled with setting up CI, and we would love to learn more about the available CI tools.

  3. I feel hobbled using CI because I'm not an expert in the use of opam. And opam seems quite complex to me, so I am not well motivated to become expert in opam.

  4. Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

  5. I only started using it recently and it’s insanely helpful!

  6. I love Coq :D keep on the good work !

  7. A bit of delay with the coq/ocaml most recent versions

  8. A coq/setup-coq repo is what people will look for/expect when it comes to github-actions.
    That repo would install coq using the tool cache at the desired version.

    Getting coq into the actions/virtual-environments images will make everyone's CI jobs faster and make it simpler for people to get started. They are pretty generous with including niche software in their base images.

  9. For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

  10. I would love to see well-supported binary tarballs of Coq and ocaml and etc instead of special solutions for each platform of the day.

  11. I love it!

  12. Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

  13. I have used NixOS ages ago and I'm not an expert. With my basic knowledge I find the documentation on the nix solutions hard to follow, in particular when it comes to adding dependencies and having them cached with cachix. I didn't do a lot of digging because it was not too important, but overall I would very much like to switch from our custom docker images to a nix-based solution.

view this post on Zulip Coq Github Bot (Oct 01 2022 at 14:06):

Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:

We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.

cc @erikmd @CohenCyril

CI usage

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-use-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/not-ci-reasons-barplot.png)

The other answers were:

  1. Insufficient project maturity (somewhat like don't need it)
  2. Waste of energy (save the planet)
  3. I only have small Coq projects at this date
  4. Don't know advantages of doing so
  5. Time to set it up
  6. low priority
  7. I didn't think about it yet
  8. I'm not sure how my small projects would benefit from it
  9. Laziness :-)
  10. Just too small projects so far
  11. All of the above
  12. I didn't get around to it yet.
  13. I'm not sure how CI looks for coq, didn't think about it
  14. My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
  15. not needed for mostly exercise problems
  16. It was not necessary for my doctoral work.
  17. I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
  18. lazyness
  19. I'm too lazy / busy with other things to set it up.
  20. Waste of cycles. Nightly or weekly automated build runs are more than sufficient.

CI platforms

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-upset.png)

The other answers were:

We can also see that Travis CI has not been used by a lot of newcomers:

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-platform-multiple-barplot.png)

CI tools

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-tools-upset.svg)

The other answers were:

  1. UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
  2. can't remember
  3. I don't know, a team member set this up
  4. https://github.com/ocaml/setup-ocaml
  5. Opam
  6. Someone else set up CI
  7. ubuntu packages at https://launchpad.net/~jgross-h

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-barplot.png)

![](https://thzimmer.gitlabpages.inria.fr/coq-survey-2022-assets/ci-why-custom-upset.png)

The other answers were:

  1. the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
  2. I don't know what we did, a team member set this up
  3. I reused & adapted scripts made by a colleague
  4. Learning how to use them might pay off in the future, but it is hard to give it a try with limited time when something else is already working.
  5. at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
  6. I had trouble making it work together with a Haskell environment in the past

General CI feedback

  1. I think that CI support is good. I wish that the docker images were released more tightly since that is the main bottleneck in updating coq projects to a newer version of coq.

  2. I am not at all aware about the CI tools that the Coq ecosystem provides.

    In UniMath, we have somewhat struggled with setting up CI, and we would love to learn more about the available CI tools.

  3. I feel hobbled using CI because I'm not an expert in the use of opam. And opam seems quite complex to me, so I am not well motivated to become expert in opam.

  4. Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

  5. I only started using it recently and it’s insanely helpful!

  6. I love Coq :D keep on the good work !

  7. A bit of delay with the coq/ocaml most recent versions

  8. A coq/setup-coq repo is what people will look for/expect when it comes to github-actions.
    That repo would install coq using the tool cache at the desired version.

    Getting coq into the actions/virtual-environments images will make everyone's CI jobs faster and make it simpler for people to get started. They are pretty generous with including niche software in their base images.

  9. For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

  10. I would love to see well-supported binary tarballs of Coq and ocaml and etc instead of special solutions for each platform of the day.

  11. I love it!

  12. Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

  13. I have used NixOS ages ago and I'm not an expert. With my basic knowledge I find the documentation on the nix solutions hard to follow, in particular when it comes to adding dependencies and having them cached with cachix. I didn't do a lot of digging because it was not too important, but overall I would very much like to switch from our custom docker images to a nix-based solution.

view this post on Zulip Coq Github Bot (Oct 04 2022 at 12:01):

Zimmi48:

view this post on Zulip Coq Github Bot (Oct 14 2022 at 02:36):

huynhtrankhanh edited issue #140 Volunteer interim maintainers needed for VsCoq:

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.

VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.

An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.

During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).

view this post on Zulip Coq Github Bot (Oct 14 2022 at 05:32):

palmskog closed issue #140 Volunteer interim maintainers needed for VsCoq:

The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.

VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.

As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.

VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.

An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.

During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).

view this post on Zulip Coq Github Bot (Oct 17 2022 at 13:54):

palmskog labeled issue #142 Proposal to move project MMaps to coq-community:

Project name: MMaps: Modular Finite Maps overs Ordered Types

Initial author(s): @letouzey

Current URL: https://github.com/letouzey/coq-mmaps

Kind: pure Coq library

License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)

Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.

Status: no changes since 2020

New maintainers: @palmskog and @letouzey

This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).

I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?

view this post on Zulip Coq Github Bot (Oct 17 2022 at 13:54):

palmskog labeled issue #142 Proposal to move project MMaps to coq-community:

Project name: MMaps: Modular Finite Maps overs Ordered Types

Initial author(s): @letouzey

Current URL: https://github.com/letouzey/coq-mmaps

Kind: pure Coq library

License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)

Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.

Status: no changes since 2020

New maintainers: @palmskog and @letouzey

This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).

I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?

view this post on Zulip Coq Github Bot (Oct 17 2022 at 13:54):

palmskog opened issue #142 Proposal to move project MMaps to coq-community:

Project name: MMaps: Modular Finite Maps overs Ordered Types

Initial author(s): @letouzey

Current URL: https://github.com/letouzey/coq-mmaps

Kind: pure Coq library

License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)

Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.

Status: no changes since 2020

New maintainers: @palmskog and @letouzey

This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).

I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?

view this post on Zulip Coq Github Bot (Oct 17 2022 at 15:28):

palmskog closed issue #142 Proposal to move project MMaps to coq-community:

Project name: MMaps: Modular Finite Maps overs Ordered Types

Initial author(s): @letouzey

Current URL: https://github.com/letouzey/coq-mmaps

Kind: pure Coq library

License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)

Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.

Status: no changes since 2020

New maintainers: @palmskog and @letouzey

This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).

I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?

view this post on Zulip Coq Github Bot (Oct 31 2022 at 13:49):

palmskog:

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:08):

palmskog labeled issue #143 Consolidation of Coq code from Coq-community into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:08):

palmskog opened issue #143 Consolidation of Coq code from Coq-community into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:22):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:23):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:24):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 10 2022 at 15:29):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 12 2022 at 10:48):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 12 2022 at 12:33):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 12 2022 at 12:45):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 14 2022 at 15:04):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Dec 15 2022 at 07:30):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Jan 01 2023 at 18:41):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Jan 01 2023 at 23:39):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Jan 09 2023 at 14:23):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Jan 11 2023 at 10:50):

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.

This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

view this post on Zulip Coq Github Bot (Jan 17 2023 at 16:02):

palmskog opened issue #144 Volunteer co-maintainer needed for Docker-Coq:

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.

Maintainer core tasks:

During their tenure, a maintainer will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and a short summary of relevant experience, for becoming a Docker-Coq maintainer. The maintainer will be selected from the issue responders by the Coq Team and Coq-community owners.

view this post on Zulip Coq Github Bot (Jan 17 2023 at 16:02):

palmskog labeled issue #144 Volunteer co-maintainer needed for Docker-Coq:

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.

Maintainer core tasks:

During their tenure, a maintainer will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and a short summary of relevant experience, for becoming a Docker-Coq maintainer. The maintainer will be selected from the issue responders by the Coq Team and Coq-community owners.

view this post on Zulip Coq Github Bot (Jan 17 2023 at 16:21):

palmskog edited issue #144 Volunteer co-maintainer needed for Docker-Coq:

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.

Desirable skills:

Maintainer core tasks:

During their tenure, a maintainer will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and a short summary of relevant experience, for becoming a Docker-Coq maintainer. The maintainer will be selected from the issue responders by the Coq Team and Coq-community owners.

view this post on Zulip Coq Github Bot (Jan 24 2023 at 21:02):

erikmd closed issue #144 Volunteer co-maintainer needed for Docker-Coq:

The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.

Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.

Desirable skills:

Maintainer core tasks:

During their tenure, a maintainer will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.

Please respond to this GitHub issue with your motivation, and a short summary of relevant experience, for becoming a Docker-Coq maintainer. The maintainer will be selected from the issue responders by the Coq Team and Coq-community owners.


Last updated: Feb 05 2023 at 14:02 UTC