coq_kernel: init at 1.6.0

{ lib

, stdenv

, callPackage

, runCommand

, makeWrapper

, coq

, imagemagick

, python3

}:

# 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 notebook:

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

let

  python = python3.withPackages (ps: [ ps.traitlets ps.jupyter_core ps.ipykernel (callPackage ./kernel.nix {}) ]);

  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

  '';

in

rec {

  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

  '';

  definition = definitionWithPackages [];

  definitionWithPackages = packages: {

    displayName = "Coq " + coq.version;

    argv = [

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

      "-f"

      "{connection_file}"

    ];

    language = "coq";

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

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

    env = {

      COQPATH = lib.concatStringsSep ":" (map (x: "${x}/lib/coq/${coq.coq-version}/user-contrib/") packages);

    };

  };

}

{ lib

, fetchFromGitHub

, python3

, coq

}:

python3.pkgs.buildPythonPackage rec {

  pname = "coq-jupyter";

  version = "1.6.0";

  src = fetchFromGitHub {

    owner = "EugeneLoy";

    repo = "coq_jupyter";

    rev = "v${version}";

    sha256 = "sha256-+Pp51cxeqjg5MW4CEccNWVjNcY9iyFNATIEage9RWJ0=";

  };

  propagatedBuildInputs = (with python3.pkgs; [ ipykernel future ]) ++ [ coq ];

  nativeBuildInputs = [ coq ];

  doCheck = false;

  meta = with lib; {

    homepage = "https://github.com/EugeneLoy/coq_jupyter";

    description = "Jupyter kernel for Coq";

    license = licenses.asl20;

    maintainers = with maintainers; [ thomasjm ];

  };

}

  coq2html = callPackage ../tools/typesetting/coq2html { };

  coq-kernel = callPackage ../applications/editors/jupyter-kernels/coq { };

  cryptoverif = callPackage ../applications/science/logic/cryptoverif { };

  crypto-org-wallet = callPackage ../applications/blockchains/crypto-org-wallet { };