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

Test with Alectryon 1.4 and Coq 8.14.

Author: Zimmi48

.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.