nathan/nixpkgs
1
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2026-08-25 17:55:21 +00:00
Code Issues Packages Projects Releases Wiki Activity

rocqPackages.stdlib: merge with coqPackages.stdlib

Browse Source
This commit is contained in:
Pierre Roux
2026-07-23 15:06:34 +02:00
committed by Vincent Laporte
parent cc09ca4e4b
commit e8ec89d76f
3 changed files with 50 additions and 82 deletions
Download Patch File Download Diff File Expand all files Collapse all files

55
pkgs/development/coq-modules/stdlib/default.nix
View File

@@ -1,55 +0,0 @@
{
coq,
mkCoqDerivation,
lib,
version ? null,
}:
let
derivation = mkCoqDerivation {
pname = "stdlib";
repo = "stdlib";
owner = "coq";
opam-name = "coq-stdlib";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch coq.coq-version [
(case (isLe "9.1") "9.0.0")
# the < 9.0 above is artificial as stdlib was included in Coq before
] null;
releaseRev = v: "V${v}";
release."9.0.0".hash = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
configurePhase = ''
echo no configuration
'';
buildPhase = ''
echo building nothing
'';
installPhase = ''
echo installing nothing
# Make an output directory rather than a file, so this is more friendly to buildEnv
mkdir $out
'';
meta = {
description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
license = lib.licenses.lgpl21Only;
};
};
in
# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
if coq.rocqPackages ? stdlib then
coq.rocqPackages.stdlib.override {
inherit version;
inherit (coq.rocqPackages) rocq-core;
}
else
derivation

75
pkgs/development/rocq-modules/stdlib/default.nix
View File

@@ -4,35 +4,58 @@
lib,
version ? null,
}:
mkRocqDerivation {
pname = "stdlib";
repo = "stdlib";
owner = "rocq-prover";
opam-name = "rocq-stdlib";
let
derivation = mkRocqDerivation {
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.version [
(case (range "9.3" "9.3") "9.2.0")
(case (range "9.2" "9.2") "9.1.0")
(case (range "9.0" "9.1") "9.0.0")
] null;
releaseRev = v: "V${v}";
pname = "stdlib";
repo = "stdlib";
owner = "rocq-prover";
opam-name = "rocq-stdlib";
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.version [
(case (range "9.3" "9.3") "9.2.0")
(case (range "9.2" "9.2") "9.1.0")
(case (isLe "9.1") "9.0.0")
] null;
releaseRev = v: "V${v}";
mlPlugin = true;
release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
mlPlugin = true;
meta = {
description = "Rocq Proof Assistant -- Standard Library";
license = lib.licenses.lgpl21Only;
};
meta = {
description = "Rocq Proof Assistant -- Standard Library";
license = lib.licenses.lgpl21Only;
};
}
# the < 9.0 above is artificial as stdlib was included in Coq before
patched-derivation = derivation.overrideAttrs (
o:
lib.optionalAttrs
(rocq-core.rocq-version != "dev" && lib.versions.isLe "8.20" rocq-core.rocq-version)
{
configurePhase = ''
echo no configuration
'';
buildPhase = ''
echo building nothing
'';
installPhase = ''
echo installing nothing
# Make an output directory rather than a file, so this is more friendly to buildEnv
mkdir $out
'';
}
);
in
patched-derivation

2
pkgs/top-level/coq-packages.nix
View File

@@ -230,7 +230,7 @@ let
ssprove = callPackage ../development/coq-modules/ssprove { };
stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
stalmarck = self.stalmarck-tactic.stalmarck;
stdlib = callPackage ../development/coq-modules/stdlib { };
stdlib = callPackage ../development/rocq-modules/stdlib { };
stdpp = callPackage ../development/coq-modules/stdpp { };
StructTact = callPackage ../development/coq-modules/StructTact { };
tlc = callPackage ../development/coq-modules/tlc { };