##########################################################
# Main derivation:                                       #
#   mathcomp-finmap mathcomp-analysis mathcomp-bigenough #
#   mathcomp-multinomials mathcomp-real-closed coqeal    #
# Additionally:                                          #
#   mathcomp-extra-all  contains all the extra packages  #
#   mathcomp-extra-fast contains the one not marked slow #
########################################################################
# This file mainly provides the above derivations, which are packages  #
# extra mathcomp libraries based on mathcomp.                          #
########################################################################

#####################################################
# Compiling customs versions using `mathcomp-extra` #
##############################################################################
# The prefered way to compile a custom version of mathcomp extra packages    #
# (other than released versions which should be added to                     #
# `rec-mathcomp-extra-config` and pushed to nixpkgs, see below),             #
# is to use `coqPackages.mathcomp-extra name version` where                  #
# 1. `name` is a string representing the name of a declared package          #
#    OR undeclared package.                                                  #
# 2. `version` is either:                                                    #
# - a string without slash, which is interpreted as a github revision,       #
#   i.e. either a tag, a branch or a commit hash                             #
# - a string with slashes "owner/p_1/.../p_n", which is interpreted as       #
#   github owner "owner" and revision "p_1/.../p_n".                         #
# - a path which is interpreted as a local source for the repository,        #
#   the name of the version is taken to be the basename of the path          #
#   i.e. if the path is /home/you/git/package/branch/,                       #
#        then "branch" is the name of the version                            #
# - an attribute set which overrides some attributes (e.g. the src)          #
#   if the version is updated, the name is automatically regenerated using   #
#   the conventional schema "coq${coq.coq-version}-${pkgname}-${version}"    #
# - a "standard" override function (old: new_attrs) to override the default  #
#   attribute set, so that you can use old.${field} to patch the derivation. #
#                                                                            #
# Should you choose to use `pkg.overrideAttrs` instead, we provide the       #
# function mathcomp-extra-override which takes a name and a version exactly  #
# as above and returns an override function.                                 #
##############################################################################

#########################################################################
# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix #
#########################################################################

###########################################
# Adding a new package or package version #
################################################################################
# 1. Update or add a `package` entry to `initial`, it must be a function       #
#    taking the version as argument and returning an attribute set. Everything #
#    is optional and the default for the sources of the repository and the     #
#    homepage will be https://github.com/math-comp/${package}.                 #
#                                                                              #
# 2. Update or add a `package` entry to `sha256` for each release.             #
#    You may use                                                               #
#    ```sh                                                                     #
#    nix-prefetch-url --unpack                                                 #
#    https://github.com/math-comp/math-comp/archive/version.tar.gz             #
#    ```                                                                       #
#                                                                              #
# 3. Update or create a new consistent set of extra packages.                  #
#    /!\ They must all be co-compatible. /!\                                   #
#    Do not use versions that may disappear: it must either be                 #
#    - a tag from the main repository (e.g. version or tag), or                #
#    - a revision hash that has been *merged in master*                        #
################################################################################

