Interactive Proof Presentations with Cobra

TL;DR

Cobra is an innovative proof presentation framework that combines advanced presentation tools with an interactive theorem prover, enabling live, interactive, and verifiable formalized mathematics presentations.

Contribution

It introduces Cobra, a novel system that integrates live theorem proving with interactive presentation technology for formalized mathematics.

Findings

Live proof checking during presentations enhances accuracy.

Audience interaction allows real-time modifications to proofs.

Cobra facilitates engaging and verifiable mathematical talks.

Abstract

We present Cobra, a modern proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows for live changes both by the presenter and the audience.

Figures

Tables

Table 1. Table 1 : Some of the settings available through cobra.conf

title	display title of the presentation
language	main language of the presentation
theme.slides	main style sheet that should be used to render the slides
theme.code	main style sheet that should be used to render code snippets
binding.interface	network interface to bind the server on (default localhost)
binding.port	port under which the server will be available (default 8080)
reveal.transition	the default transition between slides (e.g. slide, fade, none)
env.isabelle_home	environment variable to be picked up by language servers

Full text

1 Introduction

Presenting formalized mathematical proofs is a challenge by itself. Formalized proofs, by their very nature, tend to be lengthy, as every side condition and assumption has to be tackled, and often the amount of proof text devoted to the main argument is small in relation to those necessary but tedious side issues. Further, the actual proof usually contains technical information such as setting up the syntactic machinery and automatic proof assistance of the prover, which is not necessary for the comprehension of the mathematical argument, but crucial if the audience wants to rerun the proof in the actual prover. Thus, when presenting formalized proofs to students, fellow researchers, or other audiences, we only present a view on the actual proof text. This view only contains excerpts of the original proof, and is constructed manually; it is left to the punctiliousness of the presenter to not introduce errors. The correlation between the presentation and the actual proof text is left to the critical audience to verify, as the resulting view cannot be checked by the prover anymore. Further, when made with traditional presentation aids (such as PowerPoint, LaTeX, or writing on plain old blackboards) these presentations are not interactive — we cannot easily change them during the presentation, e.g. to demonstrate why a particular approach will not prove the desired goal. However, a proof made with an interactive theorem prover is an active document and should be treated, and presented, as such. The stop-gap measure often used up to now has been to switch back and forth between the presentation and the actual running prover, but the resulting change of focus makes it hard to follow the proof, and as the whole proof text is shown, the audience is potentially overwhelmed with technical details. Another fix is to animate the presentation manually by means of PDF overlays or PowerPoint animations, but this is inflexible, error-prone and cumbersome.

Fortunately, the advances of modern web technologies have opened up new ways of presentation, which allow us to treat a proof as an active document rather than an inanimate piece of PDF. Tools such as reveal.js implement presentations as active documents, and thus it seems logical to leverage this technology for interactive provers. In this paper, we present Cobra, an integrated presentation environment for interactive proofs and code. Cobra allows us to declaratively define interactive slides containing Isabelle theories (or snippets from a theory), LaTeX-style formulae and program code. The intriguing aspect about these slides is that they can not only be presented with annotated semantic information provided by the underlying prover (or compiler in the case of code), but also the content can be altered (or completed), resulting in updated semantic annotations. This way, the presenter can develop the proof in front of, and even in interaction with, the audience, instead of following a strict predetermined path.

The paper is structured as follows: Section 2 describes how to work with Cobra from a users perspective. Section 3 sketches the architecture of the project, and Section 4 briefly discusses related work. We conclude in Section 5 by describing proposed use cases and providing an outlook onto future work.

2 Presenting with Cobra

Creating slides is one of the most time consuming tasks in the preparation of a lecture or a talk. Thus it should involve no additional overhead, to allow the speaker to focus on content rather than technical details. Cobra aims to be even simpler than presenting with the LaTeX beamer class but a lot more powerful. It comes as a self-contained command line tool111The binary can be obtained from http://www.flatmap.net/cobra for all major operating systems, or alternatively as source code from https://github.com/flatmap/cobra/., and supports Isabelle/HOL, Scala and Haskell as well as LaTeX-style formulae out of the box, and furthermore can be extended to suit individual needs. The only strong prerequisite is an active installation of Java 8 or above. To check whether the system setup supports interactive presentation of a specific language, there is the cobra configure command which accepts a language identifier as an argument (i.e. isabelle, scala, haskell), which analyses whether the optional prerequisites for the selected language are met and provides further advice.

