coq-kernel: fix breakage from Python 3 update and handle Rocq update (#439791)

{

  lib,

  stdenv,

  callPackage,

  runCommand,

  makeWrapper,

  coq,

  imagemagick,

  python3,

  python312,

}:

# Jupyter console:

# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel coq-kernel.definition'

# Jupyter console with packages:

# nix run --impure --expr 'with import <nixpkgs> {}; jupyter-console.withSingleKernel (coq-kernel.definitionWithPackages [coqPackages.bignums])'

# 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

  python = python3.withPackages (ps: [

  # 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

    (callPackage ./kernel.nix { })

    coq-jupyter

  ]);

  logos = runCommand "coq-logos" { buildInputs = [ imagemagick ]; } ''

    mkdir -p $out

    convert ${coq.src}/ide/coqide/coq.png -resize 32x32 $out/logo-32x32.png

    convert ${coq.src}/ide/coqide/coq.png -resize 64x64 $out/logo-64x64.png

  '';

  # 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

    '';

rec {

  launcher =

    runCommand "coq-kernel-launcher"

      {

          --suffix PATH : ${coq}/bin

      '';

  definition = definitionWithPackages [ ];

  definitionWithPackages = packages: {

    displayName = "Coq " + coq.version;

    displayName = (if isRocq then "Rocq " else "Coq ") + coq.version;

    argv = [

      "${launcher}/bin/coq-kernel"

      "-f"

    language = "coq";

    logo32 = "${logos}/logo-32x32.png";

    logo64 = "${logos}/logo-64x64.png";

    env = {

      COQPATH = lib.concatStringsSep ":" (

    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 [ ];

  };

}

})