clide

What is clide?

Clide is a web interface for the interactive theorem prover Isabelle. It uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.

Features

• State of the art HTML5 interface
• Server-side syntax highlighting
• Editable mathematical notation

Known Issues

• The interface is not optimized yet for tablet devices.
• User management is rudementary and has bugs. It is currently beeing completely redesigned.
• File management is also rudementary and beeing redesigned. This will also include hyperlinking to definitions.
• If the internet connection is lost, the session can't be restored right now. This will also be addressed in the redesign.
• Unfortunately right now it can happen, that inconsistencies in the server-synced highlighting occur. In these cases please refresh the page.

Live demo

Please use a current WebKit-Based Browser (Google Chrome, Apple Safari or recent Opera) and visit:

http://clide.informatik.uni-bremen.de

Setup local server

To set up your on experimental server just follow these simple steps:

• Make sure Isabelle 2012 is installed on your machine and ISABELLE_HOME environment variable is set.
• Install play! webframework Version 2.1 or later

• Clone the clide repo

  > git clone https://github.com/martinring/clide.git
  

• Start the server

  > cd clide
  > play start