OCamlPro was created to help OCaml and formal methods spread into the industry. We grew from 1 to 21 engineers, still strongly sharing this ambitious goal! The year 2019 at OCamlPro was very lively, with fantastic accomplishments all along!

Let’s quickly review the past years’ works, first in the world of OCaml (flambda2 & compiler optimisations, opam 2, our Rust-based UI for memprof, tools like tryOCaml, ocp-indent, and supporting the OCaml Software Foundation), then in the wor…

OCamlPro was created to help OCaml and formal methods spread into the industry. We grew from 1 to 21 engineers, still strongly sharing this ambitious goal! The year 2019 at OCamlPro was very lively, with fantastic accomplishments all along!

Let’s quickly review the past years’ works, first in the world of OCaml (flambda2 & compiler optimisations, opam 2, our Rust-based UI for memprof, tools like tryOCaml, ocp-indent, and supporting the OCaml Software Foundation), then in the world of formal methods (new versions of our SMT Solver Alt-Ergo, launch of the Alt-Ergo Users’ Club, the Love language, etc.).

Flambda & Compilation Team

* Work by Pierre Chambart, Vincent Laviron, Guillaume Bury and Pierrick Couderc

Pierre and Vincent’s considerable work on Flambda 2 (the optimizing intermediate representation of the OCaml compiler – on which inlining occurs), in close cooperation with Jane Street (Mark Shinwell, Leo White and their team) aims at overcoming some of flambda’s limitations. We have continued our work on making OCaml programs always faster: internal types are clearer, more concise, and possible control flow transformations are more flexible. Overall a precious outcome for industrial users. In 2019, the major breakthrough was to go from the initial prototype to a complete compiler, which allowed us to compile simple examples first and then to bootstrap it.

On the OCaml compiler side, we also worked with Leo on two new features: functorized compilation units and functorized packs, and recursive packs. The former will allow any developer to implement ‘.ml’ files as if they were functors and not simply modules, and more importantly generate packs that are real functors. As such, this allows to split big functors into several files or to parameterize libraries on other modules. The latter allows two distinct usages: recursive interfaces, to implement recursive types into distinct `.mlis` as long as they do not need any implementation; and recursive packs, whose components are typed and compiled as recursive modules.

• These new features are described on the new RFC repository for OCaml (a similar idea was suggested and implemented in 2011 by Fabrice Le Fessant).
• The implementation is available on GitHub for both functorized packs and recursive packs. Be aware that both are based on an old version of OCaml for now, but should be in sync with the current trunk in the near future.
• See also Vincent’s OCamlPro’s compiler team work update of August 2019.

This work is allowed thanks to Jane Street’s funding.

• More details: on http://opam.ocaml.org
• Releases on Releases on https://github.com/ocaml/opam/releases & our blog

This work is allowed thanks to Jane Street’s funding.

Encouraging OCaml adoption

OCaml Expert trainings for professional programmers

We proposed in 2019 some OCaml expert training specially designed for developers who want to use advanced features and master all the open-source tools and libraries of OCaml.

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 also an opportunity to come discuss with our OPAM & Flambda lead developers and core contributors in Paris.

• Next session: 3-4 March 2020, Paris (registration)

Past projects: blockchain-related achievements (2018-beginning of 2019)

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

This new version contains some small backported fixes and build update:

