Coq Github Bot (May 31 2020 at 17:27): Coq Github Bot (May 31 2020 at 17:27):GitHub webhook has been successfully configured by Zimmi48.
Coq Github Bot (Jun 02 2020 at 14:03):palmskog closed Issue #104 Change maintainer of project Stalmarck:
Project name and URL: https://github.com/coq-community/stalmarck
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
@herbelin is currently maintaining this project (and also qarith-stern-brocot and bertrand), but because he's also the one taking care of all the remaining coq-contribs, he'd gladly accept if someone else wanted to take over this package (or one of the other two I suppose). Cf. https://github.com/coq-community/stalmarck/pull/12#issuecomment-636029984.
Coq Github Bot (Jun 07 2020 at 23:40):palmskog unlabeled Issue #16 proviola:
Move a project to coq-community
Project name: proviola
Initial author(s): Carst Tankink @Carst-Tankink
Current URL: https://bitbucket.org/Carst/proviola-source
Kind: tool
License: GPL v3
Description: A tool to be able to replay the proofs when browsing a coqdoc-generated HTML file.
Status: Not maintained.
New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer -->
cc @JasonGross @mgrabovsky @yforster who have shown interest by having a fork on GitHub and @spitters @aa755 @siddharthist who have shown interest otherwise.
For those of you that do not already know about coq-community, have a look at the README at https://github.com/coq-community/manifesto. And sorry for the noise if you do not feel concerned (you can easily unsubscribe from this issue).
Coq Github Bot (Jun 07 2020 at 23:45):palmskog closed Issue #16 proviola:
Move a project to coq-community
Project name: proviola
Initial author(s): Carst Tankink @Carst-Tankink
Current URL: https://bitbucket.org/Carst/proviola-source
Kind: tool
License: GPL v3
Description: A tool to be able to replay the proofs when browsing a coqdoc-generated HTML file.
Status: Not maintained.
New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer -->
cc @JasonGross @mgrabovsky @yforster who have shown interest by having a fork on GitHub and @spitters @aa755 @siddharthist who have shown interest otherwise.
For those of you that do not already know about coq-community, have a look at the README at https://github.com/coq-community/manifesto. And sorry for the noise if you do not feel concerned (you can easily unsubscribe from this issue).
Coq Github Bot (Jun 10 2020 at 22:32):palmskog unlabeled Issue #86 Proposal to move JMLCoq to coq-community:
Project name: JMLCoq
Initial author(s): Hermann Lehner (http://people.inf.ethz.ch/lehnerh/ http://www.hermann-lehner.com)
Current URL: http://jmlcoq.info (http://jmlcoq.info/index_files/JMLCoq.tar.gz)
Kind: pure Coq library
License: MIT
Description: Coq formalization of the Java Modeling Language.
Status: unmaintained since 2011
New maintainer: looking for a volunteer
There are many Coq formalizations of fragments of Java floating around, but this one is quite well documented (a whole thesis) and has applications in runtime checking, and thus may be interesting to maintain for the long term. It seems likely the author should agree to license this work under an open source license, since the final thesis paragraph reads:
We hope that our work will be of good use in the research community and help to motivate others to choose a more formal approach to software verification.
Coq Github Bot (Jun 12 2020 at 10:42):palmskog closed Issue #86 Proposal to move JMLCoq to coq-community:
Project name: JMLCoq
Initial author(s): Hermann Lehner (http://people.inf.ethz.ch/lehnerh/ http://www.hermann-lehner.com)
Current URL: http://jmlcoq.info (http://jmlcoq.info/index_files/JMLCoq.tar.gz)
Kind: pure Coq library
License: MIT
Description: Coq formalization of the Java Modeling Language.
Status: unmaintained since 2011
New maintainer: looking for a volunteer
There are many Coq formalizations of fragments of Java floating around, but this one is quite well documented (a whole thesis) and has applications in runtime checking, and thus may be interesting to maintain for the long term. It seems likely the author should agree to license this work under an open source license, since the final thesis paragraph reads:
We hope that our work will be of good use in the research community and help to motivate others to choose a more formal approach to software verification.
Coq Github Bot (Jun 15 2020 at 15:19):Zimmi48 opened PR #105 Remove remaining references to Gitter. from fix-remaining-gitter to master.
Coq Github Bot (Jun 15 2020 at 15:19):Zimmi48 requested palmskog for a review on PR #105 Remove remaining references to Gitter..
Coq Github Bot (Jun 15 2020 at 16:16):Zimmi48 merged PR #105 Remove remaining references to Gitter.
Coq Github Bot (Jun 19 2020 at 15:04):palmskog opened PR #106 Refine code of conduct from refine-code-of-conduct to master:
I want to ensure that coq-community members are not attacked or reported for code-of-conduct violations based on (possibly politically-charged) statements or behavior that occur outside of coq-community, e.g., on Twitter, in personal blogs, and in issues in other GitHub organizations.
Here are two refinements of the code of conduct which I believe are conducive to this goal.
Note that the explicit mention of political views as an aspect of personal identity also exist in the Julia community standards, which the current code is based on.
Coq Github Bot (Jun 19 2020 at 15:06):palmskog requested Zimmi48 for a review on PR #106 Refine code of conduct.
Coq Github Bot (Jun 19 2020 at 15:25):palmskog merged PR #106 Refine code of conduct.
Coq Github Bot (Jun 19 2020 at 19:37):palmskog opened PR #107 fix dead link to Idris community standards from fix-idris-standards-url to master.
Coq Github Bot (Jun 20 2020 at 18:46):palmskog edited Issue #97 Proposal to move Almost Full to coq-community:
Project name: Almost Full
Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt
Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)
Kind: pure Coq library & formalization of a mathematical theorem
License: Unknown
Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).
There is also an Agda translation from 2014.
Status: Unmaintained since 2012
New maintainer: looking for a volunteer
Coq Github Bot (Jun 20 2020 at 20:18):palmskog merged PR #107 fix dead link to Idris community standards.
Coq Github Bot (Jun 23 2020 at 07:52):Zimmi48 opened Issue #108 Proposal to move Hydra battles in Coq to coq-community:
Project name: Hydra battles in Coq
Initial author(s): Pierre Castéran @Casteran
Current URL: https://framagit.org/casteran/hydra-battles-in-coq
Kind: documentation project composed of Coq scripts + LaTeX sources
License: CeCILL-B
Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).
Status: draft stage (complete but needs reviewing)
New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48
When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.
Coq Github Bot (Jun 23 2020 at 07:52):Zimmi48 labeled Issue #108 Proposal to move Hydra battles in Coq to coq-community:
Project name: Hydra battles in Coq
Initial author(s): Pierre Castéran @Casteran
Current URL: https://framagit.org/casteran/hydra-battles-in-coq
Kind: documentation project composed of Coq scripts + LaTeX sources
License: CeCILL-B
Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).
Status: draft stage (complete but needs reviewing)
New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48
When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.
Coq Github Bot (Jun 23 2020 at 10:03):palmskog unlabeled Issue #97 Proposal to move Almost Full to coq-community:
Project name: Almost Full
Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt
Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)
Kind: pure Coq library & formalization of a mathematical theorem
License: Unknown
Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).
There is also an Agda translation from 2014.
Status: Unmaintained since 2012
New maintainer: looking for a volunteer
Coq Github Bot (Jun 23 2020 at 10:04):palmskog edited Issue #97 Proposal to move Almost Full to coq-community:
Project name: Almost Full
Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt
Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)
Kind: pure Coq library & formalization of a mathematical theorem
License: MIT License
Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).
There is also an Agda translation from 2014.
Status: Unmaintained since 2012
New maintainer: looking for a volunteer
Coq Github Bot (Jun 23 2020 at 10:04):palmskog edited Issue #97 Proposal to move Almost Full to coq-community:
Project name: Almost Full
Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt
Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)
Kind: pure Coq library & formalization of a mathematical theorem
License: MIT License
Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).
There is also an Agda translation from 2014.
Status: Unmaintained since 2012
New maintainer: @palmskog
Coq Github Bot (Jun 23 2020 at 10:57):palmskog closed Issue #97 Proposal to move Almost Full to coq-community:
Project name: Almost Full
Initial author(s): Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt
Current URL: https://github.com/palmskog/almost-full (tested on Coq 8.11 - 8.12)
Kind: pure Coq library & formalization of a mathematical theorem
License: MIT License
Description: Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination. As per this comment the theorem might be used to obtain a constructive version of Hilbert's basis theorem (a challenge posed in this blog post).
There is also an Agda translation from 2014.
Status: Unmaintained since 2012
New maintainer: @palmskog
Coq Github Bot (Jul 02 2020 at 20:13):palmskog opened Issue #109 Proposal to move High School Geometry to coq-community:
Project name: High School Geometry
Initial author(s): Frédérique Guilhot
Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry
Kind: pure Coq library / formalization of mathematical theorems
License: LGPL-2.1-or-later
Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.
Status: Unmaintained since 2019
New maintainer: @thery
This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.
@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the
coq-communityorganization on GitHub. Please let us know here if there are any issues.
Coq Github Bot (Jul 02 2020 at 20:13):palmskog labeled Issue #109 Proposal to move High School Geometry to coq-community:
Project name: High School Geometry
Initial author(s): Frédérique Guilhot
Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry
Kind: pure Coq library / formalization of mathematical theorems
License: LGPL-2.1-or-later
Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.
Status: Unmaintained since 2019
New maintainer: @thery
This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.
@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the
coq-communityorganization on GitHub. Please let us know here if there are any issues.
Coq Github Bot (Jul 02 2020 at 20:15):palmskog labeled Issue #109 Proposal to move High School Geometry to coq-community:
Project name: High School Geometry
Initial author(s): Frédérique Guilhot
Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry
Kind: pure Coq library / formalization of mathematical theorems
License: LGPL-2.1-or-later
Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.
Status: Unmaintained since 2019
New maintainer: @thery
This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.
@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the
coq-communityorganization on GitHub. Please let us know here if there are any issues.
Coq Github Bot (Jul 02 2020 at 23:30):palmskog closed Issue #109 Proposal to move High School Geometry to coq-community:
Project name: High School Geometry
Initial author(s): Frédérique Guilhot
Current URL: https://github.com/thery/HighSchoolGeometry and https://github.com/coq-contribs/high-school-geometry
Kind: pure Coq library / formalization of mathematical theorems
License: LGPL-2.1-or-later
Description: This library is dedicated to high-shool geometry teaching. The axiomatisation for affine euclidean space is in a non analytic setting.
Status: Unmaintained since 2019
New maintainer: @thery
This is a project whose earlier releases and website on gforge will soon disappear, as discussed here. It was recently ported by to 8.11 by Laurent Théry, who graciously offered to transfer his repository to coq-community.
@thery as per discussion the opam-archive issue, I have invited you to become a member of coq-community to allow your repository to be maintained here. Once you are a member, you should be able to transfer your repository to the
coq-communityorganization on GitHub. Please let us know here if there are any issues.
Coq Github Bot (Jul 13 2020 at 09:10):Zimmi48 transferred Issue #37 State of CI testing with Nix:
It's been a long time since I said I would write this summary issue (cc @siddharthist who was interested in particular).
Overall, the current state of CI testing with Nix is documented in the wiki. It is one of the two newly established and officially supported ways of testing projects depending on Coq, the other being opam + Docker (see comparison here). Both setups avoid to rebuild Coq at every test or depend on an outdated opam cache.
Both setups should allow in theory to reuse build artifacts to build reverse-dependencies (e.g. corn which depends on math-classes) or the various packages depending on math-comp. In the case of Docker, it is a matter of generating a Dockerfile and pushing the new image to a Docker registry (either dockerhub when building the master branch, or GitLab's registry when building any branch, see discussion at https://github.com/math-comp/math-comp/pull/256).
In the case of Nix, it requires pushing to a cache on Cachix. This should be very easy to setup as soon as this is tested and documented. However, my initial tests did not work. The main difficulty is to make sure that the exact same derivation is built on the CI that is going to push to Cachix as is required in the depending builds. The problem is that the derivation depends in turn on the source derivation. Depending how it is built, it may be sensible to the name of the directory which contains it.
For instance, the
default.nixfile of Coq takes it source from the current directory, and this is also the case for the proposed templatedefault.nixin this repository. When building withnix build, the source will be copied to the nix store in a repository like/nix/store/l14sddwdd8lrji8qp900jcd12h4w1sgq-namewherenameis 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 runnix buildon the sources but we donix build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}". ThefetchTarballoperation will always copy the sources to a location in the Nix store that only depends on the content of the tarball. Then our templatedefault.nixfor projects depending on Coq will load the Coq dependency in the same way (usingfetchTarballagain).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).
Coq Github Bot (Aug 03 2020 at 12:55):Zimmi48 opened PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:
For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.
Coq Github Bot (Aug 04 2020 at 11:23):Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:
For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.
Coq Github Bot (Aug 04 2020 at 13:08):Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:
For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.
Coq Github Bot (Aug 04 2020 at 14:22):Zimmi48 updated PR #110 Add an FAQ on choice of licenses. from licensing-advice to master:
For reasons which I've explained elsewhere (cf. https://github.com/coq-community/templates/issues/34#issuecomment-634565291 and https://github.com/coq-community/corn/pull/99#issuecomment-667997810), I believe that we should encourage the Coq community in general, and the coq-community projects in particular, to adopt more permissive licenses and to move away from LGPL (at least for new projects). This FAQ item in the manifesto's README should be a step in this direction.
Coq Github Bot (Aug 04 2020 at 20:17):palmskog merged PR #110 Add an FAQ on choice of licenses.
Coq Github Bot (Aug 14 2020 at 18:29):palmskog labeled Issue #111 Listing and preserving formalized mathematical results in Coq:
This is a meta issue asking the general question:
How can coq-community work towards better listing and preservation of formalized mathematics in Coq?
A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
As one example, consider Wiedijk's list of 100 theorems as formalized Coq, where the code for most entries are currently inaccessible or obsolete.
coq-community members can address this situation in at least two ways:
- 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:
Coq Github Bot (Aug 14 2020 at 18:29):palmskog opened Issue #111 Listing and preserving formalized mathematical results in Coq:
This is a meta issue asking the general question:
How can coq-community work towards better listing and preservation of formalized mathematics in Coq?
A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
As one example, consider Wiedijk's list of 100 theorems as formalized Coq, where the code for most entries are currently inaccessible or obsolete.
coq-community members can address this situation in at least two ways:
- 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:
Coq Github Bot (Aug 14 2020 at 19:34):liyishuai closed Issue #70 Add Coq to Travis CI:
Meta-issue
Our current template builds everything in Docker, which is less flexible than what Travis can do with other languages. It'll be nice if we could have
language: coqand 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
Coq Github Bot (Aug 15 2020 at 20:15):palmskog edited Issue #111 Listing and preserving formalized mathematical results in Coq:
This is a meta issue asking the general question:
How can coq-community work towards better listing and preservation of formalized mathematics in Coq?
A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
As one example, consider Madiot's list of Coq theorems from Wiedijk's general list. Quite a few of the links in Madiot's list point to Coq code that does not build with the current stable version of Coq.
coq-community members can address this situation in at least two ways:
- 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:
Coq Github Bot (Aug 19 2020 at 10:18):palmskog opened Issue #112 Change maintainer of project Binary Rational Numbers :
Project name and URL: https://github.com/coq-community/qarith-stern-brocot
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 10:18):palmskog labeled Issue #112 Change maintainer of project Binary Rational Numbers :
Project name and URL: https://github.com/coq-community/qarith-stern-brocot
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 10:20):palmskog opened Issue #113 Change maintainer of project Bertrand:
Project name and URL: https://github.com/coq-community/bertrand
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 10:20):palmskog labeled Issue #113 Change maintainer of project Bertrand:
Project name and URL: https://github.com/coq-community/bertrand
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 10:24):Zimmi48 labeled Issue #113 Change maintainer of project Bertrand:
Project name and URL: https://github.com/coq-community/bertrand
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 10:25):Zimmi48 labeled Issue #112 Change maintainer of project Binary Rational Numbers :
Project name and URL: https://github.com/coq-community/qarith-stern-brocot
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Aug 19 2020 at 11:32):palmskog:
Coq Github Bot (Aug 19 2020 at 11:42):palmskog:
Coq Github Bot (Aug 19 2020 at 11:46):palmskog:
Coq Github Bot (Aug 19 2020 at 11:51):palmskog:
Coq Github Bot (Aug 19 2020 at 12:04):palmskog:
Coq Github Bot (Aug 19 2020 at 12:10):palmskog:
Coq Github Bot (Aug 19 2020 at 13:10):palmskog:
Coq Github Bot (Aug 25 2020 at 11:29):lthms opened Issue #114 Proposal to publish project coqffi to coq-community:
Project name:
coqffiInitial 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:
coqffiautomatically generates FFI binding (i.e., extraction primitives) to OCaml libraries for Coq.Status: Maintained, not yet publlished.
New maintainer: @lthms
Coq Github Bot (Aug 25 2020 at 14:21):lthms edited Issue #114 Proposal to publish project coqffi to coq-community:
Project name:
coqffiInitial 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:
coqffiautomatically generates FFI binding to OCaml libraries for Coq. For instance, given the following.mlifiletype 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]
coqffigenerates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity tocoq-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
Thomas Letan (Aug 25 2020 at 14:31):thanks for your feedback @Bas Spitters and sorry for the previous unhelpful description of the project
Coq Github Bot (Aug 30 2020 at 10:14):palmskog:
Coq Github Bot (Aug 30 2020 at 10:29):palmskog:
Coq Github Bot (Aug 30 2020 at 10:32):palmskog:
Coq Github Bot (Aug 30 2020 at 10:34):palmskog:
Coq Github Bot (Aug 30 2020 at 10:35):palmskog:
Coq Github Bot (Aug 30 2020 at 10:45):palmskog:
Coq Github Bot (Aug 30 2020 at 11:00):palmskog:
Coq Github Bot (Aug 30 2020 at 11:15):palmskog:
Coq Github Bot (Aug 30 2020 at 11:31):palmskog:
Coq Github Bot (Aug 30 2020 at 11:38):palmskog:
Coq Github Bot (Aug 30 2020 at 11:38):palmskog:
Coq Github Bot (Aug 31 2020 at 12:27):chdoc opened Issue #115 Proposal to move project comp-dec-modal to coq-community:
Project name: Completeness and Decidability of Modal-Logic Calculi
Initial author(s): Christian Doczkal (me)
Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl
Kind: pure Coq library / formalization of mathematical theorems
License: CeCILL-B
Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).
Status: maintained
New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.
Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current
recursive makebuild infrastructure to a single centralized Makefile.
Coq Github Bot (Aug 31 2020 at 12:27):chdoc labeled Issue #115 Proposal to move project comp-dec-modal to coq-community:
Project name: Completeness and Decidability of Modal-Logic Calculi
Initial author(s): Christian Doczkal (me)
Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl
Kind: pure Coq library / formalization of mathematical theorems
License: CeCILL-B
Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).
Status: maintained
New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.
Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current
recursive makebuild infrastructure to a single centralized Makefile.
Coq Github Bot (Aug 31 2020 at 12:29):palmskog labeled Issue #115 Proposal to move project comp-dec-modal to coq-community:
Project name: Completeness and Decidability of Modal-Logic Calculi
Initial author(s): Christian Doczkal (me)
Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl
Kind: pure Coq library / formalization of mathematical theorems
License: CeCILL-B
Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).
Status: maintained
New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.
Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current
recursive makebuild infrastructure to a single centralized Makefile.
Coq Github Bot (Aug 31 2020 at 17:03):jmadiot opened Issue #116 Proposal to move project coq100 to coq-community:
Project name: coq-100-theorems
Initial author(s): Jean-Marie Madiot
Current URL: https://madiot.fr/coq100/
Kind: web page + formalizations of a few mathematical theorems
License: MIT
Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.
Status: maintained
New maintainer: I wish to continue to maintain if that's possible
Coq Github Bot (Aug 31 2020 at 17:03):jmadiot labeled Issue #116 Proposal to move project coq100 to coq-community:
Project name: coq-100-theorems
Initial author(s): Jean-Marie Madiot
Current URL: https://madiot.fr/coq100/
Kind: web page + formalizations of a few mathematical theorems
License: MIT
Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.
Status: maintained
New maintainer: I wish to continue to maintain if that's possible
Coq Github Bot (Aug 31 2020 at 17:05):jmadiot edited Issue #116 Proposal to move project coq100 to coq-community:
Project name: coq-100-theorems
Initial author(s): Jean-Marie Madiot
Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100
Kind: web page + formalizations of a few mathematical theorems
License: MIT
Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.
Status: maintained
New maintainer: I wish to continue to maintain if that's possible
Coq Github Bot (Aug 31 2020 at 18:22):palmskog labeled Issue #116 Proposal to move project coq100 to coq-community:
Project name: coq-100-theorems
Initial author(s): Jean-Marie Madiot
Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100
Kind: web page + formalizations of a few mathematical theorems
License: MIT
Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.
Status: maintained
New maintainer: I wish to continue to maintain if that's possible
Coq Github Bot (Aug 31 2020 at 19:37):palmskog closed Issue #116 Proposal to move project coq100 to coq-community:
Project name: coq-100-theorems
Initial author(s): Jean-Marie Madiot
Current URL: https://madiot.fr/coq100/ repository: https://github.com/jmadiot/coq100
Kind: web page + formalizations of a few mathematical theorems
License: MIT
Description: This is an appendix to Freek Wiedijk's web page on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq.
Status: maintained
New maintainer: I wish to continue to maintain if that's possible
Coq Github Bot (Sep 07 2020 at 15:57):chdoc closed Issue #115 Proposal to move project comp-dec-modal to coq-community:
Project name: Completeness and Decidability of Modal-Logic Calculi
Initial author(s): Christian Doczkal (me)
Current URL: https://github.com/chdoc/comp-dec-modal, https://github.com/chdoc/comp-dec-pdl
Kind: pure Coq library / formalization of mathematical theorems
License: CeCILL-B
Description: Constructive machine-checked proofs of soundness and completeness of calculi for for various modal logics (i.e, K,K*, CTL, (C)PDL).
Status: maintained
New maintainer: Christian Doczkal (@chdoc) / looking for co-maintainer.
Remark: Currently these results are spread out over the two aforementioned repositories and their shared submodule. To simplify long-term maintenance, I would gather everything in a single repository and convert the current
recursive makebuild infrastructure to a single centralized Makefile.
Coq Github Bot (Sep 08 2020 at 15:43):palmskog opened Issue #117 Proposal to move project Gaia to coq-community:
Project name: Gaia (Geometry, Algebra, Informatics and Applications)
Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson
Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/
Kind: pure Coq library and formalization of a mathematical theorems
License: MIT
Status: unmaintained since José Grimm passed away in 2019
Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).
New maintainer: Laurent Théry (@thery)
Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).
I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.
Coq Github Bot (Sep 08 2020 at 15:43):palmskog labeled Issue #117 Proposal to move project Gaia to coq-community:
Project name: Gaia (Geometry, Algebra, Informatics and Applications)
Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson
Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/
Kind: pure Coq library and formalization of a mathematical theorems
License: MIT
Status: unmaintained since José Grimm passed away in 2019
Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).
New maintainer: Laurent Théry (@thery)
Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).
I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.
Coq Github Bot (Sep 08 2020 at 15:44):palmskog labeled Issue #117 Proposal to move project Gaia to coq-community:
Project name: Gaia (Geometry, Algebra, Informatics and Applications)
Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson
Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/
Kind: pure Coq library and formalization of a mathematical theorems
License: MIT
Status: unmaintained since José Grimm passed away in 2019
Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).
New maintainer: Laurent Théry (@thery)
Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).
I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.
Coq Github Bot (Sep 08 2020 at 16:15):anton-trunov:
Coq Github Bot (Sep 08 2020 at 16:21):Zimmi48:
Coq Github Bot (Sep 08 2020 at 16:37):Zimmi48:
Coq Github Bot (Sep 08 2020 at 16:42):anton-trunov:
Coq Github Bot (Sep 08 2020 at 18:22):anton-trunov:
Coq Github Bot (Sep 09 2020 at 08:20):palmskog closed Issue #117 Proposal to move project Gaia to coq-community:
Project name: Gaia (Geometry, Algebra, Informatics and Applications)
Initial author(s): José Grimm, with help from Alban Quadrat and using a set theory axiomatization originally by Carlos Simpson
Current URL: https://github.com/palmskog/gaia http://www-sop.inria.fr/marelle/gaia/
Kind: pure Coq library and formalization of a mathematical theorems
License: MIT
Status: unmaintained since José Grimm passed away in 2019
Description: Gaia was a project by José Grimm to implement the "Elements of Mathematics" books by N. Bourbaki. It is based on the Mathematical Components (MathComp) library and contains formalizations of many concepts and results from set and number theory (150k+ lines of Coq code).
New maintainer: Laurent Théry (@thery)
Thanks to @ybertot, the final version of Gaia released by José in 2018 has been released under the MIT license. I (@palmskog) have ported this release to Coq 8.10 and later (depending on MathComp 1.11 and later).
I propose that the Coq community continues the maintenance of this project and at least maintains compatibility with latest Coq and MathComp. @thery has generously offered to be the initial coq-community maintainer. I will also help out but can't commit to being co-maintainer for the time being.
Coq Github Bot (Sep 11 2020 at 17:07):anton-trunov labeled Issue #118 Automated deployment of coqdoc HTML documentation for each new release:
Looks like the instructions in the wiki can be used in conjunction with Github Actions to do this, provided the build system has the
coqdocgoal.
Coq Github Bot (Sep 11 2020 at 17:07):anton-trunov opened Issue #118 Automated deployment of coqdoc HTML documentation for each new release:
Looks like the instructions in the wiki can be used in conjunction with Github Actions to do this, provided the build system has the
coqdocgoal.
Coq Github Bot (Sep 14 2020 at 12:38):palmskog edited Issue #111 Listing and preserving formalized mathematical results in Coq:
This is a meta issue asking the general question:
How can coq-community work towards better listing and preservation of formalized mathematics in Coq?
A lot of mathematics has been formalized in Coq, but unless it ends up in a library such Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
As one example, consider Madiot's list of Coq theorems from Wiedijk's general list. Quite a few of the links in Madiot's list point to Coq code that does not build with the current stable version of Coq.
coq-community members can address this situation in at least two ways:
- 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:
Coq Github Bot (Sep 16 2020 at 13:02):lthms edited Issue #114 Proposal to publish project coqffi to coq-community:
Project name:
coqffiInitial 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:
coqffiautomatically generates FFI binding to OCaml libraries for Coq. For instance, given the following.mlifiletype 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]
coqffigenerates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity tocoq-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
Coq Github Bot (Oct 08 2020 at 16:53):palmskog closed Issue #114 Proposal to publish project coqffi to coq-community:
Project name:
coqffiInitial 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:
coqffiautomatically generates FFI binding to OCaml libraries for Coq. For instance, given the following.mlifiletype 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]
coqffigenerates the necessary Coq boilerplate to use these functions in a Coq development, and to configure the extraction mechanism accordingly, delegating impurity tocoq-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
Coq Github Bot (Oct 12 2020 at 10:31):jmadiot opened Issue #119 Proposal to move project Coqtail to coq-community:
Project name: Coqtail
Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot
Current URL: https://coqtail.github.io/
Kind: formalization of mathematical theorems
License: LGPL 3.0
Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.
Status: maintained
New maintainer: I (@jmadiot ) am volunteering to maintain
Coq Github Bot (Oct 12 2020 at 10:31):jmadiot labeled Issue #119 Proposal to move project Coqtail to coq-community:
Project name: Coqtail
Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot
Current URL: https://coqtail.github.io/
Kind: formalization of mathematical theorems
License: LGPL 3.0
Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.
Status: maintained
New maintainer: I (@jmadiot ) am volunteering to maintain
Coq Github Bot (Oct 12 2020 at 12:36):palmskog labeled Issue #119 Proposal to move project Coqtail to coq-community:
Project name: Coqtail
Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot
Current URL: https://coqtail.github.io/
Kind: formalization of mathematical theorems
License: LGPL 3.0
Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.
Status: maintained
New maintainer: I (@jmadiot ) am volunteering to maintain
Coq Github Bot (Oct 12 2020 at 15:14):jmadiot edited Issue #119 Proposal to move project Coqtail to coq-community:
Project name: Coqtail
Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, Amaury Pouly
Current URL: https://coqtail.github.io/
Kind: formalization of mathematical theorems
License: LGPL 3.0
Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.
Status: maintained
New maintainer: I (@jmadiot ) am volunteering to maintain
Coq Github Bot (Oct 13 2020 at 08:26):Zimmi48 edited Issue #108 Proposal to move Hydra battles in Coq to coq-community / to create a documented-examples project.
Project name: Hydra battles in Coq
Initial author(s): Pierre Castéran @Casteran
Current URL: https://framagit.org/casteran/hydra-battles-in-coq
Kind: documentation project composed of Coq scripts + LaTeX sources
License: CeCILL-B
Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).
Status: draft stage (complete but needs reviewing)
New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48
When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.
Coq Github Bot (Oct 17 2020 at 12:04):palmskog edited Issue #25 Proposal to add RelationExtraction:
Move a project to coq-community
Project name: RelationExtraction
Initial author(s): Catherine Dubois, David Delahaye, and Pierre-Nicolas Tollitte
Current URLs: https://github.com/coq-contribs/relation-extraction https://github.com/picnic/RelationExtraction
Kind: OCaml plugin
License: GPL3
Description: A plugin for generating functions from inductive types which make this possible. The functions can either be functions inside Coq or functions in an extraction language, such as OCaml. The underlying theory and implementation of the plugin is described in the paper Producing Certified Functional Code from Inductive Specifications.
Status: Currently maintained by Coq devs in Coq-contribs
New maintainer: looking for a volunteer
Coq Github Bot (Oct 17 2020 at 13:46):palmskog edited Issue #25 Proposal to add RelationExtraction:
Move a project to coq-community
Project name: RelationExtraction
Initial author(s): Catherine Dubois, David Delahaye, and Pierre-Nicolas Tollitte
Current URLs: https://github.com/coq-contribs/relation-extraction https://github.com/picnic/RelationExtraction https://github.com/herbelin/RelationExtraction
Kind: OCaml plugin
License: GPL3
Description: A plugin for generating functions from inductive types which make this possible. The functions can either be functions inside Coq or functions in an extraction language, such as OCaml. The underlying theory and implementation of the plugin is described in the paper Producing Certified Functional Code from Inductive Specifications.
Status: Currently maintained by Coq devs in Coq-contribs
New maintainer: looking for a volunteer
Coq Github Bot (Oct 19 2020 at 13:25):anton-trunov opened Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 19 2020 at 13:25):anton-trunov labeled Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 19 2020 at 13:25):anton-trunov labeled Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 19 2020 at 13:26):anton-trunov edited Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT (GPL v3 at the time of publication)
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I'm volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 19 2020 at 14:14):anton-trunov edited Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT (GPL v3 at the time of publication)
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 20 2020 at 07:18):palmskog closed Issue #119 Proposal to move project Coqtail to coq-community:
Project name: Coqtail
Initial author(s): Guillaume Allais, Sylvain Dailler, Hugo Férée, Jean-Marie Madiot, Pierre-Marie Pédrot, Amaury Pouly
Current URL: https://coqtail.github.io/
Kind: formalization of mathematical theorems
License: LGPL 3.0
Description: Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis.
Status: maintained
New maintainer: I (@jmadiot ) am volunteering to maintain
Coq Github Bot (Oct 20 2020 at 08:19):aerabi opened Issue #121 Proposal to move project generic-environments to coq-community:
Project name: Generic Environments
Initial author(s): Emmanuel Polonowski
Current URL: https://github.com/coq-contribs/generic-environments
Kind: pure Coq library
License: LGPL
Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.
Status: Not maintained recently. The last available version works with Coq 8.10.
New maintainer: I volunteer: @aerabi
Coq Github Bot (Oct 20 2020 at 08:19):aerabi labeled Issue #121 Proposal to move project generic-environments to coq-community:
Project name: Generic Environments
Initial author(s): Emmanuel Polonowski
Current URL: https://github.com/coq-contribs/generic-environments
Kind: pure Coq library
License: LGPL
Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.
Status: Not maintained recently. The last available version works with Coq 8.10.
New maintainer: I volunteer: @aerabi
Coq Github Bot (Oct 20 2020 at 08:20):anton-trunov labeled Issue #121 Proposal to move project generic-environments to coq-community:
Project name: Generic Environments
Initial author(s): Emmanuel Polonowski
Current URL: https://github.com/coq-contribs/generic-environments
Kind: pure Coq library
License: LGPL
Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.
Status: Not maintained recently. The last available version works with Coq 8.10.
New maintainer: I volunteer: @aerabi
Coq Github Bot (Oct 20 2020 at 15:27):palmskog closed Issue #113 Change maintainer of project Bertrand:
Project name and URL: https://github.com/coq-community/bertrand
Current maintainer: @herbelin
Status: maintained
New maintainer: looking for a volunteer
As described by @Zimmi48 in #104, @herbelin is taking care of the coq-contribs, so a new maintainer is wanted for this project.
Coq Github Bot (Oct 21 2020 at 08:52):anton-trunov closed Issue #120 Proposal to move project regexp-Brzozowski to coq-community:
Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)
Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)
Current URL: https://github.com/vsiles/regexp-Brzozowski
Kind: pure Coq library
License: MIT (GPL v3 at the time of publication)
Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.
Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).
New maintainer: I volunteer to maintain the library. Looking for co-maintainers.
Here is the link to the corresponding issue I opened in the original repo: https://github.com/vsiles/regexp-Brzozowski/issues/2.
Coq Github Bot (Oct 29 2020 at 11:54):palmskog closed Issue #121 Proposal to move project generic-environments to coq-community:
Project name: Generic Environments
Initial author(s): Emmanuel Polonowski
Current URL: https://github.com/coq-contribs/generic-environments
Kind: pure Coq library
License: LGPL
Description: Generic_Environments is a library which provides an abstract data type of environments, as a functor parameterized by a module defining variables, and a function which builds environments for such variables with any Type of type. Usual operations over environments are defined, along with an extensive set of basic and more advanced properties. Moreover, an implementation using lists satisfying and all the required properties is provided.
Status: Not maintained recently. The last available version works with Coq 8.10.
New maintainer: I volunteer: @aerabi
Coq Github Bot (Nov 04 2020 at 21:02):KevOrr:
Coq Github Bot (Nov 06 2020 at 17:08):anton-trunov:
Coq Github Bot (Nov 13 2020 at 00:55):palmskog closed Issue #108 Proposal to move Hydra battles in Coq to coq-community / to create a documented-examples project.
Project name: Hydra battles in Coq
Initial author(s): Pierre Castéran @Casteran
Current URL: https://framagit.org/casteran/hydra-battles-in-coq
Kind: documentation project composed of Coq scripts + LaTeX sources
License: CeCILL-B
Description: An exploration of some properties of Kirby and Paris' hydra battles, with the help of the Coq Proof assistant (draft).
Status: draft stage (complete but needs reviewing)
New maintainer: @Casteran with help of other coq-community members, e.g. @Zimmi48
When we created coq-community, the goals were not just to provide a place for the long term maintenance of Coq packages but also for the collaborative writing of documentation around code, with this project as a first brick. Despite still being a draft, this project is now sufficiently complete to join coq-community as a first example of this documentation objective. It is our hope that other community members will help review the project, and especially the documentation part. Note also that for now this part is written in LaTeX, but it should be possible to experiment migrating to other formats that would be better suited to be viewed online as HTML pages.
Coq Github Bot (Nov 13 2020 at 02:04):palmskog opened Issue #122 Proposal to move Autosubst version 1 to coq-community:
Project name: Autosubst (version 1)
Initial author(s): Steven Schäfer and Tobias Tebbi
Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)
Kind: pure Coq library
License: MIT
Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.
Status: unmaintained
New maintainers: @RalfJung and @co-dan
This is based on a discussion on Zulip.
The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.
Coq Github Bot (Nov 13 2020 at 02:04):palmskog labeled Issue #122 Proposal to move Autosubst version 1 to coq-community:
Project name: Autosubst (version 1)
Initial author(s): Steven Schäfer and Tobias Tebbi
Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)
Kind: pure Coq library
License: MIT
Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.
Status: unmaintained
New maintainers: @RalfJung and @co-dan
This is based on a discussion on Zulip.
The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.
Coq Github Bot (Nov 13 2020 at 02:04):palmskog labeled Issue #122 Proposal to move Autosubst version 1 to coq-community:
Project name: Autosubst (version 1)
Initial author(s): Steven Schäfer and Tobias Tebbi
Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)
Kind: pure Coq library
License: MIT
Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.
Status: unmaintained
New maintainers: @RalfJung and @co-dan
This is based on a discussion on Zulip.
The current proposal is that someone with access rights in the uds-pl organization transfers the above repo to the coq-community. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.
Coq Github Bot (Nov 13 2020 at 06:03):palmskog edited Issue #122 Proposal to move Autosubst version 1 to coq-community:
Project name: Autosubst (version 1)
Initial author(s): Steven Schäfer and Tobias Tebbi
Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)
Kind: pure Coq library
License: MIT
Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.
Status: unmaintained
New maintainers: @RalfJung and @co-dan
This is based on a discussion on Zulip.
The current proposal is that someone with access rights in the uds-psl organization transfers the above repo to the coq-community organization. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.
Coq Github Bot (Nov 27 2020 at 07:44):palmskog closed Issue #122 Proposal to move Autosubst version 1 to coq-community:
Project name: Autosubst (version 1)
Initial author(s): Steven Schäfer and Tobias Tebbi
Current URL: https://github.com/uds-psl/autosubst (the most recent version is found in the branch: https://github.com/uds-psl/autosubst/tree/coq86-devel)
Kind: pure Coq library
License: MIT
Description: A Coq library for parallel de Bruijn substitutions, useful when developing formal metatheory.
Status: unmaintained
New maintainers: @RalfJung and @co-dan
This is based on a discussion on Zulip.
The current proposal is that someone with access rights in the uds-psl organization transfers the above repo to the coq-community organization. @yforster can you confirm that you are able to do the transfer? If so, I can invite you to the coq-community organization.
Coq Github Bot (Dec 10 2020 at 16:25):anton-trunov:
Coq Github Bot (Dec 12 2020 at 00:04):erikmd:
Coq Github Bot (Dec 12 2020 at 00:06):erikmd:
Coq Github Bot (Dec 15 2020 at 08:43):palmskog opened Issue #123 Change maintainer of ATBR:
Project name and URL: https://github.com/coq-community/atbr
Current maintainer: @tchajed
Status: unmaintained
New maintainer: looking for a volunteer
@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.
Coq Github Bot (Dec 15 2020 at 08:43):palmskog labeled Issue #123 Change maintainer of ATBR:
Project name and URL: https://github.com/coq-community/atbr
Current maintainer: @tchajed
Status: unmaintained
New maintainer: looking for a volunteer
@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.
Coq Github Bot (Dec 15 2020 at 08:44):palmskog labeled Issue #123 Change maintainer of ATBR:
Project name and URL: https://github.com/coq-community/atbr
Current maintainer: @tchajed
Status: unmaintained
New maintainer: looking for a volunteer
@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.
Coq Github Bot (Dec 15 2020 at 08:44):palmskog labeled Issue #123 Change maintainer of ATBR:
Project name and URL: https://github.com/coq-community/atbr
Current maintainer: @tchajed
Status: unmaintained
New maintainer: looking for a volunteer
@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.
Coq Github Bot (Dec 15 2020 at 08:44):palmskog labeled Issue #123 Change maintainer of ATBR:
Project name and URL: https://github.com/coq-community/atbr
Current maintainer: @tchajed
Status: unmaintained
New maintainer: looking for a volunteer
@tchajed has indicated he wants to step down as maintainer of ATBR due to other commitments. Until a new maintainer is found, other coq-community members can collaborate to do basic project maintenance. The project is likely to work at least through 8.13 with only minor changes required.
Coq Github Bot (Dec 20 2020 at 18:03):palmskog:
Coq Github Bot (Dec 20 2020 at 18:04):palmskog:
Coq Github Bot (Dec 20 2020 at 18:05):palmskog:
Coq Github Bot (Dec 21 2020 at 08:16):palmskog:
Coq Github Bot (Jan 01 2021 at 13:29):palmskog opened Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: looking for a volunteer
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 13:29):palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: looking for a volunteer
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 13:29):palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: looking for a volunteer
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 13:29):palmskog labeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: looking for a volunteer
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 15:29):palmskog unlabeled Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: looking for a volunteer
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 15:35):palmskog edited Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: @Casteran
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 01 2021 at 18:02):palmskog closed Issue #124 Proposal to move projects Goedel and Pocklington to coq-community:
Project names: Goedel and Pocklington
Initial author(s): Russell O'Connor (Goedel), Olga Caprotti and Martijn Oostdijk (Pocklington)
Current URL: https://github.com/coq-contribs/goedel https://github.com/coq-contribs/pocklington
Kind: pure Coq libraries
License: CC-0/public domain (Goedel) LGPL-2.1-or-later (Pocklington)
Description: A constructive proof of the Gödel-Rosser incompleteness theorem in Coq, and its supporting library of primality certification. As pointed out by @Casteran, the incompleteness proof may have pedagogical uses and contains a formalization of Peano arithmetic that may be useful elsewhere.
Status: unmaintained
New maintainer: @Casteran
The last version of Coq known to work is 8.10:
Coq Github Bot (Jan 05 2021 at 15:50):palmskog:
Coq Github Bot (Feb 15 2021 at 16:51):Zimmi48 opened PR #125 Update manifesto with current state of affairs. from update-manifesto to master:
- Link to Hydra Battles and cie (cc @Casteran).
- No more editorial board (didn't materialize).
Coq Github Bot (Feb 15 2021 at 16:51):Zimmi48 requested palmskog for a review on PR #125 Update manifesto with current state of affairs..
Coq Github Bot (Mar 10 2021 at 13:58):Zimmi48 updated PR #125 Update manifesto with current state of affairs. from update-manifesto to master.
Coq Github Bot (Mar 10 2021 at 14:01):Zimmi48 updated PR #125 Update manifesto with current state of affairs. from update-manifesto to master.
Coq Github Bot (Mar 10 2021 at 14:03):Zimmi48 edited PR #125 Update manifesto with current state of affairs. from update-manifesto to master:
- 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.
Coq Github Bot (Mar 10 2021 at 14:16):Zimmi48 merged PR #125 Update manifesto with current state of affairs.
Coq Github Bot (May 05 2021 at 17:22):siraben opened Issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): @ notin (not on GitHub) @herbelin
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (May 05 2021 at 17:22):siraben labeled Issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): @ notin (not on GitHub) @herbelin
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (May 05 2021 at 18:18):Zimmi48 edited Issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): Laurent Théry @thery
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (Jul 03 2021 at 03:28):siraben closed issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): Laurent Théry @thery
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (Jul 27 2021 at 18:03):Zimmi48 opened issue #127 Proposal to move project CoqEAL to coq-community:
Project name: CoqEAL
Initial author(s): according to the README, the authors are
- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)Current URL: https://github.com/CoqEAL/CoqEAL
Kind: pure Coq library, which depends on the parmcoq plugin.
License: MIT
Description:
This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:
- 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.
Coq Github Bot (Jul 27 2021 at 18:03):Zimmi48 labeled issue #127 Proposal to move project CoqEAL to coq-community:
Project name: CoqEAL
Initial author(s): according to the README, the authors are
- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)Current URL: https://github.com/CoqEAL/CoqEAL
Kind: pure Coq library, which depends on the parmcoq plugin.
License: MIT
Description:
This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:
- 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.
Coq Github Bot (Jul 27 2021 at 19:09):palmskog labeled issue #127 Proposal to move project CoqEAL to coq-community:
Project name: CoqEAL
Initial author(s): according to the README, the authors are
- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)Current URL: https://github.com/CoqEAL/CoqEAL
Kind: pure Coq library, which depends on the parmcoq plugin.
License: MIT
Description:
This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:
- 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.
Coq Github Bot (Aug 08 2021 at 11:16):Zimmi48:
Coq Github Bot (Aug 08 2021 at 13:09):Zimmi48:
Coq Github Bot (Aug 08 2021 at 13:21):Zimmi48:
Coq Github Bot (Aug 08 2021 at 15:41):Zimmi48:
Coq Github Bot (Aug 16 2021 at 13:14):ybertot opened issue #128 Proposal to move project X to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Aug 16 2021 at 13:14):ybertot labeled issue #128 Proposal to move project X to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Aug 16 2021 at 13:16):palmskog edited issue #128 Proposal to move project matric-canonical-forms to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Aug 16 2021 at 13:17):palmskog labeled issue #128 Proposal to move project matric-canonical-forms to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Aug 16 2021 at 13:17):palmskog edited issue #128 Proposal to move project matrix-canonical-forms to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Aug 17 2021 at 13:39):thery reopened issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): Laurent Théry @thery
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (Aug 18 2021 at 04:27):palmskog closed issue #126 Proposal to move sudoku to coq-community:
Project name: https://github.com/coq-contribs/sudoku
Initial author(s): Laurent Théry @thery
Current URL: https://github.com/coq-contribs/sudoku/
Kind: certified Sudoku solver
License: LGPL-2.1
Description: This is a project that implements a certified Sudoku solver in Coq
Status: Hasn't seen commits in over two years, except recently by @siraben
New maintainer: @siraben
Coq Github Bot (Aug 31 2021 at 19:58):Zimmi48:
Coq Github Bot (Sep 01 2021 at 09:52):palmskog closed issue #127 Proposal to move project CoqEAL to coq-community:
Project name: CoqEAL
Initial author(s): according to the README, the authors are
- Guillaume Cano (initial)
- Cyril Cohen (initial)
- Maxime Dénès (initial)
- Anders Mörtberg (initial)
- Damien Rouhling
- Vincent Siles (initial)Current URL: https://github.com/CoqEAL/CoqEAL
Kind: pure Coq library, which depends on the parmcoq plugin.
License: MIT
Description:
This libary contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). It has two parts:
- 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.
Coq Github Bot (Sep 07 2021 at 08:47):palmskog closed issue #128 Proposal to move project matrix-canonical-forms to coq-community:
Project name:
matrix-canonical-forms (capitalization and hyphenation can be changed). Another name could be more appropriate if we also want to include the result about the Perron-Frobenius theorem.Initial author(s):
Guillaume CanoCurrent URL:
https://www-sop.inria.fr/marelle/Guillaume.Cano/ (initial work by Guillaume Cano)
https://github.com/ybertot/canonical_forms (partial port of Guillaume's work: directory canonical_forms)Kind: pure Coq library / formalization of a mathematical theorem / ...
License: MIT
Description:
This library builds on mathematical components and CoqEAL to provide formal proofs about matrices: the existence of Smith normal forms, Jordan Normal forms, etc, converging towards a proof of the Perron-Frobenius theorem.Status: <!-- is it maintained or not? if not, since when? -->
Partial maintenance has been done: the development about matrix canonical forms has been ported to recent versions of math-comp and CoqEAL.New maintainer: Yves Bertot <!-- update if you are a volunteer / know a volunteer -->
Coq Github Bot (Sep 14 2021 at 07:18):ejgallego opened issue #129 Current setup vs full repository project templates?
Hi folks,
this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.
Moreover, we have the current alternative Coq project templates in the wild:
- 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-fooand have this repository just be an index to all the existing templates, as suggested in the thread?
Coq Github Bot (Sep 14 2021 at 07:19):palmskog labeled issue #129 Current setup vs full repository project templates?
Hi folks,
this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.
Moreover, we have the current alternative Coq project templates in the wild:
- 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-fooand have this repository just be an index to all the existing templates, as suggested in the thread?
Coq Github Bot (Sep 14 2021 at 07:20):palmskog labeled issue #129 Current setup vs full repository project templates?
Hi folks,
this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.
Moreover, we have the current alternative Coq project templates in the wild:
- 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-fooand have this repository just be an index to all the existing templates, as suggested in the thread?
Coq Github Bot (Sep 14 2021 at 07:25):Zimmi48 edited issue #129 Hosting project templates in coq-community?
Hi folks,
this is a follow up from the discussion at https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/.E2.9C.94.20Dune.2C.20_CoqProject.20and.20tests ; indeed, it seems to me that the current "template" setup may be a bit limited (see also coq-community/templates#95 ) , in particular as to setup full projects such as the plugin template.
Moreover, we have the current alternative Coq project templates in the wild:
- 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-fooand have this repository just be an index to all the existing templates, as suggested in the thread?
Coq Github Bot (Sep 23 2021 at 06:00):mycroft92 opened issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:
Project name: vcs-prettify-symbols-mode
Initial author(s): Seige Bell
Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode
Kind: Visual Studio Code Plugin
License: MIT License
Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.
Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)
New maintainer: Looking for a volunteer.
Coq Github Bot (Sep 23 2021 at 06:00):mycroft92 labeled issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:
Project name: vcs-prettify-symbols-mode
Initial author(s): Seige Bell
Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode
Kind: Visual Studio Code Plugin
License: MIT License
Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.
Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)
New maintainer: Looking for a volunteer.
Coq Github Bot (Sep 23 2021 at 06:59):Zimmi48 labeled issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:
Project name: vcs-prettify-symbols-mode
Initial author(s): Seige Bell
Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode
Kind: Visual Studio Code Plugin
License: MIT License
Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.
Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)
New maintainer: Looking for a volunteer.
Coq Github Bot (Sep 23 2021 at 06:59):Zimmi48 edited issue #130 Proposal to move project vcs-prettify-symbols-mode to coq-community:
Project name: vcs-prettify-symbols-mode
Initial author(s): CJ Bell
Current URL: https://github.com/siegebell/vsc-prettify-symbols-mode
Kind: Visual Studio Code Plugin
License: MIT License
Description: Prettify symbols mode makes visual substitutions to your source code, e.g. displaying fun as λ, while never touching your code.
Status: Not maintained since 5 years. However two forks of the project are currently maintained (https://github.com/silver-dragon/vsc-prettify-symbols-mode) & (https://github.com/Pancaek/vsc-conceal)
New maintainer: Looking for a volunteer.
Coq Github Bot (Sep 27 2021 at 12:18):ybertot labeled issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> Yves Bertot Volunteers, will be happy to onboard any other volunteer.
Coq Github Bot (Sep 27 2021 at 12:18):ybertot opened issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: looking for a volunteer <!-- update if you are a volunteer / know a volunteer --> Yves Bertot Volunteers, will be happy to onboard any other volunteer.
Coq Github Bot (Sep 27 2021 at 14:04):Zimmi48 edited issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: Yves Bertot, will be happy to onboard any other volunteer.
Coq Github Bot (Sep 27 2021 at 14:11):Zimmi48 edited issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: Yves Bertot, will be happy to onboard any other volunteer.
Coq Github Bot (Sep 27 2021 at 14:12):palmskog labeled issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: Yves Bertot, will be happy to onboard any other volunteer.
Coq Github Bot (Sep 28 2021 at 09:21):palmskog closed issue #131 Proposal to move project coq-dpdgraph to coq-community:
Project name: coq-dpdgraph
Initial author(s): Anne Pacalet (@Karmaki), Yves Bertot, Olivier Pons
Current URL: https://github.com/karmaki/coq-dpdgraph
Kind: OCaml plugin
License: GNU LGPL 2.1
Description: an Ocaml plugin to traverse the dependency graph between defined functions, types, and theorems in the Coq memory.
Status: <!-- is it maintained or not? if not, since when? --> It is maintained, part of Coq-CI, with a new version produced for each release of Coq, thanks to the kind help of the main Coq developers.
New maintainer: Yves Bertot, will be happy to onboard any other volunteer.
Coq Github Bot (Oct 02 2021 at 10:57):BinderDavid opened issue #132 Proposal to move project Autosubst2 to coq-community:
Project name: Autosubst2
Initial author(s): Kathrin Stark
Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/
Kind: Automatic boilerplate generation for substitutions.
License: Unclear at the moment, the website is down and not archived with the wayback machine :(
Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101
Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the
Coq a la carteproject: https://dl.acm.org/doi/10.1145/3372885.3373817 ?New maintainer: looking for a volunteer
Coq Github Bot (Oct 02 2021 at 10:57):BinderDavid labeled issue #132 Proposal to move project Autosubst2 to coq-community:
Project name: Autosubst2
Initial author(s): Kathrin Stark
Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/
Kind: Automatic boilerplate generation for substitutions.
License: Unclear at the moment, the website is down and not archived with the wayback machine :(
Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101
Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the
Coq a la carteproject: https://dl.acm.org/doi/10.1145/3372885.3373817 ?New maintainer: looking for a volunteer
Coq Github Bot (Oct 02 2021 at 11:12):palmskog closed issue #132 Proposal to move project Autosubst2 to coq-community:
Project name: Autosubst2
Initial author(s): Kathrin Stark
Current URL: https://www.ps.uni-saarland.de/extras/autosubst2/
Kind: Automatic boilerplate generation for substitutions.
License: Unclear at the moment, the website is down and not archived with the wayback machine :(
Description: Similar to Autosubst, which is already a part of coq-community. Has been described in a CPP 2019 article: https://dl.acm.org/doi/10.1145/3293880.3294101
Status: Unclear. It was available for download as an archive, but to my knowledge no public git repository exists. The website is currently offline as well, so there is no way to obtain the sources right now. It is possible that development continued for the
Coq a la carteproject: https://dl.acm.org/doi/10.1145/3372885.3373817 ?New maintainer: looking for a volunteer
Coq Github Bot (Oct 30 2021 at 15:45):kbrummert opened PR #133 Update README.md from master to master.
Coq Github Bot (Oct 30 2021 at 16:02):Zimmi48 merged PR #133 Update README.md.
Coq Github Bot (Nov 03 2021 at 11:05):palmskog:
Coq Github Bot (Nov 05 2021 at 11:14):palmskog:
Coq Github Bot (Nov 06 2021 at 17:05):palmskog opened PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master:
We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.
I change from "choose" to "use", since these are in many requirements that restrict choice rather than mere recommendations on top of free choice.
Coq Github Bot (Nov 06 2021 at 17:06):palmskog requested Zimmi48 for a review on PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI.
Coq Github Bot (Nov 06 2021 at 17:20):palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.
Coq Github Bot (Nov 06 2021 at 18:57):palmskog edited PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master:
We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.
I change from "choose" to "use", since these are requirements that restrict choice rather than mere recommendations on top of free choice.
Coq Github Bot (Nov 08 2021 at 07:55):palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.
Coq Github Bot (Nov 09 2021 at 09:09):palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.
Coq Github Bot (Nov 09 2021 at 09:16):palmskog updated PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI from osi-fsf-license to master.
Coq Github Bot (Nov 09 2021 at 09:40):palmskog edited PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI-FSF intersection from osi-fsf-license to master:
We want to explicitly allow non-OSI free software licenses such as CECILL-B and CECILL-C, while encouraging MIT/MPL-2.0 and preferring OSI over non-OSI. Based on this discussion in the Coq Zulip.
I change from "choose" to "use", since these are requirements that restrict choice rather than mere recommendations on top of free choice.
Coq Github Bot (Nov 09 2021 at 09:41):palmskog merged PR #134 restrict licenses to OSI approved or FSF free software, encourage OSI-FSF intersection.
Coq Github Bot (Nov 14 2021 at 02:14):palmskog opened PR #135 new name and description for hydra-battles repo project from hydras-update to master.
Coq Github Bot (Nov 14 2021 at 02:14):palmskog requested Zimmi48 for a review on PR #135 new name and description for hydra-battles repo project.
Coq Github Bot (Nov 14 2021 at 16:03):Zimmi48 merged PR #135 new name and description for hydra-battles repo project.
Coq Github Bot (Dec 08 2021 at 17:55):palmskog opened issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 08 2021 at 17:55):palmskog labeled issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 08 2021 at 17:55):palmskog labeled issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 08 2021 at 17:56):palmskog labeled issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 08 2021 at 17:56):palmskog labeled issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 09 2021 at 10:23):proux01 unlabeled issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: looking for a volunteer
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 09 2021 at 10:23):proux01 edited issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: @proux01 (and others?)
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Dec 09 2021 at 15:08):palmskog closed issue #136 Proposal to move bignums to coq-community:
Project name: Bignums
Initial author(s): Laurent Théry (@thery), Benjamin Grégoire, Arnaud Spiwack, Evgeny Makarov, Pierre Letouzey
Current URL: https://github.com/coq/bignums
Kind: Coq library and OCaml plugin
License: LGPL-2.1-only ("same as Coq")
Description: Provides BigN, BigZ, BigQ that used to be part of Coq standard library. Part of the Coq Platform, installed by default in the official Coq Docker images.
Status: part of Coq's CI and sometimes changed by Coq team members
New maintainer: @proux01 (and others?)
Based on the discussion and consensus in the latest Coq Call, I am proposing that Bignums transitions from the Coq GitHub organization to coq-community. The advantage is that coq-community has a process for maintaining a standalone repo, and many people who can do releases, merge PRs, etc.
@erikmd @proux01 would any of you consider being the maintainer of bignums in coq-community? I can help out with templates and other build boilerplate, but I can't be the maintainer myself.
@Zimmi48 should a representative from the Coq core team "officially" approve the move perhaps? Even before we have a maintainer lined up, or after? Grateful if you can help ping the right people.
Coq Github Bot (Feb 02 2022 at 10:13):amahboubi opened issue #137 Proposal to move project Apery to coq-community:
Project name: Apery
Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote
Current URL: https://github.com/math-comp/apery
Kind: pure Coq library, formalization of a mathematical theorem
License: CeCiLL-C
Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.
Status: Maintained, part of MathComp CI
New maintainer: @amahboubi
Coq Github Bot (Feb 02 2022 at 10:13):amahboubi labeled issue #137 Proposal to move project Apery to coq-community:
Project name: Apery
Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote
Current URL: https://github.com/math-comp/apery
Kind: pure Coq library, formalization of a mathematical theorem
License: CeCiLL-C
Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.
Status: Maintained, part of MathComp CI
New maintainer: @amahboubi
Coq Github Bot (Feb 02 2022 at 10:15):palmskog labeled issue #137 Proposal to move project Apery to coq-community:
Project name: Apery
Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote
Current URL: https://github.com/math-comp/apery
Kind: pure Coq library, formalization of a mathematical theorem
License: CeCiLL-C
Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.
Status: Maintained, part of MathComp CI
New maintainer: @amahboubi
Coq Github Bot (Feb 02 2022 at 10:48):Zimmi48 requested palmskog for a review on PR #138 Update info on editorial work..
Coq Github Bot (Feb 02 2022 at 10:48):Zimmi48 opened PR #138 Update info on editorial work. from editorial-work-update to master:
To reflect what has been done. See https://github.com/coq-community/coq-community.github.io/issues/2.
Coq Github Bot (Feb 02 2022 at 10:58):Zimmi48 updated PR #138 Update info on editorial work. from editorial-work-update to master.
Coq Github Bot (Feb 02 2022 at 10:58):Zimmi48 updated PR #138 Update info on editorial work. from editorial-work-update to master.
Coq Github Bot (Feb 02 2022 at 10:59):Zimmi48 merged PR #138 Update info on editorial work.
Coq Github Bot (Feb 03 2022 at 10:27):palmskog closed issue #137 Proposal to move project Apery to coq-community:
Project name: Apery
Initial author(s): Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote
Current URL: https://github.com/math-comp/apery
Kind: pure Coq library, formalization of a mathematical theorem
License: CeCiLL-C
Description: This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.
Status: Maintained, part of MathComp CI
New maintainer: @amahboubi
Coq Github Bot (Mar 09 2022 at 10:29):ybertot opened issue #139 Proposal to move project fourcolor to coq-community:
Project name: fourcolor
Initial author(s): Georges Gonthier
Current URL: https://github.com/math-comp/fourcolor
Kind: formalization of a mathematical theorem
License: CeCILL-B
Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
Status: <!-- is it maintained or not? if not, since when? --> maintained
New maintainer: @ybertot
Coq Github Bot (Mar 09 2022 at 10:29):ybertot labeled issue #139 Proposal to move project fourcolor to coq-community:
Project name: fourcolor
Initial author(s): Georges Gonthier
Current URL: https://github.com/math-comp/fourcolor
Kind: formalization of a mathematical theorem
License: CeCILL-B
Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
Status: <!-- is it maintained or not? if not, since when? --> maintained
New maintainer: @ybertot
Coq Github Bot (Mar 09 2022 at 10:31):palmskog labeled issue #139 Proposal to move project fourcolor to coq-community:
Project name: fourcolor
Initial author(s): Georges Gonthier
Current URL: https://github.com/math-comp/fourcolor
Kind: formalization of a mathematical theorem
License: CeCILL-B
Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
Status: <!-- is it maintained or not? if not, since when? --> maintained
New maintainer: @ybertot
Coq Github Bot (Mar 10 2022 at 14:29):palmskog closed issue #139 Proposal to move project fourcolor to coq-community:
Project name: fourcolor
Initial author(s): Georges Gonthier
Current URL: https://github.com/math-comp/fourcolor
Kind: formalization of a mathematical theorem
License: CeCILL-B
Description: The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.
The formal proof is based on the Mathematical Components library for the Coq proof assistant.
Status: <!-- is it maintained or not? if not, since when? --> maintained
New maintainer: @ybertot
Coq Github Bot (Sep 27 2022 at 18:45):palmskog labeled issue #140 Volunteer interim maintainers needed for VsCoq:
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).
Coq Github Bot (Sep 27 2022 at 18:45):palmskog opened issue #140 Volunteer interim maintainers needed for VsCoq:
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).
Coq Github Bot (Sep 27 2022 at 19:50):palmskog labeled issue #140 Volunteer interim maintainers needed for VsCoq:
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).
Coq Github Bot (Sep 30 2022 at 13:47):Zimmi48 labeled issue #141 CI feedback from the Coq Community Survey 2022:
We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.
cc @erikmd @CohenCyril
CI usage
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
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:
CI tools
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
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.
Coq Github Bot (Sep 30 2022 at 13:47):Zimmi48 opened issue #141 CI feedback from the Coq Community Survey 2022:
We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.
cc @erikmd @CohenCyril
CI usage
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
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:
CI tools
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
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.
Coq Github Bot (Sep 30 2022 at 14:20):Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:
We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.
cc @erikmd @CohenCyril
CI usage
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
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:
CI tools
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
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.
Coq Github Bot (Sep 30 2022 at 16:29):Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:
We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.
cc @erikmd @CohenCyril
CI usage
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
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:
CI tools
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
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.
Coq Github Bot (Oct 01 2022 at 14:06):Zimmi48 edited issue #141 CI feedback from the Coq Community Survey 2022:
We asked several questions about CI for Coq projects in the Coq Community Survey 2022. Here are the results.
cc @erikmd @CohenCyril
CI usage
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
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:
CI tools
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
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.
Coq Github Bot (Oct 04 2022 at 12:01):Zimmi48:
Coq Github Bot (Oct 14 2022 at 02:36):huynhtrankhanh edited issue #140 Volunteer interim maintainers needed for VsCoq:
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).
Coq Github Bot (Oct 14 2022 at 05:32):palmskog closed issue #140 Volunteer interim maintainers needed for VsCoq:
The Coq core team and Coq-community are looking for volunteer interim maintainers of the VsCoq project.
VsCoq is an extension of the Visual Studio Code (VS Code) editor to support Coq source files and interaction with Coq. In a recent survey of Coq users, around one third of respondents reported that they use VS Code for Coq.
As described in the public roadmap, VsCoq developers are currently focusing on building a new simplified architecture for VsCoq. This means that there are no longer any resources available for maintaining the current codebase.
VsCoq is an open source project available under the MIT license and developed in the Coq-community organization on GitHub. VsCoq is written in TypeScript and uses an XML-based protocol to communicate with Coq. Interim maintainers are expected to implement bugfixes, respond to pull requests and issues on GitHub, and release new versions of VsCoq on the Visual Studio Marketplace and Open VSX.
An important goal of interim maintenance is to provide a good experience for Coq users relying on VS Code for Coq while the new VsCoq architecture (and support for this architecture in Coq itself) is being developed and tested. However, interim maintainers should be aware that substantial parts of the current codebase are due to be replaced as the roadmap is implemented.
During their tenure, interim maintainers will be considered part of the Coq Team and credited for their work in release notes for Coq releases, for example on Zenodo.
Please respond to this GitHub issue with your motivation, and summary of relevant experience, for becoming an interim maintainer of VsCoq. The interim maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community owners. Those not selected will still be encouraged to contribute to VsCoq in collaboration with the new maintainer(s).
Coq Github Bot (Oct 17 2022 at 13:54):palmskog labeled issue #142 Proposal to move project MMaps to coq-community:
Project name: MMaps: Modular Finite Maps overs Ordered Types
Initial author(s): @letouzey
Current URL: https://github.com/letouzey/coq-mmaps
Kind: pure Coq library
License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)
Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.
Status: no changes since 2020
New maintainers: @palmskog and @letouzey
This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).
I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?
Coq Github Bot (Oct 17 2022 at 13:54):palmskog labeled issue #142 Proposal to move project MMaps to coq-community:
Project name: MMaps: Modular Finite Maps overs Ordered Types
Initial author(s): @letouzey
Current URL: https://github.com/letouzey/coq-mmaps
Kind: pure Coq library
License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)
Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.
Status: no changes since 2020
New maintainers: @palmskog and @letouzey
This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).
I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?
Coq Github Bot (Oct 17 2022 at 13:54):palmskog opened issue #142 Proposal to move project MMaps to coq-community:
Project name: MMaps: Modular Finite Maps overs Ordered Types
Initial author(s): @letouzey
Current URL: https://github.com/letouzey/coq-mmaps
Kind: pure Coq library
License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)
Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.
Status: no changes since 2020
New maintainers: @palmskog and @letouzey
This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).
I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?
Coq Github Bot (Oct 17 2022 at 15:28):palmskog closed issue #142 Proposal to move project MMaps to coq-community:
Project name: MMaps: Modular Finite Maps overs Ordered Types
Initial author(s): @letouzey
Current URL: https://github.com/letouzey/coq-mmaps
Kind: pure Coq library
License: LGPL-2.1-only (based on LICENSE file and file headers, can we clarify?)
Description: Several implementations of finite maps over arbitrary ordered types using Coq functors. This is an udpdated version of Coq Stdlib's FMaps. It is meant to complement the MSet library.
Status: no changes since 2020
New maintainers: @palmskog and @letouzey
This is a very useful library for which it would be useful to have an opam package, and that should reasonably be included in the Coq Platform (and eventually maybe Coq's stdlib).
I would like to volunteer to be interim maintainer to get the project on track towards the Coq Platform. @letouzey are you fine with this and with transferring the project to the coq-community GitHub organization?
Coq Github Bot (Oct 31 2022 at 13:49):palmskog:
Coq Github Bot (Dec 10 2022 at 15:08):palmskog labeled issue #143 Consolidation of Coq code from Coq-community into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 10 2022 at 15:08):palmskog opened issue #143 Consolidation of Coq code from Coq-community into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 10 2022 at 15:22):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 10 2022 at 15:23):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation in Coq-community projects by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 10 2022 at 15:24):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 10 2022 at 15:29):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 12 2022 at 10:48):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 12 2022 at 12:33):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
Coq Github Bot (Dec 12 2022 at 12:45):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Dec 14 2022 at 15:04):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Dec 15 2022 at 07:30):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Jan 01 2023 at 18:41):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Jan 01 2023 at 23:39):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Jan 09 2023 at 14:23):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Jan 11 2023 at 10:50):palmskog edited issue #143 Consolidation of generally useful Coq code into Coq Platform projects:
Generally useful Coq code is often fragmented into many projects working at different levels of abstraction. For example, Coq code with results about primes may be part of a program verification project, which can make reuse difficult in other projects. A solution to this problem is continuous consolidation of general results into Coq libraries that are part of the Coq Platform, such as CoqPrime or Coq's Standard library itself.
This issue is an attempt at driving consolidation of Coq projects (focusing primarily on Coq-community projects) by facilitating discussion and tracking consolidation issues.
- [ ] 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
Coq Github Bot (Jan 17 2023 at 16:02):palmskog opened issue #144 Volunteer co-maintainer needed for Docker-Coq:
The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.
Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.
Maintainer core tasks:
- 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.
Coq Github Bot (Jan 17 2023 at 16:02):palmskog labeled issue #144 Volunteer co-maintainer needed for Docker-Coq:
The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.
Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.
Maintainer core tasks:
- 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.
Coq Github Bot (Jan 17 2023 at 16:21):palmskog edited issue #144 Volunteer co-maintainer needed for Docker-Coq:
The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.
Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.
Desirable skills:
- 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.
Coq Github Bot (Jan 24 2023 at 21:02):erikmd closed issue #144 Volunteer co-maintainer needed for Docker-Coq:
The Coq Team and Coq-community are looking for a volunteer co-maintainer of the Docker-Coq project, which provides Docker container images of many versions of Coq as a service to Coq users.
Docker-Coq is an open source project on GitHub under the BSD-3-Clause license. It maintains definitions of a set of Docker images that provide a basic Coq environment for continuous integration and local use. Thanks to the docker-keeper software, images built from Docker-Coq definitions are continuously deployed to the public Docker registry, where users can pull them without worry of rate limitations.
Desirable skills:
- 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.
Coq Github Bot (Jun 02 2023 at 12:28):palmskog labeled issue #145 Proposal to move CoqIDE to Coq-community:
Project name: CoqIDE
Initial author(s): The Coq development team, INRIA, CNRS, and contributors
Current URL: https://github.com/coq/coq
Kind: Integrated Development Environment (IDE) for Coq
License: LGPL-2.1-only
Description: CoqIDE is an IDE implemented using the OCaml programming language and the GTK3 widget toolkit for graphical user interfaces (GUIs), thanks to the lablgtk3 OCaml package. CoqIDE uses a legacy XML-based protocol to communicate with Coq and is licensed under the open source LGPL-2.1 license.
Status: CoqIDE's source code is currently part of Coq's GitHub repository. Due to a desire to shift IDE-related work toward LSP and VS Code support, the Coq core team no longer considers CoqIDE maintenance and evolution a priority. With this proposal issue, the team wants to give an opportunity to the Coq community to take over CoqIDE maintenance and lead its future evolution.
More details about the context and the plans for the future of IDEs for Coq can be found in Coq CEP 68 leading to this proposal issue.
New maintainer: looking for volunteers
To volunteer, please respond to this GitHub issue with a brief motivation and summary of relevant experience for becoming a CoqIDE maintainer. As part of their reply to this issue, volunteers are encouraged to briefly present their short-term and long-term plans for CoqIDE and how long they think they will remain active on CoqIDE maintenance. However, this won't be considered as a commitment, as plans and priorities can evolve based on the context and personal circumstances. The maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community organization owners. Responders not selected will still be encouraged to contribute to CoqIDE in collaboration with the new maintainer(s) and other contributors.
Anyone else planning to get involved as an active and regular contributor to the CoqIDE project is also welcome to make themselves known in this GitHub issue and to briefly present which improvements and changes they plan to propose.
Coq Github Bot (Jun 02 2023 at 12:28):palmskog opened issue #145 Proposal to move CoqIDE to Coq-community:
Project name: CoqIDE
Initial author(s): The Coq development team, INRIA, CNRS, and contributors
Current URL: https://github.com/coq/coq
Kind: Integrated Development Environment (IDE) for Coq
License: LGPL-2.1-only
Description: CoqIDE is an IDE implemented using the OCaml programming language and the GTK3 widget toolkit for graphical user interfaces (GUIs), thanks to the lablgtk3 OCaml package. CoqIDE uses a legacy XML-based protocol to communicate with Coq and is licensed under the open source LGPL-2.1 license.
Status: CoqIDE's source code is currently part of Coq's GitHub repository. Due to a desire to shift IDE-related work toward LSP and VS Code support, the Coq core team no longer considers CoqIDE maintenance and evolution a priority. With this proposal issue, the team wants to give an opportunity to the Coq community to take over CoqIDE maintenance and lead its future evolution.
More details about the context and the plans for the future of IDEs for Coq can be found in Coq CEP 68 leading to this proposal issue.
New maintainer: looking for volunteers
To volunteer, please respond to this GitHub issue with a brief motivation and summary of relevant experience for becoming a CoqIDE maintainer. As part of their reply to this issue, volunteers are encouraged to briefly present their short-term and long-term plans for CoqIDE and how long they think they will remain active on CoqIDE maintenance. However, this won't be considered as a commitment, as plans and priorities can evolve based on the context and personal circumstances. The maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community organization owners. Responders not selected will still be encouraged to contribute to CoqIDE in collaboration with the new maintainer(s) and other contributors.
Anyone else planning to get involved as an active and regular contributor to the CoqIDE project is also welcome to make themselves known in this GitHub issue and to briefly present which improvements and changes they plan to propose.
Coq Github Bot (Jun 02 2023 at 12:28):palmskog labeled issue #145 Proposal to move CoqIDE to Coq-community:
Project name: CoqIDE
Initial author(s): The Coq development team, INRIA, CNRS, and contributors
Current URL: https://github.com/coq/coq
Kind: Integrated Development Environment (IDE) for Coq
License: LGPL-2.1-only
Description: CoqIDE is an IDE implemented using the OCaml programming language and the GTK3 widget toolkit for graphical user interfaces (GUIs), thanks to the lablgtk3 OCaml package. CoqIDE uses a legacy XML-based protocol to communicate with Coq and is licensed under the open source LGPL-2.1 license.
Status: CoqIDE's source code is currently part of Coq's GitHub repository. Due to a desire to shift IDE-related work toward LSP and VS Code support, the Coq core team no longer considers CoqIDE maintenance and evolution a priority. With this proposal issue, the team wants to give an opportunity to the Coq community to take over CoqIDE maintenance and lead its future evolution.
More details about the context and the plans for the future of IDEs for Coq can be found in Coq CEP 68 leading to this proposal issue.
New maintainer: looking for volunteers
To volunteer, please respond to this GitHub issue with a brief motivation and summary of relevant experience for becoming a CoqIDE maintainer. As part of their reply to this issue, volunteers are encouraged to briefly present their short-term and long-term plans for CoqIDE and how long they think they will remain active on CoqIDE maintenance. However, this won't be considered as a commitment, as plans and priorities can evolve based on the context and personal circumstances. The maintainer(s) will be selected from the issue responders by the Coq core team and Coq-community organization owners. Responders not selected will still be encouraged to contribute to CoqIDE in collaboration with the new maintainer(s) and other contributors.
Anyone else planning to get involved as an active and regular contributor to the CoqIDE project is also welcome to make themselves known in this GitHub issue and to briefly present which improvements and changes they plan to propose.
Last updated: Jun 03 2023 at 15:31 UTC
