Skip to content

Releases: coq-community/fourcolor

v1.3.1

26 Oct 13:45
@proux01 proux01
v1.3.1
43719c0
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.3.1 Latest
Latest

This release is compatible with math-comp 2.0.0 and 2.1.0 on Coq 8.16 to 8.18

Assets 2

v1.3.0

26 May 07:30
@proux01 proux01
v1.3.0
3e39e52
Compare
Choose a tag to compare
v1.3.0

This release is compatible with math-comp 2.0.0 and Coq 8.16 to 8.17

Assets 2

v1.2.5

13 Jul 12:59
@CohenCyril CohenCyril
v1.2.5
851949d
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.2.5

This release is compatible with math-comp 1.12 to 1.15 and Coq 8.11 to 8.16

Assets 2

v1.2.4

26 Jan 14:13
@CohenCyril CohenCyril
v1.2.4
4769864
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.2.4

This release is compatible with math-comp 1.11 to 1.14

Assets 2

v1.2.3

16 Dec 15:13
@ybertot ybertot
v1.2.3
a72978a
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.2.3

This release is compatible with math-comp1.12

Assets 2

v1.2.2

23 Jun 10:54
@ybertot ybertot
v1.2.2
2d5a4ed
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.2.2

This release is compatible with math-comp 1.11

Assets 2

v1.2.1

27 Feb 15:02
@ybertot ybertot
v1.2.1
4f99351
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
v1.2.1

This release is compatible with math-comp 1.10.0

Assets 2

MathComp baseline

25 Apr 13:01
@ggonthier ggonthier
v1.2
ae4a210
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.
Compare
Choose a tag to compare
MathComp baseline

This is the first release of the Four Colour Theorem proof that is rebased on the SSReflect plugin and the MathComp library. The release number accounts for two much older releases:

  • v1.0 for the initial 2005 release of the Coq v7.3 proof, which implemented the precursor to SSReflect using extensible grammars.
  • v1.1 for the 2006 baseline release for the Mathematical Components project, which included the first native SSReflect implementation for Coq v8.0 and a few core files of the future MathComp library.
    While there were no public releases of the proof since, it had been regularly updated to track the evolution of Coq and SSReflect. This release takes advantage of the improvements in both the SSReflect proof language and the MathComp library, updates the proof style to the modern standards that have evolved from the MathComp development, and also substantially extends the internal documentation of the proof.
Assets 2