Unverified Commit 18f99b11 authored by 4ever2's avatar 4ever2
Browse files

rocqPackages.iris: init at 4.5.0

parent f136d4a6

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

+1 −1
Original line number Diff line number Diff line
@@ -58,7 +58,7 @@ in 
# this is just a wrapper for rocqPackages.stdpp for Rocq >= 9.0

if coq.rocqPackages ? stdpp then

  coq.rocqPackages.stdpp.override {

    inherit version;

    inherit version stdlib;

    inherit (coq.rocqPackages) rocq-core;

  }

else

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/top-level/rocq-packages.nix

+1 −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;