Merge pull request #97 from coq-community/test-alectryon-1.4

Test with Alectryon 1.4 and Coq 8.14.

.nix/config.nix

@@ -41,7 +41,7 @@
 
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
-    coqPackages.coq.override.version = "8.13";
+    coqPackages.coq.override.version = "8.14";
 
     ## In some cases, light overrides are not available/enough
     ## in which case you can use either

.nix/nixpkgs.nix

@@ -1,4 +1,4 @@
 fetchTarball {
-         url = https://github.com/Zimmi48/nixpkgs/archive/451f727a09e43ba16021448a20e5ef8b20e8c421.tar.gz;
-         sha256 = "18h92bb4sijih1klivjg75r19wci6gbgasnc0d8mpq57yj7ma8ys";
+         url = https://github.com/Zimmi48/nixpkgs/archive/0300b6ef8480620bfa2d668cf19314df11507ab1.tar.gz;
+         sha256 = "12hw8sc4krqfxpc5pdb78ccnl824maxhl967yyvn5mql0mncd359";
        }

README.md

@@ -75,7 +75,7 @@ This contribution contains two parts:
   `nix-shell --argstr job hydra-battles` or `nix-shell --argstr job
   addition-chains`.
 
-- Building the PDF documentation also requires Alectryon 1.2 and SerAPI.
+- Building the PDF documentation also requires Alectryon 1.4 and SerAPI.
   See [`doc/movies/Readme.md`](doc/movies/Readme.md) for details.
 
 - The general Makefile is in the top directory:

_CoqProject

@@ -5,8 +5,9 @@
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
--arg -w -arg -deprecated-instance-without-locality
 -arg -w -arg -deprecated-hint-rewrite-without-locality
+-arg -w -arg -unknown-option
+-arg -w -arg -deprecated-option
 
 theories/ordinals/OrdinalNotations/ON_Omega.v
 theories/ordinals/OrdinalNotations/ON_Generic.v

doc/movies/Readme.md