To create an empty Cobra presentation

just run cobra new <name> on the command line. This creates a directory <name> containing two files: cobra.conf and slides.html. The former contains meta information and environment configurations, while the latter contains the actual content of the presentation. The user may add other files to the directory, which will then be served by Cobra. This allows to include graphics, videos, custom style sheets and other arbitrary files, which can then be included in the slides.html file. During presentation, Cobra will run an embedded web server, and serve the slides as HTML pages (see Section 2.5).

2.1 Configuration

The cobra.conf file is a HOCON (Human-Optimised Config Object Notation) [2] configuration file. The file reference.conf is included in the distribution which contains all available settings together with default values and short descriptions. There is no need to change cobra.conf for most presentations. However, among others, the customisations shown in Table 1 are available. Other available settings include the configuration of the underlying presentation framework reveal.js, the math engine MathJax as well as Isabelle. All settings provide reasonable default values (“convention over configuration”).

Changing a setting has immediate effect without reloading the application (except for the network interface which can not be switched while cobra is running), such that the user can always observe the effects of the current configuration in the browser.

2.2 Adding slides

The presentation facilities of Cobra are based on the reveal.js framework [4]. The presentation resides in one HTML file (called slides.html). However, this file has no top html element (and is thus not valid HTML); instead, the slides are represented by top-level section elements and behave as reveal.js slides with the exception of code elements, which are described in Section 2.4. All the boilerplate needed to make this a valid HTML document, and add the necessary JavaScript and style sheets is automatically generated by Cobra.

reveal.js has a two dimensional slide layout: It is possible to nest section elements by one level, which results in vertically arranged slides. This can be used to group slides together. The content of the section elements can be arbitrary HTML, allowing for rich presentations. However, typically a small subset will suffice. Particularly relevant are header elements (h1, h2, …) for the title of a slide; img elements to include vector or raster graphics; and unordered and ordered list elements (ul, ol) for itemisations or enumerations respectively. reveal.js supports so-called fragments, which allow the user to unhide or emphasise certain parts of the slide. Fragments are added through class attributes. Listing 1(a) contains a small example with five slides.

2.3 Integrating LaTeX-style formulae

Text surrounded with dollar signs (i.e. $a \rightarrow b$) is interpreted as LaTeX and rendered by MathJax, a JavaScript library that can render MathML and a large subset of TeX/ LaTeX and is compatible with all modern browsers [10]. The MathJax configuration can be altered through the cobra.conf file.

2.4 Including proofs and code

As mentioned above, code elements are treated specially by Cobra. By default, every code element creates an editable code snippet. By adding certain class attributes to the element, its behaviour can be altered, e.g. the language mode can be defined by adding either scala, haskell or isabelle as a class. When such a class attribute is added, the rich semantic assistance engine is automatically invoked to provide information about the snippet, that will be visualised during the presentation.

The simplest way to include code is to add it as content of a code element. However, it is often desirable to include only certain snippets of a larger code example. For such situations, Cobra allows us to include hidden code elements and then reference snippets. Snippets are marked by special comments within the target language, which is more robust than referencing lines. Snippets may overlap. When dealing with large code examples it is also possible to include just a reference to an external source file. In this case, the language does not have to be specified as it can be derived from the file extension.

Behavioural Classes

can be added to a code element to alter its presentation behaviour: states enables inline proof states (for Isabelle only), state-fragments reveals one proof after another during the presentation, no-infos hides info messages during the presentation, and no-warnings hides warning messages during the presentation.

Code Fragments

are parts of code that are revealed or altered interactively during the presentation. There is a special comment syntax which preserves the semantics of the original source file. The variants of a section of source code are enclosed in parentheses and separated by a pipe symbol. The parentheses are then enclosed in block comments, including either the left or right variant. e.g. val x = /(/???/|3 * 7)/ or val x = /(???|/3 * 7/)/, which will both result in the same sequence during the presentation but obviously produce different meanings in the source file. When no alternative is provided (as in lemma $x$: $A\Rightarrow$ (()$A$())) the code fragment is selected during the presentation and semantic information is annotated if available.

