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

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

# Coq 8.11+beta1 is out — Coq, Dec 06, 2019

The first beta release of Coq 8.11 is available for testing.

There are two main changes brought by Coq version 8.11. First, it introduces Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. Second, primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the Coq.Float.Floats library. Many other cleanups and improvements have been performed and a…

# Testing OCaml releases with opamcheck — GaGallium (Florian Angeletti), Dec 03, 2019

I (Florian Angeletti) have started working at Inria Paris this August. A part of my new job is to help deal with the day-to-day care for the OCaml compiler, particularly during the release process. This blog post is a short glimpse into the life of an OCaml release.

## OCaml and the opam repository

Currently, the song of the OCaml development process is a canon with two voices: a compiler release spends the first 6 months of its life as the trunk branch of the OCaml compiler git repository…

# Coq 8.10.2 is out — Coq, Nov 29, 2019

The 8.10.2 release of Coq is available.

Main changes:

• Fixed a critical bug of template polymorphism and nonlinear universes
• Fixed a few anomalies
• Fixed an 8.10 regression related to the printing of coercions associated to notations
• Fixed uneven dimensions of CoqIDE panels when window has been resized
• Fixed queries in CoqIDE

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

# Announcing Irmin 2.0.0 — MirageOS (Anil Madhavapeddy), Nov 26, 2019

We are pleased to announce Irmin 2.0.0, a major release of the Git-like distributed branching and storage substrate that underpins MirageOS. We began the release process for all the components that make up Irmin back in May 2019, and there have been close to 1000 commits since Irmin 1.4.0 release back in June

1. To celebrate this milestone, we have a new logo and opened a dedicated website: irmin.org.

You can read more details about the new features in the Irmin v2 blog post. Enjoy the new releas…

# BAP 2.0 is released — The BAP Blog, Nov 19, 2019

The Carnegie Mellon University Binary Analysis Platform (CMU BAP) is a suite of utilities and libraries that enables analysis of programs in their machine representation. BAP is written in OCaml, relies on dynamically loaded plugins for extensibility, and is widely used for security analysis, program verification, and reverse engineering.

This is a major update that includes lots of new features, libraries, and tools, as well as improvements and bug fixes to the existing code. The following sma…

# CI/CD pipelines: Monad, Arrow or Dart? — Thomas Leonard, Nov 14, 2019

In this post I describe three approaches to building a language for writing CI/CD pipelines. My first attempt used a monad, but this prevented static analysis of the pipelines. I then tried using an arrow, but found the syntax very difficult to use. Finally, I ended up using a light-weight alternative to arrows that I will refer to here as a dart (I don’t know if this has a name already). This allows for static analysis like an arrow, but has a syntax even simpler than a monad.

Table of Con…

# On fixed-point theorems in synthetic computability — Andrej Bauer, Nov 06, 2019

I forgot to record the fact that already two years ago I wrote a paper on Lawvere's fixed-point theorem in synthetic computability:

Andrej Bauer: On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, Volume 10: Issue 3, pp. 167–181.

It was a special issue in honor of Professors Peter J. Freyd and F. William Lawvere on the occasion of their 80th birthdays.

Lawvere's paper "Diagonal arguments and cartesian closed categories proves a beautifully simple fixed poi…

# Runners in action — Andrej Bauer, Oct 27, 2019

It has been almost a decade since Matija Pretnar and I posted the first blog posts about programming with algebraic effects and handlers and the programming language Eff. Since then handlers have become a well-known control mechanism in programming languages.

Handlers and monads excel at simulating effects, either in terms of other effects or as pure computations. For example, the familiar state monad implements mutable state with (pure) state-passing functions, and there are many more examples…

# Coq 8.10.1 is out — Coq, Oct 25, 2019

The 8.10.1 release of Coq is available.

Main changes:

• fix proof of False when using SProp;
• fix an anomaly when unsolved evar in Add Ring;
• fix Ltac regression in binding free names in uconstr;
• fix handling of unicode input before space;
• fix custom extraction of inductives to JSON.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

# MirageOS 3.6.0 release

We are pleased to announce the release of MirageOS 3.6.0. This release updates MirageOS to support Solo5 0.6.0 and later.

New features:

• Support for the Solo5 spt (sandboxed process tender) target via mirage configure -t spt. The spt target runs MirageOS unikernels in a minimal strict seccomp sandbox on Linux x86_64, aarch64 and ppc64le hosts.
• Support for the Solo5 application manifest, enabling support for multiple network and block storage devices on the hvt, spt and muen

# Commas in big numbers everywhere: An OpenType adventure — Jane Street, Oct 14, 2019

My job involves a lot of staring at large numbers, mostly latencies in nanoseconds, and picking out magnitudes like microseconds. I noticed myself constantly counting digits in my text editor, in my terminal, and in Jupyter notebooks in my browser.

# Coq 8.10.0 is out — Coq, Oct 07, 2019

The 8.10.0 release of Coq is available.

Main changes:

