From b51ff9c120d82ae48679058691eff32b1fdf3e87 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 29 Mar 2022 10:04:50 -0700
Subject: [PATCH] Update to work with Coq 8.10-8.15

---
 .github/workflows/coq-ci.yml   | 28 +++++++++++++
 coq-haskell.opam               | 26 ++++++++++++
 default.nix                    | 76 +++++++++++++++-------------------
 shell.nix                      |  2 +
 src/Control/Category.v         |  7 ++++
 src/Control/Impl.v             |  6 +--
 src/Control/Lens.v             |  6 +--
 src/Control/Monad/Indexed.v    |  2 +-
 src/Control/Monad/Trans/Free.v |  4 +-
 src/Crush.v                    |  6 +--
 src/Ltac.v                     |  4 +-
 src/Prelude.v                  | 14 +++----
 12 files changed, 117 insertions(+), 64 deletions(-)
 create mode 100644 .github/workflows/coq-ci.yml
 create mode 100644 coq-haskell.opam
 create mode 100644 shell.nix

diff --git a/.github/workflows/coq-ci.yml b/.github/workflows/coq-ci.yml
new file mode 100644
index 0000000..77e4b4a
--- /dev/null
+++ b/.github/workflows/coq-ci.yml
@@ -0,0 +1,28 @@
+name: CI
+
+on: [push, pull_request]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.15'
+          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.10'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-haskell.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/coq-haskell.opam b/coq-haskell.opam
new file mode 100644
index 0000000..c7ea92e
--- /dev/null
+++ b/coq-haskell.opam
@@ -0,0 +1,26 @@
+opam-version: "2.0"
+maintainer: "johnw@newartisans.com"
+version: "dev"
+
+homepage: "https://github.com/jwiegley/coq-haskell"
+dev-repo: "git+https://github.com/jwiegley/coq-haskell.git"
+bug-reports: "https://github.com/jwiegley/coq-haskell/issues"
+license: "BSD-3-Clause"
+
+synopsis: "A library to provide Haskell-familiar constructions in Coq"
+description: """
+An axiom-free formalization of category theory in Coq for personal study and
+practical work.
+"""
+
+build: [make "JOBS=%{jobs}%" ]
+install: [make "install"]
+depends: [
+  "coq" {(>= "8.10" & < "8.16~") | (= "dev")}
+]
+
+tags: [
+]
+authors: [
+  "John Wiegley"
+]
diff --git a/default.nix b/default.nix
index 3bd7ad9..5dd6701 100644
--- a/default.nix
+++ b/default.nix
@@ -1,55 +1,45 @@
-{ packages ? "coqPackages_8_10"
-
-, rev      ? "8da81465c19fca393a3b17004c743e4d82a98e4f"
-, sha256   ? "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"
-
-, pkgs     ? import (builtins.fetchTarball {
+args@{
+  rev    ? "9222ae36b208d1c6b55d88e10aa68f969b5b5244"
+, sha256 ? "0dvl990alr4bb64w9b32dhzacvchpsspj8p3zqcgk7q5akvqh1mw"
+, pkgs   ? import (builtins.fetchTarball {
     url = "https://github.com/NixOS/nixpkgs/archive/${rev}.tar.gz";
     inherit sha256; }) {
     config.allowUnfree = true;
     config.allowBroken = false;
-    overlays = [
-      (self: super:
-       let
-         nixpkgs = { rev, sha256 }:
-           import (super.fetchFromGitHub {
-             owner = "NixOS";
-             repo  = "nixpkgs";
-             inherit rev sha256;
-           }) { config.allowUnfree = true; };
-
-         known-good-20191113_070954 = nixpkgs {
-           rev    = "620124b130c9e678b9fe9dd4a98750968b1f749a";
-           sha256 = "0xgy2rn2pxii3axa0d9y4s25lsq7d9ykq30gvg2nzgmdkmy375rr";
-         };
-       in
-       {
-         inherit (known-good-20191113_070954) shared-mime-info;
-       })
-    ];
   }
 }:
 
-with pkgs.${packages};
+let coq-haskell = coqPackages:
+  with pkgs.${coqPackages}; pkgs.stdenv.mkDerivation rec {
+    name = "coq${coq.coq-version}-coq-haskell-${version}";
+    version = "1.0";
 
-pkgs.stdenv.mkDerivation rec {
-  name = "coq${coq.coq-version}-haskell-${version}";
-  version = "1.0";
+    src = if pkgs ? coqFilterSource
+          then pkgs.coqFilterSource [] ./.
+          else ./.;
 
-  src =
-    if pkgs ? coqFilterSource
-    then pkgs.coqFilterSource [] ./.
-    else ./.;
-
-  buildInputs = [ coq coq.ocaml coq.camlp5 coq.findlib equations ];
-  enableParallelBuilding = true;
+    buildInputs = [
+      coq coq.ocaml coq.camlp5 coq.findlib
+    ];
+    enableParallelBuilding = true;
 
-  buildPhase = "make -j$NIX_BUILD_CORES";
-  preBuild = "coq_makefile -f _CoqProject -o Makefile";
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+    buildFlags = [
+      "JOBS=$(NIX_BUILD_CORES)"
+    ];
 
-  env = pkgs.buildEnv { name = name; paths = buildInputs; };
-  passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" ];
- };
+    installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+    env = pkgs.buildEnv { inherit name; paths = buildInputs; };
+    passthru = {
+      compatibleCoqVersions = v: builtins.elem v [ "8.10" "8.11" "8.12" "8.13" "8.14" "8.15" ];
+    };
+  };
+
+in {
+  coq-haskell_8_10 = coq-haskell "coqPackages_8_10";
+  coq-haskell_8_11 = coq-haskell "coqPackages_8_11";
+  coq-haskell_8_12 = coq-haskell "coqPackages_8_12";
+  coq-haskell_8_13 = coq-haskell "coqPackages_8_13";
+  coq-haskell_8_14 = coq-haskell "coqPackages_8_14";
+  coq-haskell_8_15 = coq-haskell "coqPackages_8_15";
 }
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 0000000..2015ac1
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,2 @@
+{ version ? "coq-haskell_8_15" }:
+(import ./default.nix {}).${version}
diff --git a/src/Control/Category.v b/src/Control/Category.v
index 07e4869..cdaada5 100644
--- a/src/Control/Category.v
+++ b/src/Control/Category.v
@@ -1,3 +1,10 @@
+Set Warnings "-notation-overridden".
+
+Generalizable All Variables.
+Set Primitive Projections.
+Set Universe Polymorphism.
+Set Transparent Obligations.
+
 (* Copyright (c) 2014, John Wiegley
  *
  * This work is licensed under a
diff --git a/src/Control/Impl.v b/src/Control/Impl.v
index e585c46..950585e 100644
--- a/src/Control/Impl.v
+++ b/src/Control/Impl.v
@@ -21,7 +21,7 @@ Instance Impl_Monad {A} : Monad (fun B => A -> B) := {
   join := fun A run => fun xs => run xs xs
 }.
 
-Program Instance Impl_Monad_Distributes `{Monad N} :
+Program Instance Impl_Monad_Distributes {A} `{Monad N} :
   @Monad_Distributes (fun B => A -> B) Impl_Monad N is_applicative.
 Obligation 1.
   exact (X >>= fun f => f X0).
@@ -33,11 +33,11 @@ Import MonadLaws.
 
 Program Instance Impl_FunctorLaws {A} : FunctorLaws (fun B => A -> B).
 Program Instance Impl_ApplicativeLaws {A} : ApplicativeLaws (fun B => A -> B).
-Program Instance Impl_MonadLaws : MonadLaws (fun B => A -> B).
+Program Instance Impl_MonadLaws {A} : MonadLaws (fun B => A -> B).
 
 Require Import FunctionalExtensionality.
 
-Program Instance Impl_Monad_DistributesLaws `{MonadLaws N} :
+Program Instance Impl_Monad_DistributesLaws {A} `{MonadLaws N} :
   @Monad_DistributesLaws (fun B => A -> B) N _ Impl_Monad is_applicative
                          Impl_Monad_Distributes.
 Obligation 1.
diff --git a/src/Control/Lens.v b/src/Control/Lens.v
index 763f6de..2d151da 100644
--- a/src/Control/Lens.v
+++ b/src/Control/Lens.v
@@ -76,8 +76,8 @@ Class LensLaws `(l : Lens' s a) := {
   lens_set_set  : forall (x : s) (y z : a), set l z (set l y x) = set l z x
 }.
 
-Program Instance Lens__1 : LensLaws (s:=a * b) _1.
-Program Instance Lens__2 : LensLaws (s:=a * b) _2.
+Program Instance Lens__1 {a b} : LensLaws (s:=a * b) _1.
+Program Instance Lens__2 {a b} : LensLaws (s:=a * b) _2.
 
 Example lens_ex1 : view _1 (10, 20) = 10.
 Proof. reflexivity. Qed.
@@ -97,4 +97,4 @@ Proof. reflexivity. Qed.
 Example lens_ex6 : ((10, 20) &+ _1 %~ plus 1) = (11, 20).
 Proof. reflexivity. Qed.
 
-End LensLaws.
\ No newline at end of file
+End LensLaws.
diff --git a/src/Control/Monad/Indexed.v b/src/Control/Monad/Indexed.v
index 59754a6..6722a4c 100644
--- a/src/Control/Monad/Indexed.v
+++ b/src/Control/Monad/Indexed.v
@@ -20,7 +20,7 @@ Class IFunctor (F : Type -> Type -> Type -> Type) :=
 }.
 
 Arguments imap             [F] [IFunctor] [I O X] [Y] f g.
-Arguments ifun_identity    [F] [IFunctor] [I O X].
+Arguments ifun_identity    {F} {IFunctor} {I O X}.
 Arguments ifun_composition [F] [IFunctor] [I O X] [Y] [Z] f g.
 
 Notation "f <$$> g" := (imap f g) (at level 28, left associativity).
diff --git a/src/Control/Monad/Trans/Free.v b/src/Control/Monad/Trans/Free.v
index 8c28fcb..b1c4c3f 100644
--- a/src/Control/Monad/Trans/Free.v
+++ b/src/Control/Monad/Trans/Free.v
@@ -104,8 +104,8 @@ Module FreeTLaws.
 Include MonadLaws.
 
 (* It's not always this easy. *)
-Program Instance FreeT_FunctorLaws     : FunctorLaws (FreeT f m).
-Program Instance FreeT_ApplicativeLaws : ApplicativeLaws (FreeT f m).
+Program Instance FreeT_FunctorLaws     {f m} : FunctorLaws (FreeT f m).
+Program Instance FreeT_ApplicativeLaws {f m} : ApplicativeLaws (FreeT f m).
 (* Program Instance FreeT_MonadLaws       : MonadLaws (FreeT f m). *)
 
 End FreeTLaws.
diff --git a/src/Crush.v b/src/Crush.v
index b7ea782..563be67 100644
--- a/src/Crush.v
+++ b/src/Crush.v
@@ -9,7 +9,7 @@
 
 Require Import Coq.Logic.Eqdep Coq.Lists.List.
 
-Require Import Omega.
+Require Import Coq.micromega.Lia.
 
 Set Implicit Arguments.
 Generalizable All Variables.
@@ -198,8 +198,8 @@ Ltac crush' lemmas invOne :=
           repeat (simplHyp invOne; intuition)); un_done
       end;
       sintuition; rewriter; sintuition;
-      (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
-      try omega; try (elimtype False; omega)).
+      (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *)
+      try lia; try (elimtype False; lia)).
 
 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
 Ltac crush := crush' false fail.
diff --git a/src/Ltac.v b/src/Ltac.v
index c58ded0..6b5f117 100644
--- a/src/Ltac.v
+++ b/src/Ltac.v
@@ -1,4 +1,4 @@
-Require Import Omega.
+Require Import Coq.micromega.Lia.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -13,7 +13,7 @@ Tactic Notation "invert" "as" simple_intropattern(pat) :=
   intros top; inversion top as pat; clear top.
 
 Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p.
-Proof. intros. omega. Qed.
+Proof. intros. lia. Qed.
 
 Definition comp {a b c} (f : b -> c) (g : a -> b) (x : a) : c := f (g x).
 Arguments comp {a b c} f g x /.
diff --git a/src/Prelude.v b/src/Prelude.v
index 0b169af..51ce974 100644
--- a/src/Prelude.v
+++ b/src/Prelude.v
@@ -3,7 +3,7 @@ Require Export Hask.Data.Either.
 Require Export Hask.Data.Maybe.
 Require Export Hask.Data.Tuple.
 Require Export Hask.Data.Functor.
-Require Export Omega.
+Require Export Coq.micromega.Lia.
 Require Import Coq.Classes.Equivalence.
 
 Generalizable All Variables.
@@ -102,16 +102,16 @@ Definition distance (n m : nat) : nat := if n < m then m - n else n - m.
 *)
 
 Lemma ltn_plus : forall m n, 0 < n -> m < m + n.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.
 
 Lemma leq_plus : forall m n, m <= m + n.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.
 
 Lemma leq_add2r : forall p m n : nat, m <= n -> m + p <= n + p.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.
 
 Lemma leq_add2l : forall p m n : nat, m <= n -> p + m <= p + n.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.
 
 (*
 Lemma leq_eqF : forall n m, (n == m) = false -> n <= m -> n < m.
@@ -131,7 +131,7 @@ Qed.
 *)
 
 Lemma ltn0ltn : forall n m, n < m -> 0 < m.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.
 
 Lemma ltn_subn : forall n m, n < m -> m > 0 -> n <= m - 1.
-Proof. intros; omega. Qed.
+Proof. intros; lia. Qed.