Commit 151a2ece authored by Pierre Roux's avatar Pierre Roux Committed by Vincent Laporte
Browse files

coqPackages: fix Rocq shim for Coq >= 9

parent 2bbba780

pkgs/applications/science/logic/coq/default.nix

+3 −3
Original line number Diff line number Diff line
@@ -19,6 +19,7 @@ 
  ocamlPackages_4_10,

  ocamlPackages_4_12,

  ocamlPackages_4_14,

  rocqPackages, # for versions >= 9.0 that are transition shims on top of Rocq

  ncurses,

  buildIde ? null, # default is true for Coq < 8.14 and false for Coq >= 8.14

  glib,
@@ -27,7 +28,6 @@ 
  makeDesktopItem,

  copyDesktopItems,

  csdp ? null,

  rocq-core, # for versions >= 9.0 that are transition shims on top of Rocq

  version,

  coq-version ? null,

}@args:
@@ -148,7 +148,6 @@ let 
  self = stdenv.mkDerivation {

    pname = "coq";

    inherit (fetched) version src;

    exact-version = args.version;



    passthru = {

      inherit coq-version;
@@ -161,6 +160,7 @@ let 
        findlib

        num

        ;

      rocqPackages = lib.optionalAttrs (coqAtLeast "8.21") rocqPackages;

      emacsBufferSetup = pkgs: ''

        ; Propagate coq paths to children

        (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
@@ -334,7 +334,7 @@ if coqAtLeast "8.21" then 
  self.overrideAttrs (o: {

    # coq-core is now a shim for rocq

    propagatedBuildInputs = o.propagatedBuildInputs ++ [

      (rocq-core.override { version = o.exact-version; })

      rocqPackages.rocq-core

    ];

    buildPhase = ''

      runHook preBuild

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

+50 −73
Original line number Diff line number Diff line
@@ -2,14 +2,12 @@ 
  lib,

  mkCoqDerivation,

  coq,

  rocqPackages_9_0,

  rocqPackages_9_1,

  rocqPackages,

  stdlib,

  version ? null,

}:



(mkCoqDerivation {

let

  derivation = mkCoqDerivation {

    pname = "bignums";

    owner = "rocq-community";

    inherit version;
@@ -19,13 +17,10 @@ 
      in

      with lib.versions;

      lib.switch coq.coq-version [

      (case (range "9.0" "9.1") "9.0.0+rocq${coq.coq-version}")

        (case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}")

        (case (range "8.6" "8.17") "${coq.coq-version}.0")

      ] null;



  release."9.0.0+rocq9.1".sha256 = "sha256-MSjlfJs3JOakuShOj+isNlus0bKlZ+rkvzRoKZQK5RQ=";

  release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";

    release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";

    release."9.0.0+coq8.19".sha256 = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";

    release."9.0.0+coq8.18".sha256 = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
@@ -56,31 +51,13 @@ 
    meta = {

      license = lib.licenses.lgpl2;

    };

}).overrideAttrs

  (

    o:

    # this is just a wrapper for rocPackages.bignums for Rocq >= 9.0

    lib.optionalAttrs

      (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))

      (

        let

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

          rp = lib.switch coq.coq-version [

            (case (lib.versions.isEq "9.0") rocqPackages_9_0)

            (case (lib.versions.isEq "9.1") rocqPackages_9_1)

          ] rocqPackages;

  };

in

        {

          configurePhase = ''

            echo no configuration

          '';

          buildPhase = ''

            echo building nothing

          '';

          installPhase = ''

            echo installing nothing

          '';

          propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.bignums ];

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

if coq.rocqPackages ? bignums then

  coq.rocqPackages.bignums.override {

    inherit version stdlib;

    inherit (coq.rocqPackages) rocq-core;

  }

      )

  )
 
else

  derivation

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

+17 −35
Original line number Diff line number Diff line
@@ -3,9 +3,6 @@ 
  mkCoqDerivation,

  which,

  coq,

  rocqPackages_9_0,

  rocqPackages_9_1,

  rocqPackages,

  stdlib,

  version ? null,

  elpi-version ? null,
@@ -23,7 +20,7 @@ let 
        in

        with lib.versions;

        lib.switch coq.coq-version [

          (case (range "8.20" "9.1") "2.0.7")

          (case (range "8.20" "8.20") "2.0.7")

          (case (range "8.18" "8.19") "1.18.1")

          (case (range "8.16" "8.17") "1.17.0")

          (case "8.15" "1.15.0")
@@ -47,8 +44,8 @@ let 
      in

      with lib.versions;

      lib.switch coq.coq-version [

        (case (range "8.20" "9.1") "2.6.0")

        (case (range "8.20" "9.0") "2.5.2")

        (case (range "8.20" "8.20") "2.6.0")

        (case (range "8.20" "8.20") "2.5.2")

        (case "8.19" "2.0.1")

        (case "8.18" "2.0.0")

        (case "8.17" "1.18.0")
@@ -141,28 +138,6 @@ let 
  );

  patched-derivation4 = patched-derivation3.overrideAttrs (

    o:

    # this is just a wrapper for rocPackages.rocq-elpi for Rocq >= 9.0

    if coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version) then

      let

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

        rp = lib.switch coq.coq-version [

          (case "9.0" rocqPackages_9_0)

          (case "9.1" rocqPackages_9_1)

        ] rocqPackages;

      in

      {

        configurePhase = ''

          echo no configuration

        '';

        buildPhase = ''

          echo building nothing

        '';

        installPhase = ''

          echo installing nothing

        '';

        propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.rocq-elpi ];

      }

    else

    lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))

      {

        configurePhase = ''
@@ -179,4 +154,11 @@ let 
      }

  );

