From d4e70d0724619940656a9f797b65034a1b06a6ca Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 17 Oct 2022 14:58:47 +0200
Subject: [PATCH] Rewrite installation process to be fully Python-based

This allows using Jupyter's Python API to install the kernel. It returns
the location of the newly installed kernelspec, which allows copying the
kernel jar file into the kernelspec directory instead of the ProB home
directory. This is cleaner and allows fully uninstalling the kernel
using a single command.

Additionally, we no longer depend on Guice to generate the kernel.json
(we use Python's json module instead) and no longer use the deprecated
Main.getProBDirectory method from ProB 2.

The Python script for installing the kernel is bundled into the kernel
jar as __main__.py, which allows running the jar file using Python. The
installation can still be started using Java, in which case the jar
re-executes itself using Python. Yes, this is a little bit cursed, but
it works.
---
 CHANGELOG.md                             |   1 +
 Makefile                                 |  10 +-
 README.md                                |  15 +-
 build.gradle                             |  30 +---
 src/main/java/de/prob2/jupyter/Main.java | 219 ++++-------------------
 src/main/resources/__main__.py           | 138 ++++++++++++++
 6 files changed, 186 insertions(+), 227 deletions(-)
 create mode 100644 src/main/resources/__main__.py

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 817b268..c75c43f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,7 @@
 * Updated ProB 2 to version 4.0.0-SNAPSHOT.
 * Added position information to formula evaluation errors (e. g. type or well-definedness errors).
 * Changed `:exec` and `:init` to automatically set up constants and initialize the machine if necessary. Previously this caused an error "Machine is not initialised".
+* Rewrote the kernel installation code in Python. This is mostly an internal change and shouldn't affect most users. As a side effect, uninstalling the kernel is now simpler and requires no extra steps after `jupyter kernelspec remove`.
 * Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
 
 ## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
diff --git a/Makefile b/Makefile
index d10a4e2..803dfad 100644
--- a/Makefile
+++ b/Makefile
@@ -5,14 +5,14 @@ rebuild:
 install:
 	./gradlew installKernelSpec
 USERNAME=
-PHOME=/Users/$(USERNAME)/git_root/prob_prolog
-JUPYTER=/Users/$(USERNAME)/opt/miniconda3/bin/jupyter
-#JUPYTER=/Users/$(USERNAME)/opt/miniconda3/envs/py10/bin/jupyter
+PROB_HOME=/Users/$(USERNAME)/git_root/prob_prolog
+PYTHON=/Users/$(USERNAME)/opt/miniconda3/bin/python3
+#PYTHON=/Users/$(USERNAME)/opt/miniconda3/envs/py10/bin/python3
 installph:
-	./gradlew -PprobHome=$(PHOME) -PjupyterCommand=$(JUPYTER) installKernelSpec
+	./gradlew -PpythonCommand=$(PYTHON) installKernelSpec
 installphuser:
     echo "Installing for user, so that, e.g., VSCode sees the kernel"
-	./gradlew -PprobHome=$(PHOME) -PjupyterCommand=$(JUPYTER) -PkernelspecUserInstall=true installKernelSpec
+	./gradlew -PpythonCommand=$(PYTHON) -PkernelspecUserInstall=true installKernelSpec
 
 console:
 	jupyter console --kernel prob2
diff --git a/README.md b/README.md
index ae4b53b..6fe1d49 100644
--- a/README.md
+++ b/README.md
@@ -31,10 +31,9 @@ See the [requirements](#requirements) and [installation instructions](#installat
 1. Ensure that all [requirements](#requirements) are installed.
 2. [Download the latest version of the kernel](#downloads).
 3. If Jupyter is installed in a virtual environment, activate it.
-4. Run `java -jar <jarfile> install` to install the kernel. (`<jarfile>` is the name of the jar file that you just downloaded.)
+4. Run `python3 <jarfile> install` to install the kernel. (`<jarfile>` is the name of the jar file that you just downloaded. Yes, you need to run the jar file using Python.)
 	* If you get a permission error when installing the kernel spec, add the option `--user` after `install`. This will install the kernel spec into your user home instead of the Python install directory (which may not be writable).
-	* This assumes that Jupyter can be called using the command `jupyter`. To use a different command in place of `jupyter`, pass it as an argument after `install`, e. g. `java -jar <jarfile> install /path/to/jupyter`.
-	* To use a different ProB home directory than the default, pass `-Dprob.home=/path/to/prob/home` before the `-jar` option. (The path must be absolute.)
+	* To use a different ProB home directory than the default, set the environment variable `PROB_HOME` to the desired path. (The path must be absolute.)
 5. (Optional) The jar file can be deleted after installation.
 
 ### For developers
@@ -43,10 +42,10 @@ See the [requirements](#requirements) and [installation instructions](#installat
 2. Clone this repository (`git clone https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel.git`) or download an archive from [the repository page](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel).
 3. If Jupyter is installed in a virtual environment, activate it.
 4. In the root directory of the repository, run `./gradlew installKernelSpec`.
-	* If Jupyter is installed in a virtual environment and you get an error that the `jupyter` command could not be found/executed, try running the Gradle command with the `--no-daemon` option. This ensures that Gradle sees all environment changes performed by the activation of the virtual environment.
+	* If Jupyter is installed in a virtual environment and you get an error that Jupyter could not be found, try running the Gradle command with the `--no-daemon` option. This ensures that Gradle sees all environment changes performed by the activation of the virtual environment.
 	* If you get a permission error when installing the kernel spec, pass `-PkernelspecUserInstall=true` to the `./gradlew` command. This will install the kernel spec into your user home instead of the Python install directory (which may not be writable).
-	* This assumes that Jupyter can be called using the command `jupyter`. To use a different command in place of `jupyter`, you can pass `-PjupyterCommand=/path/to/jupyter` to the `./gradlew` command.
-	* To use a different ProB home directory than the default, pass `-PprobHome=/path/to/prob/home` to the `./gradlew` command. (The path must be absolute.)
+	* This assumes that Python can be called using the command `python3`. To use a different command in place of `python3`, you can pass `-PpythonCommand=/path/to/python` to the `./gradlew` command.
+	* To use a different ProB home directory than the default, set the environment variable `PROB_HOME` to the desired path. (The path must be absolute.)
 
 ## Updating
 
@@ -56,7 +55,9 @@ To update from an older version of the kernel, follow the installation instructi
 
 To remove the kernel from Jupyter, run `jupyter kernelspec remove prob2`.
 
-If the kernel was installed using `java -jar <jarfile> install`, the kernel jar has been copied into `prob2-<version>/jupyter` in your ProB home directory (`~/.prob` by default). To uninstall the kernel completely, delete this `jupyter` folder.
+For previous versions of the kernel (1.3.0 and older),
+you may also need to manually delete the kernel jar file from the ProB home directory (under `~/.prob` by default).
+It should be located in a `jupyter` subdirectory.
 
 ## Usage
 
diff --git a/build.gradle b/build.gradle
index 40405f8..c60d1fb 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,4 +1,3 @@
-import java.nio.file.Paths
 import java.util.concurrent.TimeUnit
 
 plugins {
@@ -37,7 +36,6 @@ configurations.all {
 
 dependencies {
 	implementation(group: "ch.qos.logback", name: "logback-classic", version: "1.2.10")
-	implementation(group: "com.google.code.gson", name: "gson", version: "2.8.9")
 	implementation(group: "com.google.guava", name: "guava", version: "31.0.1-jre")
 	implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
 	implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
@@ -76,31 +74,11 @@ application {
 	mainClass = "de.prob2.jupyter.Main"
 }
 
-final KERNEL_SPEC_OUTPUT_PATH = project.buildDir.toPath().resolve(Paths.get("kernelspec"))
-
-task createKernelSpec(type: JavaExec) {
-	dependsOn = [shadowJar]
-	mainClass = application.mainClass
-	args = ["createKernelSpec", KERNEL_SPEC_OUTPUT_PATH.toString()]
-	classpath(shadowJar.archiveFile)
-	if (project.hasProperty("probHome")) {
-		systemProperty("prob.home", project.probHome)
-	}
-	outputs.dir(KERNEL_SPEC_OUTPUT_PATH.toFile())
-	doFirst {
-		delete(KERNEL_SPEC_OUTPUT_PATH)
-		mkdir(KERNEL_SPEC_OUTPUT_PATH)
-	}
-}
-
 task installKernelSpec(type: Exec) {
-	dependsOn = [createKernelSpec]
-	executable = project.hasProperty("jupyterCommand") ? project.jupyterCommand : "jupyter"
-	def installFlag
+	dependsOn = [shadowJar]
+	executable = project.hasProperty("pythonCommand") ? project.pythonCommand : "python3"
+	args = [shadowJar.archiveFile.get().asFile, "--jar-path=" + shadowJar.archiveFile.get().asFile, "install"]
 	if (project.hasProperty("kernelspecUserInstall") && project.kernelspecUserInstall == "true") {
-		installFlag = "--user"
-	} else {
-		installFlag = "--sys-prefix"
+		args << "--user"
 	}
-	args = ["kernelspec", "install", installFlag, "--name=prob2", KERNEL_SPEC_OUTPUT_PATH.toString()]
 }
diff --git a/src/main/java/de/prob2/jupyter/Main.java b/src/main/java/de/prob2/jupyter/Main.java
index d5fee3b..28afae5 100644
--- a/src/main/java/de/prob2/jupyter/Main.java
+++ b/src/main/java/de/prob2/jupyter/Main.java
@@ -1,24 +1,18 @@
 package de.prob2.jupyter;
 
 import java.io.IOException;
-import java.io.InputStream;
-import java.io.UncheckedIOException;
-import java.io.Writer;
 import java.net.URISyntaxException;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.nio.file.Paths;
-import java.nio.file.StandardCopyOption;
 import java.security.CodeSource;
 import java.security.InvalidKeyException;
 import java.security.NoSuchAlgorithmException;
-import java.util.stream.Stream;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
 
-import com.google.gson.Gson;
-import com.google.gson.GsonBuilder;
-import com.google.gson.JsonArray;
-import com.google.gson.JsonObject;
 import com.google.inject.Guice;
 import com.google.inject.Injector;
 import com.google.inject.Stage;
@@ -30,18 +24,8 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class Main {
-	private static final @NotNull String USAGE_TEXT = "Usage: java -jar prob2-jupyter-kernel-all.jar [--help | install [--user] [JUPYTER] | createKernelSpec KERNELSPECDIR | run CONNECTIONFILE]";
-	private static final @NotNull String FULL_HELP_TEXT = "--help: Prints this information.\n"
-		+ "\n"
-		+ "install: Copies the kernel into the ProB home directory, and installs the kernel in Jupyter.\n"
-		+ "\tBy default the kernel spec is installed into the sys.prefix of Jupyter's Python installation. If the sys.prefix is not writable (for example when using the system Python installation instead of a virtual environment), the --user flag can be used to install the kernel only for the current user.\n"
-		+ "\tBy default the command \"jupyter\" is used to install the kernel. If the kernel should be installed in a different Jupyter installation, a different Jupyter command can be passed as an argument to the install command.\n"
-		+ "\n"
-		+ "createKernelSpec: Creates a Jupyter kernel spec for this jar file at the given location.\n"
-		+ "\tThis option is for advanced users or developers, who don't want the jar file to be copied, or who want to install the kernel spec manually.\n"
-		+ "\n"
-		+ "run: Runs the kernel using the given connection file.\n"
-		+ "\tThis option is not meant to be used manually, it is used internally when Jupyter starts the kernel.";
+	private static final @NotNull String GENERIC_PYTHON_ERROR_MESSAGE = "Try running the installation directly using Python, e. g.:\n"
+		+ "$ python3 prob2-jupyter-kernel-all.jar install";
 	
 	private Main() {
 		super();
@@ -63,99 +47,31 @@ public final class Main {
 			final CodeSource cs = Main.class.getProtectionDomain().getCodeSource();
 			if (cs == null) {
 				System.err.println("Unable to determine location of kernel jar file (CodeSource is null)");
+				System.err.println(GENERIC_PYTHON_ERROR_MESSAGE);
 				throw die(1);
 			}
 			return Paths.get(cs.getLocation().toURI());
 		} catch (final RuntimeException | URISyntaxException e) {
 			System.err.println("Unable to determine location of kernel jar file");
+			System.err.println(GENERIC_PYTHON_ERROR_MESSAGE);
 			e.printStackTrace();
 			throw die(1, e);
 		}
 	}
 	
-	private static Path getDestPath(final Path jarPath) {
-		return Paths.get(de.prob.Main.getProBDirectory(), "jupyter", jarPath.getFileName().toString());
-	}
-	
-	private static void copyJar(final Path jarPath, final Path destPath) {
-		System.out.println("Installing kernel jar file...");
-		System.out.println("Path to kernel jar file: " + jarPath);
-		System.out.println("Kernel jar will be copied to: " + destPath);
-		try {
-			Files.createDirectories(destPath.getParent());
-		} catch (final IOException e) {
-			System.err.println("Failed to create destination directory");
-			e.printStackTrace();
-			throw die(1, e);
-		}
-		try {
-			Files.copy(jarPath, destPath, StandardCopyOption.REPLACE_EXISTING);
-		} catch (final IOException e) {
-			System.err.println("Failed to copy kernel jar file");
-			e.printStackTrace();
-			throw die(1, e);
-		}
-		System.out.println("Kernel jar file installed");
-	}
-	
-	private static void createKernelSpec(final Path jarPath, final Path kernelSpecDir) {
-		System.out.println("Creating kernel spec...");
-		System.out.println("Path to kernel jar file: " + jarPath);
-		System.out.println("Kernel spec directory: " + kernelSpecDir);
-		Stream.of("kernel.js", "logo-32x32.png", "logo-64x64.png").forEach(name -> {
-			System.out.println("Extracting: " + name);
-			try (final InputStream is = Main.class.getResourceAsStream("kernelspecfiles/" + name)) {
-				Files.copy(is, kernelSpecDir.resolve(name));
-			} catch (final IOException e) {
-				System.err.println("Failed to extract kernel spec file: " + name);
-				e.printStackTrace();
-				throw die(1, e);
-			}
-		});
-		
-		final JsonArray kernelJsonArgv = new JsonArray();
-		kernelJsonArgv.add("java");
-		
-		final String probHome = System.getProperty("prob.home");
-		if (probHome != null) {
-			System.out.println("prob.home is set, adding a corresponding prob.home defintion to kernel.json: " + probHome);
-			kernelJsonArgv.add("-Dprob.home=" + probHome);
-		} else {
-			System.out.println("prob.home is not set, not adding a prob.home definition to kernel.json");
-		}
-		
-		kernelJsonArgv.add("-jar");
-		kernelJsonArgv.add(jarPath.toString());
-		kernelJsonArgv.add("run");
-		kernelJsonArgv.add("{connection_file}");
-		
-		final JsonObject kernelJsonData = new JsonObject();
-		kernelJsonData.add("argv", kernelJsonArgv);
-		kernelJsonData.addProperty("display_name", "ProB 2");
-		kernelJsonData.addProperty("language", "prob");
-		kernelJsonData.addProperty("interrupt_mode", "message");
-		
-		final Gson gson = new GsonBuilder()
-			.setPrettyPrinting()
-			.serializeNulls()
-			.create();
-		
-		System.out.println("Creating kernel.json");
-		try (final Writer writer = Files.newBufferedWriter(kernelSpecDir.resolve("kernel.json"))) {
-			gson.toJson(kernelJsonData, writer);
-		} catch (final IOException e) {
-			System.err.println("Failed to create kernel.json");
-			e.printStackTrace();
-			throw die(1, e);
-		}
-		System.out.println("Kernel spec created");
-	}
-	
-	private static void installKernelSpec(final String jupyterCommand, final boolean userInstall, final Path kernelSpecDir) {
-		System.out.println("Installing kernel spec...");
-		System.out.println("Jupyter command: " + jupyterCommand);
-		System.out.println("Kernel spec directory: " + kernelSpecDir);
-		final ProcessBuilder pb = new ProcessBuilder(jupyterCommand, "kernelspec", "install", userInstall ? "--user" : "--sys-prefix", "--name=prob2", kernelSpecDir.toString());
+	/**
+	 * Run the install script (__main__.py) bundled inside the jar file.
+	 * This makes use of Python's zipapp support
+	 * and the fact that jar files are valid zip files.
+	 * 
+	 * @param args arguments to pass to __main__.py
+	 */
+	private static void runInstallScript(final String[] args) {
+		final List<String> command = new ArrayList<>();
+		command.add("python3");
+		command.add(getJarPath().toString());
+		command.addAll(Arrays.asList(args));
+		final ProcessBuilder pb = new ProcessBuilder(command);
 		pb.redirectInput(ProcessBuilder.Redirect.INHERIT);
 		pb.redirectOutput(ProcessBuilder.Redirect.INHERIT);
 		pb.redirectError(ProcessBuilder.Redirect.INHERIT);
@@ -163,7 +79,8 @@ public final class Main {
 		try {
 			pythonProcess = pb.start();
 		} catch (final IOException e) {
-			System.err.println("Failed to install kernel spec");
+			System.err.println("Failed to start Python to install the kernel");
+			System.err.println(GENERIC_PYTHON_ERROR_MESSAGE);
 			e.printStackTrace();
 			throw die(1, e);
 		}
@@ -178,37 +95,9 @@ public final class Main {
 		}
 		if (statusCode != 0) {
 			System.err.println("Python exited with status " + statusCode);
+			System.err.println(GENERIC_PYTHON_ERROR_MESSAGE);
 			throw die(1);
 		}
-		System.out.println("Kernel spec installed");
-	}
-	
-	private static void install(final String jupyterCommand, final boolean userInstall) {
-		final Path jarPath = getJarPath();
-		final Path destPath = getDestPath(jarPath);
-		copyJar(jarPath, destPath);
-		try {
-			final Path kernelSpecDir = Files.createTempDirectory("prob2kernelspec");
-			createKernelSpec(destPath, kernelSpecDir);
-			installKernelSpec(jupyterCommand, userInstall, kernelSpecDir);
-			try (final Stream<Path> contents = Files.list(kernelSpecDir)) {
-				contents.forEach(path -> {
-					try {
-						Files.delete(path);
-					} catch (final IOException e) {
-						throw new UncheckedIOException(e);
-					}
-				});
-			}
-			Files.delete(kernelSpecDir);
-		} catch (final IOException | UncheckedIOException e) {
-			System.err.println("Failed to create kernel spec");
-			e.printStackTrace();
-			throw die(1, e);
-		}
-		System.out.println("The ProB 2 Jupyter kernel has been installed.");
-		System.out.println("To use it, start Jupyter Notebook and select \"ProB 2\" when creating a new notebook.");
-		System.out.println("This jar file can be safely deleted after installation.");
 	}
 	
 	private static void startKernel(final Path connectionFile) throws IOException, NoSuchAlgorithmException, InvalidKeyException {
@@ -224,63 +113,15 @@ public final class Main {
 	}
 	
 	public static void main(final String[] args) throws IOException, InvalidKeyException, NoSuchAlgorithmException {
-		if (args.length < 1) {
-			System.err.println(USAGE_TEXT);
-			System.err.println();
-			System.err.println("To install the kernel, run: java -jar prob2-jupyter-kernel-all.jar install");
-			System.err.println();
-			System.err.println("For a full description of all options, run: java -jar prob2-jupyter-kernel-all.jar --help");
-			throw die(2);
-		} else if (args.length == 1 && "--help".equals(args[0])) {
-			System.out.println(USAGE_TEXT);
-			System.out.println();
-			System.out.println(FULL_HELP_TEXT);
-			throw die(0);
-		}
-		switch (args[0]) {
-			case "install":
-				final boolean userInstall = args.length > 1 && "--user".equals(args[1]);
-				final String jupyterCommand;
-				if (userInstall) {
-					if (args.length > 3) {
-						System.err.println("install --user expects at most one argument, not " + (args.length-2));
-						System.err.println("Use --help for more info.");
-						throw die(2);
-					}
-					jupyterCommand = args.length > 2 ? args[2] : "jupyter";
-				} else {
-					if (args.length > 2) {
-						System.err.println("install expects at most one argument, not " + (args.length-1));
-						System.err.println("Use --help for more info.");
-						throw die(2);
-					}
-					jupyterCommand = args.length > 1 ? args[1] : "jupyter";
-				}
-				install(jupyterCommand, userInstall);
-				break;
-			
-			case "createKernelSpec":
-				if (args.length != 2) {
-					System.err.println("createKernelSpec expects exactly one argument, not " + (args.length-1));
-					System.err.println("Use --help for more info.");
-					throw die(2);
-				}
-				createKernelSpec(getJarPath(), Paths.get(args[1]));
-				break;
-			
-			case "run":
-				if (args.length != 2) {
-					System.err.println("run expects exactly one argument, not " + (args.length-1));
-					System.err.println("Use --help for more info.");
-					throw die(2);
-				}
-				startKernel(Paths.get(args[1]));
-				break;
-			
-			default:
-				System.err.println("Unknown subcommand: " + args[0]);
+		if ("run".equals(args[0])) {
+			if (args.length != 2) {
+				System.err.println("run expects exactly one argument, not " + (args.length-1));
 				System.err.println("Use --help for more info.");
 				throw die(2);
+			}
+			startKernel(Paths.get(args[1]));
+		} else {
+			runInstallScript(args);
 		}
 	}
 }
diff --git a/src/main/resources/__main__.py b/src/main/resources/__main__.py
new file mode 100644
index 0000000..6162875
--- /dev/null
+++ b/src/main/resources/__main__.py
@@ -0,0 +1,138 @@
+# Installer script for the ProB 2 Jupyter kernel.
+# This script can be run by executing the kernel jar file with Python.
+# This makes use of Python's zipapp support
+# and the fact that jar files are valid zip files.
+
+
+import sys
+
+
+if sys.version_info < (2, 7):
+	sys.stderr.write("ERROR: This Python installation is too old! At least Python 2.7 is required.\n")
+	sys.stderr.write("ERROR: You are using Python " + str(sys.version_info[0]) + "." + str(sys.version_info[1]) + " installed at " + sys.executable + "\n")
+	sys.exit(1)
+
+
+import argparse
+import io
+import json
+import logging
+import os.path
+import shutil
+import tempfile
+import zipfile
+
+
+KERNELSPEC_FILES = [
+	"kernel.js",
+	"logo-32x32.png",
+	"logo-64x64.png",
+]
+
+logger = logging.getLogger(__name__)
+
+
+def create_kernel_json(jar_path, prob_home, dest_dir):
+	with io.open(os.path.join(dest_dir, "kernel.json"), "w", encoding="utf-8") as f:
+		kernel_argv = ["java"]
+		if prob_home is not None:
+			kernel_argv.append("-Dprob.home=" + prob_home)
+		kernel_argv += ["-jar", jar_path, "run", "{connection_file}"]
+		
+		kernel_json = {
+			"argv": kernel_argv,
+			"display_name": "ProB 2",
+			"language": "prob",
+			"interrupt_mode": "message",
+		}
+		json.dump(kernel_json, f, ensure_ascii=False, indent=4)
+
+
+def create_kernelspec(jar_path, prob_home, dest_dir):
+	create_kernel_json(jar_path, prob_home, dest_dir)
+	
+	with zipfile.ZipFile(jar_path) as zf:
+		for file in KERNELSPEC_FILES:
+			with zf.open("de/prob2/jupyter/kernelspecfiles/" + file) as fin:
+				with io.open(os.path.join(dest_dir, file), "wb") as fout:
+					shutil.copyfileobj(fin, fout)
+
+
+def main():
+	logging.basicConfig(
+		format="%(levelname)s: %(message)s",
+		level=logging.INFO,
+	)
+	
+	ap = argparse.ArgumentParser(
+		description="To install the kernel, run: python3 %(prog)s install",
+		add_help=False,
+	)
+	
+	ap.add_argument("--help", action="help")
+	ap.add_argument("--jar-path", help="Run the kernel jar using the specified fixed path (this disables copying the jar into the kernelspec directory)")
+	
+	subs = ap.add_subparsers(dest="subcommand")
+	
+	ap_create = subs.add_parser("createKernelSpec", help="Generate a kernelspec for this kernel without installing it")
+	ap_create.add_argument("destination", help="Name of the directory into which to generate the kernelspec (the directory must exist already and should be empty)")
+	
+	ap_install = subs.add_parser("install", help="Install this kernel")
+	ap_install.add_argument("--user", action="store_true", help="Install to the per-user kernel registry")
+	ap_install.add_argument("--prefix", help="Install to a different prefix than the default")
+	
+	ns = ap.parse_args()
+	
+	if ns.jar_path is None:
+		jar_path = sys.argv[0]
+	else:
+		jar_path = ns.jar_path
+	
+	prob_home = os.environ.get("PROB_HOME", None)
+	
+	if ns.subcommand is None:
+		logger.error("Missing subcommand")
+		logger.info("To install the kernel, run: python3 %s install", os.path.basename(sys.argv[0]))
+		logger.info("For detailed help, run: python3 %s --help", os.path.basename(sys.argv[0]))
+		sys.exit(2)
+	elif ns.subcommand == "createKernelSpec":
+		create_kernelspec(jar_path, prob_home, ns.destination)
+	elif ns.subcommand == "install":
+		if ns.prefix is None and not ns.user:
+			ns.prefix = sys.prefix
+		
+		try:
+			from jupyter_client import kernelspec
+		except ImportError:
+			logger.error("This Python installation doesn't have Jupyter installed!")
+			logger.error("You are using Python %d.%d installed at %s", sys.version_info[0], sys.version_info[1], sys.executable)
+			logger.error("%s", sys.exc_info()[1])
+			sys.exit(1)
+		
+		temp_dir = tempfile.mkdtemp()
+		try:
+			create_kernelspec(jar_path, prob_home, temp_dir)
+			destination = kernelspec.KernelSpecManager().install_kernel_spec(temp_dir, "prob2", user=ns.user, prefix=ns.prefix)
+		finally:
+			shutil.rmtree(temp_dir)
+		
+		if not ns.jar_path:
+			# If the user didn't override the jar path,
+			# copy the jar into the installed kernelspec directory
+			# and adjust argv in kernel.json accordingly.
+			installed_jar_path = os.path.join(destination, "prob2-jupyter-kernel-all.jar")
+			shutil.copyfile(jar_path, installed_jar_path)
+			create_kernelspec(installed_jar_path, prob_home, destination)
+		
+		logger.info("The ProB 2 Jupyter kernel has been installed successfully.")
+		logger.info('To use it, start Jupyter Notebook and select "ProB 2" when creating a new notebook.')
+		if not ns.jar_path:
+			logger.info("This jar file can be safely deleted after installation.")
+	else:
+		raise AssertionError("Subcommand not handled: " + ns.subcommand)
+	
+	sys.exit(0)
+
+
+if __name__ == "__main__":
+	sys.exit(main())
-- 
GitLab