Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

compatibility with Coq 8.20 #131

Merged
merged 3 commits into from
Oct 24, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix
affeldt-aist committed Oct 24, 2024
commit 0aea37ed30d676ffc57008be73a12fb5abd47211
1 change: 0 additions & 1 deletion .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
@@ -17,7 +17,6 @@ jobs:
strategy:
matrix:
image:
- 'mathcomp/mathcomp:2.2.0-coq-8.18'
- 'mathcomp/mathcomp:2.2.0-coq-8.19'
- 'mathcomp/mathcomp:2.2.0-coq-8.20'
fail-fast: false
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -32,7 +32,7 @@ information theory, and linear error-correcting codes.
- Naruomi Obata, Titech (M2)
- Alessandro Bruni, IT-University of Copenhagen
- License: [LGPL-2.1-or-later](LICENSE)
- Compatible Coq versions: Coq 8.18--8.20
- Compatible Coq versions: Coq 8.19--8.20
- Additional dependencies:
- [MathComp ssreflect](https://math-comp.github.io)
- [MathComp fingroup](https://math-comp.github.io)
4 changes: 2 additions & 2 deletions coq-infotheo.opam
Original file line number Diff line number Diff line change
@@ -21,13 +21,13 @@ build: [
]
install: [make "install"]
depends: [
"coq" { (>= "8.18" & < "8.21~") | (= "dev") }
"coq" { (>= "8.19" & < "8.21~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
"coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
"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.2.0") }
"coq-mathcomp-analysis" { (>= "1.5.0") }
"coq-hierarchy-builder" { >= "1.5.0" }
"coq-mathcomp-algebra-tactics" { >= "1.2.0" }
"coq-interval" { >= "4.10.0"}
8 changes: 3 additions & 5 deletions meta.yml
Original file line number Diff line number Diff line change
@@ -43,12 +43,10 @@ license:
nix: true

supported_coq_versions:
text: Coq 8.18--8.20
opam: '{ (>= "8.18" & < "8.21~") | (= "dev") }'
text: Coq 8.19--8.20
opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'

tested_coq_opam_versions:
- version: '2.2.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
@@ -82,7 +80,7 @@ dependencies:
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-analysis
version: '{ (>= "1.2.0") }'
version: '{ (>= "1.5.0") }'
description: |-
[MathComp analysis](https://github.com/math-comp/analysis)
- opam:
2 changes: 1 addition & 1 deletion robust/weightedmean.v
Original file line number Diff line number Diff line change
@@ -407,7 +407,7 @@ by move=> *; exact/sq_dev_ge0.
Qed.

Lemma sq_dev_max_ge0 : 0 <= sq_dev_max.
Proof. by rewrite /sq_dev_max; apply/topology.bigmax_geP; left. Qed.
Proof. by rewrite /sq_dev_max; apply/boolp.bigmax_geP; left. Qed.

Lemma sq_dev_max_ge u : C u != 0 -> sq_dev u <= sq_dev_max.
Proof. by move=> Cu0; rewrite /sq_dev_max; apply/le_bigmax_cond. Qed.

Unchanged files with check annotations Beta

(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum.

Check warning on line 4 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

Check warning on line 4 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "\pi ( _ )" defined at level 2 and "\pi"
Require Import Reals.
From mathcomp Require Import lra.
From mathcomp Require Import Rstruct.
(* *)
(******************************************************************************)
Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").

Check warning on line 63 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Postfix notations (i.e. starting with a nonterminal symbol and
Reserved Notation "'min(' x ',' y ')'" (format "'min(' x ',' y ')'").
Reserved Notation "'max(' x ',' y ')'" (format "'max(' x ',' y ')'").
Proof. by rewrite -{1}(addR0 x) ltR_add2l. Qed.
Lemma subR_gt0 x y : (0 < y - x) <-> (x < y).
Proof. by split; [exact: Rminus_gt_0_lt | exact: Rlt_Rminus]. Qed.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rminus_gt_0_lt is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rlt_Rminus is deprecated since 8.19.

Check warning on line 492 in lib/ssrR.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notation Rminus_gt_0_lt is deprecated since 8.19.
Lemma subR_lt0 x y : (y - x < 0) <-> (y < x).
Proof. by split; [exact: Rminus_lt | exact: Rlt_minus]. Qed.
Lemma subR_ge0 x y : (0 <= y - x) <-> (x <= y).
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg ssrnum.

Check warning on line 4 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments

Check warning on line 4 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "\pi ( _ )" defined at level 2 and "\pi"
From mathcomp Require Import reals normedtype.

Check warning on line 5 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Notations "{ ' _ | _ }" defined at level 0
From mathcomp Require Import mathcomp_extra boolp.
From mathcomp Require Import lra ring Rstruct.
End dominance.
Notation "P '`<<' Q" := (dominates Q P) : reals_ext_scope.

Check warning on line 121 in lib/realType_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Declaring a scope implicitly is deprecated; use in advance an
Notation "P '`<<b' Q" := (dominatesb Q P) : reals_ext_scope.
(* ---- Prob ---- *)
Proof.
have [/RleP ? /RleP ?] : (0 <= / IZR (Zpos p) <= 1)%coqR.
split; first exact/Rlt_le/Rinv_0_lt_compat/IZR_lt/Pos2Z.is_pos.
rewrite -[X in (_ <= X)%coqR]Rinv_1; apply Rle_Rinv => //.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.

Check warning on line 302 in lib/Reals_ext.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Rle_Rinv is deprecated since 8.19. Use Rinv_le_contravar.
- exact/IZR_lt/Pos2Z.is_pos.
- exact/IZR_le/Pos2Z.pos_le_pos/Pos.le_1_l.
exact/andP.
Section trivIset.
Import boolp classical_sets.
From mathcomp Require Import measure probability.

Check warning on line 964 in probability/fsdist.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Use of “Require” inside a section is fragile. It is not recommended
Local Open Scope classical_set_scope.
Context [T : Type] [I : eqType].
Variables (D : set I) (F : I -> set T)
Variable n : nat.
Variable types : 'I_n -> eqType.
Definition univ_types : eqType :=
[eqType of {dffun forall i, types i}].

Check warning on line 111 in probability/bayes.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation "[ eqType of _ ]" is deprecated since mathcomp 2.0.0.
Section prod_types.
(* sets of indices *)
Variable I : {set 'I_n}.
Definition prod_types :=
[eqType of

Check warning on line 118 in probability/bayes.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation "[ eqType of _ ]" is deprecated since mathcomp 2.0.0.
{dffun forall i : 'I_n, if i \in I then types i else unit}].
Lemma prod_types_app i (A B : prod_types) : A = B -> A i = B i.
(* TODO: we should maybe extend mczify's ssrZ... *)
Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").

Check warning on line 15 in lib/ssrZ.v

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20)

Postfix notations (i.e. starting with a nonterminal symbol and
Declare Scope zarith_ext_scope.