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

rocqPackages.mathcomp: init at 2.5.0 (#413917)

parents 0d576c36 a4d52834

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

+47 −11
Original line number Diff line number Diff line
@@ -99,6 +99,15 @@ let 
    "character" = [ "field" ];

    "all" = [ "character" ];

  };

  meta = {

    homepage = "https://math-comp.github.io/";

    license = lib.licenses.cecill-b;

    maintainers = with lib.maintainers; [

      vbgl

      jwiegley

      cohencyril

    ];

  };



  mathcomp_ =

    package:
@@ -121,6 +130,7 @@ let 
            releaseRev

            repo

            owner

            meta

            ;



          mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
@@ -147,16 +157,6 @@ let 
            cd ${pkgpath} || cd ssreflect  # before 2.5, boot didn't exist, make it behave as ssreflect

          ''

          + lib.optionalString (package == "all") pkgallMake;



          meta = {

            homepage = "https://math-comp.github.io/";

            license = lib.licenses.cecill-b;

            maintainers = with lib.maintainers; [

              vbgl

              jwiegley

              cohencyril

            ];

          };

        }

        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }

        // lib.optionalAttrs withDoc {
@@ -244,4 +244,40 @@ let 
    in

    patched-derivation5;

in

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

if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then

  let

    mc = coq.rocqPackages.mathcomp.override {

      inherit version withDoc single;

      inherit

        ncurses

        graphviz

        lua

        fetchzip

        hierarchy-builder

        ;

      inherit (coq.rocqPackages) rocq-core;

    };

  in

  mc

  // {

    ssreflect = mkCoqDerivation {

      inherit

        version

        defaultVersion

        release

        releaseRev

        repo

        owner

        meta

        ;

      pname = "mathcomp-ssreflect";

      propagatedBuildInputs = [

        mc.boot

        mc.order

      ];

      preBuild = "cd ssreflect";

    };

  }

else

  mathcomp_ (if single then "single" else "all")

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

0 → 100644
+138 −0
Original line number Diff line number Diff line 
############################################################################

# This file mainly provides the `mathcomp` derivation, which is            #

# essentially a meta-package containing all core mathcomp libraries        #

# (boot order fingroup algebra solvable field character). They can be      #

# accessed individually through the passthrough attributes of mathcomp     #

# bearing the same names (mathcomp.boot, etc).                             #

############################################################################

# Compiling a custom version of mathcomp using `mathcomp.override`.        #

# This is the replacement for the former `mathcomp_ config` function.      #

# See the documentation at doc/languages-frameworks/coq.section.md.        #

############################################################################



{

  lib,

  ncurses,

  graphviz,

  lua,

  fetchzip,

  mkRocqDerivation,

  withDoc ? false,

  single ? false,

  rocq-core,

  hierarchy-builder,

  version ? null,

}@args:



let

  repo = "mathcomp";

  owner = "math-comp";

  withDoc = single && (args.withDoc or false);

  defaultVersion =

    let

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

      inherit (lib.versions) range;

    in

    lib.switch rocq-core.rocq-version [

      (case (range "9.0" "9.1") "2.5.0")

    ] null;

  release = {

    "2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";

  };

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



  # list of core mathcomp packages sorted by dependency order

  packages = {

    "boot" = [ ];

    "order" = [ "boot" ];

    "fingroup" = [ "boot" ];

    "algebra" = [

      "order"

      "fingroup"

    ];

    "solvable" = [ "algebra" ];

    "field" = [ "solvable" ];

    "character" = [ "field" ];

    "all" = [ "character" ];

  };



  mathcomp_ =

    package:

    let

      mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});

      pkgpath = if package == "single" then "." else package;

      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";

      pkgallMake = ''

        echo "all.v"  > Make

        echo "-I ." >>   Make

        echo "-R . mathcomp.all" >> Make

      '';

      derivation = mkRocqDerivation (

        {

          inherit

            version

            pname

            defaultVersion

            release

            releaseRev

            repo

            owner

            ;



          nativeBuildInputs = lib.optionals withDoc [

            graphviz

            lua

          ];

          buildInputs = [ ncurses ];

          propagatedBuildInputs = mathcomp-deps ++ [ hierarchy-builder ];



          buildFlags = lib.optional withDoc "doc";



          preBuild = ''

            if [[ -f etc/buildlibgraph ]]

            then patchShebangs etc/buildlibgraph

            fi

          ''

          + ''

            cd ${pkgpath}

          ''

          + lib.optionalString (package == "all") pkgallMake;



          meta = {

            homepage = "https://math-comp.github.io/";

            license = lib.licenses.cecill-b;

            maintainers = with lib.maintainers; [

              vbgl

              jwiegley

              cohencyril

            ];

          };

        }

        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }

        // lib.optionalAttrs withDoc {

          htmldoc_template = fetchzip {

            url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";

            sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";

          };

          postBuild = ''

            cp -rf _build_doc/* .

            rm -r _build_doc

          '';

          postInstall =

            let

              tgt = "$out/share/coq/${rocq-core.rocq-version}/";

            in

            lib.optionalString withDoc ''

              mkdir -p ${tgt}

              cp -r htmldoc ${tgt}

              cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/

            '';

          buildTargets = "doc";

          extraInstallFlags = [ "-f Makefile.coq" ];

        }

      );

      # patched-derivation1 = derivation.overrideAttrs ...

    in

    derivation;

in

mathcomp_ (if single then "single" else "all")

pkgs/top-level/rocq-packages.nix

+8 −0
Original line number Diff line number Diff line
@@ -37,6 +37,14 @@ let 


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

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

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

      mathcomp-boot = self.mathcomp.boot;

      mathcomp-order = self.mathcomp.order;

      mathcomp-fingroup = self.mathcomp.fingroup;

      mathcomp-algebra = self.mathcomp.algebra;

      mathcomp-solvable = self.mathcomp.solvable;

      mathcomp-field = self.mathcomp.field;

      mathcomp-character = self.mathcomp.character;

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

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

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