Unverified Commit 8231b97a authored by Vincent Laporte's avatar Vincent Laporte Committed by GitHub
Browse files

rocqPackages.stdpp: init at 1.13.0 (#498212)

parents 17865bec 18f99b11

pkgs/development/coq-modules/iris/default.nix

+53 −43
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ 
  version ? null,

}:



mkCoqDerivation {

let

  derivation = mkCoqDerivation {

    pname = "iris";

    domain = "gitlab.mpi-sws.org";

    owner = "iris";
@@ -52,4 +53,13 @@ mkCoqDerivation { 
        lib.maintainers.ineol

      ];

    };

  };

in

# this is just a wrapper for rocqPackages.iris for Rocq >= 9.0

if coq.rocqPackages ? iris then

  coq.rocqPackages.iris.override {

    inherit version stdpp;

    inherit (coq.rocqPackages) rocq-core;

  }

else

  derivation

pkgs/development/coq-modules/stdpp/default.nix

+53 −43
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ 
  version ? null,

}:



mkCoqDerivation {

let

  derivation = mkCoqDerivation {

    pname = "stdpp";

    inherit version;

    domain = "gitlab.mpi-sws.org";
@@ -52,4 +53,13 @@ mkCoqDerivation { 
        lib.maintainers.ineol

      ];

    };

  };

in

# this is just a wrapper for rocqPackages.stdpp for Rocq >= 9.0

if coq.rocqPackages ? stdpp then

  coq.rocqPackages.stdpp.override {

    inherit version stdlib;

    inherit (coq.rocqPackages) rocq-core;

  }

else

  derivation

pkgs/development/rocq-modules/iris/default.nix

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

  lib,

  mkRocqDerivation,

  stdlib,

  rocq-core,

  stdpp,

  version ? null,

}:



mkRocqDerivation {

  pname = "iris";

  domain = "gitlab.mpi-sws.org";

  owner = "iris";

  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.2") "4.5.0")

    ] null;

  release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";

  releaseRev = v: "iris-${v}";



  propagatedBuildInputs = [

    stdlib

    stdpp

  ];



  preBuild = ''

    if [[ -f coq-lint.sh ]]

    then patchShebangs coq-lint.sh

    fi

  '';



  meta = {

    description = "Rocq development of the Iris Project";

    license = lib.licenses.bsd3;

    maintainers = [

      lib.maintainers.vbgl

      lib.maintainers.ineol

    ];

  };

}

pkgs/development/rocq-modules/stdpp/default.nix

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

  lib,

  mkRocqDerivation,

  rocq-core,

  stdlib,

  version ? null,

}:



mkRocqDerivation {

  pname = "stdpp";

  inherit version;

  domain = "gitlab.mpi-sws.org";

  owner = "iris";

  defaultVersion =

    let

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

    in

    with lib.versions;

    lib.switch rocq-core.rocq-version [

      (case (range "9.0" "9.2") "1.13.0")

    ] null;

  release."1.13.0".sha256 = "sha256-kj8oBzarsLB4DDQ43yz4ViQbyzuISqext28wC2Fh3Sw=";

  releaseRev = v: "stdpp-${v}";



  propagatedBuildInputs = [ stdlib ];



  preBuild = ''

    if [[ -f coq-lint.sh ]]

    then patchShebangs coq-lint.sh

    fi

  '';



  meta = {

    description = "Extended “Standard Library” for Rocq";

    license = lib.licenses.bsd3;

    maintainers = [

      lib.maintainers.vbgl

      lib.maintainers.ineol

    ];

  };

}

pkgs/top-level/rocq-packages.nix

+2 −0
Original line number Diff line number Diff line
@@ -38,6 +38,7 @@ let 


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

      hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };

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

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

      mathcomp-boot = self.mathcomp.boot;

      mathcomp-order = self.mathcomp.order;
@@ -52,6 +53,7 @@ let 
      relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };

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

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

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

      vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };



      filterPackages = doesFilter: if doesFilter then filterRocqPackages self else self;