GitHub webhook has been successfully configured by Zimmi48.

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.

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).

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).

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 volunteerThere 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.

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 volunteerThere 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.

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

to `master`

.

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

Zimmi48 merged PR #105 Remove remaining references to Gitter.

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

outsideof 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.

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

palmskog merged PR #106 Refine code of conduct.

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

to `master`

.

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

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

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. @Zimmi48When 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.

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. @Zimmi48When 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.

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

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

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

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

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:@theryThis 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.

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:@theryThis 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.

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:@theryThis 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.

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`coq-community`

organization on GitHub. Please let us know here if there are any issues.

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

derivationis 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 thesource 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).

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.

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.

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.

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

to `master`

:

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

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:

- 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)
- 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:

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:

- 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)
- 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:

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

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:

- 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)
- 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:

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 volunteerAs described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

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 volunteerAs described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

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 volunteerAs described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.

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

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

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

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

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

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

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

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

palmskog:

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.

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.

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.

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

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

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

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

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

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.

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.

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.

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.

anton-trunov:

- created Recommended Project Structure

Zimmi48:

Zimmi48:

anton-trunov:

anton-trunov:

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)

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.

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.

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?

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:

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

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

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

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

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

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

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

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. @Zimmi48When 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.

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

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

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.

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.

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.

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.

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.

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

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

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

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

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

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.

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

KevOrr:

anton-trunov:

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

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-danThis 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.

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-danThis 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.

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-danThis 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.

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-danThis 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.

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-danThis 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.

anton-trunov:

erikmd:

erikmd:

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.

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.

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.

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

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

palmskog:

palmskog:

palmskog:

palmskog:

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 volunteerThe last version of Coq known to work is 8.10:

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 volunteerThe last version of Coq known to work is 8.10:

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 volunteerThe last version of Coq known to work is 8.10:

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 volunteerThe last version of Coq known to work is 8.10:

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 volunteerThe last version of Coq known to work is 8.10:

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:@CasteranThe last version of Coq known to work is 8.10:

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:@CasteranThe last version of Coq known to work is 8.10:

palmskog:

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

to `master`

:

- Link to Hydra Battles and cie (cc @Casteran).
- No more editorial board (didn't materialize).

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

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

to `master`

.

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

to `master`

.

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

to `master`

:

- Link to Hydra Battles and cie (cc @Casteran).
- No more editorial board (didn't materialize).
- Reorganize and extend FAQ (new questions pointing to the contributing guide).
- Fix links to issue templates in the contributing guide.

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

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

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

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

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

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:

- theory (module CoqEAL_theory), which contains formal developments in algebra and optimized algorithms on mathcomp data structures.
- refinements (module CoqEAL_refinements), which is a framework to ease change of data representation during a proof.

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.

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:

- theory (module CoqEAL_theory), which contains formal developments in algebra and optimized algorithms on mathcomp data structures.
- refinements (module CoqEAL_refinements), which is a framework to ease change of data representation during a proof.

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.

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:

- theory (module CoqEAL_theory), which contains formal developments in algebra and optimized algorithms on mathcomp data structures.
- refinements (module CoqEAL_refinements), which is a framework to ease change of data representation during a proof.

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.

Zimmi48:

Zimmi48:

Zimmi48:

- edited To Do

Zimmi48:

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: directorycanonical_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 -->

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: directorycanonical_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 -->

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: directorycanonical_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 -->

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: directorycanonical_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 -->

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: directorycanonical_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 -->

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

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

Zimmi48:

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

- 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:

Status:maintained

New maintainer:the current maintainers would stay in place.

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: directorycanonical_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 -->

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:

- https://github.com/ejgallego/coq-plugin-template
- https://github.com/palmskog/coq-program-verification-template
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?

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:

- https://github.com/ejgallego/coq-plugin-template
- https://github.com/palmskog/coq-program-verification-template
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?

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:

- https://github.com/ejgallego/coq-plugin-template
- https://github.com/palmskog/coq-program-verification-template
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?

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

Hi folks,

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

- https://github.com/ejgallego/coq-plugin-template
- https://github.com/palmskog/coq-program-verification-template
`coq-template-foo`

and have this repository just be an index to all the existing templates, as suggested in the thread?

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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

kbrummert opened PR #133 Update README.md from `master`

to `master`

.

Zimmi48 merged PR #133 Update README.md.

palmskog:

palmskog:

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.

**palmskog** requested Zimmi48 for a review on PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI.

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from `osi-fsf-license`

to `master`

.

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.

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from `osi-fsf-license`

to `master`

.

palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from `osi-fsf-license`

to `master`

.

`osi-fsf-license`

to `master`

.

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.

palmskog merged PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI-FSF intersection.

palmskog opened PR #135 new name and description for hydra-battles repo project from `hydras-update`

to `master`

.

**palmskog** requested Zimmi48 for a review on PR #135 new name and description for hydra-battles repo project.

Zimmi48 merged PR #135 new name and description for hydra-battles repo project.

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 volunteerBased 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.

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 volunteerBased 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.

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 volunteerBased 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.

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

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

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

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?)

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?)

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

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

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

**Zimmi48** requested palmskog for a review on PR #138 Update info on editorial work..

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.

Zimmi48 updated PR #138 Update info on editorial work. from `editorial-work-update`

to `master`

.

Zimmi48 updated PR #138 Update info on editorial work. from `editorial-work-update`

to `master`

.

Zimmi48 merged PR #138 Update info on editorial work.

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

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

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

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

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

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).

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).

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).

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:

- Insufficient project maturity (somewhat like don't need it)
- Waste of energy (save the planet)
- I only have small Coq projects at this date
- Don't know advantages of doing so
- Time to set it up
- low priority
- I didn't think about it yet
- I'm not sure how my small projects would benefit from it
- Laziness :-)
- Just too small projects so far
- All of the above
- I didn't get around to it yet.
- I'm not sure how CI looks for coq, didn't think about it
- My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
- not needed for mostly exercise problems
- It was not necessary for my doctoral work.
- I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
- lazyness
- I'm too lazy / busy with other things to set it up.
- 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:

- 3 Jenkins
- 1 SVN
- 1 builds.sr.ht
- 1 "our own CI"
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:

- UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
- can't remember
- I don't know, a team member set this up
- https://github.com/ocaml/setup-ocaml
- Opam
- Someone else set up CI
- 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:

- the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
- I don't know what we did, a team member set this up
- I reused & adapted scripts made by a colleague
- 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.
- at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
- I had trouble making it work together with a Haskell environment in the past
## General CI feedback

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.

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.

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.

Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

I only started using it recently and it’s insanely helpful!

I love Coq :D keep on the good work !

A bit of delay with the coq/ocaml most recent versions

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.

For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

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.

I love it!

Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

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.

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:

- Insufficient project maturity (somewhat like don't need it)
- Waste of energy (save the planet)
- I only have small Coq projects at this date
- Don't know advantages of doing so
- Time to set it up
- low priority
- I didn't think about it yet
- I'm not sure how my small projects would benefit from it
- Laziness :-)
- Just too small projects so far
- All of the above
- I didn't get around to it yet.
- I'm not sure how CI looks for coq, didn't think about it
- My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
- not needed for mostly exercise problems
- It was not necessary for my doctoral work.
- I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
- lazyness
- I'm too lazy / busy with other things to set it up.
- 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:

- 3 Jenkins
- 1 SVN
- 1 builds.sr.ht
- 1 "our own CI"
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:

- UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
- can't remember
- I don't know, a team member set this up
- https://github.com/ocaml/setup-ocaml
- Opam
- Someone else set up CI
- 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:

- the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
- I don't know what we did, a team member set this up
- I reused & adapted scripts made by a colleague
- 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.
- at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
- I had trouble making it work together with a Haskell environment in the past
## General CI feedback

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.

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.

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.

Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

I only started using it recently and it’s insanely helpful!

I love Coq :D keep on the good work !

