646b892680
Some checks failed
Periodic Merges (6h) / master → staging-nixos (push) Failing after 12m50s
Periodic Merges (6h) / master → staging-next (push) Failing after 12m54s
Periodic Merges (24h) / merge-base(master,staging) → haskell-updates (push) Failing after 11m54s
Periodic Merges (6h) / staging-next → staging (push) Failing after 12m13s
Periodic Merges (24h) / staging-next-25.05 → staging-25.05 (push) Failing after 13m24s
Periodic Merges (24h) / release-25.05 → staging-next-25.05 (push) Failing after 14m28s
98 lines
2.7 KiB
Nix
98 lines
2.7 KiB
Nix
{
|
|
lib,
|
|
callPackage,
|
|
runCommand,
|
|
makeWrapper,
|
|
coq,
|
|
imagemagick,
|
|
python312,
|
|
}:
|
|
|
|
# Jupyter console:
|
|
# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel coq-kernel.definition'
|
|
|
|
# Jupyter console with packages: (using Coq 8.20, before the Rocq transition at version 9.0)
|
|
# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel ((coq-kernel.override { coq = coq_8_20; }).definitionWithPackages (with coqPackages_8_20; [bignums stdlib]))'
|
|
|
|
# Jupyter notebook:
|
|
# nix run --impure --expr 'with import <nixpkgs> {}; jupyter.override { definitions.coq = coq-kernel.definition; }'
|
|
|
|
let
|
|
# Nixpkgs master is currently on python3 >= python313. This doesn't work with
|
|
# this package, because it depends on the "future" package, which is no longer
|
|
# compatible with Python 3.13.
|
|
|
|
coq-jupyter = callPackage ./kernel.nix {
|
|
inherit coq;
|
|
python3 = python312;
|
|
};
|
|
|
|
python = python312.withPackages (ps: [
|
|
ps.traitlets
|
|
ps.jupyter-core
|
|
ps.ipykernel
|
|
coq-jupyter
|
|
]);
|
|
|
|
# At version 9.0, Coq underwent a name change to Rocq.
|
|
# A couple paths and environment variables need to change at this point.
|
|
isRocq = lib.versionAtLeast coq.coq-version "9.0";
|
|
|
|
logos =
|
|
let
|
|
dir = if isRocq then "rocqide" else "coqide";
|
|
in
|
|
runCommand "coq-logos" { buildInputs = [ imagemagick ]; } ''
|
|
mkdir -p $out
|
|
convert ${coq.src}/ide/${dir}/coq.png -resize 32x32 $out/logo-32x32.png
|
|
convert ${coq.src}/ide/${dir}/coq.png -resize 64x64 $out/logo-64x64.png
|
|
'';
|
|
|
|
launcher =
|
|
runCommand "coq-kernel-launcher"
|
|
{
|
|
nativeBuildInputs = [ makeWrapper ];
|
|
}
|
|
''
|
|
mkdir -p $out/bin
|
|
|
|
makeWrapper ${python.interpreter} $out/bin/coq-kernel \
|
|
--add-flags "-m coq_jupyter" \
|
|
--suffix PATH : ${coq}/bin
|
|
'';
|
|
|
|
definitionWithPackages = packages: {
|
|
displayName = (if isRocq then "Rocq " else "Coq ") + coq.version;
|
|
argv = [
|
|
"${launcher}/bin/coq-kernel"
|
|
"-f"
|
|
"{connection_file}"
|
|
];
|
|
language = "coq";
|
|
logo32 = "${logos}/logo-32x32.png";
|
|
logo64 = "${logos}/logo-64x64.png";
|
|
env = lib.listToAttrs [
|
|
{
|
|
name = if isRocq then "ROCQPATH" else "COQPATH";
|
|
value = lib.concatStringsSep ":" (
|
|
map (x: "${x}/lib/coq/${coq.coq-version}/user-contrib/") packages
|
|
);
|
|
}
|
|
{
|
|
name = "OCAMLPATH";
|
|
value = lib.concatStringsSep ":" (
|
|
map (x: "${x}/lib/ocaml/${coq.ocaml.version}/site-lib/") ([ coq.ocamlPackages.findlib ] ++ packages)
|
|
);
|
|
}
|
|
];
|
|
};
|
|
|
|
in
|
|
|
|
launcher.overrideAttrs (_oldAttrs: {
|
|
passthru = {
|
|
inherit coq-jupyter definitionWithPackages logos;
|
|
definition = definitionWithPackages [ ];
|
|
};
|
|
})
|