update to Coq 8.20

uds-psl · Feb 5, 2025 · b967df4 · b967df4
1 parent f2ff92e
commit b967df4
Show file tree

Hide file tree

Showing 10 changed files with 26 additions and 15 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -12,7 +12,7 @@ jobs:
     strategy:
       matrix:
         coq_version: 
-          - '8.18'
+          - '8.20'
         ocaml_version:
           - '4.14-flambda'
       fail-fast: true

diff --git a/opam b/opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "1.0+8.18"
+version: "1.0+8.20"
 maintainer: "[email protected]"
 homepage: "https://github.com/uds-psl/coq-library-fol/"
 dev-repo: "git+https://github.com/uds-psl/coq-library-fol/"
@@ -25,11 +25,11 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {>= "8.18" & < "8.19~"}
-  "coq-library-undecidability" {= "1.1.1+8.18"}
+  "coq" {>= "8.20" & < "9.0~"}
+  "coq-library-undecidability" {= "1.1.2+8.20"}
 ]
 synopsis: "A Coq Library for First-Order Logic"
 url {
-  git: "https://github.com/uds-psl/coq-library-fol.git#v1.0+8.18"
+  git: "https://github.com/uds-psl/coq-library-fol.git#v1.0+8.20"
 }
 
diff --git a/theories/Completeness/HeytingMacNeille.v b/theories/Completeness/HeytingMacNeille.v
@@ -7,8 +7,11 @@ Require Export Coq.Program.Basics.
 From FOL Require Import FullSyntax.
 From FOL Require Import Heyting.Heyting.
 
-
-Structure HeytingMorphism (HA1 HA2 : HeytingAlgebra) (F : HA1 -> HA2) : Type :=
+(* Morally this is in [Type]. But since all fields are in [Prop], putting this into
+   [Prop] is fine due to subsingleton elimination, and because it is not computationally
+   relevant anyways. *)
+(* Changing it back to [Type] makes Coq warn that this could just as well be in [Prop]. *)
+Structure HeytingMorphism (HA1 HA2 : HeytingAlgebra) (F : HA1 -> HA2) : Prop :=
   {
     F_inj : forall u v, F u = F v -> u = v ;
     F_mono : forall u v, u <= v -> F u <= F v ;

diff --git a/theories/Completeness/KripkeCompleteness.v b/theories/Completeness/KripkeCompleteness.v
@@ -239,7 +239,7 @@ Section KripkeCompleteness.
 
     Notation "A <<=C B" := (ctx_incl A B) (at level 20).
     Notation "A ⊢SC phi" := ((proj1_sig A) ⊢SE phi) (at level 20).
-    Notation "A ;; psi ⊢sC phi" := ((proj1_sig A) ;; psi ⊢sE phi) (at level 20).
+    Notation "A ;; psi ⊢sC phi" := ((proj1_sig A) ;; psi ⊢sE phi) (at level 70).
 
     Ltac dest_con_ctx :=
       match goal with

diff --git a/theories/Incompleteness/bin_qdec.v b/theories/Incompleteness/bin_qdec.v
@@ -10,6 +10,8 @@ Open Scope string_scope.
 
 Require Import Setoid.
 
+(* TODO FIXME the conflicting notation is not actually enabled (it is only Reserved), it should be refactored in coq-library-undecidability. *)
+#[warnings="notation-incompatible-prefix"]
 Require Import Undecidability.Shared.Libs.DLW.Vec.vec.
 
 Require Import String.

diff --git a/theories/Incompleteness/ctq.v b/theories/Incompleteness/ctq.v
@@ -7,7 +7,6 @@ From FOL.Proofmode Require Import Theories ProofMode.
 From FOL.Incompleteness Require Import Axiomatisations utils fol_utils qdec bin_qdec sigma1 epf epf_mu.
 
 Require Import Lia String List Cantor.
-Import ListNotations.
 
 (** ** Church's Thesis for Q *)
 Section ctq.

diff --git a/theories/Incompleteness/epf_mu.v b/theories/Incompleteness/epf_mu.v
@@ -12,8 +12,8 @@ Require Import Undecidability.Synthetic.EnumerabilityFacts.
 From Coq.Logic Require Import ConstructiveEpsilon.
 From FOL.Incompleteness Require Import utils epf fol_utils qdec sigma1.
 
-Import ListNotations.
-
+(* Coq's ListNotation clashes with notations from MuRec *)
+Local Notation "[ e ]" := (cons e nil) (at level 70).
 
 Derive Signature for Vector.t.
 
@@ -46,7 +46,7 @@ End recalg_enum.
 
 
 Lemma erase_ra_rel alg x y :
-  (exists k, evalfun k (erase alg) [x] = Some y) <-> 
+  (exists k, evalfun k (erase alg) ([x]) = Some y) <-> 
   ra_rel alg (Vector.cons _ x _ (Vector.nil _)) y.
 Proof.
   split.
@@ -63,7 +63,7 @@ Qed.
 Definition mu_step : recalg 1 -> nat -\ nat.
 Proof.
   intros c x. unshelve eexists.
-  { intros k. exact (evalfun k (erase c) [x]). }
+  { intros k. exact (evalfun k (erase c) ([x])). }
   unfold core_valid.
   intros y1 y2 k1 k2 H1 H2. unfold evalfun in *.
   eapply ra_rel_fun.

diff --git a/theories/Incompleteness/fol_incompleteness.v b/theories/Incompleteness/fol_incompleteness.v
@@ -9,7 +9,6 @@ From FOL.Incompleteness Require Import Axiomatisations utils fol_utils qdec bin_
 From FOL.Proofmode Require Import Theories ProofMode.
 
 Require Import Lia String List.
-Import ListNotations.
 
 (* * Incompleteness of first-order logic *)
 

diff --git a/theories/Proofmode/Hoas.v b/theories/Proofmode/Hoas.v
@@ -58,7 +58,7 @@ Notation "¬ A" := ((A → ⊥)%hoas) (at level 42) : hoas_scope.
 Notation "A '↔' B" := ((A → B)%hoas ∧ (B → A)%hoas) (at level 43) : hoas_scope.
 
 Definition convert `{funcs_signature, preds_signature, operators} f := (@conv _ _ _ 0 f).
-Arguments convert {_ _ _} f%hoas.
+Arguments convert {_ _ _} f%_hoas.
 
 Notation "<< f" := (ltac:(let y := eval cbn -[subst_form] in (convert f) in exact y)) (at level 200, only parsing).
 

diff --git a/theories/_CoqProject b/theories/_CoqProject
@@ -5,6 +5,14 @@ COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html
 
 -Q . FOL
 
+
+# Warning seems incorrect, see https://github.com/coq/coq/issues/19631
+# Disabled for now to reduce spam.
+-arg -w -arg -notation-incompatible-prefix
+# Disable warnings about vectors being hard to use. We know how to work with them.
+-arg -w -arg -warn-library-file-stdlib-vector
+
+
 FullSyntax.v
 FragmentSyntax.v
 Arithmetics.v