A bit of delay with the coq/ocaml most recent versions

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.

For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

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.

I love it!

Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

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.

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:

- Insufficient project maturity (somewhat like don't need it)
- Waste of energy (save the planet)
- I only have small Coq projects at this date
- Don't know advantages of doing so
- Time to set it up
- low priority
- I didn't think about it yet
- I'm not sure how my small projects would benefit from it
- Laziness :-)
- Just too small projects so far
- All of the above
- I didn't get around to it yet.
- I'm not sure how CI looks for coq, didn't think about it
- My latest projects have been too small to merit using CI and so I haven't yet figured out how to do it
- not needed for mostly exercise problems
- It was not necessary for my doctoral work.
- I don't need it for my personal projects, but my company uses it for work projects (I'm not the DevOps guy, though)
- lazyness
- I'm too lazy / busy with other things to set it up.
- 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:

- 3 Jenkins
- 1 SVN
- 1 builds.sr.ht
- 1 "our own CI"
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:

- UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
- can't remember
- I don't know, a team member set this up
- https://github.com/ocaml/setup-ocaml
- Opam
- Someone else set up CI
- 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:

- the docker images can't cache libraries I depend on. If the library compiles slowly, my CI compiles slowly. Caching .opam fixes this problem
- I don't know what we did, a team member set this up
- I reused & adapted scripts made by a colleague
- 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.
- at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
- I had trouble making it work together with a Haskell environment in the past
## General CI feedback

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.

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.

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.

Honestly CI is pretty great these days with pre-built images, the template, and GitHub Actions in general.

I only started using it recently and it’s insanely helpful!

I love Coq :D keep on the good work !

A bit of delay with the coq/ocaml most recent versions

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.

For plugin testing, it is necessary to combine specific OCaml and Coq versions, which the current images do not provide.

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.

I love it!

Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

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.

Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:

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:

- Insufficient project maturity (somewhat like don't need it)
- Waste of energy (save the planet)
- I only have small Coq projects at this date
- Don't know advantages of doing so
- Time to set it up
- low priority
- I didn't think about it yet
- I'm not sure how my small projects would benefit from it
- Laziness :-)
- Just too small projects so far
- All of the above
- I didn't get around to it yet.
- I'm not sure how CI looks for coq, didn't think about it
- not needed for mostly exercise problems
- It was not necessary for my doctoral work.
- lazyness
- I'm too lazy / busy with other things to set it up.
- 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:

- 3 Jenkins
- 1 SVN
- 1 builds.sr.ht
- 1 "our own CI"
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:

- UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
- can't remember
- I don't know, a team member set this up
- https://github.com/ocaml/setup-ocaml
- Opam
- Someone else set up CI
- 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:

- I don't know what we did, a team member set this up
- I reused & adapted scripts made by a colleague
- at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
- I had trouble making it work together with a Haskell environment in the past
## General CI feedback

I am not at all aware about the CI tools that the Coq ecosystem provides.

I only started using it recently and it’s insanely helpful!

I love Coq :D keep on the good work !

A bit of delay with the coq/ocaml most recent versions

That repo would install coq using the tool cache at the desired version.I love it!

Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:

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:

- Insufficient project maturity (somewhat like don't need it)
- Waste of energy (save the planet)
- I only have small Coq projects at this date
- Don't know advantages of doing so
- Time to set it up
- low priority
- I didn't think about it yet
- I'm not sure how my small projects would benefit from it
- Laziness :-)
- Just too small projects so far
- All of the above
- I didn't get around to it yet.
- I'm not sure how CI looks for coq, didn't think about it
- not needed for mostly exercise problems
- It was not necessary for my doctoral work.
- lazyness
- I'm too lazy / busy with other things to set it up.
- 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:

- 3 Jenkins
- 1 SVN
- 1 builds.sr.ht
- 1 "our own CI"
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:

- UniMath CI installs Coq from source on Ubuntu and via homebrew on MacOS
- can't remember
- I don't know, a team member set this up
- https://github.com/ocaml/setup-ocaml
- Opam
- Someone else set up CI
- 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:

