Merge branch 'master' into command_parameter_structure

CHANGELOG.md

@@ -2,7 +2,14 @@
 
 ## [(next version)](./README.md#for-developers)
 
+* (no changes yet)
+
+## [1.2.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.2.0-all.jar)
+
 * Added support for Java 14.
+* Added B parser version information to `:version` output.
+* Improved interrupt handling so that only the currently running command is interrupted, rather than terminating the entire kernel. This means that interrupts now no longer reset the kernel state (loaded machine, current animator state, local variables, etc.).
+* Updated ProB 2 to version 3.11.0.
 * Fixed a parse error when a line comment is used on the last line of an expression while any `:let` variables are defined.
 * Fixed detection of B machines in cells without `::load`. Previously only single-line machines were recognized.
 

README.md

@@ -14,29 +14,31 @@ See the [requirements](#requirements) and [installation instructions](#installat
 
 * Java 8 or newer
 	* Tested up to Java 14.
-* A Python 3 interpeter with Jupyter installed (`python3 -m pip install jupyter`)
-	* Tested with CPython 3.6, jupyter-core 4.4.0, jupyter-client 5.2.3, notebook 5.6.0.
-	* Newer Jupyter versions should also work.
-	* Older Jupyter versions may work, as long as they support version 5.0 of the Jupyter message protocol.
-	* The Python version does not matter, as long as it is supported by Jupyter.
+* A Python 3 interpreter with Jupyter installed
+	* Tested with CPython 3.8 and Jupyter core/Notebook 6.x.
+	* Older Python and Jupyter versions should also work (see below), but if possible please use the current versions of Python and Jupyter.
+	* This kernel requires version 5.0 of the kernel message protocol, which is supported by all versions of Jupyter (since the split from IPython, i. e. 4.x and later), as well as IPython Notebook 3.x.
+	* The Python version does not matter, as long as it is supported by the Jupyter version in use. Jupyter Notebook 6.x (the current version) supports Python 3.5 and later. Older Jupyter versions also support Python 2.7 (before Jupyter 6.0), and 3.4 and 3.3 (before Juypter 5.3.0).
 
 ## Installation
 
 ### For end users
 
-1. [Download the latest version of the kernel][current-download].
-2. If Jupyter is installed in a virtual environment, activate it.
-3. Run `java -jar <jarfile> install` to install the kernel. (`<jarfile>` is the name of the jar file that you just downloaded.)
+1. Ensure that all [requirements](#requirements) are installed.
+2. [Download the latest version of the kernel][current-download].
+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.)
 	* 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.)
-4. (Optional) The jar file can be deleted after installation.
+5. (Optional) The jar file can be deleted after installation.
 
 ### For developers
 
