• en

OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

1083 blog posts are available. You can read the 30 more recent ones below or view older ones.

Cryptography updates in OCaml and MirageOS — Hannes Mehnert (hannes), Apr 23, 2021


Tl;DR: mirage-crypto-ec, with x509 0.12.0, and tls 0.13.0, provide fast and secure elliptic curve support in OCaml and MirageOS - using the verified fiat stack (Coq to OCaml to executable which generates C code that is interfaced by OCaml). In x509, a long standing issue (countryName encoding), and archive (PKCS 12) format is now supported, in addition to EC keys. In tls, ECDH key exchanges are supported, and ECDSA and EdDSA certificates.

Elliptic curve cryptography

Since May 20…


New Try-Alt-Ergo — OCamlPro, Mar 29, 2021

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it’s high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In t…


TZComet's New Token Viewer — Sebastien Mondet, Mar 26, 2021

TZComet and CleanNFT Metadata: a generic token-viewer ☄ Also new domain tzcomet.io 🌠

Release of Frama-Clang 0.0.10 — Frama-C, Mar 08, 2021

Qubes-lite with KVM and Wayland — Thomas Leonard, Mar 07, 2021

I’ve been running QubesOS as my main desktop since 2015. It provides good security, by running applications in different Xen VMs. However, it is also quite slow and has some hardware problems. I’ve recently been trying out NixOS, KVM, Wayland and SpectrumOS, and attempting to create something similar with more modern/compatible/faster technology.

This post gives my initial impressions of these tools and describes my current setup.

Table of Contents


Florence and beyond: the future of Tezos storage — Tarides, Mar 04, 2021

In collaboration with Nomadic Labs, Marigold and DaiLambda, we're happy to announce the completion of the next Tezos protocol proposal: Florence.

Tezos is an open-source decentralised blockchain network providing a platform for smart contracts and digital assets. A crucial feature of Tezos is self-amendment: the network protocol can be upgraded dynamically by the network participants themselves. This amendment process is initiated when a participant makes a proposal, which is then subject to a v…


The ReScript Association — Reason Documentation Blog, Mar 03, 2021

After the rebranding of ReScript, its Reason Association has now followed through to become the ReScript Association.

Coq Platform 2021.02.0 is out — Coq, Feb 26, 2021

The Coq development team is proud to announce the immediate availability of the Coq Platform 2021.02.0

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install OPAM, Coq, Coq libraries and Coq plugins on MacOS, Windows and many Linux distributions in a reliable way with consistent results.

This release is based on Coq 8.13.1 and provides binary installers for Windows and Linux. We plan t…


Coq 8.13.1 is out — Coq, Feb 22, 2021

The Coq development team is proud to announce the immediate availability of Coq 8.13.1


  • Fix arities of VM opcodes for some floating-point operations that could cause memory corruption

Please see the changelog to learn more about this release.

The Burali-Forti argument in HoTT/UF — Andrej Bauer (Martin Escardo), Feb 21, 2021

This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.

We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.

Ordinals in univalent type theory

The Burali-Forti paradox is about…


Partnering for more diversity in Tech — Tarides, Feb 15, 2021

Tarides is very glad to announce our partnership with Ada Tech School.

Founded in 2019 and based in Paris (France), Ada Tech School, named for pioneer computer scientist Ada Lovelace, is a programming school designed for women but open to all. The program is driven by three values: feminism, empathy and singularity. Its mission is to facilitate access to programming positions and promote the feminization of tech, by creating training that tackles the gender and cultural biases of IT.



