diff --git a/CHANGELOG.md b/CHANGELOG.md
index 817b268c70d88567f5470385756b5fe8a11f3733..c75c43fe7f025cf35116d6e18aa1307875991cc7 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 d10a4e2e0fbd02ea1f7f3cf1cf7dc5e89838015e..803dfad0547bbfa9dea989ee478f56748045f655 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 ae4b53b67e433d4ba65275ff2bde32df15d34b8e..6fe1d49525ca8b74e52f901cd7c8535fe5c2dba2 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 40405f88e5845e7c94e4e120a023cf4591cc5b69..c60d1fb3031906134819d5a848385f7944609754 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 d5fee3bf9810d75c8e0348bccfebf5d195b2ef49..28afae5567a61e2d827a556023ea8f7711306ff0 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 0000000000000000000000000000000000000000..616287552080652861483328b45947a5cc534e89
--- /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())