2.5 Interactive presentations

Use cobra <dir> on the command line to start a presentation server within the specified directory. After a short while Cobra will be initialised. The presentation can now be opened with any modern web browser. The user will see the first slide. It is possible to navigate through the slides with the keyboard or a presenter. reveal.js provides controls similar to those of PowerPoint; an overview of the available key bindings can be displayed by pressing "?".

When a slide includes a code snippet, the viewer will find it augmented with semantic information (Figure 2). The syntax highlighting will reflect the semantic meaning of tokens, just like in Isabelle/jEdit [21] or Clide [17, 14]. For Isabelle theories, the proof states can be iterated (just like other fragments) if the class state-fragments is added. It is also possible to mark certain fractions of the code as fragments which will behave like any other reveal.js fragment but also affect the semantic annotations. Errors are prominently rendered as a red background behind the affected part of the snippet (Figure 4), which is useful when presenting a situation where an error is of importance (we found the usual red underlining to be too innocuous). It is also possible to view additional information about entities by selecting with the mouse (or a finger when using a touch enabled device). The displayed tool-tips are displayed in a way that is suitable for presentations, and contain similar information to the tool tips in Isabelle/jEdit (Figure 3). Since manually selecting can be cumbersome it is also possible to use selection fragments, which automate this by allowing to step through predefined ranges as described in Section 2.4.

Furthermore, it is possible to alter the content of snippets just like in a text editor. 222Note that for security reasons, the Safari web browser does not allow keystrokes in full screen mode, which unfortunately makes the browser unsuitable for presenting interactive proofs. When snippets are changed, the content is synchronised across all connected devices as well as the underlying assistant, which then annotates the code with updated semantic annotations, similar to the non-human collaborators in Clide. It is also possible that someone from the audience alters the code with his own device, if the speaker allows access to the presentation server333The default setting of serving to localhost prevents this.. The changes will then be synchronised to everybody else and become visible in the main presentation. Snippets are synchronised continuously; e.g. if there is one running code example that is referenced across various slides, changes made in one slide might affect the others. Overlapping snippets will always display consistent information. If this is not desired, the snippets have to be separated into different origins.

2.6 Publishing and distribution

There are three intended ways of publishing slides. All three have unique advantages and disadvantages. Thus, it is desirable to provide at least two different ways to access slides for the audience.

Central presentation server:

The presentation can be provided on a central presentation server which then also runs the Isabelle process. Viewers can access the presentation and play around with proofs through their web browser. This approach requires a lot of resources on the presentation server when many viewers access different presentations at the same time.

Local presentation servers:

It is possible to distribute a Cobra presentation as an archive file. This will require the viewers to install the Cobra command line tool as described above, and install Isabelle locally.

PDF export:

Having active slides is not always desirable, especially when it comes to just viewing and printing. In this case it is possible to export PDF. This can be done the same way as in reveal.js; Cobra then takes care of the correct rendering of snippets for printing.

3 Cobra internals

The PIDE framework [21] which was developed together with the Isabelle/jEdit integration has already been successfully integrated into the collaborative web environment Clide in previous work [17]. We were able to reuse significant portions of the code to implement Cobra. However, due to the limitations at the time, while the Clide server is implemented in Scala, a strongly typed and reasonably well specified language, the client was implemented in CoffeeScript, a thin wrapper language compiling directly to JavaScript. Both CoffeScript and JavaScript are dynamically typed languages, with an object system based on prototyping, and lacking a module system. While this makes these languages suited for “quick and dirty” solutions, complex projects like Clide or Cobra become hard to maintain and reason about. Recently, several independent approaches, like TypeScript [7], arose to remedy these shortcomings. A particularly interesting solution in our context is ScalaJS [11], a JavaScript back-end for the Scala compiler, which compiles Scala code to JavaScript which can run in a web browser; it has officially been labelled “ready for production” by the creators of Scala in 2015.

By using ScalaJS the Cobra code base does not need to include a single line of JavaScript. We do depend on JavaScript libraries like CodeMirror (the editor component) or reveal.js (the underlying presentation framework), but were able to create Scala facade types from existing TypeScript types. Especially the basis of Clide, the collaboration algorithm, is now identical on the JVM and all connected browsers.