in

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

if coq.rocqPackages ? rocq-elpi then

  coq.rocqPackages.rocq-elpi.override {

    inherit version elpi-version;

    inherit (coq.rocqPackages) rocq-core;

  }

else

  patched-derivation4

pkgs/development/coq-modules/hierarchy-builder/default.nix

+24 −43
Original line number Diff line number Diff line
@@ -2,9 +2,6 @@ 
  lib,

  mkCoqDerivation,

  coq,

  rocqPackages_9_0,

  rocqPackages_9_1,

  rocqPackages,

  stdlib,

  coq-elpi,

  version ? null,
@@ -21,7 +18,7 @@ let 
      in

      with lib.versions;

      lib.switch coq.coq-version [

        (case (range "8.20" "9.1") "1.9.1")

        (case (range "8.20" "8.20") "1.9.1")

        (case (range "8.19" "8.20") "1.8.0")

        (case (range "8.18" "8.20") "1.7.1")

        (case (range "8.16" "8.18") "1.6.0")
@@ -60,8 +57,7 @@ let 
      license = licenses.mit;

    };

  };

in

hb.overrideAttrs (

  hb2 = hb.overrideAttrs (

    o:

    lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {

      buildPhase = "make build";
@@ -75,29 +71,14 @@ hb.overrideAttrs ( 
    // lib.optionalAttrs (o.version != null && o.version == "1.8.1") {

      propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];

    }

  # this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0

  //

    lib.optionalAttrs

      (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))

      (

        let

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

          rp = lib.switch coq.coq-version [

            (case "9.0" rocqPackages_9_0)

            (case "9.1" rocqPackages_9_1)

          ] rocqPackages;

  );

in

        {

          configurePhase = ''

            echo no configuration

          '';

          buildPhase = ''

            echo building nothing

          '';

          installPhase = ''

            echo installing nothing

          '';

          propagatedBuildInputs = o.propagatedBuildInputs ++ [ rp.hierarchy-builder ];

# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0

if coq.rocqPackages ? hierarchy-builder then

  coq.rocqPackages.hierarchy-builder.override {

    inherit version;

    inherit (coq.rocqPackages) rocq-core;

    rocq-elpi = coq-elpi;

  }

      )

)
 
else

  hb2

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

+30 −54
Original line number Diff line number Diff line 
{

  lib,

  mkCoqDerivation,

  rocqPackages_9_0,

  rocqPackages_9_1,

  rocqPackages,

  which,

  coq,

  version ? null,

}:



with lib;

(mkCoqDerivation {

let

  derivation = mkCoqDerivation {

    pname = "parseque";

    repo = "parseque";

    owner = "rocq-community";



    inherit version;

    defaultVersion =

      let

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

      in

      with versions;

    switch

      [ coq.coq-version ]

      [

        {

          cases = [ (range "8.16" "9.0") ];

          out = "0.2.2";

        }

      ]

      null;

      switch coq.coq-version [

        (case (range "8.16" "8.20") "0.2.2")

      ] null;



    release."0.2.2".sha256 = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
@@ -37,31 +31,13 @@ with lib; 
      maintainers = with maintainers; [ womeier ];

      license = licenses.mit;

    };

}).overrideAttrs

  (

    o:

    # this is just a wrapper for rocPackages.parseque for Rocq >= 9.0

    lib.optionalAttrs

      (coq.version != null && (coq.version == "dev" || lib.versions.isGe "9.0" coq.version))

      (

        let

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

          rp = lib.switch coq.coq-version [

            (case "9.0" rocqPackages_9_0)

            (case "9.1" rocqPackages_9_1)

          ] rocqPackages;

  };

in

        {

          configurePhase = ''

            echo no configuration

          '';

          buildPhase = ''

            echo building nothing

          '';

          installPhase = ''

            echo installing nothing

          '';

          propagatedBuildInputs = [ rp.parseque ];

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

if coq.rocqPackages ? parseque then

  coq.rocqPackages.parseque.override {

    inherit version;

    inherit (coq.rocqPackages) rocq-core;

  }

      )

  )
 
else

  derivation