{ stdenv, fetchFromGitHub, recurseIntoAttrs,
  which, mathcomp, coqPackages,
  mathcomp-extra-config, mathcomp-extra-override,
  mathcomp-extra, current-mathcomp-extra,
}:
with builtins // stdenv.lib;
let
  ##############################
  # CONFIGURATION, please edit #
  ##############################
  ############################
  # Packages base delaration #
  ############################
  rec-mathcomp-extra-config = {
    initial = {
      mathcomp-finmap = version: {
        meta = {
          description = "A finset and finmap library";
          repo = "finmap";
          homepage = "https://github.com/math-comp/finmap";
        };
        passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ];
      };

      mathcomp-bigenough = version: {
        meta = {
          description = "A small library to do epsilon - N reasonning";
          repo = "bigenough";
          homepage = "https://github.com/math-comp/bigenough";
        };
        passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ];
      };

      multinomials = version: {
        buildInputs = [ which ];
        propagatedBuildInputs = with coqPackages;
          [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
        meta = {
          description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
          repo = "multinomials";
          homepage = "https://github.com/math-comp/multinomials";
        };
        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
      };

      mathcomp-analysis = version: {
        propagatedBuildInputs = with coqPackages;
          [ mathcomp.field mathcomp-finmap mathcomp-bigenough ];
        meta = {
          description = "Analysis library compatible with Mathematical Components";
          homepage = "https://github.com/math-comp/analysis";
          repo = "analysis";
          license = stdenv.lib.licenses.cecill-c;
        };
        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
      };

      mathcomp-real-closed = version: {
        propagatedBuildInputs = with coqPackages;
          [ coq mathcomp.field  mathcomp-bigenough ];
        meta = {
          description = "Mathematical Components Library on real closed fields";
          repo = "real-closed";
          homepage = "https://github.com/math-comp/real-closed";
        };
        passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ];
      };

      coqeal = version: {
        buildInputs = [ which ];
        propagatedBuildInputs = with coqPackages;
          [ mathcomp-algebra bignums paramcoq multinomials ];
        meta = {
          description = "CoqEAL - The Coq Effective Algebra Library";
          homepage = "https://github.com/coqeal/coqeal";
          license = stdenv.lib.licenses.mit;
          owner = "CoqEAL";
        };
        passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ];
      };
    };

    ###############################
    # sha256 of released versions #
    ###############################
    sha256 = {
      mathcomp-finmap = {
        "1.5.0"          = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
        "1.4.1"          = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
        "1.4.0+coq-8.11" = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
        "1.4.0"          = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
        "1.3.4"          = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
        "1.3.3"          = "1n844zjhv354kp4g4pfbajix0plqh7yxv6471sgyb46885298am5";
        "1.3.1"          = "14rvm0rm5hd3pd0srgak3jqmddzfv6n7gdpjwhady5xcgrc7gsx7";
        "1.2.1"          = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
        "1.2.0"          = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4";
        "1.1.0"          = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
        "1.0.0"          = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
      };
      mathcomp-bigenough = {
        "1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
      };
      mathcomp-analysis = {
        "0.2.3" = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
        "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk";
        "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd";
        "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al";
      };
      multinomials = {
        "1.5.1" = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
        "1.5"   = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
        "1.4"   = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p";
        "1.3"   = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4";
        "1.2"   = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq";
        "1.1"   = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s";
        "1.0"   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
      };
      mathcomp-real-closed = {
        "1.0.5" = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
        "1.0.4" = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
        "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
        "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl";
        "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
      };
      coqeal = {
        "1.0.3" = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
        "1.0.2" = "1brmf3gj03iky1bcl3g9vx8vknny7xfvs0y2rfr85am0296sxsfj";
        "1.0.1" = "19jhdrv2yp9ww0h8q73ihb2w1z3glz4waf2d2n45klafxckxi7bm";
        "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii";
      };
    };

    ################################
    # CONSISTENT sets of packages. #
    ################################
    for-coq-and-mc = let
      v5 = {
        mathcomp-finmap       = "1.5.0";
        mathcomp-bigenough    = "1.0.0";
        mathcomp-analysis     = "678d3cc37f5f3c71b1bd550836eb44e3ba2a5459";
        multinomials           = "1.5.1";
        mathcomp-real-closed  = "1.0.5";
        coqeal                = "CohenCyril/bdfc96771644b082e41268edc43d61dc5fda2358";
      };
      v4 = v3 // { coqeal = "1.0.3"; };
      v3 = {
        mathcomp-finmap       = "1.4.0";
        mathcomp-bigenough    = "1.0.0";
        mathcomp-analysis     = "0.2.3";
        multinomials          = "1.5";
        mathcomp-real-closed  = "1.0.4";
        coqeal                = "1.0.0";
      };
      v2 = {
        mathcomp-finmap       = "1.3.4";
        mathcomp-bigenough    = "1.0.0";
        mathcomp-analysis     = "0.2.3";
        multinomials          = "1.4";
        mathcomp-real-closed  = "1.0.3";
        coqeal                = "1.0.0";
      };
      v1 = {
        mathcomp-finmap       = "1.1.0";
        mathcomp-bigenough    = "1.0.0";
        multinomials          = "1.1";
        mathcomp-real-closed  = "1.0.1";
        coqeal                = "1.0.0";
      };
    in
      {
        "8.11" = {
          "1.11.0+beta1" = v5;
          "1.10.0"       = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";};
        };
        "8.10" = {
          "1.11.0+beta1" = v5;
          "1.10.0"       = v4;
          "1.9.0"        = removeAttrs v3 ["coqeal"];
        };
        "8.9" = {
          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
          "1.10.0"       = v4;
          "1.9.0"        = removeAttrs v3 ["coqeal"];
          "1.8.0"        = removeAttrs v2 ["coqeal"];
        };
        "8.8" = {
          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
          "1.9.0"        = removeAttrs v3 ["coqeal"];
          "1.8.0"        = removeAttrs v2 ["coqeal"];
          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
        };
        "8.7" = {
          "1.11.0+beta1" = removeAttrs v5 ["mathcomp-analysis"];
          "1.10.0"       = removeAttrs v4 ["mathcomp-analysis"];
          "1.9.0"        = removeAttrs v3 ["coqeal"];
          "1.8.0"        = removeAttrs v2 ["coqeal"];
          "1.7.0"        = removeAttrs v1 ["coqeal" "multinomials"];
        };
      };
  };

  ##############################
  # GENERATION, EDIT WITH CARE #
  ##############################
  coq = coqPackages.coq;

  default-attrs = {
    version = "master";
    buildInputs = [];
    propagatedBuildInputs = (with coqPackages; [ ssreflect ]);
    installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
    meta = {
      inherit (mathcomp.meta) platforms license;
      owner = "math-comp";
      maintainers = [ maintainers.vbgl maintainers.cohencyril ];
    };
    passthru.compatibleCoqVersions = (_: true);
  };

  pkgUp = recursiveUpdateUntil (path: l: r: !(isAttrs l && isAttrs r) || path == ["src"]);

  # Fixes a partial attribute set using the configuration
  # in the style of the above mathcomp-extra-config.initial,
  # and generates a name according to the conventional naming scheme below
  fix-attrs = pkgcfg:
    let attrs = pkgUp default-attrs pkgcfg; in
    pkgUp attrs (rec {
      name = "coq${coq.coq-version}mathcomp${mathcomp.version}-${attrs.meta.repo or attrs.meta.package or "anonymous"}-${attrs.version}";
      src = attrs.src or (fetchTarball "${meta.homepage}/archive/${attrs.version}.tar.gz");
      meta = rec {
        homepage = attrs.meta.homepage or attrs.src.meta.homepage or "https://github.com/${owner}/${repo}";
        owner    = attrs.meta.owner or "math-comp";
        repo     = attrs.meta.repo or attrs.meta.package or "math-comp-nix";
      };
    });

  # Gets a version out of a string, path or attribute set.
  getVersion = arg:
    if isFunction arg then (arg {}).version
    else  if arg == "" then "master"
    else  if isDerivation arg then arg.drvAttrs.version or "master"
    else  if isAttrs arg then arg.version or "master"
    else  if isString arg then head (reverseList (split "/" arg))
    else  if isPath arg   then (baseNameOf arg)
    else "master";

  # Converts a string, path or attribute set into an override function
  # It tries to fill the `old` argument of the override function using
  # `mathcomp-extra-config.initial` first and finishes with `fix-attrs`
  rec-mathcomp-extra-override = generic: old: let
    version = getVersion generic;
    package = old.meta.package or "math-comp-nix";
    cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {})) version) old
          // { inherit version; };
    fix = attrs: fix-attrs (pkgUp cfg attrs);
  in
    if isFunction generic then fix (generic cfg)
    else  if generic == null || generic == "" then fix {}
    else  if isDerivation generic then fix generic.drvAttrs
    else  if isAttrs generic then fix generic
    else  if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; }
    else  let fixedcfg = fix cfg; in fixedcfg // (
      if isString generic then
        if (mathcomp-extra-config.sha256.${package} or {})?${generic} then {
          src = fetchFromGitHub {
            inherit (fixedcfg.meta) owner repo;
            rev = version;
            sha256 = mathcomp-extra-config.sha256.${package}.${version};
          };
        }
        else  let splitted = filter isString (split "/" generic); in {
        src = fetchTarball
          ("https://github.com/" +
           (if length splitted == 1 then "${fixedcfg.meta.owner}/${fixedcfg.meta.repo}/archive/${version}.tar.gz"
            else "${head splitted}/${fixedcfg.meta.repo}/archive/${concatStringsSep "/" (tail splitted)}.tar.gz"));
        }
      else  if isPath generic then { src = generic; }
      else abort "${toString generic} not a legitimate generic version/override");

  # applies mathcomp-extra-config.for-coq-and-mc to the current mathcomp version
  for-this = mathcomp-extra-config.for-coq-and-mc.${coq.coq-version}.${mathcomp.version} or {};

  # specializes mathcomp-extra to the current mathcomp version.
  rec-current-mathcomp-extra = package: mathcomp-extra package (for-this.${package} or {});
in
  {
    mathcomp-extra-override = rec-mathcomp-extra-override;
    mathcomp-extra-config   = rec-mathcomp-extra-config;
    current-mathcomp-extra  = rec-current-mathcomp-extra;
    mathcomp-extra          = package: version:
      stdenv.mkDerivation (mathcomp-extra-override version {meta = {inherit package;};});

    mathcomp-finmap       = current-mathcomp-extra "mathcomp-finmap";
    mathcomp-analysis     = current-mathcomp-extra "mathcomp-analysis";
    mathcomp-bigenough    = current-mathcomp-extra "mathcomp-bigenough";
    multinomials          = current-mathcomp-extra "multinomials";
    mathcomp-real-closed  = current-mathcomp-extra "mathcomp-real-closed";
    coqeal                = current-mathcomp-extra "coqeal";

    mathcomp-extra-fast    = map (pkg: current-mathcomp-extra pkg)
      (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this));
    mathcomp-extra-all    = map (pkg: current-mathcomp-extra pkg) (attrNames for-this);
  }