From 64cf675e1d1f5517b9289d2955bd26efb3dca50e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 15:28:04 +0900 Subject: [PATCH 1/4] compact with mathcomp-analysis 1.7.0 --- .github/workflows/docker-action.yml | 2 ++ README.md | 1 + coq-infotheo.opam | 3 ++- information_theory/kraft.v | 2 +- meta.yml | 11 ++++++++++- 5 files changed, 16 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 90e3c33a..27da9be5 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,6 +19,8 @@ jobs: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.2.0-coq-8.20' + - 'mathcomp/mathcomp:2.3.0-coq-8.19' + - 'mathcomp/mathcomp:2.3.0-coq-8.20' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 9cfc7bdb..32c37515 100644 --- a/README.md +++ b/README.md @@ -40,6 +40,7 @@ information theory, and linear error-correcting codes. - [MathComp solvable](https://math-comp.github.io) - [MathComp field](https://math-comp.github.io) - [MathComp analysis](https://github.com/math-comp/analysis) + - [MathComp analysis reals standard library](https://github.com/math-comp/analysis) - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - MathComp algebra tactics - A Coq tactic for proving bounds diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 6d20793e..20b3c972 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -27,7 +27,8 @@ depends: [ "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-analysis" { (>= "1.5.0") } + "coq-mathcomp-analysis" { (>= "1.7.0") } + "coq-mathcomp-reals-stdlib" { (>= "1.7.0) } "coq-hierarchy-builder" { >= "1.5.0" } "coq-mathcomp-algebra-tactics" { >= "1.2.0" } "coq-interval" { >= "4.10.0"} diff --git a/information_theory/kraft.v b/information_theory/kraft.v index 4895cd4b..cb2ba05e 100644 --- a/information_theory/kraft.v +++ b/information_theory/kraft.v @@ -1,6 +1,6 @@ (* infotheo: information theory and error-correcting codes in Coq *) (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect path ssralg ssrnum. +From mathcomp Require Import all_ssreflect ssralg ssrnum. Require FunctionalExtensionality. Require Import ssr_ext. diff --git a/meta.yml b/meta.yml index ac8b8431..8bed4c9b 100644 --- a/meta.yml +++ b/meta.yml @@ -51,6 +51,10 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.20' repo: 'mathcomp/mathcomp' +- version: '2.3.0-coq-8.19' + repo: 'mathcomp/mathcomp' +- version: '2.3.0-coq-8.20' + repo: 'mathcomp/mathcomp' dependencies: - opam: @@ -80,9 +84,14 @@ dependencies: [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "1.5.0") }' + version: '{ (>= "1.7.0") }' description: |- [MathComp analysis](https://github.com/math-comp/analysis) +- opam: + name: coq-mathcomp-reals-stdlib + version: '{ (>= "1.7.0) }' + description: |- + [MathComp analysis reals standard library](https://github.com/math-comp/analysis) - opam: name: coq-hierarchy-builder version: '{ >= "1.5.0" }' From aabf95308637a7400ea31c72bcf88f0bd78eba5d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 15:56:40 +0900 Subject: [PATCH 2/4] wip --- .github/workflows/docker-action.yml | 2 -- meta.yml | 4 ---- 2 files changed, 6 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 27da9be5..90e3c33a 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,8 +19,6 @@ jobs: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.2.0-coq-8.20' - - 'mathcomp/mathcomp:2.3.0-coq-8.19' - - 'mathcomp/mathcomp:2.3.0-coq-8.20' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/meta.yml b/meta.yml index 8bed4c9b..12f67a1a 100644 --- a/meta.yml +++ b/meta.yml @@ -51,10 +51,6 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.20' repo: 'mathcomp/mathcomp' -- version: '2.3.0-coq-8.19' - repo: 'mathcomp/mathcomp' -- version: '2.3.0-coq-8.20' - repo: 'mathcomp/mathcomp' dependencies: - opam: From 5db9f90b119f0a3ea0d48f2dcfab00242fbe70af Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 16:04:23 +0900 Subject: [PATCH 3/4] fix --- changelog.txt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/changelog.txt b/changelog.txt index 81eff2e2..b53a6b45 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,3 +1,9 @@ +------------------- +from 0.7.4 to 0.7.5 +------------------- + +- compatibility with MathComp-Analysis 1.7.0 only + ------------------- from 0.7.3 to 0.7.4 ------------------- From 9ae9558d2f14cc53fd4fc8cf71b0744350d19dc3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 16:26:49 +0900 Subject: [PATCH 4/4] wip --- coq-infotheo.opam | 2 +- meta.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 20b3c972..a067e5fd 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -28,7 +28,7 @@ depends: [ "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-analysis" { (>= "1.7.0") } - "coq-mathcomp-reals-stdlib" { (>= "1.7.0) } + "coq-mathcomp-reals-stdlib" { (>= "1.7.0") } "coq-hierarchy-builder" { >= "1.5.0" } "coq-mathcomp-algebra-tactics" { >= "1.2.0" } "coq-interval" { >= "4.10.0"} diff --git a/meta.yml b/meta.yml index 12f67a1a..64b84ffd 100644 --- a/meta.yml +++ b/meta.yml @@ -85,7 +85,7 @@ dependencies: [MathComp analysis](https://github.com/math-comp/analysis) - opam: name: coq-mathcomp-reals-stdlib - version: '{ (>= "1.7.0) }' + version: '{ (>= "1.7.0") }' description: |- [MathComp analysis reals standard library](https://github.com/math-comp/analysis) - opam: