2

I'm trying to get an overview on the Isabelle Project and everywhere I look new Isabelle/sth's are mentioned.

How do all of them relate to each other?

I'll try to go first:

  • Isabelle/? - The Isabelle Language itself
  • Isabelle/Isar - Language used to write proofs in
  • Isabelle/Pure - ?
  • Isabelle/HOL - Toolkit for a higher-order logic proving environment
  • Isabelle/jEdit - Isabelle IDE
  • Isabelle/Scalar - ?
  • Isabelle/PIDE - ?
Max
  • 965
  • 1
  • 10
  • 28

1 Answers1

3
  • I would not really say that Isabelle is a language; it's more the entire system.
  • Isabelle/Isar is indeed the language to write structured proofs. Isabelle had actually been around for over 10 years before Isar was developed (it was Makarius Wenzel's PhD thesis in 2002).
  • Isabelle/Pure is the most basic logic in Isabelle, the one that is implemented in its kernel. It is a simply-typed intuitionistic higher-order logic that only knows about functions, propositions (the prop type), universal quantification, and implication. All the other logics are axiomatised on top of this (Pure serves as a metalogic).
  • Isabelle/HOL is an axiomatisation of classical simply-typed higher-order logic on top of this. The prop type is mostly hidden from the user; instead you usually work with bool (there is an injection Trueprop : bool ⇒ prop)
  • Isabelle/jEdit is indeed the IDE that is typically used for Isabelle these days. It consists of the jEdit editor with a lot of Isabelle-specific extras.
  • Isabelle/ML is the ML (as in, the ML programming language) environment that Isabelle uses. These days this is Poly/ML, but with a custom library and some additions like antiquotations (a kind of macro system).
  • Isabelle/Scala is the part of Isabelle that is written in Scala. This handles the "plumbing" in the background such as building sessions in batch, communicating with Isabelle/jEdit, etc. whereas Isabelle/ML is where all the logic happens (manipulation of terms and theorems etc.)
  • Isabelle/PIDE is the ‘Isabelle Prover IDE framework’. I honestly don't really know what it actually does, but as far as I am aware it is a kind of protocol that is used by the Isabelle/ML process to communicate with e.g. IDEs such as Isabelle/jEdit and VSCode, i.e. it enables interactive use of Isabelle (as opposed to batch use with isabelle build). This includes things such as giving Isabelle a bit of code to process, or telling it that some code has been deleted and should be undone, and displaying information such as type information, error messages, which parts of the theory have already been processed etc.
Manuel Eberl
  • 7,858
  • 15
  • 24