Monthly Archives: January 2016

ML

Release of Poly/ML 5.6

David Matthews has released Poly/ML 5.6 on 25-Jan-2016. Poly/ML is one of the oldest and most sophisticated implementations of Standard ML. It routinely supports multi-threading with true parallelism on multicore hardware, fast incremental compilation, source-level debugging. The latest release is also notable for native support on Windows (32/64 bit).

Poly/ML 5.6 is used for Isabelle2016 (February 2016).

Coq, PIDE

Release of Coq 8.5

On 21-Jan-2016 Coq 8.5 has been released, with an unusually long distance of about 3.5 years to Coq 8.4.

Coq 8.5 is notable for having a little bit of PIDE (Prover IDE) support (by Enrico Tassi), without using that name nor the Scala-based PIDE library of Isabelle. It is all based on OCaml, and connects to the regular CoqIde frontend.

Isabelle, Local

Isabelle presentation at Curry Club Augsburg

On Thu 17-Mar-2016 there will be a presentation about “Programs and Proofs in Isabelle/HOL” at Curry Club Augsburg.

Start: approximately 19:30–20:00
Duration: approximately 60min
Language of the talk: German

Outline:

  • Isabelle and the LCF prover family: origin of ML (Meta-Language)
  • Isabelle as framework for domain-specific formal languages
  • Isabelle document preparation: formal LaTeX + Markdown
  • Isabelle/ML: tool implementation language
  • Isabelle/Scala: system programming language
  • “Programming” in Isabelle/HOL: the main Object-Logic
  • Example: list operations and induction proofs (with code-generation to SML, OCaml, Scala, Haskell)
  • Structured proofs in Isabelle/Isar
  • Example: Cantor’s Theorem in HOL
  • Example: Run-Length Encoding in HOL
Isabelle

Release candidates for Isabelle2016

The coming Isabelle2016 release is scheduled for February 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.

  • On 01-Jan-2016 an informal snapshot Isabelle2016-RC0 was published. In this version, the website, NEWS, ANNOUNCE etc. are already mostly up-to-date. Some documentation is still lagging behind, notably the Isabelle/jEdit manual.
  • On 15-Jan-2016 the first formal release candidate Isabelle2016-RC1 was published. The main work is finished. Some documentation requires further revisions. We now need serious testing by users to expose remaining problems.
  • On 25-Jan-2016 the second release candidate Isabelle2016-RC2 was published. It includes the latest jdk-8u72 from Oracle: it is important to test this thoroughly on all platforms.
  • On 01-Feb-2016 the third release candidate Isabelle2016-RC3 was published. It includes the official Poly/ML 5.6 release. Some minor points have been polished in the Isabelle code base and documentation.
  • On 06-Feb-2016 the fourth release candidate Isabelle2016-RC4 was published. Some minor points have been improved in Sledgehammer and Isabelle/jEdit GUI reactivity.
  • On 12-Feb-2016 the fifth release candidate Isabelle2016-RC5 was published. It includes more material on Isar language updates in the isar-ref manual. Poly/ML 5.6 has been modified to use GNU bash for OS.Process.system, in order to help Debian-testing-unstable propagate the Isabelle settings environment – with shell functions, as documented in the bash man page!

As usual it is important to keep general laws of causality in mind: release candidates may still change, but the final release is final. So the best time to start testing is now!

The main forum for discussion of Isabelle2016 release candidates is on isabelle-users mailing list.

Update: The final release of Isabelle2016 (February 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.