• some quality-of-life bug fixes;
• a critical bug fix related to template polymorphism;
• native 63-bit machine integers;
• a new sort of definitionally proof-irrelevant propositions: SProp;
• private universes for opaque polymorphic constants;
• string notations and numeral notations;
• a new simplex-based proof engine for the tactics lia, nia, lra and nra;
• new introduction patterns for SSReflect;
• a tactic to rewrite under binders: under;
• easy input of…

# OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

In our endeavour to encourage professional programmers to understand and use OCaml, OCamlPro will be giving two training sessions, in French, in our Paris offices:

1. OCaml Beginner course for professional programmers (5-6 Nov)
2. OCaml Expertise (7-8 Nov).

The “Expert” OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write “compiler-optimizable” code.

These sessions are …

# Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

We're glad to announce the first release of mrmime, a parser and a generator of emails. This library provides an OCaml way to analyze and craft an email. The eventual goal is to build an entire unikernel-compatible stack for email (such as SMTP or IMAP).

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

## An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the h…

# A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

As you already know if you’ve read our last blogpost, we have updated our OCaml cheat sheets starting with the language and stdlib ones. We know some of you have students to initiate in September and we wanted these sheets to be ready for the start of the school year! We’re working on more sheets for OCaml tools like opam or Dune and important libraries such as Obj Lwt or Core. Keep an eye on our blog or the repo on GitHub to follow all the updates.

Going through the documentation was a jour…

# Coq 8.10+beta3 is out — Coq, Sep 16, 2019

The third beta release of Coq 8.10 is available for testing.

This third β version includes various bug fixes and improvements, including:

• improved warning on coercion path ambiguity;
• support for OCaml extraction of primitive machine integers;
• fix for the soundness issue with template polymorphism;
• fix extraction of dependent record projections to OCaml.

More details are given in the user manual.

Feedback and bug reports are extremely welcome.

# Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

In 2011, we shared several cheat sheets for OCaml. Cheat sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. We hope they will help you out when your rubber duck is rubbish at debugging your code!

Since we first shared them, OCaml and its related tools have evolved. We decided to refresh them and started…

# Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

In our first article we mostly discussed the API design of decompress and did not talk too much about the issue of optimizing performance. In this second article, we will relate our experiences of optimizing decompress.

As you might suspect, decompress needs to be optimized a lot. It was used by several projects as an underlying layer of some formats (like Git), so it can be a real bottleneck in those projects. Of course, we start with a footgun by using a garbage-collected language; comparing t…

# On complete ordered fields — Andrej Bauer, Sep 08, 2019

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

1. A complete ordered field is archimedean.
2. Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If \$b \in …

# An introduction to fuzzing OCaml with AFL, Crowbar and Bun — Tarides (Nathan Rebours), Sep 04, 2019

American Fuzzy Lop or AFL is a fuzzer: a program that tries to find bugs in other programs by sending them various auto-generated inputs. This article covers the basics of AFL and shows an example of fuzzing a parser written in OCaml. It also introduces two extensions: the Crowbar library which can be used to fuzz any kind of OCaml program or function and the Bun tool for integrating fuzzing into your CI.

All of the examples given in this article are available on GitHub at ocaml-afl-examples. Th…

# What is algebraic about algebraic effects? — Andrej Bauer, Sep 02, 2019

Published as arXiv:1807.05923.

Abstract: This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra.…

# The blog moved from Wordpress to Jekyll — Andrej Bauer, Sep 02, 2019

You may have noticed that lately I have had trouble with the blog. It was dying periodically because the backend database kept crashing. It was high time I moved away from Wordpress anyway, so I bit the bullet and ported the blog.

All in all, it was a typical system administration experience: lots of installing Ruby and Node.js packages, figuring out which of several equivalent tools actually is worth using, dealing with scarce and obsolete documentation (a blog post is not a good substitute …

# OCamlPro’s compiler team work update — OCamlPro, Aug 30, 2019

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

A lot of work has been done towards a new framework for optimizations in the compiler, called Flambda2, aiming at solving the shortcomings that became apparent in the Flambda optimization framework (see below for more details). While that work is in progress, the team also worked on some more short-term improvements, notably on the current Flambda optimization framework, a…

# What the interns have wrought, 2019 edition — Jane Street, Aug 30, 2019

Jane Street’s intern program yet again is coming to an end, which is a nice opportunity to look back over the summer and see what they’ve accomplished.

# Decompress: The New Decompress API — Tarides (Romain Calascibetta), Aug 26, 2019

RFC 1951 is one of the most used standards. Indeed, when you launch your Linux kernel, it inflates itself according zlib standard, a superset of RFC 1951. Being a widely-used standard, we decided to produce an OCaml implementation. In the process, we learned many lessons about developing OCaml where we would normally use C. So, we are glad to present decompress.

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress

# Derivations as computations (ICFP 2019 slides) — Andrej Bauer, Aug 21, 2019

Abstract: According to the propositions-as-types reading, programs correspond to proofs, i.e., a term t of type A encodes a derivation D whose conclusion is t : A. But to be quite precise, D may have parts which are not represented in t, such as subderivations of judgmental equalities. In general, a term does not record an e…

View older blog posts.