opam 2.0.8 release — OCamlPro, Feb 09, 2021

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

  • Critical for fish users! Don’t add . to PATH. [#4078]
  • Fix sandbox script for newer ccache versions. [#4079 and #4087]
  • Fix sandbox crash when ~/.cache is a symlink. [#4068]
  • User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
  • macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-reposi…

ReScript 9.0 — Reason Documentation Blog, Feb 09, 2021

Featuring a new external stdlib configuration, some syntax improvements and a small breaking change for nested records.

opam 2.0.8 release — OCaml Platform (Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Feb 08, 2021

We are pleased to announce the minor release of opam 2.0.8.

This new version contains some backported fixes:

  • Critical for fish users! Don't add . to PATH. [#4078]
  • Fix sandbox script for newer ccache versions. [#4079 and #4087]
  • Fix sandbox crash when ~/.cache is a symlink. [#4068]
  • User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092]
  • macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339]

opam 2.1.0~beta4 released — OCaml Platform (David Allsopp), Feb 08, 2021

Feedback on this post is welcomed on Discuss!

On behalf of the opam team, it gives me great pleasure to announce the third beta release of opam 2.1. Don’t worry, you didn’t miss beta3 - we had an issue with a configure script that caused beta2 to report as beta3 in some instances, so we skipped to beta4 to avoid any further confusion!

We encourage you to try out this new beta release: there are instructions for doing so in our wiki. The instructions include taking a backup of your ~/.opam


Synthetic mathematics with an excursion into computability theory — Andrej Bauer, Feb 02, 2021

It is my pleasure to have the opportunity to speak at the University of Wisconsin Logic seminar. The hosts are graciously keeping the seminar open for everyone. I will speak about a favorite topic of mine:

Synthetic mathematics with an excursion into computability theory

Speaker: Andrej Bauer (University of Ljubljana)
Location: University of Wisconsin Logic seminar
Time: February 8th 2021, 21:30 UTC (3:30pm CST in Wisconsin, 22:30 CET in Ljubljana)
Video link: the Zoom link is available at the…


2020 at OCamlPro — OCamlPro, Feb 02, 2021

OCamlPro was created in 2011 to advocate the adoption of the OCaml language and formal methods in general in the industry. While building a team of highly-skilled engineers, we navigated through our expertise domains, delivering works on the OCaml language and tooling, training companies to the use of strongly-typed languages like OCaml but also Rust, tackling formal verification challenges with formal methods, maintaining the SMT solver Alt-Ergo, designing languages and tools for smart contrac…


Recent and upcoming changes to Merlin — Tarides, Jan 26, 2021

Merlin is a language server for the OCaml programming language; that is, a daemon that connects to your favourite text editor and provides the usual services of an IDE: instant feedback on warnings and errors, autocompletion, "type of the code under the cursor", "go to definition", etc. As we (Frédéric Bour, Ulysse Gérard and I) are about to do a new major release, we thought now would be a good time to talk a bit about some of the changes that are going into this release.

Project configurati…


The road ahead for MirageOS in 2021 — Hannes Mehnert (hannes), Jan 25, 2021


2020 was an intense year. I hope you're healthy and keep being healthy. I am privileged (as lots of software engineers and academics are) to be able to work from home during the pandemic. Let's not forget people in less privileged situations, and let’s try to give them as much practical, psychological and financial support as we can these days. And as much joy as possible to everyone around :)

I cancelled the autumn MirageOS retreat due to the pandemic. Instead I colle…


Release of Alt-Ergo 2.4.0 — OCamlPro, Jan 22, 2021

A new release of Alt-Ergo (version 2.4.0) is available.

You can get it from Alt-Ergo’s website. The associated opam package will be published in the next few days.

This release contains some major novelties:

  • Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
  • We switched command line parsing to use cmdliner. You will need to use --<option name> instead of -<option name>. Some options have also been renamed, see the manpage or the documentati…

Coq 8.13.0 is out — Coq, Jan 07, 2021

The Coq development team is proud to announce the immediate availability of Coq 8.13.0


  • Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays.
  • Introduction of definitional proof irrelevance for the equality type defined in the SProp sort.
  • Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation availab…

How We Lost at The Delphi Oracle Challenge — Sebastien Mondet, Dec 23, 2020

Because the method — some messing around with the tezos-crypto library — could be useful to others. Also, some code annotated in SVG.

Tarides sponsors the Oxbridge Women in Computer Science Conference 2020 — Tarides, Dec 14, 2020

The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually…


Coq 8.12.2 is out — Coq, Dec 11, 2020

We are happy to announce the release of Coq 8.12.2.

This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the exists tactic). See the changelog for details.

First release of MetAcsl plugin — Frama-C, Dec 09, 2020

Announcing MirageOS 3.10 — MirageOS (Hannes Mehnert), Dec 08, 2020

MirageOS 3.10 release - IPv6

IPv6 and dual (IPv4 and IPv6) stack support https://github.com/mirage/mirage/pull/1187 https://github.com/mirage/mirage/issues/1190

Since a long time, IPv6 code was around in our TCP/IP stack (thanks to @nojb who developed it in 2014). Some months ago, @hannesm and @MagnusS got excited to use it. After we managed to fix some bugs and add some test cases, and writing more code to setup IPv6-only and dual stacks, we are eager to share this support for MirageOS in a re…


ReScript 8.4 — Reason Documentation Blog, Dec 07, 2020

bsb improvements

Coq 8.13+beta1 is out — Coq, Dec 07, 2020

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1

Here the full list of changes.

We encourage our users to test this beta release, in particular:

  • The windows installer is now based on the Coq platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter.
  • The…

Memthol: exploring program profiling — OCamlPro, Dec 01, 2020

Memthol is a visualizer and analyzer for program profiling. It works on memory dumps containing information about the size and (de)allocation date of part of the allocations performed by some execution of a program.

For information regarding building memthol, features, browser compatibility… refer to the memthol github repository.
Please note that Memthol, as a side project, is a work in progress that remains in beta status for now.

Memthol’s background

The Memthol wor…


Growing the Hardcaml toolset — Jane Street, Dec 01, 2020

I am pleased to announce that we have recently released a slew of new Hardcaml libraries!

View older blog posts.