• Don’t remove git cache objects that may be used [#3831 @AltGr]
• Don’t include .gitattributes in index.tar.gz [#3873 @dra27]
• Update FAQ uri [#3941 @dra27]
• Lock: add warning in case of missing locked file [#3939 @rjbou]
• Directory tracking: fix cached entries retrieving with precise tracking [#4038 @hannesm]
• Build:
  • Add sanity checks [#3934 @dra27]
  • Build man pages …

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

This new version contains some small backported fixes and build update:

• Don’t remove git cache objects that may be used [#3831 @AltGr]
• Don’t include .gitattributes in index.tar.gz [#3873 @dra27]
• Update FAQ uri [#3941 @dra27]
• Lock: add warning in case of missing locked file [#3939 @rjbou]
• Directory tracking: fix cached entries retrieving with precise tracking [#4038 @hannesm]
• Build:
  • Add sanity checks [#3934 @dra27]
  • Build man pages using dune [#3902] #dra27]
  • Add patch and bunzip check for make cold [#4006 @rjbou – fix #3842]
• Shell:
  • fish: add colon for fish manpath [#3886 @rjbou – fix #3878]
• Sandbox:
  • Add dune cache as rw [#4019 @rjbou – fix #4012]
  • Do not fail if $HOME/.ccache is missing [#3957 @mseri]
• opam-devel file: avoid copying extraneous files in opam-devel example [#3999 @maroneze]

As sandbox scripts have been updated, don’t forget to run opam init --reinit -ni to update yours.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, to not break jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

Installation instructions (unchanged):

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github “Releases” page to your PATH. In this case, don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don’t forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for the comments!

If you need more opam in your life, print our cheat sheet!

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

This new version contains some small backported fixes and build update:

• Don't remove git cache objects that may be used [#3831 @AltGr]
• Don't include .gitattributes in index.tar.gz [#3873 @dra27]
• Update FAQ uri [#3941 @dra27]
• Lock: add warning in case of missing locked file [#3939 @rjbou]
• Directory tracking: fix cached entries retrieving with precise tracking [#4038 @hannesm]
• Build:
  • Add sanity checks [#3934 @dra27]
  • Build man pages using dune…

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

This new version contains some small backported fixes and build update:

• Don't remove git cache objects that may be used [#3831 @AltGr]
• Don't include .gitattributes in index.tar.gz [#3873 @dra27]
• Update FAQ uri [#3941 @dra27]
• Lock: add warning in case of missing locked file [#3939 @rjbou]
• Directory tracking: fix cached entries retrieving with precise tracking [#4038 @hannesm]
• Build:
  • Add sanity checks [#3934 @dra27]
  • Build man pages using dune [#3902 ]
  • Add patch and bunzip check for make cold [#4006 @rjbou - fix #3842]
• Shell:
  • fish: add colon for fish manpath [#3886 @rjbou - fix #3878]
• Sandbox:
  • Add dune cache as rw [#4019 @rjbou - fix #4012]
  • Do not fail if $HOME/.ccache is missing [#3957 @mseri]
• opam-devel file: avoid copying extraneous files in opam-devel example [#3999 @maroneze]

As sandbox scripts have been updated, don't forget to run opam init --reinit -ni to update yours.

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, to not break jobs & CIs, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will be kept.

1. From binaries: run

   sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

NOTE: this article is cross-posted on opam.ocaml.org and ocamlpro.com. Please head to the latter for the comments!

Hackers and climate activists join forces in Leipzig

By Damien Leloup, special correspondent, Le Monde. Originally published by Le Monde on December 30, 2019. English translation by the MirageOS Core Team.

The Chaos Communication Congress, the world's largest self-managed event dedicated to IT security, hosted its 36th edition this weekend in Germany.

In front of Leipzig station, around fifty students and high school students are gathered. It's Sunday, but the local branch of the Fridays for F…

Hackers and climate activists join forces in Leipzig

By Damien Leloup, special correspondent, Le Monde. Originally published by Le Monde on December 30, 2019. English translation by the MirageOS Core Team.

The Chaos Communication Congress, the world's largest self-managed event dedicated to IT security, hosted its 36th edition this weekend in Germany.

In front of Leipzig station, around fifty students and high school students are gathered. It's Sunday, but the local branch of the Fridays for Future movement, which organizes demonstrations on Fridays at the call of activist Greta Thunberg, made an exception to its usual calendar to take advantage of the presence, a few kilometers from there, of the Chaos Communication Congress (CCC).

Organized each year for thirty-six years, this gigantic gathering of hackers and activists - 18,000 participants, dozens of conference talks around the clock - invades the Leipzig convention center for four days, in an atmosphere that is both anarcho-libertarian and very family oriented. For the first time, the slogan of the 2019 edition is devoted to the environment: “Resource exhaustion”, a reference both to a computer attack technique and to the preservation of the planet.

"It makes sense: it's a major issue, and the environmental movement is a highlight of the year, isn't it?", notes, hair dyed pink and megaphone in hand, Rune, one of the organizers of the event. “In any case, we are very happy that the CCC opened its doors to us and supports us."

The conference program gave pride of place to ecological themes and organizations such as Fridays for Future or Extinction Rebellion. These themes were all features in the main talks. The audience for the event, marked on the far left, is quite sensitive to environmental issues. Fridays for Future's review of the year was sold out; the track where some scientists explained how they build their climate models was full and was not able to host all the attendees.

Safety of power plants and the right to repair

But if the CCC has given a lot of space to environmental issues, it has done it in its own way. In this mecca of cyber-security, we could for example discover long lists of vulnerabilities affecting the on-board systems used to manage the turbines of power plants. Do not panic: "These flaws do not block a power plant, or cut the power of a city," relativized Radu Motspan, the author of the study. Some of them have been corrected; for others, it is up to plant managers to carry out verifications. The researcher and his associates produced a small turnkey guide to help them: “No need to hire expensive consultants, you can do everything yourself."

This “do it yourself” spirit, omnipresent in hacker culture in general and at the CCC in particular, easily lends itself to an environmental translation. The collective Runder Tisch Reparatur, which campaigns for the adoption at European level of a "right to repair", was thus invited for the first time to the conference. The philosophy of the movement, which aims above all to reduce the amount of waste produced by obsolescence whether or not it is programmed, is very similar to that of the free software movement, say Eduard and Erik, who run the stand of the association. "An object that you cannot repair does not really belong to you," they believe, just as the promoters of free software believe that software that you cannot modify yourself deprives you of certain freedoms.

But the main issue, at the heart of many talks during the four days of the CCC, is that of the energy impact of the Internet. No one in the aisles of the Leipzig congress center plans to reduce their use of the Internet; but everyone concedes that the network consumes a lot of electricity unnecessarily, or uses too much fossil energy. "There are simple things to do to improve the carbon footprint of a site or service," said Chris Adams, environmental activist and member of the Green Web Foundation. “If your service uses Amazon Web Service [AWS, a very popular cloud service], you can choose the data center you want to use, for example. The one assigned to you by default may be in a country that produces little renewable electricity and uses a lot of coal for its power plants… ”

Existing non-digital systems (like boilers) already have ways to function more efficiently, such as off-peak hours at night, when electricity is both cheaper and more eco-friendly. There are equivalent options for more modern, digital systems, for instance: Chris Adams advocates the use of the Low Carbon Kubernetes Scheduler, an orchestration tool which allows to optimise the power consumption of a server in order to reduce its environmental impact.

Safety and minimum consumption, get the best of both worlds

Despite everything, the “greenest” electricity remains that which we do not consume in the first place. There too, promising solutions exist: Hannes Mehnert, a German computer scientist, presented at the opening of the CCC the MirageOS project, an operating system for ultra-minimalist servers, coded in a language renowned for its lightness, and which runs each process in a dedicated virtual machine. A radical approach - and reserved for connoisseurs - which allows the software to embed only the bare minimum of lines of code in each compiled version. "Reducing complexity mathematically reduces the number of calculation operations required," explains Mehnert. Result: "A carbon footprint that drops drastically, with ten times less computing power used by the processor, and up to twenty-five times less memory used", according to his measurements.

Above all, and this is a strong argument at a conference dedicated to computer security, minimalism is also a real advantage in terms of potential vulnerabilities: the more compact the code is, the less it risks containing flaws or errors. And such systems are also better protected and safer than more conventional systems, as they are not vulnerable to memory-safety issues.

But the collaboration between environmentalists and privacy advocates seemed much broader than just focusing on technical issues. That mix was everywhere: for instance the corridor walls had graffiti concerned with the the excessive consumption of CO2 on the planet close to others highlighting the fact that every human being generates, on average, 1.7 MB of data per second. The posters of the anarchist or anti-fascist movements were also mixed with the flyers of the collective Hackers against Climate Change, which attracted the curious with a joke typical of the place: "cli / mate crisis is real", in reference to Club-Mate, an ubiquitous drink at the event.

This community of views between hackers and climate activists comes as little surprise in Germany, where both movements are very present, and even less in Leipzig, the flagship city of the former GDR where pre-Internet mass surveillance tools from the Stasi were also directed against environmental activists in the 1980s. Some environmental movements feel naturally close to the anarchist spirit of the German hackers of the Chaos Computer Club, which organizes the CCC: a talk by Extinction Rebellion detailed the security measures they took to ensure their privacy, and how they didn't depend on third-party tools from Facebook, Google or Amazon - responsible, in their eyes, both for mass surveillance and green washing.

However, in this atmosphere of global collaboration some questions remained unanswered. In some specific cases, better IT security can also consume more resources. A talk dedicated to encrypted messaging thus presented many tools which make it possible to reinforce the confidentiality of exchanges, but also require using more computing power, to encrypt or decrypt messages, or even request the sending of large quantities of data to scramble the origin or volume of a message. This first CCC under the sign of environmental protection did not really address this contradiction - pending, perhaps, a next edition?

Goal

Have your domain served by OCaml-DNS authoritative name servers. Data is stored in a git remote, and let's encrypt certificates can be requested to DNS. This software is deployed since more than two years for several domains such as nqsb.io and robur.coop. This present the authoritative server side, and certificate library of the OCaml-DNS implementation formerly known as µDNS.

Prerequisites

You need to own a domain, and be able to delegate the name service to your own servers. You…

Goal

Have your domain served by OCaml-DNS authoritative name servers. Data is stored in a git remote, and let's encrypt certificates can be requested to DNS. This software is deployed since more than two years for several domains such as nqsb.io and robur.coop. This present the authoritative server side, and certificate library of the OCaml-DNS implementation formerly known as µDNS.

Prerequisites

You need to own a domain, and be able to delegate the name service to your own servers. You also need two spare public IPv4 addresses (in different /24 networks) for your name servers. A git server or remote repository reachable via git over ssh. Servers which support solo5 guests, and have the corresponding tender installed. A computer with opam (>= 2.0.0) installed.

Data preparation

Figure out a way to get the DNS entries of your domain in a "master file format", i.e. what bind uses.

This is a master file for the mirage domain, defining $ORIGIN to avoid typing the domain name after each hostname (use @ if you need the domain name only; if you need to refer to a hostname in a different domain end it with a dot (.), i.e. ns2.foo.com.). The default time to live $TTL is an hour (3600 seconds). The zone contains a start of authority (SOA) record containing the nameserver, hostmaster, serial, refresh, retry, expiry, and minimum. Also, a single name server (NS) record ns1 is specified with an accompanying address (A) records pointing to their IPv4 address.

git-repo> cat mirage
$ORIGIN mirage.
$TTL 3600
@    SOA    ns1    hostmaster    1    86400    7200    1048576    3600
@    NS    ns1
ns1     A       127.0.0.1
www    A    1.1.1.1
git-repo> git add mirage && git commit -m initial && git push

Installation

On your development machine, you need to install various OCaml packages. You don't need privileged access if common tools (C compiler, make, libgmp) are already installed. You have opam installed.

Let's create a fresh switch for the DNS journey:

$ opam init
$ opam update
$ opam switch create udns 4.09.0
# waiting a bit, a fresh OCaml compiler is getting bootstrapped
$ eval `opam env` #sets some environment variables

The last command set environment variables in your current shell session, please use the same shell for the commands following (or run eval $(opam env) in another shell and proceed in there - the output of opam switch sohuld point to udns).

Validation of our zonefile

First let's check that OCaml-DNS can parse our zonefile:

$ opam install dns-cli #installs ~/.opam/udns/bin/ozone and other binaries
$ ozone <git-repo>/mirage # see ozone --help
successfully checked zone

Great. Error reporting is not great, but line numbers are indicated (ozone: zone parse problem at line 3: syntax error), lexer and parser are lex/yacc style (PRs welcome).

FWIW, ozone accepts --old <filename> to check whether an update from the old zone to the new is fine. This can be used as pre-commit hook in your git repository to avoid bad parse states in your name servers.

Getting the primary up

The next step is to compile the primary server and run it to serve the domain data. Since the git-via-ssh client is not yet released, we need to add a custom opam repository to this switch.

# git via ssh is not yet released, but this opam repository contains the branch information
$ opam repo add git-ssh git+https://github.com/roburio/git-ssh-dns-mirage3-repo.git
# get the `mirage` application via opam
$ opam install lwt mirage

# get the source code of the unikernels
$ git clone -b future https://github.com/roburio/unikernels.git
$ cd unikernels/primary-git

# let's build the server first as unix application
$ mirage configure --prng fortuna #--no-depext if you have all system dependencies
$ make depend
$ make

# run it
$ ./primary_git
# starts a unix process which clones https://github.com/roburio/udns.git
# attempts to parse the data as zone files, and fails on parse error
$ ./primary-git --remote=https://my-public-git-repository
# this should fail with ENOACCESS since the DNS server tries to listen on port 53

# which requires a privileged user, i.e. su, sudo or doas
$ sudo ./primary-git --remote=https://my-public-git-repository
# leave it running, run the following programs in a different shell

# test it
$ host ns1.mirage 127.0.0.1
ns1.mirage has address 127.0.0.1
$ dig any mirage @127.0.0.1
# a DNS packet printout with all records available for mirage

That's exciting, the DNS server serving answers from a remote git repository.

Securing the git access with ssh

Let's authenticate the access by using ssh, so we feel ready to push data there as well. The primary-git unikernel already includes an experimental ssh client, all we need to do is setting up credentials - in the following a RSA keypair and the server fingerprint.

# collect the RSA host key fingerprint
$ ssh-keyscan <git-server> > /tmp/git-server-public-keys
$ ssh-keygen -l -E sha256 -f /tmp/git-server-public-keys | grep RSA
2048 SHA256:a5kkkuo7MwTBkW+HDt4km0gGPUAX0y1bFcPMXKxBaD0 <git-server> (RSA)
# we're interested in the SHA256:yyy only

# generate a ssh keypair
$ awa_gen_key # installed by the make depend step above in ~/.opam/udns/bin
seed is pIKflD07VT2W9XpDvqntcmEW3OKlwZL62ak1EZ0m
ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQC5b2cSSkZ5/MAu7pM6iJLOaX9tJsfA8DB1RI34Zygw6FA0y8iisbqGCv6Z94ZxreGATwSVvrpqGo5p0rsKs+6gQnMCU1+sOC4PRlxy6XKgj0YXvAZcQuxwmVQlBHshuq0CraMK9FASupGrSO8/dW30Kqy1wmd/IrqW9J1Cnw+qf0C/VEhIbo7btlpzlYpJLuZboTvEk1h67lx1ZRw9bSPuLjj665yO8d0caVIkPp6vDX20EsgITdg+cFjWzVtOciy4ETLFiKkDnuzHzoQ4EL8bUtjN02UpvX2qankONywXhzYYqu65+edSpogx2TuWFDJFPHgcyO/ZIMoluXGNgQlP awa@awa.local
# please run your own awa_gen_key, don't use the numbers above

The public key needs is in standard OpenSSH format and needs to be added to the list of accepted keys on your server - the exact steps depend on your git server, if you're running your own with gitosis, add it as new public key file and grant that key access to the data repository. If you use gitlab or github, you may want to create a new user account and with the generated key.

The private key is not displayed, but only the seed required to re-generate it, when using the same random number generator, in our case fortuna implemented by nocrypto - used by both awa_gen_key and primary_git. The seed is provided as command-line argument while starting primary_git:

# execute with git over ssh, authenticator from ssh-keyscan, seed from awa_gen_key
$ ./primary_git --authenticator=SHA256:a5kkkuo7MwTBkW+HDt4km0gGPUAX0y1bFcPMXKxBaD0 --seed=pIKflD07VT2W9XpDvqntcmEW3OKlwZL62ak1EZ0m --remote=ssh://git@<git-server>/repo-name.git
# started up, you can try the host and dig commands from above if you like

To wrap up, we now have a primary authoritative name server for our zone running as Unix process, which clones a remote git repository via ssh on startup and then serves it.

Authenticated data updates

Our remote git repository is the source of truth, if you need to add a DNS entry to the zone, you git pull, edit the zone file, remember to increase the serial in the SOA line, run ozone, git commit and push to the repository.

So, the primary_git needs to be informed of git pushes. This requires a communication channel from the git server (or somewhere else, e.g. your laptop) to the DNS server. I prefer in-protocol solutions over adding yet another protocol stack, no way my DNS server will talk HTTP REST.

The DNS protocol has an extension for notifications of zone changes (as a DNS packet), usually used between the primary and secondary servers. The primary_git accepts these notify requests (i.e. bends the standard slightly), and upon receival pulls the remote git repository, and serves the fresh zone files. Since a git pull may be rather excessive in terms of CPU cycles and network bandwidth, only authenticated notifications are accepted.

The DNS protocol specifies in another extension authentication (DNS TSIG) with transaction signatures on DNS packets including a timestamp and fudge to avoid replay attacks. As key material hmac secrets distribued to both the communication endpoints are used.

To recap, the primary server is configured with command line parameters (for remote repository url and ssh credentials), and serves data from a zonefile. If the secrets would be provided via command line, a restart would be necessary for adding and removing keys. If put into the zonefile, they would be publicly served on request. So instead, we'll use another file, still in zone file format, in the top-level domain _keys, i.e. the mirage._keys file contains keys for the mirage zone. All files ending in ._keys are parsed with the normal parser, but put into an authentication store instead of the domain data store, which is served publically.

For encoding hmac secrets into DNS zone file format, the DNSKEY format is used (designed for DNSsec). The bind software comes with dnssec-keygen and tsig-keygen to generate DNSKEY output: flags is 0, protocol is 3, and algorithm identifier for SHA256 is 163 (SHA384 164, SHA512 165). This is reused by the OCaml DNS library. The key material itself is base64 encoded.

Access control and naming of keys follows the DNS domain name hierarchy - a key has the form name._operation.domain, and has access granted to domain and all subdomains of it. Two operations are supported: update and transfer. In the future there may be a dedicated notify operation, for now we'll use update. The name part is ignored for the update operation.

Since we now embedd secret information in the git repository, it is a good idea to restrict access to it, i.e. make it private and not publicly cloneable or viewable. Let's generate a first hmac secret and send a notify:

$ dd if=/dev/random bs=1 count=32 | b64encode -
begin-base64 644 -
kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg=
====
[..]
git-repo> echo "personal._update.mirage. DNSKEY 0 3 163 kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg=" > mirage._keys
git-repo> git add mirage._keys && git commit -m "add hmac secret" && git push

# now we need to restart the primary git to get the git repository with the key
$ ./primary_git --seed=... # arguments from above, remote git, host key fingerprint, private key seed

# now test that a notify results in a git pull
$ onotify 127.0.0.1 mirage --key=personal._update.mirage:SHA256:kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg=
# onotify was installed by dns-cli in ~/.opam/udns/bin/onotify, see --help for options
# further changes to the hmac secrets don't require a restart anymore, a notify packet is sufficient :D

Ok, this onotify command line could be setup as a git post-commit hook, or run manually after each manual git push.

Secondary

It's time to figure out how to integrate the secondary name server. An already existing bind or something else that accepts notifications and issues zone transfers with hmac-sha256 secrets should work out of the box. If you encounter interoperability issues, please get in touch with me.

The secondary subdirectory of the cloned unikernels repository is another unikernel that acts as secondary server. It's only command line argument is a list of hmac secrets used for authenticating that the received data originates from the primary server. Data is initially transferred by a full zone transfer (AXFR), later updates (upon refresh timer or notify request sent by the primary) use incremental (IXFR). Zone transfer requests and data are authenticated with transaction signatures again.

Convenience by OCaml DNS is that transfer key names matter, and are of the form <primary-ip>.<secondary-ip>._transfer.domain, i.e. 1.1.1.1.2.2.2.2._transfer.mirage if the primary server is 1.1.1.1, and the secondary 2.2.2.2. Encoding the IP address in the name allows both parties to start the communication: the secondary starts by requesting a SOA for all domains for which keys are provided on command line, and if an authoritative SOA answer is received, the AXFR is triggered. The primary server emits notification requests on startup and then on every zone change (i.e. via git pull) to all secondary IP addresses of transfer keys present for the specific zone in addition to the notifications to the NS records in the zone.

$ cd ../secondary
$ mirage configure --prng fortuna
# make depend should not be needed since all packages are already installed by the primary-git
$ make
$ ./secondary

IP addresses and routing

Both primary and secondary serve the data on the DNS port (53) on UDP and TCP. To run both on the same machine and bind them to different IP addresses, we'll use a layer 2 network (ethernet frames) with a host system software switch (bridge interface service), the unikernels as virtual machines (or seccomp-sandboxed) via the solo5 backend. Using xen is possible as well. As IP address range we'll use 10.0.42.0/24, and the host system uses the 10.0.42.1.

The primary git needs connectivity to the remote git repository, thus on a laptop in a private network we need network address translation (NAT) from the bridge where the unikernels speak to the Internet where the git repository resides.

# on FreeBSD:
# configure NAT with pf, you need to have forwarding enabled
$ sysctl net.inet.ip.forwarding: 1
$ echo 'nat pass on wlan0 inet from 10.0.42.0/24 to any -> (wlan0)' >> /etc/pf.conf
$ service pf restart

# make tap interfaces UP on open()
$ sysctl net.link.tap.up_on_open: 1

# bridge creation, naming, and IP setup
$ ifconfig bridge create
bridge0
$ ifconfig bridge0 name service
$ ifconfig bridge0 10.0.42.1/24

# two tap interfaces for our unikernels
$ ifconfig tap create
tap0
$ ifconfig tap create
tap1
# add them to the bridge
$ ifconfig service addm tap0 addm tap1

Primary and secondary setup

Let's update our zone slightly to reflect the IP changes.

git-repo> cat mirage
$ORIGIN mirage.
$TTL 3600
@    SOA    ns1    hostmaster    2    86400    7200    1048576    3600
@    NS    ns1
@    NS    ns2
ns1     A       10.0.42.2
ns2    A    10.0.42.3

# we also need an additional transfer key
git-repo> cat mirage._keys
personal._update.mirage. DNSKEY 0 3 163 kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg=
10.0.42.2.10.0.42.3._transfer.mirage. DNSKEY 0 3 163 cDK6sKyvlt8UBerZlmxuD84ih2KookJGDagJlLVNo20=
git-repo> git commit -m "udpates" . && git push

Ok, the git repository is ready, now we need to compile the unikernels for the virtualisation target (see other targets for further information).

# back to primary
$ cd ../primary-git
$ mirage configure -t hvt --prng fortuna # or e.g. -t spt (and solo5-spt below)
# installs backend-specific opam packages, recompiles some
$ make depend
$ make
[...]
$ solo5-hvt --net:service=tap0 -- primary_git.hvt --ipv4=10.0.42.2/24 --ipv4-gateway=10.0.42.1 --seed=.. --authenticator=.. --remote=ssh+git://...
# should now run as a virtual machine (kvm, bhyve), and clone the git repository
$ dig any mirage @10.0.42.2
# should reply with the SOA and NS records, and also the name server address records in the additional section

# secondary
$ cd ../secondary
$ mirage configure -t hvt --prng fortuna
$ make
$ solo5-hvt --net:service=tap1 -- secondary.hvt --ipv4=10.0.42.3/24 --keys=10.0.42.2.10.0.42.3._transfer.mirage:SHA256:cDK6sKyvlt8UBerZlmxuD84ih2KookJGDagJlLVNo20=
# an ipv4-gateway is not needed in this setup, but in real deployment later
# it should start up and transfer the mirage zone from the primary

$ dig any mirage @10.0.42.3
# should now output the same information as from 10.0.42.2

# testing an update and propagation
# edit mirage zone, add a new record and increment the serial number
git-repo> echo "foo A 127.0.0.1" >> mirage
git-repo> vi mirage <- increment serial
git-repo> git commit -m 'add foo' . && git push
$ onotify 10.0.42.2 mirage --key=personal._update.mirage:SHA256:kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg=

# now check that it worked
$ dig foo.mirage @10.0.42.2 # primary
$ dig foo.mirage @10.0.42.3 # secondary got notified and transferred the zone

You can also check the behaviour when restarting either of the VMs, whenever the primary is available the zone is synchronised. If the primary is down, the secondary still serves the zone. When the secondary is started while the primary is down, it won't serve any data until the primary is online (the secondary polls periodically, the primary sends notifies on startup).

Dynamic data updates via DNS, pushed to git

DNS is a rich protocol, and it also has builtin updates that are supported by OCaml DNS, again authenticated with hmac-sha256 and shared secrets. Bind provides the command-line utility nsupdate to send these update packets, a simple oupdate unix utility is available as well (i.e. for integration of dynamic DNS clients). You know the drill, add a shared secret to the primary, git push, notify the primary, and voila we can dynamically in-protocol update. An update received by the primary via this way will trigger a git push to the remote git repository, and notifications to the secondary servers as described above.

# being lazy, I reuse the key above
$ oupdate 10.0.42.2 personal._update.mirage:SHA256:kJJqipaQHQWqZL31Raar6uPnepGFIdtpjkXot9rv2xg= my-other.mirage 1.2.3.4

# let's observe the remote git
git-repo> git pull
# there should be a new commit generated by the primary
git-repo> git log

# test it, should return 1.2.3.4
$ dig my-other.mirage @10.0.42.2
$ dig my-other.mirage @10.0.42.3

So we can deploy further oupdate (or nsupdate) clients, distribute hmac secrets, and have the DNS zone updated. The source of truth is still the git repository, where the primary-git pushes to. Merge conflicts and timing of pushes is not yet dealt with. They are unlikely to happen since the primary is notified on pushes and should have up-to-date data in storage. Sorry, I'm unsure about the error semantics, try it yourself.

Let's encrypt!

Let's encrypt is a certificate authority (CA), which certificate is shipped as trust anchor in web browsers. They specified a protocol for automated certificate management environment (ACME), used to get X509 certificates for your services. In the protocol, a certificate signing request (publickey and hostname) is sent to let's encrypt servers, which sends a challenge to proof the ownership of the hostnames. One widely-used way to solve this challenge is running a web server, another is to serve it as text record from the authoritative DNS server.

Since I avoid persistent storage when possible, and also don't want to integrate a HTTP client stack in the primary server, I developed a third unikernel that acts as (hidden) secondary server, performs the tedious HTTP communication with let's encrypt servers, and stores all data in the public DNS zone.

For encoding of certificates, the DANE working group specified TLSA records in DNS. They are quadruples of usage, selector, matching type, and ASN.1 DER-encoded material. We set usage to 3 (domain-issued certificate), matching type to 0 (no hash), and selector to 0 (full certificate) or 255 (private usage) for certificate signing requests. The interaction is as follows:

1. Primary, secondary, and let's encrypt unikernels are running
2. A service (ocertify, unikernels/certificate, or the dns-certify.mirage library) demands a TLS certificate, and has a hmac-secret for the primary DNS
3. The service generates a certificate signing request with the desired hostname(s), and performs an nsupdate with TLSA 255 <DER encoded signing-request>
4. The primary accepts the update, pushes the new zone to git, and sends notifies to secondary and let's encrypt unikernels which (incrementally) transfer the zone
5. The let's encrypt unikernel notices while transferring the zone a signing request without a certificate, starts HTTP interaction with let's encrypt
6. The let's encrypt unikernel solves the challenge, sends the response as update of a TXT record to the primary nameserver
7. The primary pushes the TXT record to git, and notifies secondaries (which transfer the zone)
8. The let's encrypt servers request the TXT record from either or both authoritative name servers
9. The let's encrypt unikernel polls for the issued certificate and send an update to the primary TLSA 0 <DER encoded certificate>
10. The primary pushes the certificate to git, notifies secondaries (which transfer the zone)
11. The service polls TLSA records for the hostname, and use it upon retrieval

Note that neither the signing request nor the certificate contain private key material, thus it is fine to serve them publically. Please also note, that the service polls for the certificate for the hostname in DNS, which is valid (start and end date) certificate and uses the same public key, this certificate is used and steps 3-10 are not executed.

The let's encrypt unikernel does not serve anything, it is a reactive system which acts upon notification from the primary. Thus, it can be executed in a private address space (with a NAT). Since the OCaml DNS server stack needs to push notifications to it, it preserves all incoming signed SOA requests as candidates for notifications on update. The let's encrypt unikernel ensures to always have a connection to the primary to receive notifications.

# getting let's encrypt up and running
$ cd ../lets-encrypt
$ mirage configure -t hvt --prng fortuna
$ make depend
$ make

# run it
$ solo5-hvt --net:service=tap2 -- letsencrypt.hvt --keys=...

# test it
$ ocertify 10.0.42.2 foo.mirage

For actual testing with let's encrypt servers you need to have the primary and secondary deployed on your remote hosts, and your domain needs to be delegated to these servers. Good luck. And ensure you have backup your git repository.

As fine print, while this tutorial was about the mirage zone, you can stick any number of zones into the git repository. If you use a _keys file (without any domain prefix), you can configure hmac secrets for all zones, i.e. something to use in your let's encrypt unikernel and secondary unikernel. Dynamic addition of zones is supported, just create a new zonefile and notify the primary, the secondary will be notified and pick it up. The primary responds to a signed SOA for the root zone (i.e. requested by the secondary) with the SOA response (not authoritative), and additionally notifications for all domains of the primary.

Conclusion and thanks

This tutorial presented how to use the OCaml DNS based unikernels to run authoritative name servers for your domain, using a git repository as the source of truth, dynamic authenticated updates, and let's encrypt certificate issuing.

There are further steps to take, such as monitoring -- have a look at the monitoring branch of the opam repository above, and the future-robur branch of the unikernels repository above, which use a second network interface for reporting syslog and metrics to telegraf / influx / grafana. Some DNS features are still missing, most prominently DNSSec.

I'd like to thank all people involved in this software stack, without other key components, including git, irmin 2.0, nocrypto, awa-ssh, cohttp, solo5, mirage, ocaml-letsencrypt, and more.

If you want to support our work on MirageOS unikernels, please donate to robur. I'm interested in feedback, either via twitter, hannesm@mastodon.social or an issue on the data repository.

Reproducible builds summit

I'm just back from the Reproducible builds summit 2019. In 2018, several people developing OCaml and opam and MirageOS, attended the Reproducible builds summit in Paris. The notes from last year on opam reproducibility and MirageOS reproducibility are online. After last years workshop, Raja started developing the opam reproducibilty builder orb, which I extended at and after this years summit. This year before and after the facilitated summit there were hacking …

Reproducible builds summit

I'm just back from the Reproducible builds summit 2019. In 2018, several people developing OCaml and opam and MirageOS, attended the Reproducible builds summit in Paris. The notes from last year on opam reproducibility and MirageOS reproducibility are online. After last years workshop, Raja started developing the opam reproducibilty builder orb, which I extended at and after this years summit. This year before and after the facilitated summit there were hacking days, which allowed further interaction with participants, writing some code and conduct experiments. I had this year again an exciting time at the summit and hacking days, thanks to our hosts, organisers, and all participants.

Goal

Stepping back a bit, first look on the goal of reproducible builds: when compiling source code multiple times, the produced binaries should be identical. It should be sufficient if the binaries are behaviourally equal, but this is pretty hard to check. It is much easier to check bit-wise identity of binaries, and relaxes the burden on the checker -- checking for reproducibility is reduced to computing the hash of the binaries. Let's stick to the bit-wise identical binary definition, which also means software developers have to avoid non-determinism during compilation in their toolchains, dependent libraries, and developed code.

A checklist of potential things leading to non-determinism has been written up by the reproducible builds project. Examples include recording the build timestamp into the binary, ordering of code and embedded data. The reproducible builds project also developed disorderfs for testing reproducibility and diffoscope for comparing binaries with file-dependent readers, falling back to objdump and hexdump. A giant test infrastructure with lots of variations between the builds, mostly using Debian, has been setup over the years.

Reproducibility is a precondition for trustworthy binaries. See why does it matter. If there are no instructions how to get from the published sources to the exact binary, why should anyone trust and use the binary which claims to be the result of the sources? It may as well contain different code, including a backdoor, bitcoin mining code, outputting the wrong results for specific inputs, etc. Reproducibility does not imply the software is free of security issues or backdoors, but instead of a audit of the binary - which is tedious and rarely done - the source code can be audited - but the toolchain (compiler, linker, ..) used for compilation needs to be taken into account, i.e. trusted or audited to not be malicious. I will only ever publish binaries if they are reproducible.

My main interest at the summit was to enhance existing tooling and conduct some experiments about the reproducibility of MirageOS unikernels -- a unikernel is a statically linked ELF binary to be run as Unix process or virtual machine. MirageOS heavily uses OCaml and opam, the OCaml package manager, and is an opam package itself. Thus, checking reproducibility of a MirageOS unikernel is the same problem as checking reproducibility of an opam package.

Reproducible builds with opam

Testing for reproducibility is achieved by taking the sources and compile them twice independently. Afterwards the equality of the resulting binaries can be checked. In trivial projects, the sources is just a single file, or originate from a single tarball. In OCaml, opam uses a community repository where OCaml developers publish their package releases to, but can also use custom repositores, and in addition pin packages to git remotes (url including branch or commit), or a directory on the local filesystem. Manually tracking and updating all dependent packages of a MirageOS unikernel is not feasible: our hello-world compiled for hvt (kvm/BHyve) already has 79 opam dependencies, including the OCaml compiler which is distribued as opam package. The unikernel serving this website depends on 175 opam packages.

Conceptually there should be two tools, the initial builder, which takes the latest opam packages which do not conflict, and exports exact package versions used during the build, as well as hashes of binaries. The other tool is a rebuilder, which imports the export, conducts a build, and outputs the hashes of the produced binaries.

Opam has the concept of a switch, which is an environment where a package set is installed. Switches are independent of each other, and can already be exported and imported. Unfortunately the export is incomplete: if a package includes additional patches as part of the repository -- sometimes needed for fixing releases where the actual author or maintainer of a package responds slowly -- these package neither the patches end up in the export. Also, if a package is pinned to a git branch, the branch appears in the export, but this may change over time by pushing more commits or even force-pushing to that branch. In PR #4040 (under discussion and review), also developed during the summit, I propose to embed the additional files as base64 encoded values in the opam file. To solve the latter issue, I modified the export mechanism to embed the git commit hash (PR #4055), and avoid sources from a local directory and which do not have a checksum.

So the opam export contains the information required to gather the exact same sources and build instructions of the opam packages. If the opam repository would be self-contained (i.e. not depend on any other tools), this would be sufficient. But opam does not run in thin air, it requires some system utilities such as /bin/sh, sed, a GNU make, commonly git, a C compiler, a linker, an assembler. Since opam is available on various operating systems, the plugin depext handles host system dependencies, e.g. if your opam package requires gmp to be installed, this requires slightly different names depending on host system or distribution, take a look at conf-gmp. This also means, opam has rather good information about both the opam dependencies and the host system dependencies for each package. Please note that the host system packages used during compilation are not yet recorded (i.e. which gmp package was installed and used during the build, only that a gmp package has to be installed). The base utilities mentioned above (C compiler, linker, shell) are also not recorded yet.

Operating system information available in opam (such as architecture, distribution, version), which in some cases maps to exact base utilities, is recorded in the build-environment, a separate artifact. The environment variable SOURCE_DATE_EPOCH, used for communicating the same timestamp when software is required to record a timestamp into the resulting binary, is also captured in the build environment.

Additional environment variables may be captured or used by opam packages to produce different output. To avoid this, both the initial builder and the rebuilder are run with minimal environment variables: only PATH (normalised to a whitelist of /bin, /usr/bin, /usr/local/bin and /opt/bin) and HOME are defined. Missing information at the moment includes CPU features: some libraries (gmp?, nocrypto) emit different code depending on the CPU feature.

Tooling

TL;DR: A build builds an opam package, and outputs .opam-switch, .build-hashes.N, and .build-environment.N. A rebuild uses these artifacts as input, builds the package and outputs another .build-hashes.M and .build-environment.M.

The command-line utility orb can be installed and used:

$ opam pin add orb git+https://github.com/hannesm/orb.git#active
$ orb build --twice --keep-build-dir --diffoscope <your-favourite-opam-package>

It provides two subcommands build and rebuild. The build command takes a list of local opam --repos where to take opam packages from (defaults to default), a compiler (either a variant --compiler=4.09.0+flambda, a version --compiler=4.06.0, or a pin to a local development version --compiler-pin=~/ocaml), and optionally an existing switch --use-switch. It creates a switch, builds the packages, and emits the opam export, hashes of all files installed by these packages, and the build environment. The flags --keep-build retains the build products, opam's --keep-build-dir in addition temporary build products and generated source code. If --twice is provided, a rebuild (described next) is executed after the initial build.

The rebuild command takes a directory with the opam export and build environment to build the opam package. It first compares the build-environment with the host system, sets the SOURCE_DATE_EPOCH and switch location accordingly and executes the import. Once the build is finished, it compares the hashes of the resulting files with the previous run. On divergence, if build directories were kept in the previous build, and if diffoscope is available and --diffoscope was provided, diffoscope is run on the diverging files. If --keep-build-dir was provided as well, diff -ur can be used to compare the temporary build and sources, including build logs.

The builds are run in parallel, as opam does, this parallelism does not lead to different binaries in my experiments.

Results and discussion

All MirageOS unikernels I have deployed are reproducible \o/. Also, several binaries such as orb itself, opam, solo5-hvt, and all albatross utilities are reproducible.

The unikernel range from hello world, web servers (e.g. this blog, getting its data on startup via a git clone to memory), authoritative DNS servers, CalDAV server. They vary in size between 79 and 200 opam packages, resulting in 2MB - 16MB big ELF binaries (including debug symbols). The unikernel opam repository contains some reproducible unikernels used for testing. Some work-in-progress enhancements are needed to achieve this:

At the moment, the opam package of a MirageOS unikernel is automatically generated by mirage configure, but only used for tracking opam dependencies. I worked on mirage PR #1022 to extend the generated opam package with build and install instructions.

As mentioned above, if locale is set, ocamlgraph needs to be patched to emit a (locale-dependent) timestamp.

The OCaml program crunch embeds a subdirectory as OCaml code into a binary, which we use in MirageOS quite regularly for static assets, etc. This plays in several ways into reproducibility: on the one hand, it needs a timestamp for its last_modified functionality (and adheres since June 2018 to the SOURCE_DATE_EPOCH spec, thanks to Xavier Clerc). On the other hand, it used before version 3.2.0 (released Dec 14th) hashtables for storing the file contents, where iteration is not deterministic (the insertion is not sorted), fixed in PR #51 by using a Map instead.

In functoria, a tool used to configure MirageOS devices and their dependencies, can emit a list of opam packages which were required to build the unikernel. This uses opam list --required-by --installed --rec <pkgs>, which uses the cudf graph (thanks to Raja for explanation), that is during the rebuild dropping some packages. The PR #189 avoids by not using the --rec argument, but manually computing the fixpoint.

Certainly, the choice of environment variables, and whether to vary them (as debian does) or to not define them (or normalise) while building, is arguably. Since MirageOS does neither support time zone nor internationalisation, there is no need to prematurely solving this issue. On related note, even with different locale settings, MirageOS unikernels are reproducible apart from an issue in ocamlgraph #90 embedding the output of date, which is different depending on LANG and locale (LC_*) settings.

Prior art in reproducible MirageOS unikernels is the mirage-qubes-firewall. Since early 2017 it is reproducible. Their approach is different by building in a docker container with the opam repository pinned to an exact git commit.

Further work

I only tested a certain subset of opam packages and MirageOS unikernels, mainly on a single machine (my laptop) running FreeBSD, and am happy if others will test reproducibility of their OCaml programs with the tools provided. There could as well be CI machines rebuilding opam packages and reporting results to a central repository. I'm pretty sure there are more reproducibility issues in the opam ecosystem. I developed an reproducible testing opam repository with opam packages that do not depend on OCaml, mainly for further tooling development. Some tests were also conducted on a Debian system with the same result. The variations, apart from build time, were using a different user, and different locale settings.

As mentioned above, more environment, such as the CPU features, and external system packages, should be captured in the build environment.

When comparing OCaml libraries, some output files (cmt / cmti / cma / cmxa) are not deterministic, but contain minimal diverge where I was not able to spot the root cause. It would be great to fix this, likely in the OCaml compiler distribution. Since the final result, the binary I'm interested in, is not affected by non-identical intermediate build products, I hope someone (you?) is interested in improving on this side. OCaml bytecode output also seems to be non-deterministic. There is a discussion on the coq issue tracker which may be related.

In contrast to initial plans, I did not used the BUILD_PATH_PREFIX_MAP environment variable, which is implemented in OCaml by PR #1515 (and followups). The main reasons are that something in the OCaml toolchain (I suspect the bytecode interpreter) needed absolute paths to find libraries, thus I'd need a symlink from the left-hand side to the current build directory, which was tedious. Also, my installed assembler does not respect the build path prefix map, and BUILD_PATH_PREFIX_MAP is not widely supported. See e.g. the Debian zarith package with different build paths and its effects on the binary.

I'm fine with recording the build path (switch location) in the build environment for now - it turns out to end up only once in MirageOS unikernels, likely by the last linking step, which hopefully soon be solved by llvm 9.0.

What was fun was to compare the unikernel when built on Linux with gcc against a built on FreeBSD with clang and lld - spoiler: they emit debug sections with different dwarf versions, it is pretty big. Other fun differences were between OCaml compiler versions: the difference between minor versions (4.08.0 vs 4.08.1) is pretty small (~100kB as human-readable output), while the difference between major version (4.08.1 vs 4.09.0) is rather big (~900kB as human-readable diff).

An item on my list for the future is to distribute the opam export, build hashes and build environment artifacts in a authenticated way. I want to integrate this as in-toto style into conex, my not-yet-deployed implementation of tuf for opam that needs further development and a test installation, hopefully in 2020.

If you want to support our work on MirageOS unikernels, please donate to robur. I'm interested in feedback, either via twitter, hannesm@mastodon.social or an issue on the data repository.

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…

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 are further described in the reference manual.

Feedback and bug reports are extremely welcome.

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…

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. Then after those 6 first months, it is named and given a branch on its own. For instance, this happened on October 18 2019 for OCaml 4.10. Starting from this point, the branch is feature-frozen: only bug fixes are merged, whereas new feature development happens in trunk. Our objective is then to release the new version 3 months later. If we succeed, there are at most two branches active at the same time.

    Dev
    Dev
    Dev
    Dev
    Dev
    Dev
    Bug  Dev
    Bug  Dev
    RCs  Dev
         Dev
         Dev
         Dev
         Bug  Dev
         Bug  Dev
         RCs  Dev
              Dev
              Dev
              Dev
              Bug
              Bug
              Rcs

However, the OCaml compiler does not live in isolation. It makes little point to release a new version of OCaml which is not compatible with other parts of the OCaml ecosystem.

The release cycle of OCaml 4.08 was particularly painful from this point of view: we refactored parts of the compiler API that were not previously versioned by ocaml-migrate-parsetree, making it more difficult to update. In turn, without a working version of ocaml-migrate-parsetree, ppxses could not be built, breaking all packages that depend on them. It took months to correct the issue. This slip of schedule affected the 4.09.0 release and can still be felt on the 4.11 schedule.

Catching knifes before the fall

Lesson learned, we need to test the packages in the opam repository more often. Two tools in current usage can automate such testing: opamcheck and opam-health-check.

The two tools attack the problem with a different angle. The opam-health-check monitoring tool is developed to check the coherency of the opam repository, for released OCaml versions.

In a complementary way, opamcheck was written by Damien Doligez to check how well new versions of the OCaml compiler fare in terms of building the packages in the opam repository.

A typical difference between opamcheck and opam-health-check is that opamcheck is biased towards newer versions of the compiler: if an opam package builds on the latest unreleased version of the compiler, we don’t need to test it with older compilers. After all, we are mostly interested in packages that are broken by the new release. The handful of packages that may be coincidentally fixed by an unreleased compiler are at most a curiosity; pruning those unlikely events saves us some precious time.

Since I started at Inria, in the midst of the first beta of OCaml 4.09.0, I have been working with opamcheck to monitor the state of the opam repository.

The aim here is twofold. First, we want to detect expected breakages that are just a sign that a package needs to be updated before the final release of the new compiler version. The earliest we catch those, the more time the maintainers have to patch their packages. Second, we want to detect unexpected compatibility issues and breakages.

One fun example of such unexpected compatibility issue appeared in the 4.09.0 release cycle. When I first used opamcheck to test the state of the first 4.09.0 beta, there was a quite problematic broken package: dune. This was quite stunning at first, because the 4.09.0 version of OCaml contained mostly bug fixes and small quality-of-life improvements. That was at least what I had told a few worried people a few days earlier…

So what was happening here? The issue stemmed from a small change of behaviour in presence of missing compiled interface (cmi) files : dune was relying on an unspecified OCaml compiler behaviour in such cases, and this behaviour had been altered by a mostly unrelated improvement in the typechecker.

This change of behaviour was patched and dune worked fine in the second beta release of 4.09.0. And this time, the next run of opamcheck confirmed that that 4.09.0 was a quiet release.

This is currently the main use of opamcheck: check the health status of the opam repository on unreleased version of OCaml before opam-health-check more extensive coverage takes the relay. One of our objectives for the future 4.10.0 release is to achieve a much more extensive test coverage, before the first beta.

Opam and the PRs

There is another possible use of opamcheck that is probably much more useful to the anxious OCaml developer: opamcheck can be used to check that a PR or an experimental branch does not break opam packages. A good example is #8900: this PR proposes to remove the special handling of abstract types defined inside the current module. This special case looks nice locally, but it allows to write some code which is valid if and only if it is located in the right module, without any possibility to correct this behaviour by making module signatures more precise.

It is therefore quite tempting to try to remove this special case from the typechecker, but is it reasonable?

This was another task for opamcheck. First, I added a new opamcheck option to easily check any pull request on the OCaml compiler. After some work, there was some good news: this pattern is mostly unused in the current opam repository.

Knowing whether there are any opam packages that rely on this feature is definitively a big help when taking these decisions.

Using opamcheck

So if you are a worried OCaml developer and want to test your fancy compiler PR on the anvil of the opam repositoy, what are the magical incantations?

One option is to download the docker image octachron/opamcheck with

docker pull octachron/opamcheck

Beware that the image weighs around 7 GiB. It is also possible to build and run opamcheck locally as detailed in the readme. However, in this short blog post, I will present the latter option. It has the advantages of being relatively lightweight in terms of configuration, and makes it easier to test your legions of PRs simultaneously (you don’t have legions of PRs, do you?)

Once the image is downloaded, there are three main ways to run it. If you want to compare several versions of the compiler (given as switch names), let’s say 4.05, and 4.08.1+flambda and 4.10.0+trunk, you can run:

docker run -v opamcheck:/app/log -p 8080:80 --name=opamcheck opamcheck run -online-summary=10 4.05.0 4.08.1+flambda 4.10.0

The -name option is the docker container name. The -p option maps the port 80 of the container to the port 8080 of the host, this is used to connect to the http server embedded in the image. Finally, the -v flag let us choose the location of opamcheck log directory in the host file system. (If you forget this option, a random docker volume name will be used.) Here, it will be at /var/lib/docker/volumes/opamcheck.

While opamcheck is runnning, its progress can be checked with either

sudo tail -f /var/lib/docker/volumes/opamcheck_log/_data/results

or by pointing a web browser to localhost:8080/fullindex.html. Note that the first summary is only generated after the OCaml compiler is built and all uninstallable packages have been discovered. On my machine, this rounds up at a 15 minutes wait before the first summary is generated. Later updates should be more frequent.

The result should look like this summary run for OCaml 4.10.0. The integer parameter in -online-summary=n corresponds to the update period for this html summary. If the option is not provided, the html summary is only built at the end of the run.

If you are more interested by testing a specific PR, for instance #8900, the prmode mode works better

docker run -p 80:8080 opamcheck --name=opamcheck prmode -online-summary=10 -pr 8900 4.09.0

This command tries to rebase the given PR on top of the given OCaml version (switch name); it fails immediately if the PR cannot be rebased; in this case you should use the latest trunk switch as base or use the branch option, described below. When possible, it is a good idea to use a released version as the base: with a released version, there are more unbroken packages to test your patch against.

If the branch that you want to test is not yet a PR, or needs some manual rebasing to be compared against a specific compiler version, there is a -branch flag. For instance, let’s say that you have a branch my_very_experimental_branch at the location nowhere.org. You can run

docker run -p 80:8080 opamcheck --name=opamcheck prmode -online-summary=10 -branch https://nowhere.org:my_very_experimental_branch 4.09.0

This command downloads the branch at nowhere.org and compare it against the 4.09.0 switch.

Currently, a full run of opamcheck takes one or two days: you will likely get the results before your first PR review. A limitation is the false positive rate: most opam package descriptions are incomplete or out of date, so packages will fail for reasons unrelated to your PR. Unfortunately, this means that there is still some manual triage needed after an opamcheck run.

There are four main objectives for opamcheck in the next months:

• improve its usability
• share more code with opam-health-check, at least on the frontend
• reduce the false positive rate
• reduce the time required by a CI run

If you want to check on future development for opamcheck, and a potentially more up-to-date readme, you can have a look at Octachron/opamcheck.

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…

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 release, and stay tuned for the upcoming Wodan integration in 2020 that will be a stable filesystem for the hypervisor targets for MirageOS that do not have a conventional OS kernel underneath them!

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…

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 small demo showcases the modern BAP look and feel. In this announcement we would like to focus on two very important features of BAP 2.0:

• knowledge representation and reasoning system;
• the tagless final representation of program semantics.

The Knowledge Base

The Knowledge Representation and Reasoning System, or the Knowledge Base (KB) for short, is the central part of our new architecture. The KB is a step forward from the conventional approach to staging multiple analyses in which dependent analyses (aka passes) are ordered topologically, based on their dependencies. The KB is inspired by logic programming and enables an optimal and seamless staging of mutually dependent analyses. Mutually dependent analyses are also present in the source-based program analysis but are much more evident in the field of binary analysis and reverse engineering, where even such basic artifacts as control flow graph and call graph are not available as ground truth (and in general are not even computable).

Object properties in the KB are represented with directed-complete partially ordered sets. The KB also imposes the monotonicity restriction that requires that all updates to the property are monotonic, i.e., each consequent value of the same property is a refinement of the previous value. These restrictions enable the KB to compute the least fixed point of any property, is computed. A property representation could be optionally refined into a complete lattice, which gives the KB users extra control on how properties are computed.

By storing all information in an external location the KB addresses the scalability issue so relevant to binary analysis and reverse engineering. In the future, we plan to implement a distributed storage for our Knowledge Base as well as experiment with other inference engines. Soon, it should also possible to work with the knowledge base in non-OCaml programs, including our BAP Lisp dialect. That, practically, turns the knowledge base into a common runtime for binary analysis. In the current version of BAP, the Knowledge Base state is fully serializable and portable between different versions of BAP, OCaml, and even between native and bytecode runtimes. The Knowledge Base state could be imported into an application and is integrated with the BAP caching system.

New Program Representation

Employing the tagless final embedding together with our new Knowledge Base we were able to achieve our main goal - to switch to an extensible program representation without compromising any existing code that uses the current, non-extensible, BAP Intermediate Language (BIL). The new representation allows us to add new language features (like floating-point operations or superscalar pipeline manipulations) without breaking (or even recompiling) the existing analyses. The new representation also facilitates creation of new intermediate languages which all can coexist with each other, making it easier to write formally verified analyses.

Links

• The Main Page
• Documentation
• The tutorial
• Our Chat
• Our Blog
• Discuss the news

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…

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 Contents

• Introduction
• Attempt one: a monad
• Attempt two: an arrow
• Attempt three: a dart
• Comparison with arrows
• Larger examples
  • OCaml Docker base image builder
  • OCaml CI
• Conclusions

( this post also appeared on Reddit and Lobsters )

Introduction

I was asked to build a system for creating CI/CD pipelines. The initial use for it was to build a CI for testing OCaml projects on GitHub (testing each commit against multiple versions of the OCaml compiler and on multiple operating systems). Here’s a simple pipeline that gets the Git commit at the head of a branch, builds it, and then runs the tests:

The colour-scheme here is that green boxes are completed, orange ones are in progress and grey means the step can’t be started yet.

Here’s a slightly more complex example, which also downloads a Docker base image, builds the commit in parallel using two different versions of the OCaml compiler, and then tests the resulting images. Here the red box indicates that this step failed:

A more complex example is testing the project itself and then searching for other projects that depend on it and testing those against the new version too:

Here, the circle means that we should wait for the tests to pass before checking the reverse dependencies.

We could describe these pipelines using YAML or similar, but that would be very limiting. Instead, I decided to use an Embedded Domain Specific Language, so that we can use the host language’s features for free (e.g. string manipulation, variables, functions, imports, type-checking, etc).

The most obvious approach is making each box a regular function. Then the first example above could be (here, using OCaml syntax):

1
2
3
4

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

The second could be:

1
2
3
4
5
6
7
8
9
10

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  build "4.07";
  build "4.08"

And the third might look something like this:

1
2
3
4
5
6

let example3 commit =
  let src = fetch commit in
  let image = build src in
  test image;
  let revdeps = get_revdeps src in
  List.iter example1 revdeps

However, we’d like to add some extras to the language:

• Pipeline steps should run in parallel when possible. The example2 function above would do the builds one at a time.
• Pipeline steps should be recalculated whenever their input changes. e.g. when a new commit is made we need to rebuild.
• The user should be able to view the progress of each step.
• The user should be able to trigger a rebuild for any step.
• We should be able to generate the diagrams automatically from the code, so we can see what the pipeline will do before running it.
• The failure of one step shouldn’t stop the whole pipeline.

The exact extras don’t matter too much to this blog post, so for simplicity I’ll focus on just running steps concurrently.

Attempt one: a monad

Without the extra features, we have functions like this:

1
2

val fetch : commit -> source
val build : source -> image

You can read this as “build is a function that takes a source value and returns a (Docker) image”.

These functions compose together easily to make a larger function that will fetch a commit and build it:

1
2
3

let fab c =
  let src = fetch c in
  build src

We could also shorten this to build (fetch c) or to fetch c |> build. The |> (pipe) operator in OCaml just calls the function on its right with the argument on its left.

To extend these functions to be concurrent, we can make them return promises, e.g.

1
2

val fetch : commit -> source promise
val build : source -> image promise

But now we can’t compose them easily using let (or |>), because the output type of fetch doesn’t match the input of build.

However, we can define a similar operation, let* (or >>=) that works with promises. It immediately returns a promise for the final result, and calls the body of the let* later, when the first promise is fulfilled. Then we have:

1
2
3

let fab c =
  let* src = fetch c in
  build src

In order words, by sprinkling a few * characters around we can turn our plain old pipeline into a new concurrent one! The rules for when you can compose promise-returning functions using let* are exactly the same as the rules about when you can compose regular functions using let, so writing programs using promises is just as easy as writing regular programs.

Just using let* doesn’t add any concurrency within our pipeline (it just allows it to execute concurrently with other code). But we can define extra functions for that, such as all to evaluate every promise in a list at once, or an and* operator to indicate that two things should run in parallel:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

let example2 commit =
  (* Fetch the source code and Docker base image in parallel: *)
  let* src = fetch commit
  and* base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let* image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  (* Build and test against each compiler version in parallel: *)
  all [
    build "4.07";
    build "4.08"
  ]

As well as handling promises, we could also define a let* for functions that might return errors (the body of the let is called only if the first value is successful), or for live updates (the body is called each time the input changes), or for all of these things together. This is the basic idea of a monad.

This actually works pretty well. In 2016, I used this approach to make DataKitCI, which was used initially as the CI system for Docker-for-Mac. Later, Anil Madhavapeddy used it to create opam-repo-ci, which is the CI system for opam-repository, OCaml’s main package repository. This checks each new PR to see what packages it adds or modifies, tests each one against multiple OCaml compiler versions and Linux distributions (Debian, Ubuntu, Alpine, CentOS, Fedora and OpenSUSE), and then finds all versions of all packages depending on the changed packages and tests those too.

The main problem with using a monad is that we can’t statically analyse the pipeline. Consider the example2 function above. Until we have queried GitHub to get a commit to test, we cannot run the function and therefore have no idea what it will do. Once we have commit we can call example2 commit, but until the fetch and docker_pull operations complete we cannot evaluate the body of the let* to find out what the pipeline will do next.

In other words, we can only draw diagrams showing the bits of the pipeline that have already executed or are currently executing, and we must indicate opportunities for concurrency manually using and*.

Attempt two: an arrow

An arrow makes it possible to analyse pipelines statically. Instead of our monadic functions:

1
2

val fetch : commit -> source promise
val build : source -> image promise

we can define an arrow type:

1
2
3
4

type ('a, 'b) arrow

val fetch : (commit, source) arrow
val build : (source, image) arrow

An ('a, 'b) arrow is a pipeline that takes an input of type 'a and produces a result of type 'b. If we define type ('a, 'b) arrow = 'a -> 'b promise then this is the same as the monadic version. However, we can instead make the arrow type abstract and extend it to store whatever static information we require. For example, we could label the arrows:

1
2
3
4

type ('a, 'b) arrow = {
  f : 'a -> 'b promise;
  label : string;
}

Here, arrow is a record. f is the old monadic function and label is the “static analysis”.

Users can’t see the internals of the arrow type, and must build up pipelines using functions provided by the arrow implementation. There are three basic functions available:

1
2
3

val arr : ('a -> 'b) -> ('a, 'b) arrow
val ( >>> ) : ('a, 'b) arrow -> ('b, 'c) arrow -> ('a, 'c) arrow
val first : ('a, 'b) arrow -> (('a * 'c), ('b * 'c)) arrow

arr takes a pure function and gives the equivalent arrow. For our promise example, that means the arrow returns a promise that is already fulfilled. >>> joins two arrows together. first takes an arrow from 'a to 'b and makes it work on pairs instead. The first element of the pair will be processed by the given arrow and the second component is returned unchanged.

We can have these operations automatically create new arrows with appropriate f and label fields. For example, in a >>> b, the resulting label field could be the string {a.label} >>> {b.label}. This means that we can display the pipeline without having to run it first, and we could easily replace label with something more structured if needed.

With this our first example changes from:

1
2
3
4

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

to

1
2

let example1 =
  fetch >>> build >>> test

That seems quite pleasant, although we did have to give up our variable names. But things start to get complicated with larger examples. For example2, we need to define a few standard combinators:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

(** Process the second component of a tuple, leaving the first unchanged. *)
let second f =
  let swap (x, y) = (y, x) in
  arr swap >>> first f >>> arr swap

(** [f *** g] processes the first component of a pair with [f] and the second
    with [g]. *)
let ( *** ) f g =
  first f >>> second g

(** [f &&& g] processes a single value with [f] and [g] in parallel and
    returns a pair with the results. *)
let ( &&& ) f g =
  arr (fun x -> (x, x)) >>> (f *** g)

Then, example2 changes from:

1
2
3
4
5
6
7
8
9
10

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  build "4.07";
  build "4.08"

to:

1
2
3
4
5
6
7
8
9
10

let example2 =
  let build ocaml_version =
    first (arr (fun base -> make_dockerfile ~base ~ocaml_version))
    >>> build_with_dockerfile ~label:ocaml_version
    >>> test
  in
  arr (fun c -> ((), c))
  >>> (docker_pull "ocaml/opam2" *** fetch)
  >>> (build "4.07" &&& build "4.08")
  >>> arr (fun ((), ()) -> ())

We’ve lost most of the variable names and instead have to use tuples, remembering where our values are. It’s not too bad here with two values, but it gets very difficult very quickly as more are added and we start nesting tuples. We also lost the ability to use an optional labelled argument in build ~dockerfile src and instead need to use a new operation that takes a tuple of the dockerfile and the source.

Imagine that running the tests now requires getting the test cases from the source code. In the original code, we’d just change test image to test image ~using:src. In the arrow version, we need to duplicate the source before the build step, run the build with first build_with_dockerfile, and make sure the arguments are the right way around for a new test_using.

Attempt three: a dart

I started wondering whether there might be an easier way to achieve the same static analysis that you get with arrows, but without the point-free syntax, and it seems that there is. Consider the monadic version of example1. We had:

1
2
3
4
5
6
7

val build : source -> image promise
val test : image -> results promise

let example1 commit =
  let* src = fetch commit in
  let* image = build src in
  test image

If you didn’t know about monads, there is another way you might try to do this. Instead of using let* to wait for the fetch to complete and then calling build with the source, you might define build and test to take promises as inputs:

1
2

val build : source promise -> image promise
val test : image promise -> results promise

After all, fetching gives you a source promise and you want an image promise, so this seems very natural. We could even have example1 take a promise of the commit. Then it looks like this:

1
2
3
4

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

That’s good, because it’s identical to the simple version we started with. The problem is that it is inefficient:

• We call example1 with the promise of the commit (we don’t know what it is yet).
• Without waiting to find out which commit we’re testing, we call fetch, getting back a promise of some source.
• Without waiting to get the source, we call build, getting a promise of an image.
• Without waiting for the build, we call test, getting a promise of the results.

We return the final promise of the test results immediately, but we haven’t done any real work yet. Instead, we’ve built up a long chain of promises, wasting memory.

However, in this situation what we want is to perform a static analysis. i.e. we want to build up in memory some data structure representing the pipeline… and this is exactly what our “inefficient” use of the monad produces!

To make this useful, we need the primitive operations (such as fetch) to provide some information (e.g. labels) for the static analysis. OCaml’s let syntax doesn’t provide an obvious place for a label, but I was able to define an operator (let**) that returns a function taking a label argument. It can be used to build primitive operations like this:

1
2
3
4

let fetch commit =
  "fetch" |>
  let** commit = commit in
  (* (standard monadic implementation of fetch goes here) *)

So, fetch takes a promise of a commit, does a monadic bind on it to wait for the actual commit and then proceeds as before, but it labels the bind as a fetch operation. If fetch took multiple arguments, it could use and* to wait for all of them in parallel.

In theory, the body of the let** in fetch could contain further binds. In that case, we wouldn’t be able to analyse the whole pipeline at the start. But as long as the primitives wait for all their inputs at the start and don’t do any binds internally, we can discover the whole pipeline statically.

We can choose whether to expose these bind operations to application code or not. If let* (or let**) is exposed, then applications get to use all the expressive power of monads, but there will be points where we cannot show the whole pipeline until some promise resolves. If we hide them, then applications can only make static pipelines.

My approach so far has been to use let* as an escape hatch, so that any required pipeline can be built, but I later replace any uses of it by more specialised operations. For example, I added:

1

val list_map : ('a t -> 'b t) -> 'a list t -> 'b list t

This processes each item in a list that isn’t known until runtime. However, we can still know statically what pipeline we will apply to each item, even though we don’t know what the items themselves are. list_map could have been implemented using let*, but then we wouldn’t be able to see the pipeline statically.

Here are the other two examples, using the dart approach:

1
2
3
4
5
6
7
8
9
10
11
12
13
14

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile =
      let+ base = base in
      make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  all [
    build "4.07";
    build "4.08"
  ]

Compared to the original, we have an all to combine the results, and there’s an extra let+ base = base when calculating the dockerfile. let+ is just another syntax for map, used here because I chose not to change the signature of make_dockerfile. Alternatively, we could have make_dockerfile take a promise of the base image and do the map inside it instead. Because map takes a pure body (make_dockerfile just generates a string; there are no promises or errors) it doesn’t need its own box on the diagrams and we don’t lose anything by allowing its use.

1
2
3
4
5
6
7

let example3 commit =
  let src = fetch commit in
  let image = build src in
  let ok = test image in
  let revdeps = get_revdeps src in
  gate revdeps ~on:ok |>
  list_iter ~pp:Fmt.string example1

This shows another custom operation: gate revdeps ~on:ok is a promise that only resolves once both revdeps and ok have resolved. This prevents it from testing the library’s revdeps until the library’s own tests have passed, even though it could do this in parallel if we wanted it to. Whereas with a monad we have to enable concurrency explicitly where we want it (using and*), with a dart we have to disable concurrency explicitly where we don’t want it (using gate).

I also added a list_iter convenience function, and gave it a pretty-printer argument so that we can label the cases in the diagrams once the list inputs are known.

Finally, although I said that you can’t use let* inside a primitive, you can still use some other monad (that doesn’t generate diagrams). In fact, in the real system I used a separate let> operator for primitives. That expects a body using non-diagram-generating promises provided by the underlying promise library, so you can’t use let* (or let>) inside the body of a primitive.

Comparison with arrows

Given a “dart” you can create an arrow interface from it easily by defining e.g.

1

type ('a, 'b) arrow = 'a promise -> 'b promise

Then arr is just map and f >>> g is just fun x -> g (f x). first can be defined easily too, assuming you have some kind of function for doing two things in parallel (like our and* above).

So a dart API (even with let* hidden) is still enough to express any pipeline you can express using an arrow API.

The Haskell Arrow tutorial uses an example where an arrow is a stateful function. For example, there is a total arrow that returns the sum of its input and every previous input it has been called with. e.g. calling it three times with inputs 1 2 3 produces outputs 1 3 6. Running a pipeline on a sequence of inputs returns the sequence of outputs.

The tutorial uses total to define a mean1 function like this:

1

mean1 = (total &&& (arr (const 1) >>> total)) >>> arr (uncurry (/))

So this pipeline duplicates each input number, replaces the second one with 1, totals both streams, and then replaces each pair with its ratio. Each time you put another number into the pipeline, you get out the average of all values input so far.

The equivalent code using the dart style would be (OCaml uses /. for floating-point division):

1
2
3
4

let mean values =
  let t = total values in
  let n = total (const 1.0) in
  map (uncurry (/.)) (pair t n)

That seems more readable to me. We can simplify the code slightly by defining the standard operators let+ (for map) and and+ (for pair):

1
2
3
4
5
6
7

let (let+) x f = map f x
let (and+) = pair

let mean values =
  let+ t = total values
  and+ n = total (const 1.0) in
  t /. n

This is not a great example of an arrow anyway, because we don’t use the output of one stateful function as the input to another, so this is actually just a plain applicative.

We could easily extend the example pipeline with another stateful function though, perhaps by adding some smoothing. That would look like mean1 >>> smooth in the arrow notation, and values |> mean |> smooth (or smooth (mean values)) in the dart notation.

Note: Haskell does also have an Arrows syntax extension, which allows the Haskell code to be written as:

1
2
3
4

mean2 = proc value -> do
    t <- total -< value
    n <- total -< 1
    returnA -< t / n

That’s more similar to the dart notation.

Larger examples

I’ve put up a library using a slightly extended version of these ideas at ocurrent/ocurrent. The lib_term subdirectory is the part relevant to this blog post, with the various combinators described in TERM. The other directories handle more concrete details, such as integration with the Lwt promise library, and providing the admin web UI or the Cap’n Proto RPC interface, as well as plugins with primitives for using Git, GitHub, Docker and Slack.

OCaml Docker base image builder

ocurrent/docker-base-images contains a pipeline that builds Docker base images for OCaml for various Linux distributions, CPU architectures, OCaml compiler versions and configuration options. For example, to test OCaml 4.09 on Debian 10, you can do:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

$ docker run --rm -it ocurrent/opam:debian-10-ocaml-4.09

:~$ ocamlopt --version
4.09.0

:~$ opam depext -i utop
[...]

:~$ utop
----+-------------------------------------------------------------+------------------
    | Welcome to utop version 2.4.2 (using OCaml version 4.09.0)! |
    +-------------------------------------------------------------+

Type #utop_help for help about using utop.

-( 11:50:06 )-< command 0 >-------------------------------------------{ counter: 0 }-
utop # 

Here’s what the pipeline looks like (click for full-size):

It pulls the latest Git commit of opam-repository each week, then builds base images containing that and the opam package manager for each distribution version, then builds one image for each supported compiler variant. Many of the images are built on multiple architectures (amd64, arm32, arm64 and ppc64) and pushed to a staging area on Docker Hub. Then, the pipeline combines all the hashes to push a multi-arch manifest to Docker Hub. There are also some aliases (e.g. debian means debian-10-ocaml-4.09 at the moment). Finally, if there is any problem then the pipeline sends the error to a Slack channel.

You might wonder whether we really need a pipeline for this, rather than a simple script run from a cron-job. But having a pipeline allows us to see what the pipeline will do before running it, watch the pipeline’s progress, restart failed jobs individually, etc, with almost the same code we would have written anyway.

You can read pipeline.ml if you want to see the full pipeline.

OCaml CI

ocurrent/ocaml-ci is an (experimental) GitHub app for testing OCaml projects. The pipeline gets the list of installations of the app, gets the configured repositories for each installation, gets the branches and PRs for each repository, and then tests the head of each one against multiple Linux distributions and OCaml compiler versions. If the project uses ocamlformat, it also checks that the commit is formatted exactly as ocamlformat would do it.

The results are pushed back to GitHub as the commit status, and also recorded in a local index for the web and tty UIs. There’s quite a lot of red here mainly because if a project doesn’t support a particular version of OCaml then the build is marked as failed and shows up as red in the pipeline, although these failures are filtered out when making the GitHub status report. We probably need a new colour for skipped stages.

Conclusions

It’s convenient to write CI/CD pipelines as if they were single-shot scripts that run the steps once, in series, and always succeed, and then with only minor changes have the pipeline run the steps whenever the input changes, in parallel, with logging, error reporting, cancellation and rebuild support.

Using a monad allows any program to be converted easily to have these features, but, as with a regular program, we don’t know what the program will do with some data until we run it. In particular, we can only automatically generate diagrams showing steps that have already started.

The traditional way to do static analysis is to use an arrow. This is a little more limited than a monad, because the structure of the pipeline can’t change depending on the input data, although we can add limited flexibility such as optional steps or a choice between two branches. However, writing pipelines using arrow notation is difficult because we have to program in a point-free style (without variables).

We can get the same benefits of static analysis by using a monad in an unusual way, here referred to as a “dart”. Instead of functions that take plain values and return wrapped values, our functions both take and return wrapped values. This results in a syntax that looks identical to plain programming, but allows static analysis (at the cost of not being able to manipulate the wrapped values directly).

If we hide (or don’t use) the monad’s let* (bind) function then the pipelines we create can always be determined statically. If we use a bind, then there will be holes in the pipeline that may expand to more pipeline stages as the pipeline runs.

Primitive steps can be created by using a single “labelled bind”, where the label provides the static analysis for the atomic component.

I haven’t seen this pattern used before (or mentioned in the arrow documentation), and it seems to provide exactly the same benefits as arrows with much less difficulty. If this has a proper name, let me know!

This work was funded by OCaml Labs.

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…

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 point theorem.

Theorem: (Lawvere) If $e : A \to B^A$ is a surjection then every $f : B \to B$ has a fixed point.

Proof. Because $e$ is a surjection, there is $a \in A$ such that $e(a) = \lambda x : A \,.\, f(e(x)(x))$, but then $e(a)(a) = f(e(a)(a)$. $\Box$

Lawvere's original version is a bit more general, but the one given here makes is very clear that Lawvere's fixed point theorem is the diagonal argument in crystallized form. Indeed, the contrapositive form of the theorem, namely

Corollary: If $f : B \to B$ has no fixed point then there is no surjection $e : A \to B^A$.

immediately implies a number of famous theorems that rely on the diagonal argument. For example, there can be no surjection $A \to \lbrace 0, 1\rbrace^A$ because the map $x \mapsto 1 - x$ has no fixed point in $\lbrace 0, 1\rbrace$ -- and that is Cantors' theorem.

It not easy to find non-trivial instances to which Lawvere's theorem applies. Indeed, if excluded middle holds, then having a surjection $e : A \to B^A$ implies that $B$ is the singleton. We should look for interesting instances in categories other than classical sets. In my paper I do so: I show that countably based $\omega$-cpos in the effective topos are countable and closed under countable products, which gives us a rich supply of objects $B$ such that there is a surjection $\mathbb{N} \to B^\mathbb{N}$.

Enjoy the paper!

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…

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. But I have always felt that handlers and monads are not very good at explaining how a program interacts with its external environment and how it gets to perform real-world effects.

Danel Ahman and I have worked for a while on attacking the question on how to better model external resources and what programming constructs are appropriate for working with them. The time is right for us to show what we have done so far. The theoretical side of things is explained in our paper Runners in action, Danel implemented a Haskell library Haskell-Coop to go with the paper, and I implemented a programming language Coop.

General-purpose programming languages, even the so-called pure ones, have to have some account of interaction with the external environment. A popular choice is to provide a foreign-function interface that connects the language with an external library, and through it with an operating system and the universe. A more nuanced approach would differentiate between a function that just happens to be written in a different language, and one that actually performs an effect. The latter kind is known as an algebraic operation in the algebraic-effects-and-handlers way of doing things.

A bad approach to modeling the external world is to pretend that it is internal to the language. One would think that this is obvious but it is not. For instance, Haskell represents the interface to the external world through the IO monad. But what is this monad really? How does it get to interact with the external world? The Haskell Wiki page which answers this question has the following disclaimer:

"Warning: The following story about IO is incorrect in that it cannot actually explain some important aspects of IO (including interaction and concurrency). However, some people find it useful to begin developing an understanding."

The Wiki goes on to say how IO is a bit like a state monad with an imaginary RealWorld state, except that of course RealWorld is not really a Haskell type, or at least not one that actually holds the state of the real world.

The situation with Eff is not much better: it treats some operations at the top-level in a special way. For example, if print percolates to the top level, it turns into a real print that actually causes an effect. So it looks like there is some sort of "top level handler" that models the real world, but that cannot be the case: a handler may discard the continuation or run it twice, but Eff hardly has the ability to discard the external world, or to make it bifurcate into two separate realities.

If IO monad is not an honest monad and a top-level handler is not really a handler, then what we have is a case of ingenious hackery in need of proper programming-language design.

How precisely does an operation call in the program cause an effect in the external world? As we have just seen, some sort of runtime environment or top level needs to relate it to the external world. From the viewpoint of the program, the external world appears as state which is not directly accessible, or even representable in the language. The effect of calling an operation $\mathtt{op}(a,\kappa)$ is to change the state of the world, and to get back a result. We can model the situation with a map $\overline{\mathtt{op}} : A \times W \to B \times W$, where $W$ is the set of all states of the world, $A$ is the set of parameters, and $B$ the set of results of the operation. The operation call $\mathtt{op}(a, \kappa)$ is "executed" in the current world $w \in W$ by computing $\overline{\mathtt{op}}(a,w) = (b, w')$ to get the next world $w'$ and a result $b$. The program then proceeds with the continuation $\kappa\,b$ in the world $w'$. Notice how the world $w$ is an external entity that is manipulated by the external map $\overline{\mathtt{op}}$ realistically in a linear fashion, i.e., the world is neither discarded nor copied, just transformed.

What I have just described is not a monad or a handler, but a comodel, also known as a runner, and the map $\overline{\mathtt{op}}$ is not an operation, but a co-operation. This was all observed a while ago by Gordon Plotkin and John Power, Tarmo Uustalu, and generalized by Rasmus Møgelberg and Sam Staton, see our paper for references. Perhaps we should replace "top-level" handlers and "special" monads with runners?

Danel and I worked out how effectful runners (a generalization of runners that supports other effects in addition to state) provide a mathematical model of resource management. They also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own “virtual machines” and run code inside them. Such virtual machines can be nested and combined in interesting ways. We capture the core ideas of programming with runners in an equational calculus $\lambda_{\mathsf{coop}}$, that guarantees the linear use of resources and execution of finalization code.

An interesting practical aspect of $\lambda_{\mathsf{coop}}$, that was begotten by theory, is modeling of extra-ordinary circumstances. The external environment should have the ability to signal back to the program an extra-ordinary circumstance that prevents if from returning a result. This is normally accomplished by an exception mechanism, but since the external world is stateful, there are two ways of combining it with exceptions, namely the sum and the tensor of algebraic theories. Which one is the right one? Both! After a bit of head scratching we realized that the two options are (analogous to) what is variously called "checked" and "non-checked" exceptions, errors and signals, or synchronous and asynchronous exceptions. And so we included in $\lambda_{\mathsf{coop}}$ both mechanisms: ordinary exceptions, which are special events that disrupt the flow of user code but can be caught and attended to, and signals which are unrecoverable failures that irrevocably kill user code, but can still be finalized. We proved a finalization theorem which gives strong guarantees about resources always being properly finalized.

If you are familiar with handlers, as a first approximation you can think of runners as handlers that use the continuation at most once in a tail-call position. Many handlers are already of this form but not all. Non-determinism, probability, and handlers that hijack the continuation (delimcc, threads, and selection functionals) fall outside of the scope of runners. Perhaps in the future we can resurrect some of these (in particular it seems like threads, or even some form of concurrency would be worth investigating). There are many other directions of possible future investigations: efficient compilation, notions of correctness, extensions to the simple effect subtyping discipline that we implemented, etc.

To find out more, we kindly invite you to have a look at the paper, and to try out the implementations. The prototype programming language Coop implements and extends $\lambda_{\mathsf{coop}}$. You can start by skimming the Coop manual and the examples. If you prefer to experiment on your own, you might prefer the Haskell-Coop library, as it allows you to combine runners with everything else that Haskell has to offer.

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

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 targets. The genode and virtio targets are still limited to using a single network or block storage device.
• Several notable security enhancements to Solo5 targets, such as enabling stack smashing protection throughout the toolchain by default and improved page protections on some targets. For details, please refer to the Solo5 0.6.0 release notes.

Additional user-visible changes:

• Solo5 0.6.0 has removed the compile-time specialization of the solo5-hvt tender. As a result, a solo5-hvt binary is no longer built at mirage build time. Use the solo5-hvt binary installed in your $PATH by OPAM to run the unikernel.
• mirage build now produces silent ocamlbuild output by default. To get the old behaviour, run with --verbose or set the log level to info or debug.
• New functions Mirage_key.is_solo5 and Mirage_key.is_xen, analogous to Mirage_key.is_unix.

Thanks to Hannes Mehnert for help with the release engineering for MirageOS 3.6.0.

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…

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 non-ASCII symbols in CoqIDE, which now uses GTK3.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

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 …

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 also an opportunity to come discuss with OCamlPro’s OPAM & Flambda lead developers and core contributors in Paris.

Training in English can also be organized, on-demand.

Register link: http://www.ocamlpro.com/forms/preinscriptions-formation-ocaml/

This complements the excellent OCaml MOOC from Université Paris-Diderot and the learn-OCaml platform of the OCaml Software Foundation.

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…

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 human-comprehensible format (or rich-document as we said a long time ago), there are several details of emails which complicate the process of analyzing them (and can be prone to security lapses). These details are mostly described by three RFCs:

• RFC822
• RFC2822
• RFC5322

Even though they are cross-compatible, providing full legacy email parsing is an archaeological exercise: each RFC retains support for the older design decisions (which were not recognized as bad or ugly in 1970 when they were first standardized).

The latest email-related RFC (RFC5322) tried to fix the issue and provide a better formal specification of the email format – but of course, it comes with plenty of obsolete rules which need to be implemented. In the standard, you find both the current grammar rule and its obsolete equivalent.

An extended email parser

Even if the email format can defined by "only" 3 RFCs, you will miss email internationalization (RFC6532), the MIME format (RFC2045, RFC2046, RFC2047, RFC2049), or certain details needed to be interoperable with SMTP (RFC5321). There are still more RFCs which add extra features to the email format such as S/MIME or the Content-Disposition field.

Given this complexity, we took the most general RFCs and tried to provide an easy way to deal with them. The main difficulty is the multipart parser, which deals with email attachments (anyone who has tried to make an HTTP 1.1 parser knows about this).

A realistic email parser

Respecting the rules described by RFCs is not enough to be able to analyze any email from the real world: existing email generators can, and do, produce non-compliant email. We stress-tested mrmime by feeding it a batch of 2 billion emails taken from the wild, to see if it could parse everything (even if it does not produce the expected result). Whenever we noticed a recurring formatting mistake, we updated the details of the ABNF to enable mrmime to parse it anyway.

A parser usable by others

One demonstration of the usability of mrmime is `ocaml-dkim`, which wants to extract a specific field from your mail and then verify that the hash and signature are as expected.

ocaml-dkim is used by the latest implementation of `ocaml-dns` to request public keys in order to verify email.

The most important question about ocaml-dkim is: is it able to verify your email in one pass? Indeed, currently some implementations of DKIM need 2 passes to verify your email (one to extract the DKIM signature, the other to digest some fields and bodies). We focused on verifying in a single pass in order to provide a unikernel SMTP relay with no need to store your email between verification passes.

An email generator

OCaml is a good language for making little DSLs for specialized use-cases. In this case, we took advantage of OCaml to allow the user to easily craft an email from nothing.

The idea is to build an OCaml value describing the desired email header, and then let the Mr. MIME generator transform this into a stream of characters that can be consumed by, for example, an SMTP implementation. The description step is quite simple:

#require "mrmime" ;;
#require "ptime.clock.os" ;;

open Mrmime

let romain_calascibetta =
  let open Mailbox in
  Local.[ w "romain"; w "calascibetta" ] @ Domain.(domain, [ a "gmail"; a "com" ])

let john_doe =
  let open Mailbox in
  Local.[ w "john" ] @ Domain.(domain, [ a "doe"; a "org" ])
  |> with_name Phrase.(v [ w "John"; w "D." ])

let now () =
  let open Date in
  of_ptime ~zone:Zone.GMT (Ptime_clock.now ())

let subject =
  Unstructured.[ v "A"; sp 1; v "Simple"; sp 1; v "Mail" ]

let header =
  let open Header in
  Field.(Subject $ subject)
  & Field.(Sender $ romain_calascibetta)
  & Field.(To $ Address.[ mailbox john_doe ])
  & Field.(Date $ now ())
  & empty

let stream = Header.to_stream header

let () =
  let rec go () =
    match stream () with
    | Some buf -> print_string buf; go ()
    | None -> ()
  in
  go ()

This code produces the following header:

Date: 2 Aug 2019 14:10:10 GMT
To: John "D." <john@doe.org>
Sender: romain.calascibetta@gmail.com
Subject: A Simple Mail

78-character rule

One aspect about email and SMTP is about some historical rules of how to generate them. One of them is about the limitation of bytes per line. Indeed, a generator of mail should emit at most 80 bytes per line - and, of course, it should emits entirely the email line per line.

So mrmime has his own encoder which tries to wrap your mail into this limit. It was mostly inspired by Faraday and Format powered with GADT to easily describe how to encode/generate parts of an email.

A multipart email generator

Of course, the main point about email is to be able to generate a multipart email - just to be able to send file attachments. And, of course, a deep work was done about that to make parts, compose them into specific Content-Type fields and merge them into one email.

Eventually, you can easily make a stream from it, which respects rules (78 bytes per line, stream line per line) and use it directly into an SMTP implementation.

This is what we did with the project `facteur`. It's a little command-line tool to send with file attachement mails in pure OCaml - but it works only on an UNIX operating system for instance.

Behind the forest

Even if you are able to parse and generate an email, more work is needed to get the expected results.

Indeed, email is a exchange unit between people and the biggest deal on that is to find a common way to ensure a understable communication each others. About that, encoding is probably the most important piece and when a French person wants to communicate with a latin1 encoding, an American person can still use ASCII.

Rosetta

So about this problem, the choice was made to unify any contents to UTF-8 as the most general encoding of the world. So, we did some libraries which map an encoding flow to Unicode code-point, and we use uutf (thanks to dbuenzli) to normalize it to UTF-8.

The main goal is to avoid a headache to the user about that and even if contents of the mail is encoded with latin1 we ensure to translate it correctly (and according RFCs) to UTF-8.

This project is `rosetta` and it comes with:

• `uuuu` for ISO-8859 encoding
• `coin` for KOI8-{R,U} encoding
• `yuscii` for UTF-7 encoding

Pecu and Base64

Then, bodies can be encoded in some ways, 2 precisely (if we took the main standard):

• A base64 encoding, used to store your file
• A quoted-printable encoding

So, about the base64 package, it comes with a sub-package base64.rfc2045 which respects the special case to encode a body according RFC2045 and SMTP limitation.

Then, pecu was made to encode and decode quoted-printable contents. It was tested and fuzzed of course like any others MirageOS's libraries.

These libraries are needed for an other historical reason which is: bytes used to store mail should use only 7 bits instead of 8 bits. This is the purpose of the base64 and the quoted-printable encoding which uses only 127 possibilities of a byte. Again, this limitation comes with SMTP protocol.

Conclusion

mrmime is tackling the difficult task to parse and generate emails according to 50 years of usability, several RFCs and legacy rules. So, it still is an experimental project. We reach the first version of it because we are currently able to parse many mails and then generate them correctly.

Of course, a bug (a malformed mail, a server which does not respect standards or a bad use of our API) can appear easily where we did not test everything. But we have the feeling it was the time to release it and let people to use it.

The best feedback about mrmime and the best improvement is yours. So don't be afraid to use it and start to hack your emails with it.

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…

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 journey to the past: we have looked back on 8 years of evolution of the OCaml language and library. New feature after new feature, OCaml has seen many changes. Needless to say, upgrading our cheat sheets to OCaml 4.08.1 was a trip down memory lane. We wanted to share our throwback experience with you!

2011

Fabrice Le Fessant first published our cheat sheets in 2011, the year OCamlPro was created! At the time, OCaml was in its 3.12 version and just got its current name agreed upon. First-class modules were the new big thing, Camlp4 and Camlp5 were battling for the control of the syntax extension world and Godi and Oasis were the packaging rage.

2012

Right after 3.12 came the switch to OCaml 4.00 which brought a major change: GADTs (generalized algebraic data types). Most of OCaml’s developers don’t use their almighty typing power, but the possibilities they provide are really helpful in some cases, most notably the format overhaul. They’re also a fun way to troll a beginner asking how to circumvent the typing system on Stack Overflow. Since most of us might lose track of their exact syntax, GADTs deserve their place in the updated sheet (if you happen to be OCamlPro’s CTO, of course the writer of this blogpost remembers how to use GADTs at all times).

On the standard library side, the big change was the switch of Hashtbl to Murmur 3 and the support for seeded randomization.

2013

With OCaml 4.01 came constructor disambiguation, but there isn’t really a way to add this to the sheet. This feature allows you to avoid misguided usage of polymorphic variants, but that’s a matter of personal taste (there’s a well-known rule that if you refresh the comments section enough times, someone —usually called Daniel— will appear to explain polymorphic variants’ superiority to you). -ppx rewriters were introduced in this version as well.

The standard library got a few new functions. Notably, Printexc.get_callstack for stack inspection, the optimized application operators |> and @@ and Format.asprintf.

2014

Gabriel Scherer, on the Caml-list, end of January:

TL;DR: During the six next months, we will follow pull requests (PR) posted on the github mirror of the OCaml distribution, as an alternative to the mantis bugtracker. This experiment hopes to attract more people to participate in the extremely helpful and surprisingly rewarding activity of patch reviews.

Can you guess which change to the cheat-sheets came with 4.02? It’s a universally-loved language feature added in 2014. Still don’t know? It is exceptional! Got it?

Drum roll… it is the match with exception construction! It made our codes simpler, clearer and in some cases more efficient. A message to people who want to improve the language: please aim for that.

This version also added the {quoted|foo|quoted} syntax (which broke comments), generative functors, attributes and extension nodes, extensible data types, module aliases and, of course, immutable strings (which was optional at the time). Immutable strings is the one feature that prompted us to remove a line from the cheat sheets. More space is good. Camlp4 and Labltk moved out of the distribution.

In consequence of immutable strings, Bytes and BytesLabel were added to the library. For the great pleasure of optimization addicts, raise_notrace popped up. Under the hood, the format type was re-implemented using GADTs.

2015

This release was so big that 4.02.2 feels like a release in itself, with the adding of nonrec and #... operators.

The standard library was spared by this bug-fix themed release. Note that this is the last comparatively slow year of OCaml as the transition to GitHub would soon make features multiply, as hindsight teaches us.

2016

Speaking of a major release, we’re up to OCaml 4.03! It introduced inline records, a GADT exhaustiveness check on steroids (with -> . to denote unreachability) and standard attributes like warning, inlined, unboxed or immediate. Colors appeared in the compiler and last but not least, it was the dawn of a new option called Flambda.

The library saw a lot of useful new functions coming in: lots of new iterators for Array, an equal function in most basic type modules, Uchar, the *_ascii alternatives and, of course, Ephemeron.

4.04 was much more restrained, but it was the second release in a single year. Local opening of module with the M.{} syntax was added along with the let exception ... in construct. String.split_on_char was notably added to the stdlib which means we don’t have to rewrite it anymore.

2017

We now get to 4.05… which did not change the language. Not that the development team wasn’t busy, OCaml just got better without any change to the syntax.

On the library side however, much happened, with the adding of *_opt functions pretty much everywhere. If you’re using the OCaml compiler from Debian, this is where you might think the story ends. You’d be wrong…

…because 4.06 added a lot! My own favorite feature from this release has to be user-defined indexing operators. This is also when safe-string became the default, giving worthwhile work to every late maintainer in the community. This release also added one awesome function in the standard library: Map.update.

2018

4.07 was aimed towards solidifying the language. It added empty variants and type-based selection of GADT constructors to the mix.

On the library side, one old and two new modules were added, with the integration of Bigarray, Seq and Float.

2019

And here we are with 4.08, in the present day! We can now put exceptions under or-patterns, which is the only language change from this release we propagated to the sheet. Time will tell if we need to add custom binding operators or [@@alert]. Pervasives is now deprecated in profit of Stdlib and new modules are popping up (Int, Bool, Fun, Result… did we miss one?) while Sort made its final deprecation warning.

We did not add 4.09 to this journey to the past, as this release is still solidly in the now at the time of this blogpost. Rest assured, we will see much more awesome features in OCaml in the future! In the meantime, we are working on updating more cheat sheets: keep posted!