Unverified Commit 09ac1a4d authored by Vincent Laporte's avatar Vincent Laporte Committed by GitHub
Browse files

rocqPackages.mathcomp-bigenough: init at 1.0.4 (#492074)

parents 5ce2d6ae 03444186

pkgs/development/coq-modules/mathcomp-bigenough/default.nix

+39 −29
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ 
  version ? null,

}:



mkCoqDerivation {

let

  derivation = mkCoqDerivation {



    namePrefix = [

      "coq"
@@ -39,4 +40,13 @@ mkCoqDerivation { 
      description = "Small library to do epsilon - N reasonning";

      license = lib.licenses.cecill-b;

    };

  };

in

# this is just a wrapper for rocqPackages.mathcomp-bigenough for Rocq >= 9.0

if coq.rocqPackages ? mathcomp-bigenough then

  coq.rocqPackages.mathcomp-bigenough.override {

    inherit version mathcomp-boot;

    inherit (coq.rocqPackages) rocq-core;

  }

else

  derivation

pkgs/development/coq-modules/mathcomp-finmap/default.nix

+67 −57
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ 
  version ? null,

}:



mkCoqDerivation {

let

  derivation = mkCoqDerivation {



    namePrefix = [

      "coq"
@@ -66,4 +67,13 @@ mkCoqDerivation { 
      description = "Finset and finmap library";

      license = lib.licenses.cecill-b;

    };

  };

in

# this is just a wrapper for rocqPackages.mathcomp-finmap for Rocq >= 9.0

if coq.rocqPackages ? mathcomp-finmap then

  coq.rocqPackages.mathcomp-finmap.override {

    inherit version mathcomp-boot;

    inherit (coq.rocqPackages) rocq-core;

  }

else

  derivation

pkgs/development/rocq-modules/mathcomp-bigenough/default.nix

0 → 100644
+37 −0
Original line number Diff line number Diff line 
{

  rocq-core,

  mkRocqDerivation,

  mathcomp-boot,

  lib,

  version ? null,

}:



mkRocqDerivation {



  namePrefix = [

    "rocq-core"

    "mathcomp"

  ];

  pname = "bigenough";

  owner = "math-comp";



  release = {

    "1.0.4".sha256 = "sha256-cwfDCEFSXWnqV5aIrhTviUti0CXNwmFe6zVbqlD2iZw=";

  };

  inherit version;

  defaultVersion =

    let

      case = case: out: { inherit case out; };

    in

    with lib.versions;

    lib.switch rocq-core.rocq-version [

      (case (range "9.0" "9.1") "1.0.4")

    ] null;



  propagatedBuildInputs = [ mathcomp-boot ];



  meta = {

    description = "Small library to do epsilon - N reasonning";

    license = lib.licenses.cecill-b;

  };

}

pkgs/development/rocq-modules/mathcomp-finmap/default.nix

0 → 100644
+45 −0
Original line number Diff line number Diff line 
{

  rocq-core,

  mkRocqDerivation,

  mathcomp-boot,

  lib,

  version ? null,

}:



mkRocqDerivation {



  namePrefix = [

    "rocq-core"

    "mathcomp"

  ];

  pname = "finmap";

  owner = "math-comp";

  inherit version;

  defaultVersion =

    let

      case = rocq: mc: out: {

        cases = [

          rocq

          mc

        ];

        inherit out;

      };

    in

    with lib.versions;

    lib.switch

      [ rocq-core.rocq-version mathcomp-boot.version ]

      [

        (case (range "9.0" "9.1") (range "2.3" "2.5") "2.2.2")

      ]

      null;

  release = {

    "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";

  };



  propagatedBuildInputs = [ mathcomp-boot ];



  meta = {

    description = "Finset and finmap library";

    license = lib.licenses.cecill-b;

  };

}

pkgs/top-level/rocq-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -46,6 +46,8 @@ let 
      mathcomp-solvable = self.mathcomp.solvable;

      mathcomp-field = self.mathcomp.field;

      mathcomp-character = self.mathcomp.character;

      mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };

      mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };

      parseque = callPackage ../development/rocq-modules/parseque { };

      relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };

      rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };