• 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.

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

Release of Frama-Clang 0.0.11 — Frama-C, Jul 13, 2021

Permanent Engineer/Researcher Position at CEA LIST - LSL — Frama-C, Jul 08, 2021

Release of Frama-C 23.0 (Vanadium) — Frama-C, Jul 06, 2021

Deploying binary MirageOS unikernels — Hannes Mehnert (hannes), Jun 30, 2021


MirageOS development focus has been a lot on tooling and the developer experience, but to accomplish our goal to "get MirageOS into production", we need to lower the barrier. This means for us to release binary unikernels. As described earlier, we received a grant for "Deploying MirageOS" from NGI Pointer to work on the required infrastructure. This is joint work with Reynir.

We provide at builds.robur.coop binary unikernel images (and supplementary software). Do…


Tarides Introduces OSMOSE at the Open-Source Innovation Sprint — Tarides, Jun 29, 2021

Tarides is excited to announce that our CEO, Dr. Thomas Gazagnaire, and Prof. Anil Madhavapeddy, from the University of Cambridge, will present their innovative platform OSMOSE at the Open Source Innovation Sprint (OSIS) conference on 1 July 2021. This event is organized by Systematic.

OSMOSE is a software platform made to manage digital infrastructure at scale, securely and efficiently. It uses the groundbreaking creation of unikernels to radically simplify the way applications are built and de…


Roadmap 2021 & New Landing Page — Reason Documentation Blog, Jun 25, 2021

Announcing our roadmap for 2021 / 2022, release cycle plans and new landing page.

The dawn of formalized mathematics — Andrej Bauer, Jun 23, 2021

Here are the slides of my talk "The dawn of formalized mathematics" from the 8th European Congress of Mathematics, which is taking place online and in Protorož, Slovenia, from June 20 to 26, 2021:

opam 2.1.0~rc2 released — OCaml Platform (David Allsopp), Jun 23, 2021

Feedback on this post is welcomed on Discuss!

The opam team has great pleasure in announcing opam 2.1.0~rc2!

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the…


Looking for a developer experience engineer — Jane Street, Jun 15, 2021

The Jane Street Tools & Compilers team is looking to hire a developer who will act as the primary contact point with users of our tools throughout the firm.

Beta release of Frama-C 23.0~rc1 (Vanadium) — Frama-C, May 20, 2021

Building Ahrefs codebase with Melange — Ahrefs, May 18, 2021

Photo by Jens Lelie on Unsplash

At Ahrefs, we have been using BuckleScript and ReasonML in production for more than two years. We already have a codebase of tens of thousands of lines of code, with several web applications that are data intensive and communicate with backend services written in OCaml, using tools like atd.

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML proje…


Computing an integer using a Grothendieck topos — Andrej Bauer (Martin Escardo), May 17, 2021

A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,

  1. we developed our mathematics constructively,
  2. we formalized our mathematics in Martin-Löf type theory, in Agda notation,
  3. we pressed a button, and
  4. after a few seconds we saw the integer we expected in front of us.

Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).

Why formalize?

Most people formalize mathematics (in Automa…


ReScript 9.1 — Reason Documentation Blog, May 07, 2021

Featuring a new npm package, a CLI revamp, polymorphic variant interop and object cleanup.

Tutorial: Format Module of OCaml — OCamlPro, May 06, 2021

The Format module of OCaml is an extremely powerful but unfortunately often poorly used module.

It combines two distinct elements:

  • pretty-print boxes
  • semantic tags

This tutorial aims to demystify much of this module and explain the range of things that you can do with it.

Read more (in French)

Tarides project SCoP is selected as one of the brightest Data Portability projects in Europe! — Tarides, Apr 30, 2021

Tarides is taking part in the Data Portability & Services Incubator (DAPSI), a 3-year EU funded project that empowers internet innovators to develop new solutions in the Data Portability field.

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of …


Alt-Ergo Users’ Club Annual Meeting (2021) — OCamlPro, Apr 29, 2021

The third annual meeting of the Alt-Ergo Users’ Club took place on April 1! Our annual meeting is the ideal place to review the needs of each partner regarding Alt-Ergo. We were pleased to welcome our partners to discuss the roadmap for future Alt-Ergo developments and improvements.

Alt-Ergo is an automatic prover of mathematical formulas, jointly developed by LRI and OCamlPro (since 2014). To learn more or join the Club, visit https://alt-ergo.ocamlpro.com.

Our Club has several goa…


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-crypto 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…


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]

View older blog posts.