System architecture.

Cobra is designed as a client-server architecture. Unlike Clide which is based on the Play! framework, the Cobra server is built around akka-http [18], a minimal HTTP library based on the Akka implementation of reactive streams [3]. This results in a reduced size and better speed of the application. Upon connection, web clients load all static assets from the Cobra server through plain HTTP, these include the compiled JavaScript of the client. After that, a WebSocket connection is established which handles all further communication. The protocol is a very fast and size-efficient binary protocol based on the boopickle library, which is itself derived from the Scala Pickling project [15]. This allows us to pass Scala defined algebraic data types around between client and server, both of which are implemented in Scala. Since the PIDE framework is also implemented in Scala, the integration is straightforward. The same holds for the Scala compiler. Haskell is integrated by calling ghc-mod as an external command. To synchronise document states across clients and assistants, the universal collaboration approach from Clide is used (as described in [17]).

4 Related Work

There is a wealth of work on presenting formalised proof, going back right to the start of the field. Early attempts were concerned with making proof scripts more like mathematical texts rather than programming languages; one of the earliest representatives of this was the Mizar prover. However, this does not allow interaction with the proof script beyond it being checked by the prover. There have been various attempts at presenting interactive views on proofs, most of which focus on specific aspects, logics or systems: the Jape prover [8] allows direct manipulation of a natural deduction proof visualised as a tree or box, Grundy and Back use structured calculational reasoning [12, 6] where the proof can be interactively explored along its hierarchical structure, the Omega system visualised proofs interactively using proof trees [19], Theorema uses the computer algebra system Mathematica [9], and there have been various attempts to visualise geometric proofs using diagrams [22, 16, 23].

On a less conceptual and more technical level, there are systems which are technologically similar to Cobra in that they make use of web-based front-end technology: ProofWeb was an early precursor [13], Clide offers a full web interface for PIDE-enabled provers [17], and jsCoq moves the whole prover into the web browser by translating it into JavaScript [5]. However, while these are similar in some regards, differences remain; e.g. jsCoq is completely devoted to Coq, and not generic like Cobra.

Summing up, the following three characteristics distinguish Cobra from other systems: firstly, it focuses on presentations (slides) as opposed to long-form text, which means that extraction of parts of the proof plays a key role; secondly, it is interactive, allowing to change content and display the results immediately; and thirdly, it is generic, i.e. usable with different provers or programming languages.

5 Conclusion

We have presented Cobra, a framework which allows source code and interactive proof scripts to be presented as active documents, with which the viewer can interact. Our tool is ready for use in production; it is distributed in binary form for all major operating systems at http://www.flatmap.net/cobra444Please note you need to have Java 8 installed to run the Cobra binary., or alternatively in source code form at https://github.com/flatmap/cobra/.

We envisage the following usage scenarios for Cobra: Firstly, classroom teaching where a prepared proof is presented to a group of students. Here, the advantages of Cobra are that the teacher can select those parts of the proof to be presented, so the presentation remains compact and convenient to follow, avoiding cognitive overload with lots of unnecessary details. The teacher can further build up the proof gradually, like on a blackboard, but with the safety net of the Isabelle proof checker in the background. Secondly, teaching in small groups where the teacher develops a proof together with a group of students. Here, the proof can be developed collaboratively, with everybody contributing while the presentation serves as the focus of attention for all participants. Thirdly, self-study when readers (students, fellow researchers, or reviewers) can interact with the presentation, exploring the effects of changes. Finally, research talks at a workshop such as UITP, where researchers can present their work with greater confidence, and can pick up questions from the audience by demonstrating effects of changes as they might be suggested from the floor. In all of these scenarios, Cobra brings added value over the current state of the art, where interactive proofs are presented as passive documents.

In future work, we plan to include other proof assistants. The canonical way to connect other proof assistants is via the PIDE framework. As a PIDE integration exists [20], it should be feasible to integrate Coq. In addition, it would be beneficial to reduce the overhead further by introducing a simplified syntax to describe slides, possibly based on Markdown. Further, we plan to explore if more inter-dependencies between the snippets and the presentation itself could be allowed. This would allow for even richer presentations, where the structure of a presentation depends on the contained proofs or generated graphics visualise dynamic aspects of a proof.