@@ -5,10 +5,11 @@ This script has been tested with Python 3.7 or above and uses [Alectryon](https:
 to transform "coq+rst" to "latex" file.
 
 ## Requirements
-The script has been tested with a recent version of Alectryon v1.3.1 (Aug 28th, 2021). You can download it from
-[Alectryon's site](https://github.com/cpitclaudel/alectryon).
 
-you may also run `pip install -r requirements.txt`
+This script requires Alectryon 1.4.
+
+To get it, you may run `pip install -r requirements.txt` or
+`nix-shell` (at the root of the project).
 
 
 

doc/movies/requirements.txt

@@ -1 +1 @@
-alectryon >=1.3.1
+alectryon >=1.4.0

meta.yml

@@ -36,7 +36,7 @@ build: |-
     `nix-shell --argstr job hydra-battles` or `nix-shell --argstr job
     addition-chains`.
 
-  - Building the PDF documentation also requires Alectryon 1.2 and SerAPI.
+  - Building the PDF documentation also requires Alectryon 1.4 and SerAPI.
     See [`doc/movies/Readme.md`](doc/movies/Readme.md) for details.
 
   - The general Makefile is in the top directory:

theories/additions/AM.v

@@ -195,15 +195,15 @@ end.
 
 
 
-Instance Stack_equiv_refl {A}`{M : @EMonoid A op one equ} :
+#[ global ] Instance Stack_equiv_refl {A}`{M : @EMonoid A op one equ} :
   Reflexive stack_equiv.
 Proof.
   red; intros. induction x.
   - now left.
   - right; [reflexivity | assumption].
 Qed.
 
-Instance Stack_equiv_equiv {A}`{M : @EMonoid A op one equ}:
+#[ global ] Instance Stack_equiv_equiv {A}`{M : @EMonoid A op one equ}:
   Equivalence stack_equiv.
 Proof.
  split.
@@ -227,7 +227,7 @@ Proof.
            eapply IHx;eauto.
 Qed.
 
-Instance result_equiv_equiv `{M : @EMonoid A op one equ}:
+#[ global ] Instance result_equiv_equiv `{M : @EMonoid A op one equ}:
   Equivalence result_equiv.
 Proof.
   split.
@@ -298,7 +298,7 @@ Proof.
 Qed.
 
 
-Instance exec_Proper `{M : @EMonoid A op one equ} :
+#[ global ] Instance exec_Proper `{M : @EMonoid A op one equ} :
   Proper (Logic.eq ==> equiv ==> stack_equiv ==> result_equiv) (@exec A op) .
 Proof.
  intros c c' Hx x x' Hequiv s s' Hs; subst.

theories/additions/BinaryStrat.v

@@ -19,12 +19,12 @@ Definition half (p:positive) :=
 
 Definition two (p:positive) := 2%positive.
 
-Instance Binary_strat : Strategy half.
+#[ global ] Instance Binary_strat : Strategy half.
 Proof.
   split; destruct p; unfold half; try lia.
 Qed.
 
-Instance Two_strat : Strategy two.
+#[ global ] Instance Two_strat : Strategy two.
 Proof.
   split;unfold two; lia.
 Qed.

theories/additions/Dichotomy.v

@@ -186,7 +186,7 @@ Qed.
 
 
 (* begin snippet DichoStrat:: no-out *)
-Instance Dicho_strat : Strategy dicho.
+#[ global ] Instance Dicho_strat : Strategy dicho.
 (* end snippet DichoStrat *)
 Proof.
   split.

theories/additions/Euclidean_Chains.v

@@ -192,11 +192,11 @@ Definition computation_equiv {A:Type} (op: Mult_op A)
    computation_execute op c == computation_execute op c'.
 
 
-Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A):
+#[ global ] Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A):
   Equiv (@computation A) :=
   @computation_equiv A op equiv.
 
-Instance comp_equiv_equivalence {A:Type} (op: Mult_op A)
+#[ global ] Instance comp_equiv_equivalence {A:Type} (op: Mult_op A)
            (equiv : Equiv A) : Equivalence  equiv ->
                                Equivalence (computation_equiv op equiv).   
 Proof.
@@ -219,7 +219,7 @@ Class Fkont_proper
 
 
 
-Instance Return_proper `(M : @EMonoid A op E_one E_equiv) :
+#[ global ] Instance Return_proper `(M : @EMonoid A op E_one E_equiv) :
   Fkont_proper M (@Return A).
 Proof.
  intros x y Hxy; assumption.
@@ -326,7 +326,7 @@ Class Fchain_proper (fc : Fchain) := Fchain_proper_bad_prf :
 (* end snippet Bad3 *)
 
 (* begin snippet Bad3b:: no-out *)
-Instance Fcompose_proper (f1 f2 : Fchain)
+#[ global ] Instance Fcompose_proper (f1 f2 : Fchain)
          (_ : Fchain_proper f1)
          (_ : Fchain_proper f2) :
   Fchain_proper (Fcompose f1 f2).
@@ -361,15 +361,15 @@ Class Fchain_proper (fc : Fchain) := Fchain_proper_prf :
 (* end snippet correctProper *)
 
 (* begin snippet F1proper:: no-out *)
-Instance F1_proper : Fchain_proper F1.
+#[ global ] Instance F1_proper : Fchain_proper F1.
 Proof.
   intros until M ; intros k k' Hk Hk' H a b H0; unfold F1; cbn;
   now apply H.  
 Qed.
 (* end snippet F1proper *)
 
 (* begin snippet F3proper:: no-out *)
-Instance F3_proper : Fchain_proper F3.
+#[ global ] Instance F3_proper : Fchain_proper F3.
 (* end snippet F3proper *)
 Proof.
   intros  A op one equiv M  k k' Hk Hk'  Hkk' x y Hxy;  
@@ -378,7 +378,7 @@ Proof.
 Qed.
 
 (* begin snippet F2proper:: no-out *)
-Instance F2_proper : Fchain_proper F2.
+#[ global ] Instance F2_proper : Fchain_proper F2.
 (* end snippet F2proper *)
 Proof.
   intros  A op one equiv M  k k' Hk Hk'  Hkk' x y Hxy;  
@@ -423,7 +423,7 @@ Proof.
 Qed.
 
 (* begin snippet FcomposeProper:: no-out *)
-Instance Fcompose_proper (fc1 fc2: Fchain)
+#[ global ] Instance Fcompose_proper (fc1 fc2: Fchain)
                          (_ : Fchain_proper fc1)
                          (_ : Fchain_proper fc2) :
   Fchain_proper (Fcompose fc1 fc2).
@@ -436,7 +436,7 @@ Proof.
 Qed.
 
 
-Instance Fexp2_nat_proper (n:nat) : 
+#[ global ] Instance Fexp2_nat_proper (n:nat) : 
                            Fchain_proper (Fexp2_of_nat n).
 Proof.
   induction n; cbn.
@@ -473,7 +473,7 @@ Proof.
 Qed.
 
 (* begin snippet Fexp2Proper:: no-out *)
-Instance  Fexp2_proper (p:positive) : Fchain_proper (Fexp2 p).
+#[ global ] Instance  Fexp2_proper (p:positive) : Fchain_proper (Fexp2 p).
 (* end snippet Fexp2Proper *)
 Proof.
   unfold  Fexp2; apply Fexp2_nat_proper.
@@ -631,7 +631,7 @@ Kchain_proper_prf :
 (* end snippet KchainCorrectDef *)
 
 (* begin snippet K73Ok:: no-out *)
-Instance k7_3_proper : Kchain_proper k7_3.
+#[ global ] Instance k7_3_proper : Kchain_proper k7_3.
 Proof.
   intros until M; intros; red; unfold k7_3; cbn;
   add_op_proper M H3; apply H1;  rewrite H2;   reflexivity. 
@@ -690,7 +690,7 @@ Proof.
 Qed.
 
 (* begin snippet K2FProper:: no-out *)
-Instance K2F_proper (kc : Kchain)(_ : Kchain_proper kc) :
+#[ global ] Instance K2F_proper (kc : Kchain)(_ : Kchain_proper kc) :
   Fchain_proper (K2F kc).
 (* end snippet K2FProper *)
 Proof.
@@ -981,7 +981,7 @@ Proof.
 Qed.
 
 (* begin snippet FFKProper:: no-out *)
-Instance FFK_proper 
+#[ global ] Instance FFK_proper 
          (fp fq : Fchain)
          (_ :   Fchain_proper fp)
          (_ :  Fchain_proper fq)
@@ -1030,7 +1030,7 @@ Proof.
     + generalize (power_eq3 a);simpl;now symmetry.
 Qed.
 
-Instance  FK_proper  (Fp : Fchain) (_ : Fchain_proper Fp):
+#[ global ] Instance  FK_proper  (Fp : Fchain) (_ : Fchain_proper Fp):
   Kchain_proper (FK Fp).
 Proof.
   unfold FK; intros until M; intros k k' x y  H0 H1 H2 H3. 

theories/additions/Fib2.v

@@ -53,7 +53,7 @@ Lemma neutral_r p : mul2 p (0,1)  = p.
 Qed.
 
 (* begin snippet mul2Monoid  *)
-Instance Mul2 : Monoid  mul2 (0,1).
+#[ global ] Instance Mul2 : Monoid  mul2 (0,1).
 (* end snippet mul2Monoid  *)
 
 Proof.

theories/additions/Monoid_def.v

@@ -52,7 +52,7 @@ End Demo.
 
 (* begin snippet DemoStringMult:: no-out *)
 
-Instance string_op : Mult_op string := append.
+#[ global ] Instance string_op : Mult_op string := append.
 Open Scope string_scope.
 
 Example ex_string : "ab" * "cde" = "abcde".
@@ -61,7 +61,7 @@ Proof. reflexivity. Qed.
 (* end snippet DemoStringMult *)
 
 
-Instance bool_and_binop : Mult_op bool := andb.
+#[ global ] Instance bool_and_binop : Mult_op bool := andb.
 
 Example ex_bool : true * false = false.
 Proof. reflexivity. Qed.
@@ -141,25 +141,25 @@ Class EMonoid (A:Type)(E_op : Mult_op A)(E_one : A)
 (* end snippet EMonoidDef *)
 
 
-Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Equivalence E_eq.
 destruct M;auto.
 Qed.
 
-Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Reflexive E_eq.
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
-Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Symmetric E_eq.
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
-Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Transitive E_eq.
 destruct (Equiv_Equiv   M);auto.

theories/additions/Monoid_instances.v

@@ -17,17 +17,17 @@ Open Scope Z_scope.
 (** *** Multiplicative monoid on [Z] *)
 
 (* begin snippet ZMultDef *)
-Instance Z_mult_op : Mult_op Z := Z.mul.
+#[ global ] Instance Z_mult_op : Mult_op Z := Z.mul.
 
-Instance ZMult : Monoid  Z_mult_op 1. (* .no-out *)
+#[ global ] Instance ZMult : Monoid  Z_mult_op 1. (* .no-out *)
 Proof. (* .no-out *)
   split.
     all: unfold Z_mult_op, mult_op;intros;ring.
 Qed.
 (* end snippet ZMultDef *)
 
 
-Instance ZMult_Abelian : Abelian_Monoid ZMult.
+#[ global ] Instance ZMult_Abelian : Abelian_Monoid ZMult.
 Proof.
   split; exact Zmult_comm.
 Qed.
@@ -37,9 +37,9 @@ Qed.
 
 (* begin snippet natMult:: no-out *)
 
-Instance nat_mult_op : Mult_op nat | 5 := Nat.mul.
+#[ global ] Instance nat_mult_op : Mult_op nat | 5 := Nat.mul.
 
-Instance  Natmult : Monoid nat_mult_op  1%nat | 5.
+#[ global ] Instance  Natmult : Monoid nat_mult_op  1%nat | 5.
 Proof.
    split;unfold nat_mult_op, mult_op; intros; ring.
 Qed.
@@ -53,9 +53,9 @@ equal to $n$. See Sect.%~\ref{chains-exponent}.
 *)
 
 (* begin snippet natPlus:: no-out *)
