rocqPackages.mathcomp-analysis: init at 1.16.0 (#500659) (f2498f1a) · Commits · nix / nixpkgs

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

+22 −2

Original line number	Diff line number	Diff line
		@@ -7,7 +7,6 @@
		hierarchy-builder,
		stdlib,
		single ? false,
		coqPackages,
		coq,
		version ? null,
		}@args:
		@@ -232,4 +231,25 @@ let
		in
		patched-derivation;
		in
		# this is just a wrapper for rocqPackages.mathcomp-analysis for Rocq >= 9.0
		if
		coq.rocqPackages ? mathcomp-analysis
		&& !(lib.elem version [
		"1.12.0"
		"1.13.0"
		"1.14.0"
		"1.15.0"
		])
		then
		coq.rocqPackages.mathcomp-analysis.override {
		inherit version single;
		inherit
		mathcomp
		mathcomp-finmap
		mathcomp-bigenough
		stdlib
		;
		inherit (coq.rocqPackages) rocq-core;
		}
		else
		mathcomp_ (if single then "single" else "analysis")

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

+2 −0

Original line number	Diff line number	Diff line
		@@ -32,6 +32,7 @@
		lib.switch
		[ coq.coq-version mathcomp-analysis.version ]
		[
		(case (range "9.0" "9.1") (isGe "1.12") "0.9.7")
		(case (range "8.20" "9.1") (isGe "1.12") "0.9.6")
		(case (range "8.20" "8.20") (range "1.12" "1.13") "0.9.4")
		(case (range "8.19" "8.20") (range "1.10" "1.11") "0.9.3")
		@@ -46,6 +47,7 @@
		(case (range "8.15" "8.16") (range "0.5.4" "0.6.5") "0.5.1")
		]
		null;
		release."0.9.7".sha256 = "sha256-cmkBh2vw02R/UivGqaEpg89LMGR/i5Q14IEZDhjFA+Y=";
		release."0.9.6".sha256 = "sha256-7gwtqTzMMEhUDz2XdxamAqjSdST0HrbWJHQ/YTDRR5E=";
		release."0.9.4".sha256 = "sha256-btHOBNMdXvlG2jxC04+4qmIjeyuaqtyugm2Ruj3lQr8=";
		release."0.9.3".sha256 = "sha256-8+cnVKNAvZ3MVV3BpS8UmCIxJphsQRBv3swek1eEBjE=";

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

0 → 100644

+125 −0

Original line number	Diff line number	Diff line
		{
		lib,
		mkRocqDerivation,
		mathcomp,
		mathcomp-finmap,
		mathcomp-bigenough,
		stdlib,
		single ? false,
		rocq-core,
		version ? null,
		}@args:

		let
		repo = "analysis";
		owner = "math-comp";

		release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY=";

		defaultVersion =
		let
		case = rocq: mc: out: {
		cases = [
		rocq
		mc
		];
		inherit out;
		};
		in
		with lib.versions;
		lib.switch
		[ rocq-core.rocq-version mathcomp.version ]
		[
		(case (range "9.0" "9.1") (range "2.4.0" "2.5.0") "1.16.0")
		]
		null;

		# list of analysis packages sorted by dependency order
		packages = {
		"classical" = [ ];
		"reals" = [ "classical" ];
		"experimental-reals" = [ "reals" ];
		"analysis" = [ "reals" ];
		"reals-stdlib" = [ "reals" ];
		"analysis-stdlib" = [
		"analysis"
		"reals-stdlib"
		];
		};

		mathcomp_ =
		package:
		let
		classical-deps = [
		mathcomp.algebra
		mathcomp-finmap
		];
		experimental-reals-deps = [ mathcomp-bigenough ];
		analysis-deps = [
		mathcomp.field
		mathcomp-bigenough
		];
		intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
		pkgpath =
		let
		case = case: out: { inherit case out; };
		in
		lib.switch package [
		(case "single" ".")
		(case "analysis" "theories")
		(case "experimental-reals" "experimental_reals")
		(case "reals-stdlib" "reals_stdlib")
		(case "analysis-stdlib" "analysis_stdlib")
		] package;
		pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
		derivation = mkRocqDerivation {
		inherit
		version
		pname
		defaultVersion
		release
		repo
		owner
		;

		namePrefix = [
		"rocq-core"
		"mathcomp"
		];

		propagatedBuildInputs =
		intra-deps
		++ lib.optionals (lib.elem package [
		"classical"
		"single"
		]) classical-deps
		++ lib.optionals (lib.elem package [
		"experimental-reals"
		"single"
		]) experimental-reals-deps
		++ lib.optionals (lib.elem package [
		"analysis"
		"single"
		]) analysis-deps
		++ lib.optional (lib.elem package [
		"reals-stdlib"
		"analysis-stdlib"
		"single"
		]) stdlib;

		preBuild = ''
		cd ${pkgpath}
		'';

		meta = {
		description = "Analysis library compatible with Mathematical Components";
		maintainers = [ lib.maintainers.cohencyril ];
		license = lib.licenses.cecill-c;
		};

		passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
		};
		in
		derivation;
		in
		mathcomp_ (if single then "single" else "analysis")

pkgs/top-level/rocq-packages.nix

+6 −0

Original line number	Diff line number	Diff line
		@@ -47,8 +47,14 @@ let
		mathcomp-solvable = self.mathcomp.solvable;
		mathcomp-field = self.mathcomp.field;
		mathcomp-character = self.mathcomp.character;
		mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { };
		mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
		mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
		mathcomp-classical = self.mathcomp-analysis.classical;
		mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
		mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };
		mathcomp-reals = self.mathcomp-analysis.reals;
		mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
		parseque = callPackage ../development/rocq-modules/parseque { };
		relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
		rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };

Admin message