- I don't know what we did, a team member set this up
- I reused & adapted scripts made by a colleague
- at the time I chose, this was the only solution that did not rebuild Coq from scratch on each CI run
- I had trouble making it work together with a Haskell environment in the past
## General CI feedback

I am not at all aware about the CI tools that the Coq ecosystem provides.

I only started using it recently and it’s insanely helpful!

I love Coq :D keep on the good work !

A bit of delay with the coq/ocaml most recent versions

That repo would install coq using the tool cache at the desired version.I love it!

Great work! But still a bit hard to use / understand, in particular the Nix-based setup.

Zimmi48:

huynhtrankhanh edited issue #140 Volunteer interim maintainers needed for VsCoq:

palmskog closed issue #140 Volunteer interim maintainers needed for VsCoq:

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 @letouzeyThis 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?

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 @letouzeyThis 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?

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 @letouzeyThis 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?

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

palmskog:

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.

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.

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.

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.

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.

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.

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [ ] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15

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.

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [ ] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [ ] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1
- [ ] https://github.com/coq-community/coqeal/issues/55

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [ ] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1
- [ ] https://github.com/coq-community/coqeal/issues/55
- [ ] https://github.com/coq-community/coq-mmaps/issues/8

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [x] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1
- [ ] https://github.com/coq-community/coqeal/issues/55
- [ ] https://github.com/coq-community/coq-mmaps/issues/8

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [x] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1
- [ ] https://github.com/coq-community/coqeal/issues/55
- [ ] https://github.com/coq-community/coq-mmaps/issues/8
- [ ] https://github.com/coq-community/coqeal/issues/72

palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:

- [ ] https://github.com/coq-community/bertrand/issues/18
- [ ] https://github.com/mit-plv/coqutil/issues/55
- [x] https://github.com/coq-community/aac-tactics/issues/123
- [ ] https://github.com/coq-community/corn/issues/58
- [ ] https://github.com/arthuraa/extructures/issues/22
- [ ] https://github.com/jasmin-lang/coqword/issues/15
- [ ] https://github.com/thery/grobner/issues/1
- [ ] https://github.com/coq-community/coqeal/issues/55
- [ ] https://github.com/coq-community/coq-mmaps/issues/8
- [ ] https://github.com/coq-community/coqeal/issues/72
- [ ] https://github.com/coq-community/graph-theory/issues/29

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:

- Create and deploy new Coq Docker definitions to the Docker registry after Coq (pre-)releases.
- Monitor the use of Coq Docker images for continuous integration on GitHub/GitLab and rebuild images when necessary.
- Work with the current Docker-Coq and Docker-Keeper maintainer to further develop and automate the toolchain.
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.

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:

- Create and deploy new Coq Docker definitions to the Docker registry after Coq (pre-)releases.
- Monitor the use of Coq Docker images for continuous integration on GitHub/GitLab and rebuild images when necessary.
- Work with the current Docker-Coq and Docker-Keeper maintainer to further develop and automate the toolchain.
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.

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:

- Familiarity with container software like Docker
- Familiarity with software continuous integration and build automation, in particular on GitHub and/or GitLab
- Basic shell scripting
- Basic Python programming
Maintainer core tasks:

- Create and deploy new Coq Docker definitions to the Docker registry after Coq (pre-)releases.
- Monitor the use of Coq Docker images for continuous integration on GitHub/GitLab and rebuild images when necessary.
- Work with the current Docker-Coq and Docker-Keeper maintainer to further develop and automate the toolchain.
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.

erikmd closed issue #144 Volunteer co-maintainer needed for Docker-Coq:

Desirable skills:

- Familiarity with container software like Docker
- Familiarity with software continuous integration and build automation, in particular on GitHub and/or GitLab
- Basic shell scripting
- Basic Python programming
Maintainer core tasks:

- Create and deploy new Coq Docker definitions to the Docker registry after Coq (pre-)releases.

Last updated: Feb 05 2023 at 14:02 UTC