Cobra is a modern code and 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 live changes both by the presenter as well as the audience.
Cobra currently supports Isabelle proofs. Support for Coq will follow at a later point.
Thanks to the great Isabelle/ML integration, Cobra is also suitable for presentations of Standard ML code.
In addition, Cobra has (early) support for Scala and Haskell code. Consider these two modes not production ready. They are ready to play around, but are not stable, and don't support any kind of execution of code.
Note, that Java 8 or higher is required for cobra to run. It will fail to start, when used with Java 7 or below!
Download zip and extract anywhere; Add bin/cobra.bat to your PATH.
Until the notability of the cobra GitHub repository meets the requirements of homebrew-core, we have an own tap:
brew tap flatmap/cobra
brew install cobraThere is a YUM repository available which provides automatic updates
wget https://bintray.com/flatmap/rpm/rpm -O bintray-flatmap-rpm.repo
sudo mv bintray-flatmap-rpm.repo /etc/yum.repos.d/
sudo dnf install cobraThere is a PPA available for Debian / Ubuntu. Releases are signed with bintray's private key. To add the public key please ececute
apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 379CE192D401AB61 Now you can add the repo and install cobra
echo "deb https://dl.bintray.com/flatmap/deb wheezy main" | sudo tee -a /etc/apt/sources.list
sudo apt-get update
sudo apt-get install cobra-presentationsDownload zip and extract anywhere; Add bin/cobra to your PATH.
Cobra presentations are viewed in the browser. Cobra starts a very light and fast web server for every presentation.
Every presentation has an own directory. Every file within the presentation directory is served as a static resource to the web browser.
- Create a new presentation: call
cobra newfrom the command line and follow the instructions - Start the presentation server: call
cobrain the directory of the presentation. Orcobra <dir>where<dir>is the presentation directory. - View the presentation: Navigate to localhost:8080 with your web browser.
- Edit your presentation: Configuration can be edited in
cobra.conf, content inslides.html. There is no need to restart the presentation server. Changes will be immediately visible in the browser, when files are changed.
The content of a presentation is stored in a file called slides.html. Cobra will support a MarkDown slide format in Version 1.2.
To add a slide, simply add <section> tags to the slides.html file. For the general slide format please refer to the reveal.js documentation.
The simplest option is to include inline code snippets:
<code class="scala">
case class Person(name: String, age: String)
object Test {
val p = Person("Albert Einstein", ???)
}
</code>This will produce a code snippet, which will be semantically treated by the scala compiler. It is possible to edit the code in the presentation, just as in an IDE. It is also possible to select parts of the code (e.g. identifiers) to display semantic information about the code.
To include Isabelle or Haskell simply replace scala class with isabelle or haskell
Note: When including Isabelle inline you will want to set the
idof thecodetag to the name of your theory, because otherwise a name for your theory is generated and will most definitely clash with what you define in your header. (see #12)
It is possible to show inline states (for Isabelle) by adding the class states to a code tag
If you want to step through states, you can additionally add the class state-fragments
You can hide info messages by adding no-infos class
You can hide warning messages by adding no-warnings class
It is possible to include external source files. Simply place a code file within the folder of the presenation. (e.g. <presentation root>/src/Test.scala)
You can then include the snippet with
<code src="src/Test.scala"></code>Note, that you don't have to specify the language in this case, since it is recognised from the file extesion.
Often it is desired to include only parts of larger examples, for example omitting all imports for the presentation:
This can be done with special comments:
import system.io._
Object Example {
/// begin #example
val x = 7
/// begin #def-f
def f(y: Int) = ???
/// end #example
/// end #def-f
}The comments won't be shown in the presentation and the sub-snippets can be included as such:
<code src="#example></code>
Note that, the sub-snippets may be nested or even overlapping as in the example and included in several editors. They will always stay in sync.
The language mode is derived from the super-snippet.
It is also possible to hide snippets. This is convenient, when super snippets shall not be included in the presentation. This can be done by adding the class hidden to a code snippet.
The comment syntax for Haskell and Isabelle is as follows:
--- begin #snippet-name
haskell code
--- end #snippet-name(** begin #snippet-name *)
isabelle code
(** end #snippet-name *)Snippet names are global and thus have to be unique.
Within presentations it is desirable to not show everything at the beginning or exchange parts of the code. This can be achieved with special syntax:
val x = /*(*/???/*|3 * 7)*/
// or
val x = /*(???|*/3 * 7/*)*/will result both in the following sequence
val x = ???hit next
val x = 3 * 7The difference in the two lines is just their meaning in the source file.
Again the syntax for Haskell and Isabelle is analogous:
fibs = {-(-}undefined{-|0 : 1 : zipWith (+) fibs (tail fibs))-}lemma x: "A ==> A" (*(*)oops(*|by auto)*)It is also possible to select parts of the code automatically as such:
val x = /*(*/7/*)*/x = {-(-}7{-)-}lemma x: "A ==> (*(*)A(*)*)"They will act the same as manual selections, displaying semantic information about the selected portion.
In Version 1.1, it will be possible to annotate custom text to selected portions.
The file cobra.conf can be edited while the server is running, any change will have immediate effect, when the file is saved. Any running presentation will be updated in the browser, this way you can play around with setting until they suit your needs.
cobra.conf is a HOCON style configuration file with the following defaults:
cobra {
// display title of the presentation
title = "Cobra"
// display language of the presentation
language = "en"
theme {
// slide theme
// standard themes: black|white|league|sky|beige|simple|serif|blood|night|
// moon|solarized
// or reference to user theme (e.g. "/theme/mytheme.css")
slides = "white"
// code theme
// standard themes: 3024-day|3024-night|abcdef|ambiance-mobile|ambiance|
// base16-dark|base16-light|bespin|blackboard|cobalt|
// colorforth|dracula|eclipse|elegant|erlang-dark|hopscotch|
// icecoder|isotope|lesser-dark|liquibyte|material|mbo|
// mdn-like|midnight|monokai|neat|neo|night|paraiso-dark|
// paraiso-light|pastel-on-dark|railscasts|rubyblue|seti|
// solarized|the-matrix|tomorrow-night-bright|
// tomorrow-night-eighties|ttcn|twilight|vibrant-ink|
// xq-dark|xq-light|yeti|zenburn
// or reference to user theme (e.g. "/theme/my-code-theme.css")
code = "default"
}
// network interface to bind on
binding {
interface = "localhost"
port = 8080
}
// environment variables
env {
// overrides ISABELLE_HOME environment variable
// isabelle_home = "..."
}
// reveal.js related settings
reveal {
// Display controls in the bottom right corner
controls = true
// Display a presentation progress bar
progress = true
// Display the page number of the current slide
slideNumber = false
// Push each slide change to the browser history
history = true
// Enable keyboard shortcuts for navigation
keyboard = true
// Enable the slide overview mode
overview = true
// Vertical centering of slides
center = false
// Enables touch navigation on devices with touch input
touch = true
// Loop the presentation
loop = false
// Change the presentation direction to be RTL
rtl = false
// Randomizes the order of slides each time the presentation loads
shuffle = false
// Turns fragments on and off globally
fragments = true
// Flags if the presentation is running in an embedded mode,
// i.e. contained within a limited portion of the screen
embedded = false
// Flags if we should show a help overlay when the questionmark
// key is pressed
help = true
// Flags if speaker notes should be visible to all viewers
showNotes = false
// Number of milliseconds between automatically proceeding to the
// next slide, disabled when set to 0, this value can be overwritten
// by using a data-autoslide attribute on your slides
autoSlide = 0
// Stop auto-sliding after user input
autoSlideStoppable = true
// Use this method for navigation when auto-sliding
autoSlideMethod = Reveal.navigateNext
// Enable slide navigation via mouse wheel
mouseWheel = false
// Hides the address bar on mobile devices
hideAddressBar = true
// Opens links in an iframe preview overlay
previewLinks = false
// Transition style
transition = "default" // none/fade/slide/convex/concave/zoom
// Transition speed
transitionSpeed = "default" // default/fast/slow
// Transition style for full page slide backgrounds
backgroundTransition = "default" // none/fade/slide/convex/concave/zoom
// Number of slides away from the current that are visible
viewDistance = 3
// Parallax background image
parallaxBackgroundImage = "" // e.g. "'https://s3.amazonaws.com/hakim-static/reveal-js/reveal-parallax-1.jpg'"
// Parallax background size
parallaxBackgroundSize = "" // CSS syntax, e.g. "2100px 900px"
// Number of pixels to move the parallax background per slide
// - Calculated automatically unless specified
// - Set to 0 to disable movement along an axis
parallaxBackgroundHorizontal = null
parallaxBackgroundVertical = null
// The "normal" size of the presentation, aspect ratio will be preserved
// when the presentation is scaled to fit different resolutions. Can be
// specified using percentage units.
width = 960
height = 700
// Factor of the display size that should remain empty around the content
margin = 0.1
// Bounds for smallest/largest possible scale to apply to content
// Should not be changed, if in-slide code editing should be enabled!
minScale = 1.0
maxScale = 1.0
}
}
Cobra is Licensed under LGPL
| Name | Author | License | Usage |
|---|---|---|---|
| reveal.js | Hakim El Hattab | MIT | Bundeled |
| CodeMirror | Marijn Haverbeke | MIT | Bundeled |
| MathJax | MathJax Consortium | Apache 2.0 | Bundeled |
| akka / akka-http | Akka Team, Lightbend | Apache 2.0 | Library |
| Isabelle | University of Cambridge, TU Munich | BSD | Library / Optional Dependency |
| ghc-mod | IIJ Innovation Institute Inc | BSD3/AGPL3 | Optional Dependency |
| scalac | EPFL, Lightbend | Scala License | Library |
| Scala Refactoring Library | Mirko Stocker | Scala License | Library |
| Scala.js | Sébastien Doeraene | Scala License | Compile Time |
octicons (SIL OFL 1.1), LOGBack (EPL 1.0 / LGPL 2.1), Typesafe Config (Apache 2.0), webjars-locator (MIT), sbt-revolver (Apache 2.0), SBT Native Packager (MIT), sbt-web (Apache 2.0), sbt-play-scalajs (All Rights Reserved), scala-js-dom (MIT), BooPickle (MIT), better-files (MIT)