-1. 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).
-2. If Jupyter is installed in a virtual environment, activate it.
-3. In the root directory of the repository, run `./gradlew installKernelSpec`.
+1. Ensure that all [requirements](#requirements) are installed.
+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 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.
@@ -56,9 +58,31 @@ If the kernel was installed using `java -jar <jarfile> install`, the kernel jar
 
 After installation, start the Jupyter Notebook web interface using `jupyter notebook`. The ProB 2 kernel can be selected when creating a new notebook.
 
-You can also use the kernel with other frontends, such as `jupyter console` and `jupyter qtconsole`, by specifying `--kernel=prob2` on the command line.
+You can also use the kernel with other frontends. You may need to manually specify the ProB 2 kernel's ID (`prob2`). For example, to run the kernel using Jupyter's [console](https://jupyter-console.readthedocs.io/) and [Qt console](https://qtconsole.readthedocs.io/) frontends:
+
+```sh
+$ jupyter console --kernel=prob2
+$ jupyter qtconsole --kernel=prob2
+```
 
 For information on how to use the kernel, run the built-in `:help` command, or see the included [example notebooks](./notebooks).
 
-[current-download]: https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.1.0-all.jar
+## Citing
+
+An article about the ProB Jupyter kernel has been [published at ABZ'2020](https://link.springer.com/epdf/10.1007/978-3-030-48077-6_19?sharing_token=Nbvsl1StbEqfKGPhJwLMb_e4RwlQNchNByi7wbcMAY4yDpL76P5EGFEyHUVQToM3cE0JT8SrX5kUcY5Tx3NbNk7ZRhAullHYDeKKl9C6z3f2jS5d0JEraXScv4hxlPmpP-17XOXseltcKfZbcq05hOnhHWx78Wll4QMNCK8E115bSCQ7acchJqrow-mu5nzV) ([short link](https://rdcu.be/b4rql)).
+
+```bibtex
+@inproceedings{GelessusLeuschel:abz2020,
+	author = {David Gelessus and Michael Leuschel},
+	title = {{ProB} and {Jupyter} for Logic, Set Theory, Theoretical Computer Science and Formal Methods},
+	booktitle = {Proceedings ABZ 2020},
+	editor = "Raschke, Alexander and M{\'e}ry, Dominique and Houdek, Frank",
+	year = {2020},
+	series = {LNCS 12071},
+	pages = "248--254",
+	isbn = "978-3-030-48077-6"
+}
+```
+
+[current-download]: https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.2.0-all.jar
 [changelog]: ./CHANGELOG.md

build.gradle

@@ -9,7 +9,7 @@ plugins {
 	id("com.github.johnrengelman.shadow").version("5.2.0")
 }
 
-version = "1.1.1-SNAPSHOT"
+version = "1.2.1-SNAPSHOT"
 
 final isSnapshot = project.version.endsWith("-SNAPSHOT")
 
@@ -39,7 +39,7 @@ configurations.all {
 dependencies {
 	implementation(group: "com.google.code.gson", name: "gson", version: "2.8.6")
 	implementation(group: "com.google.guava", name: "guava", version: "28.2-jre")
-	implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "4.0.0-SNAPSHOT")
+	implementation(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.11.0")
 	implementation(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.3.0")
 	implementation(group: "org.jetbrains", name: "annotations", version: "18.0.0")
 	implementation(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
@@ -61,7 +61,10 @@ def readCurrentGitCommit() {
 	return proc.in.readLines()[0]
 }
 
+final currentGitCommit = readCurrentGitCommit()
 processResources {
+	inputs.property("project.version", project.version)
+	inputs.property("currentGitCommit", currentGitCommit)
 	filesMatching("de/prob2/jupyter/build.properties") {
 		expand(version: project.version, commit: readCurrentGitCommit())
 	}

notebooks/tests/version.ipynb

@@ -12,11 +12,11 @@
        ":version\n",
        "```\n",
        "\n",
-       "Display version info about the ProB 2 Jupyter kernel, ProB 2, and the underlying ProB CLI."
+       "Display version info about the ProB 2 Jupyter kernel and its underlying components."
       ],
       "text/plain": [
        ":version\n",
-       "Display version info about the ProB 2 Jupyter kernel, ProB 2, and the underlying ProB CLI."
+       "Display version info about the ProB 2 Jupyter kernel and its underlying components."
       ]
      },
      "execution_count": 1,
@@ -36,11 +36,12 @@
     {
      "data": {
       "text/plain": [
-       "ProB 2 Jupyter kernel: 1.0.1-SNAPSHOT (2b75217bf8bef7737632efee1ebb1ddbd8cfefe6)\n",
-       "ProB 2: 3.10.0 (0ee5d5eea6894b2899690565dfc3d9042098ce89)\n",
+       "ProB 2 Jupyter kernel: 1.1.1-SNAPSHOT (e5188664ec88fa6c381b5fec7b46ab44deaf9eb7)\n",
+       "ProB 2: 4.0.0-SNAPSHOT (489d93856139812923fae9b8e4c1297e9576b460)\n",
+       "ProB B parser: 2.9.26-SNAPSHOT (d2cd9ca3dba77bfff8c6eed9799794af899b3230)\n",
        "ProB CLI:\n",
-       "\t1.9.3-final (64afef0148d6ce70f2af5082e69269c950078133)\n",
-       "\tLast changed: Wed Feb 19 11:16:13 2020 +0100\n",
+       "\t1.10.0-nightly (907db892e8fdc604be6a15cea637d74da98bf1cb)\n",
+       "\tLast changed: Tue May 12 19:06:34 2020 +0200\n",
        "\tProlog: SICStus 4.5.1 (x86_64-darwin-17.7.0): Tue Apr  2 15:34:32 CEST 2019"
       ]
      },

src/main/java/de/prob2/jupyter/Main.java

@@ -13,13 +13,12 @@ import java.nio.file.StandardCopyOption;
 import java.security.CodeSource;
 import java.security.InvalidKeyException;
 import java.security.NoSuchAlgorithmException;
-import java.util.ArrayList;
-import java.util.List;
 import java.util.stream.Stream;
 
 import com.google.gson.Gson;
 import com.google.gson.GsonBuilder;
-import com.google.gson.annotations.SerializedName;
+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;
@@ -27,18 +26,22 @@ import com.google.inject.Stage;
 import io.github.spencerpark.jupyter.channels.JupyterConnection;
 import io.github.spencerpark.jupyter.kernel.KernelConnectionProperties;
 
+import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class Main {
-	private static final class KernelJsonData {
-		List<String> argv;
-		@SerializedName("display_name") String displayName;
-		String language;
-		
-		KernelJsonData() {
-			super();
-		}
-	}
+	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 Main() {
 		super();
@@ -110,7 +113,7 @@ public final class Main {
 			}
 		});
 		
-		final List<String> kernelJsonArgv = new ArrayList<>();
+		final JsonArray kernelJsonArgv = new JsonArray();
 		kernelJsonArgv.add("java");
 		
 		final String probHome = System.getProperty("prob.home");
@@ -126,10 +129,11 @@ public final class Main {
 		kernelJsonArgv.add("run");
 		kernelJsonArgv.add("{connection_file}");
 		
-		final Main.KernelJsonData kernelJsonData = new Main.KernelJsonData();
-		kernelJsonData.argv = kernelJsonArgv;
-		kernelJsonData.displayName = "ProB 2";
-		kernelJsonData.language = "prob";
+		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()
@@ -221,17 +225,18 @@ public final class Main {
 	}
 	
 	public static void main(final String[] args) throws IOException, InvalidKeyException, NoSuchAlgorithmException {
-		if (args.length < 1 || args.length == 1 && "--help".equals(args[0])) {
-			System.err.println("Usage: java -jar prob2-jupyter-kernel-all.jar [--help | install [--user] [JUPYTER] | createKernelSpec KERNELSPECDIR | run CONNECTIONFILE]");
-			System.err.println("--help: Prints this information.");
-			System.err.println("install: Copies the kernel into the ProB home directory, and installs the kernel in Jupyter.");
-			System.err.println("\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.");
-			System.err.println("\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.");
-			System.err.println("createKernelSpec: Creates a Jupyter kernel spec for this jar file at the given location.");
-			System.err.println("\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.");
-			System.err.println("run: Runs the kernel using the given connection file.");
-			System.err.println("\tThis option is not meant to be used manually, it is used internally when Jupyter starts the kernel.");
+		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":

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -14,6 +14,7 @@ import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 import java.util.Properties;
+import java.util.concurrent.atomic.AtomicReference;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
@@ -192,6 +193,7 @@ public final class ProBKernel extends BaseKernel {
 	private final @NotNull AnimationSelector animationSelector;
 	
 	private final @NotNull Map<@NotNull String, @NotNull Command> commands;
+	private final @NotNull AtomicReference<@Nullable Thread> currentEvalThread;
 	private final @NotNull Map<@NotNull String, @NotNull String> variables;
 	
 	private @NotNull Path currentMachineDirectory;
@@ -208,6 +210,7 @@ public final class ProBKernel extends BaseKernel {
 			.map(injector::getInstance)
 			.collect(Collectors.toMap(Command::getName, cmd -> cmd));
 		
+		this.currentEvalThread = new AtomicReference<>(null);
 		this.variables = new HashMap<>();
 		
 		this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
@@ -319,10 +322,7 @@ public final class ProBKernel extends BaseKernel {
 		return MACHINE_CODE_PATTERN.matcher(code).matches();
 	}
 	
-	@Override
-	public @Nullable DisplayData eval(final String expr) {
-		assert expr != null;
-		
+	private @Nullable DisplayData evalInternal(final @NotNull String expr) {
 		final Matcher commandMatcher = COMMAND_PATTERN.matcher(expr);
 		if (commandMatcher.matches()) {
 			// The input is a command, execute it directly.
@@ -340,6 +340,19 @@ public final class ProBKernel extends BaseKernel {
 		}
 	}
 	
+	@Override
+	public @Nullable DisplayData eval(final String expr) {
+		assert expr != null;
+		
+		this.currentEvalThread.set(Thread.currentThread());
+		
+		try {
+			return evalInternal(expr);
+		} finally {
+			this.currentEvalThread.set(null);
+		}
+	}
+	
 	@Override
 	public @Nullable DisplayData inspect(final @NotNull String code, final int at, final boolean extraDetail) {
 		// Note: We ignore the extraDetail parameter, because in practice it is always false. This is because the inspect_request messages sent by Jupyter Notebook always have their detail_level set to 0.
@@ -442,6 +455,15 @@ public final class ProBKernel extends BaseKernel {
 		this.animationSelector.getCurrentTrace().getStateSpace().kill();
 	}
 	
+	@Override
+	public void interrupt() {
+		final Thread evalThread = this.currentEvalThread.get();
+		if (evalThread != null) {
+			evalThread.interrupt();
+		}
+		this.animationSelector.getCurrentTrace().getStateSpace().sendInterrupt();
+	}
+	
 	private @NotNull List<@NotNull String> formatErrorSource(final @NotNull List<@NotNull String> sourceLines, final @NotNull ErrorItem.Location location) {
 		if (sourceLines.isEmpty()) {
 			return Collections.singletonList(this.errorStyler.primary("// Source code not known"));

src/main/java/de/prob2/jupyter/commands/VersionCommand.java

@@ -2,6 +2,7 @@ package de.prob2.jupyter.commands;
 
 import com.google.inject.Inject;
 
+import de.be4.classicalb.core.parser.BParser;
 import de.prob.Main;
 import de.prob.animator.command.GetVersionCommand;
 import de.prob.statespace.AnimationSelector;
@@ -43,7 +44,7 @@ public final class VersionCommand implements Command {
 	
 	@Override
 	public @NotNull String getShortHelp() {
-		return "Display version info about the ProB 2 Jupyter kernel, ProB 2, and the underlying ProB CLI.";
+		return "Display version info about the ProB 2 Jupyter kernel and its underlying components.";
 	}
 	
 	@Override
@@ -61,6 +62,10 @@ public final class VersionCommand implements Command {
 		sb.append(Main.getVersion());
 		sb.append(" (");
 		sb.append(Main.getGitSha());
+		sb.append(")\nProB B parser: ");
+		sb.append(BParser.getVersion());
+		sb.append(" (");
+		sb.append(BParser.getGitSha());
 		sb.append(")\nProB CLI:");
 		final GetVersionCommand cmd = new GetVersionCommand();
 		this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);