gador/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

coq: now a shim on top of rocq (starting with 9.0)

Browse Source
This commit is contained in:
Pierre Roux
2025-02-07 21:06:47 +01:00
committed by Vincent Laporte
parent 064a30473b
commit b34fef3268
3 changed files with 27 additions and 30 deletions
Download Patch File Download Diff File Expand all files Collapse all files
pkgs/applications/science/logic/coq/default.nix
+12 -7
View File
@@ -13,6 +13,7 @@
, buildIde ? null # default is true for Coq < 8.14 and false for Coq >= 8.14
, glib, adwaita-icon-theme, wrapGAppsHook3, makeDesktopItem, copyDesktopItems
, csdp ? null
, rocq-core # for versions >= 9.0 that are transition shims on top of Rocq
, version, coq-version ? null
}@args:
let
@@ -207,9 +208,6 @@ self = stdenv.mkDerivation {
cp bin/votour $out/bin/
'' + ''
ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix}
'' + lib.optionalString (coqAtLeast "8.21") ''
ln -s $out/lib/rocq-runtime $OCAMLFIND_DESTDIR/rocq-runtime
ln -s $out/lib/rocq-core $OCAMLFIND_DESTDIR/rocq-core
'' + lib.optionalString (coqAtLeast "8.14") ''
ln -s $out/lib/coqide-server $OCAMLFIND_DESTDIR/coqide-server
'' + lib.optionalString buildIde ''
@@ -233,17 +231,24 @@ self = stdenv.mkDerivation {
mainProgram = "coqide";
};
}; in
if coqAtLeast "8.21" then self.overrideAttrs(_: {
if coqAtLeast "8.21" then self.overrideAttrs(o: {
# coq-core is now a shim for rocq
propagatedBuildInputs = o.propagatedBuildInputs ++ [ rocq-core ];
buildPhase = ''
runHook preBuild
make dunestrap
dune build -p rocq-runtime,rocq-core,coq-core,coqide-server${lib.optionalString buildIde ",rocqide"} -j $NIX_BUILD_CORES
dune build -p coq-core,coqide-server${lib.optionalString buildIde ",rocqide"} -j $NIX_BUILD_CORES
runHook postBuild
'';
installPhase = ''
runHook preInstall
dune install --prefix $out rocq-runtime rocq-core coq-core coqide-server${lib.optionalString buildIde " rocqide"}
dune install --prefix $out coq-core coqide-server${lib.optionalString buildIde " rocqide"}
# coq and rocq are now in different directories, which sometimes confuses coq_makefile
# which expects both in the same /nix/store/.../bin/ directory
# adding symlinks to content it
ROCQBIN=$(dirname ''$(command -v rocq))
for b in csdpcert ocamllibdep rocq rocq.byte rocqchk votour ; do
ln -s ''${ROCQBIN}/''${b} $out/bin/
done
runHook postInstall
'';
}) else if coqAtLeast "8.17" then self.overrideAttrs(_: {
pkgs/development/coq-modules/stdlib/default.nix
+14 -22
View File
@@ -1,5 +1,6 @@
{
coq,
rocqPackages,
mkCoqDerivation,
lib,
version ? null,
@@ -25,22 +26,12 @@
useDune = true;
configurePhase = ''
patchShebangs dev/with-rocq-wrap.sh
'';
buildPhase = ''
dev/with-rocq-wrap.sh dune build -p rocq-stdlib,coq-stdlib @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
'';
installPhase = ''
dev/with-rocq-wrap.sh dune install --root . rocq-stdlib coq-stdlib --prefix=$out --libdir $OCAMLFIND_DESTDIR
mkdir $out/lib/coq/
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
echo installing nothing
'';
meta = {
description = "Coq Standard Library";
description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
license = lib.licenses.lgpl21Only;
};
@@ -48,14 +39,15 @@
(
o:
# stdlib is already included in Coq <= 8.20
lib.optionalAttrs
(coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version)
{
buildPhase = ''
echo building nothing
'';
installPhase = ''
touch $out
'';
}
if coq.version != null && coq.version != "dev" && lib.versions.isLt "8.21" coq.version then {
configurePhase = ''
echo no configuration
'';
buildPhase = ''
echo building nothing
'';
installPhase = ''
touch $out
'';
} else { propagatedBuildInputs = [ rocqPackages.stdlib ]; }
)
pkgs/top-level/coq-packages.nix
+1 -1
View File
@@ -235,7 +235,7 @@ in rec {
coq_8_18 = mkCoq "8.18";
coq_8_19 = mkCoq "8.19";
coq_8_20 = mkCoq "8.20";
coq_9_0 = mkCoq "9.0";
coq_9_0 = mkCoq "9.0+rc1";
coqPackages_8_5 = mkCoqPackages coq_8_5;
coqPackages_8_6 = mkCoqPackages coq_8_6;