-Instance nat_plus_op : Mult_op nat | 12 := Nat.add.
+#[ global ] Instance nat_plus_op : Mult_op nat | 12 := Nat.add.
 
-Instance Natplus : Monoid nat_plus_op  0%nat | 12.
+#[ global ] Instance Natplus : Monoid nat_plus_op  0%nat | 12.
 Proof.
    split;unfold nat_plus_op, mult_op; intros; ring.
 Qed.
@@ -65,9 +65,9 @@ Qed.
 
 Open Scope N_scope.
 
-Instance N_mult_op  : Mult_op N | 5 := N.mul.
+#[ global ] Instance N_mult_op  : Mult_op N | 5 := N.mul.
 
-Instance NMult : Monoid N_mult_op 1 | 5.
+#[ global ] Instance NMult : Monoid N_mult_op 1 | 5.
 Proof.
   split;unfold N_mult_op, mult_op; intros; ring.
 Qed.
@@ -78,9 +78,9 @@ Check NMult : EMonoid  N.mul 1%N eq.
 (* end snippet CheckCoercion *)
 
 
-Instance N_plus_op  : Mult_op N | 12 := N.add.
+#[ global ] Instance N_plus_op  : Mult_op N | 12 := N.add.
 
-Instance NPlus : Monoid N_plus_op 0 | 12.
+#[ global ] Instance NPlus : Monoid N_plus_op 0 | 12.
 Proof.
   split;unfold N_plus_op, mult_op; intros; ring.
 Qed.
@@ -89,9 +89,9 @@ Qed.
 (** Multiplicative Monoid on [positive] 
 *)
 
-Instance P_mult_op : Mult_op positive | 5  := Pos.mul .
+#[ global ] Instance P_mult_op : Mult_op positive | 5  := Pos.mul .
 
-Instance PMult : Monoid P_mult_op xH | 5.
+#[ global ] Instance PMult : Monoid P_mult_op xH | 5.
 Proof.
  split;unfold P_mult_op, Mult_op;intros.  
  -  now rewrite Pos.mul_assoc.
@@ -114,9 +114,9 @@ The type [int31] is defined in Standard Library in Module
 *)
 
 (* begin snippet int31:: no-out *)
-Instance int31_mult_op : Mult_op int31 := mul31.
+#[ global ] Instance int31_mult_op : Mult_op int31 := mul31.
 
-Instance  Int31mult : Monoid int31_mult_op  1.
+#[ global ] Instance  Int31mult : Monoid int31_mult_op  1.
 Proof.
    split;unfold int31_mult_op, mult_op; intros; ring.
 Qed.