split demo into slides

inpefess · Sep 15, 2022 · 76fede7 · 76fede7
1 parent 257c599
commit 76fede7
Show file tree

Hide file tree

Showing 3 changed files with 245 additions and 40 deletions.
diff --git a/examples/cicm2022_example.ipynb b/examples/cicm2022_example.ipynb
@@ -3,7 +3,12 @@
   {
    "cell_type": "markdown",
    "id": "114570df-02b2-4996-9901-5515a9497f2b",
-   "metadata": {},
+   "metadata": {
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
+   },
    "source": [
     "<pre>\n",
     "Copyright 2022 Boris Shminke\n",
@@ -30,13 +35,14 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "tags": []
    },
    "outputs": [],
    "source": [
-    "# since both Jupyter and `isabelle-client` use `asyncio` we need to enable\n",
-    "# nested event loops. We don't need that when using `isabelle-client` from\n",
-    "# Python scripts outside Jupyter\n",
+    "# since both Jupyter and `isabelle-client` use `asyncio` we need to\n",
+    "# enable nested event loops. We don't need that when using\n",
+    "# `isabelle-client` from Python scripts outside Jupyter\n",
     "import nest_asyncio\n",
     "\n",
     "nest_asyncio.apply()"
@@ -93,7 +99,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -202,7 +212,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -284,7 +298,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -322,7 +340,8 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -360,7 +379,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [],
    "source": [
@@ -385,7 +408,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -433,7 +460,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -512,7 +543,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -533,7 +568,9 @@
    ],
    "source": [
     "# the messages from `sledgehammer` have an easily parsable format\n",
-    "messages = [message[\"message\"] for message in data[\"nodes\"][0][\"messages\"]]\n",
+    "messages = [\n",
+    "    message[\"message\"] for message in data[\"nodes\"][0][\"messages\"]\n",
+    "]\n",
     "messages"
    ]
   },
@@ -578,7 +615,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -612,7 +653,8 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -649,7 +691,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -696,7 +742,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -739,7 +789,11 @@
     "collapsed": false,
     "jupyter": {
      "outputs_hidden": false
-    }
+    },
+    "slideshow": {
+     "slide_type": "slide"
+    },
+    "tags": []
    },
    "outputs": [
     {
@@ -813,7 +867,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.8.10"
+   "version": "3.10.4"
   },
   "name": "interactive_example.ipynb"
  },