This year marks the 25th anniversary of the OCaml Language! It's an exciting time for OCaml programmers and enthusiasts. A fun and informative way to celebrate OCaml's birthday is to attend the 26th Annual International Conference on Functional Programming (ICFP), held online this year due to ongoing Covid restrictions. While this is disappointing news for so many, it's beneficial to those of you outside France because now you can hear professionals talk about cutting edge technology from the co…

This year marks the 25th anniversary of the OCaml Language! It's an exciting time for OCaml programmers and enthusiasts. A fun and informative way to celebrate OCaml's birthday is to attend the 26th Annual International Conference on Functional Programming (ICFP), held online this year due to ongoing Covid restrictions. While this is disappointing news for so many, it's beneficial to those of you outside France because now you can hear professionals talk about cutting edge technology from the comfort of your own home.

Tarides engineers, as well as our colleagues at OCaml Labs Consultancy and Segfault Systems, have some exciting presentations at this year's ICFP! Listen to talks on running OCaml on multiple cores, generating fuzzing suites, benchmarking, and the experimental OCaml effects.

You can search the complete ICFP Timetable for other topics of interest and read below about our engineers' projects and presentations. Times are listed both in London (GMT +1) and Paris (GMT +2) for ease of planning. The following talks are scheduled for Friday, 27 August 2021.

Grab a cup of coffee for our first morning talk at 9am London / 10am Paris and learn about Adapting the OCaml Ecosystem for Multicore OCaml. With the soon-to-be released OCaml 5.0, there will be support for Shared-Memory Parallelism. There’s increasing interest in the community to port existing libraries to Multicore, so this talk will cover the arrival of Multicore and what that means to the OCaml ecosystem. Our engineers will highlight existing tools and provide methods for a smooth transition, so viewers can benefit from Multicore parallelism. They'll also share some insights from their experience porting existing libraries to Multicore OCaml.

Read more about this topic on todays' post at Segfault Systems, written by one of tomorrow's presenters, Sudha Parimala of Segfault Systems. Joining Sudha for the presentation are Enguerrand Decorne (Tarides), Sadiq Jaffer (Opsian and OCaml Labs Consultancy), Tom Kelly (OCaml Labs Consultancy), and KC Sivaramakrishnan of IIT Madras.

Next up is Leveraging Formal Specifications to Generate Fuzzing Suites at 11:10 London / 12:10 Paris, presented by Tarides's own Nicolas Osborne and Clément Pascutto. They'll discuss how developers typically first have to capture the semantics they want when checking a library and then write the code implementing these tests and find relevant test cases that expose possible misbehaviours. Through their work, they'll present a tool that automatically takes care of those last two steps by automatically generating fuzz testing suites from OCaml interfaces annotated with formal behavioural specifications. They'll also show some ongoing experiments on fuzzing capabilities and limitations applied to real-world libraries.

Next up is our talk on Continuous Benchmarking for OCaml Projects at 12:30 London / 13:30 Paris. Regular CI systems are optimised for workloads that do not require stable performance over time, which makes them unsuitable for running performance benchmarks. Tarides engineers Gargi Sharma, Rizo Isrof, and Magnus Skjegstad will discuss how current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system it runs on pull requests and branches allowing performance to be analysed and compared, and it can currently be enabled on as an app on GitHub repositories with zero configuration. Several public repositories already run current-bench, including Irmin and Dune, and they plan to enable it on more projects in the future. Read Gargi's recent blog post for more information on benchmarking.

In this presentation, they will give a technical overview of current-bench, showing how results are collected and analysed, requirements for using it, and how they built the infrastructure for stable benchmarks. They'll also cover some future work that will allow more OCaml projects to run current-bench.

Immediately after the Benchmarking talk, catch A Multiverse of Glorious Documentation scheduled at 12:50 London / 13:50 Paris. Lucas Pluvinage of Tarides and Jonathan Ludlam of OCaml Labs Consultancy will discuss the process of generating documentation for every version of every package that can be built from the Opam repository and present it as a single coherent website that's continuously updated as new packages are released and old packages are updated. They will address the challenges of caching, handling different compiler versions, and incompatible libraries. The process has been implemented as an OCurrent pipeline named ocaml-docs-ci and is already available on Github. It has been used to produce the documentation of more than 10,000 package versions, generating 2.5M HTML pages. That's 38GB of artifacts!

After a relaxing lunch, come back for Experiences with Effects at 15:30 London / 16:30 Paris. Join OCaml Labs and Tarides engineers Thomas Leonard, Craig Ferguson, Patrick Ferris, Sadiq Jaffer, Tom Kelly, KC Sivaramakrishnan, and Anil Madhavapeddy as they talk about an exciting, experimental branch of Multicore OCaml that adds support for effect handlers. In this presentation, they'll discuss their experiences with effects, both from converting existing code and from writing new code. They discovered that converting the Angstrom parser from a callback style to effects greatly simplified the code while also improving performance and reducing allocations. Their experimental Eio library uses effects that allows writing concurrent code in direct style, without the need for monads (as found in Lwt or Async).

Enjoy a full day of OCaml innovation and get to know some of our talented engineers better by joining Tarides, OCaml Labs, and Segfault Systems at ICFP on Friday, 27 August 2021. See you there!

Regular CI systems are optimised for workloads that do not require stable performance over time. This makes them unsuitable for running performance benchmarks.

current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system, it runs on pull requests and branches which allows performance to be analysed and compared. It can currently be enabled as an app on GitHub repositories with zero configuration. Several public repo…

Regular CI systems are optimised for workloads that do not require stable performance over time. This makes them unsuitable for running performance benchmarks.

current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system, it runs on pull requests and branches which allows performance to be analysed and compared. It can currently be enabled as an app on GitHub repositories with zero configuration. Several public repositories are runningcurrent-bench, including Irmin and Dune. We plan to enable it on more projects in the future.

In this article, we give a technical overview of current-bench, showing how results are collected and analysed, requirements for using it and how we built the infrastructure for stable benchmarks. We also describe future work that would allow more OCaml projects to run current-bench.

Introduction

For performance critical software, we must run benchmarks to ensure that there's no regression. Running benchmarks before the user submits their pull request is tedious, and since every user might have a different machine, you can't be sure if the benchmarks performed actually improved or regressed performance.

Our current-bench aims to solve this problem by providing a stable benchmarking platform that runs every time the user submits a pull request and compares the result to the benchmarks on the main branch. As current-bench is zero-configuration, users can enroll their repository to run benchmarks with ease. This current-bench has helped projects ensure that regression doesn't happen, so you can merge code with more confidence.

Architecture

Benchmarking Pipeline

As shown in Figure 1 (above), the benchmarking infrastructure uses ocurrent¹, an embedded Domain Specific Language to write a pipeline. The ocurrent command computes the build incrementally and helps with static analysis. Whenever a pull request is opened on a repository monitored by current-bench, a POST request is sent to the server running the pipeline. The pipeline fetches the head commit on the pull request and uses Docker to compile the code, and then it runs the make bench command inside the generated Docker image.

The pipeline runs on a single node, and the process is pinned to a single core to ensure there's no contention of resources when running the benchmarks. Once finished, the raw JSON result is stored in a Postgres database, which the frontend can query using a GraphQL API, as shown in Figure 2 below.

The frontend supports historical navigation and provides comparison with the default branch. It allows users to select a pull request of which they want to see the graphs. The graphs display the individual result of the head commit and the comparison with the commits on the default branch. The frontend permits users to select the historical interval when they want to compare benchmarks, and it also shows the standard deviation. Once the benchmarks have run successfully, the pipeline sets the pull request status to the frontend URL. Then the user can look at the graphs.

Hardware Optimisation

Our current-bench uses the hardware optimisations developed for OCaml multicore compiler benchmarks (presented at ICFP OCaml Workshop 2019) with a few modifications to allow the benchmarks to run inside Docker containers. To get stable performance, we configured the kernel to isolate some of the CPU cores. Linux then avoids scheduling other user processes automatically. We also disabled IRQ handling and power saving.

The container that runs the benchmark is pinned to one of the isolated cores. Since I/O operations can make the benchmarks less stable, we use an in-memory tmpfs partition in /dev/shm for all storage. For NUMA enabled systems, we configure this partition to be allocated on the NUMA node of the isolated core. The pipeline disables ASLR inside the container automatically, which is normally blocked by the default Docker seccomp profile, so we have modified the profile to allow the personality(2) syscall.

Enrolling a repository

To enroll a repository, you need to ensure the following:

• Enable the ocaml-benchmarks GitHub app for your repository.
• The repository needs a bench Makefile target. This is triggered from the current-bench pipeline.
• The output of the make bench target is JSON, which can be parsed by the pipeline and displayed by the frontend.

Future work

Anyone who wants to roll out a continuous, zero-configured benchmarking infrastructure can set up the current-bench infrastructure. In the future, we want to scale current-bench by isolating cores on multiple machines and adding a scheduler to ensure that benchmarks use only one core at a time per machine. We plan to add support for different benchmarking libraries that repositories can use—for example, we currently support repositories using bechamel. We also aim to make the adoption of current-bench easier by adding a conversion library that can convert any benchmark output into output parseable by current-bench. We intend to add support for quick and slow benchmarks, which would allow users to have faster feedback loops on pull requests while ensuring they can still run more extensive, time consuming benchmarks to see the performance.

Thank you for reading! You can check out the implementation for current-bench here!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What’s new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the “base packages”…

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What’s new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the “base packages” in opam 2.0 and allowing for easier compiler upgrades
• Improved options configuration (see the new option and expanded var sub-commands)
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• opam root readability by newer and older versions, even if the format changed
• Performance improvements to opam-update, conflict messages, and many other areas

Seamless integration of System dependencies handling (a.k.a. “depexts”)

opam has long included the ability to install system dependencies automatically via the depext plugin. This plugin has been promoted to a native feature of opam 2.1.0 onwards, giving the following benefits:

• You no longer have to remember to run opam depext, opam always checks depexts (there are options to disable this or automate it for CI use). Installation of an opam package in a CI system is now as easy as opam install ., without having to do the dance of opam pin add -n/depext/install. Just one command now for the common case!
• The solver is only called once, which both saves time and also stabilises the behaviour of opam in cases where the solver result is not stable. It was possible to get one package solution for the opam depext stage and a different solution for the opam install stage, resulting in some depexts missing.
• opam now has full knowledge of depexts, which means that packages can be automatically selected based on whether a system package is already installed. For example, if you have neither MariaDB nor MySQL dev libraries installed, opam install mysql will offer to install conf-mysql and mysql, but if you have the MariaDB dev libraries installed, opam will offer to install conf-mariadb and mysql.

Hint: You can set OPAMCONFIRMLEVEL=unsafe-yes or --confirm-level=unsafe-yes to launch non interactive system package commands.

opam lock files and reproducibility

When opam was first released, it had the mission of gathering together scattered OCaml source code to build a community repository. As time marches on, the size of the opam repository has grown tremendously, to over 3000 unique packages with over 19500 unique versions. opam looks at all these packages and is designed to solve for the best constraints for a given package, so that your project can keep up with releases of your dependencies.

While this works well for libraries, we need a different strategy for projects that need to test and ship using a fixed set of dependencies. To satisfy this use-case, opam 2.0.0 shipped with support for using project.opam.locked files. These are normal opam files but with exact versions of dependencies. The lock file can be used as simply as opam install . --locked to have a reproducible package installation.

With opam 2.1.0, the creation of lock files is also now integrated into the client:

• opam lock will create a .locked file for your current switch and project, that you can check into the repository.
• opam switch create . --locked can be used by users to reproduce your dependencies in a fresh switch.

This lets a project simultaneously keep up with the latest dependencies (without lock files) while providing a stricter set for projects that need it (with lock files).

Hint: You can export the full configuration of a switch with opam switch export new options, --full to have all packages metadata included, and --freeze to freeze all VCS to their current commit.

Switch invariants

In opam 2.0, when a switch is created the packages selected are put into the “base” of the switch. These packages are not normally considered for upgrade, in order to ease pressure on opam’s solver. This was a much bigger concern early on in opam 2.0’s development, but is less of a problem with the default mccs solver.

However, it’s a problem for system compilers. opam would detect that your system compiler version had changed, but be unable to upgrade the ocaml-system package unless you went through a slightly convoluted process with --unlock-base.

In opam 2.1, base packages have been replaced by switch invariants. The switch invariant is a package formula which must be satisfied on every upgrade and install. All existing switches’ base packages could just be expressed as package1 & package2 & package3 etc. but opam 2.1 recognises many existing patterns and simplifies them, so in most cases the invariant will be "ocaml-base-compiler" {= "4.11.1"}, etc. This means that opam switch create my_switch ocaml-system now creates a switch invariant of "ocaml-system" rather than a specific version of the ocaml-system package. If your system OCaml package is updated, opam upgrade will seamlessly switch to the new package.

This also allows you to have switches which automatically install new point releases of OCaml. For example:

opam switch create ocaml-4.11 --formula='"ocaml-base-compiler" {>= "4.11.0" & < "4.12.0~"}' --repos=old=git+https://github.com/ocaml/opam-repository#a11299d81591
opam install utop

Creates a switch with OCaml 4.11.0 (the --repos= was just to select a version of opam-repository from before 4.11.1 was released). Now issue:

opam repo set-url old git+https://github.com/ocaml/opam-repository
opam upgrade

and opam 2.1 will automatically offer to upgrade OCaml 4.11.1 along with a rebuild of the switch. There's not yet a clean CLI for specifying the formula, but we intend to iterate further on this with future opam releases so that there is an easier way of saying “install OCaml 4.11.x”.

Hint: You can set up a default invariant that will apply for all new switches, via a specific opamrc. The default one is ocaml >= 4.05.0

Configuring opam from the command-line

Configuring opam is not a simple task: you need to use an opamrc at init stage, or hack global/switch config file, or use opam config var for additional variables. To ease that step, and permit a more consistent opam config tweaking, a new command was added : opam option.

For example:

• opam option download-jobs gives the global download-jobs value (as it exists only in global configuration)
• opam option jobs=6 --global will set the number of parallel build jobs opam is allowed to run (along with the associated jobs variable)
• opam option depext-run-commands=false disables the use of sudo for handling system dependencies; it will be replaced by a prompt to run the installation commands
• opam option depext-bypass=m4 --global bypass m4 system package check globally, while opam option depext-bypass=m4 --switch myswitch will only bypass it in the selected switch

The command opam var is extended with the same format, acting on switch and global variables.

Hint: to revert your changes use opam option <field>=, it will take its default value.

CLI Versioning

A new --cli switch was added to the first beta release, but it's only now that it's being widely used. opam is a complex enough system that sometimes bug fixes need to change the semantics of some commands. For example:

• opam show --file needed to change behaviour
• The addition of new controls for setting global variables means that the opam config was becoming cluttered and some things want to move to opam var
• opam switch install 4.11.1 still works in opam 2.0, but it's really an OPAM 1.2.2 syntax.

Changing the CLI is exceptionally painful since it can break scripts and tools which themselves need to drive opam. CLI versioning is our attempt to solve this. The feature is inspired by the (lang dune ...) stanza in dune-project files which has allowed the Dune project to rename variables and alter semantics without requiring every single package using Dune to upgrade their dune files on each release.

Now you can specify which version of opam you expected the command to be run against. In day-to-day use of opam at the terminal, you wouldn't specify it, and you'll get the latest version of the CLI. For example: opam var --global is the same as opam var --cli=2.1 --global. However, if you issue opam var --cli=2.0 --global, you will told that --global was added in 2.1 and so is not available to you. You can see similar things with the renaming of opam upgrade --unlock-base to opam upgrade --update-invariant.

The intention is that --cli should be used in scripts, user guides (e.g. blog posts), and in software which calls opam. The only decision you have to take is the oldest version of opam which you need to support. If your script is using a new opam 2.1 feature (for example opam switch create --formula=) then you simply don't support opam 2.0. If you need to support opam 2.0, then you can't use --formula and should use --packages instead. opam 2.0 does not have the --cli option, so for opam 2.0 instead of --cli=2.0 you should set the environment variable OPAMCLI to 2.0. As with all opam command line switches, OPAMCLI is simply the equivalent of --cli which opam 2.1 will pick-up but opam 2.0 will quietly ignore (and, as with other options, the command line takes precedence over the environment).

Note that opam 2.1 sets OPAMCLI=2.0 when building packages, so on the rare instances where you need to use the opam command in a package build: command (or in your build system), you must specify --cli=2.1 if you're using new features.

Since 2.1.0~rc2, CLI versioning applies to opam environment variables. The previous behavior was to ignore unknown or wrongly set environment variable, while now you will have a warning to let you know that the environment variable won't be handled by this version of opam.

To ensure not breaking compatibility of some widely used deprecated options, a default CLI is introduced: when no CLI is specified, those deprecated options are accepted. It concerns opam exec and opam var subcommands.

There's even more detail on this feature in our wiki. We're hoping that this feature will make it much easier in future releases for opam to make required changes and improvements to the CLI without breaking existing set-ups and tools.

Note: For opam libraries users, since 2.1 environment variable are no more loaded by the libraries, only by opam client. You need to load them explicitly.

opam root portability

opam root format changes during opam life-cycle, new field are added or removed, new files are added ; an older opam version sometimes can no longer read an upgraded or newly created opam root. opam root format has been updated to allow new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots). It is a read-only best effort access, any attempt to modify the opam root fails.

Hint: for opam libraries users, you can safely load states with OpamStateConfig load functions.

Tremendous thanks to all involved people, who've developed, tested & retested, helped with issue reports, comments, feedback...

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0" or download manually from the Github "Releases" page to your PATH.
2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

About OCamlPro:
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Feedback on this post is welcomed on Discuss!

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

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect t…

Feedback on this post is welcomed on Discuss!

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

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --switch parameters in the package build [#4668]
• When built with opam-file-format 2.1.3+, opam-format 2.0.x displays better errors for newer opam files [#4394]

Bug fixes

• Linux sandbox now mounts host $TMPDIR read-only, then sets the sandbox $TMPDIR to a new separate tmpfs. Hardcoded /tmp access no longer works if TMPDIR points to another directory [#4589]
• Stop clobbering DUNE_CACHE in the sandbox script [#4535, fixing ocaml/dune#4166]
• Ctrl-C now correctly terminates builds with bubblewrap; sandbox now requires bubblewrap 0.1.8 or later [#4400]
• Linux sandbox script no longer makes PWD read-write on remove actions [#4589]
• Lint W59 and E60 no longer trigger for packages flagged conf [#4549]
• Reduce the length of temporary file names for pin caching to ease pressure on Windows [#4590]
• Security: correct quoting of arguments when removing switches [#4707]
• Stop advertising the removed option --compiler when creating local switches [#4718]
• Pinning no longer fails if the archive’s opam file is malformed [#4580]
• Fish: stop using deprecated ^ syntax to fix support for Fish 3.3.0+ [#4736]

Installation instructions (unchanged):

1. From binaries: run

bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.0.9"

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 your sandbox script)

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.

About OCamlPro:
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Feedback on this post is welcomed on Discuss!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What's new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing …

Feedback on this post is welcomed on Discuss!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What's new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the "base packages" in opam 2.0 and allowing for easier compiler upgrades
• Improved options configuration (see the new option and expanded var sub-commands)
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• opam root readability by newer and older versions, even if the format changed
• Performance improvements to opam-update, conflict messages, and many other areas

Seamless integration of System dependencies handling (a.k.a. "depexts")

opam has long included the ability to install system dependencies automatically via the depext plugin. This plugin has been promoted to a native feature of opam 2.1.0 onwards, giving the following benefits:

• You no longer have to remember to run opam depext, opam always checks depexts (there are options to disable this or automate it for CI use). Installation of an opam package in a CI system is now as easy as opam install ., without having to do the dance of opam pin add -n/depext/install. Just one command now for the common case!
• The solver is only called once, which both saves time and also stabilises the behaviour of opam in cases where the solver result is not stable. It was possible to get one package solution for the opam depext stage and a different solution for the opam install stage, resulting in some depexts missing.
• opam now has full knowledge of depexts, which means that packages can be automatically selected based on whether a system package is already installed. For example, if you have neither MariaDB nor MySQL dev libraries installed, opam install mysql will offer to install conf-mysql and mysql, but if you have the MariaDB dev libraries installed, opam will offer to install conf-mariadb and mysql.

Hint: You can set OPAMCONFIRMLEVEL=unsafe-yes or --confirm-level=unsafe-yes to launch non interactive system package commands.

opam lock files and reproducibility

When opam was first released, it had the mission of gathering together scattered OCaml source code to build a community repository. As time marches on, the size of the opam repository has grown tremendously, to over 3000 unique packages with over 19500 unique versions. opam looks at all these packages and is designed to solve for the best constraints for a given package, so that your project can keep up with releases of your dependencies.

While this works well for libraries, we need a different strategy for projects that need to test and ship using a fixed set of dependencies. To satisfy this use-case, opam 2.0.0 shipped with support for using project.opam.locked files. These are normal opam files but with exact versions of dependencies. The lock file can be used as simply as opam install . --locked to have a reproducible package installation.

With opam 2.1.0, the creation of lock files is also now integrated into the client:

• opam lock will create a .locked file for your current switch and project, that you can check into the repository.
• opam switch create . --locked can be used by users to reproduce your dependencies in a fresh switch.

This lets a project simultaneously keep up with the latest dependencies (without lock files) while providing a stricter set for projects that need it (with lock files).

Hint: You can export the full configuration of a switch with opam switch export new options, --full to have all packages metadata included, and --freeze to freeze all VCS to their current commit.

Switch invariants

In opam 2.0, when a switch is created the packages selected are put into the “base” of the switch. These packages are not normally considered for upgrade, in order to ease pressure on opam's solver. This was a much bigger concern early on in opam 2.0's development, but is less of a problem with the default mccs solver.

However, it's a problem for system compilers. opam would detect that your system compiler version had changed, but be unable to upgrade the ocaml-system package unless you went through a slightly convoluted process with --unlock-base.

In opam 2.1, base packages have been replaced by switch invariants. The switch invariant is a package formula which must be satisfied on every upgrade and install. All existing switches' base packages could just be expressed as package1 & package2 & package3 etc. but opam 2.1 recognises many existing patterns and simplifies them, so in most cases the invariant will be "ocaml-base-compiler" {= "4.11.1"}, etc. This means that opam switch create my_switch ocaml-system now creates a switch invariant of "ocaml-system" rather than a specific version of the ocaml-system package. If your system OCaml package is updated, opam upgrade will seamlessly switch to the new package.

This also allows you to have switches which automatically install new point releases of OCaml. For example:

opam switch create ocaml-4.11 --formula='"ocaml-base-compiler" {>= "4.11.0" & < "4.12.0~"}' --repos=old=git+https://github.com/ocaml/opam-repository#a11299d81591
opam install utop

Creates a switch with OCaml 4.11.0 (the --repos= was just to select a version of opam-repository from before 4.11.1 was released). Now issue:

opam repo set-url old git+https://github.com/ocaml/opam-repository
opam upgrade

and opam 2.1 will automatically offer to upgrade OCaml 4.11.1 along with a rebuild of the switch. There's not yet a clean CLI for specifying the formula, but we intend to iterate further on this with future opam releases so that there is an easier way of saying “install OCaml 4.11.x”.

Hint: You can set up a default invariant that will apply for all new switches, via a specific opamrc. The default one is ocaml >= 4.05.0

Configuring opam from the command-line

Configuring opam is not a simple task: you need to use an opamrc at init stage, or hack global/switch config file, or use opam config var for additional variables. To ease that step, and permit a more consistent opam config tweaking, a new command was added : opam option.

For example:

• opam option download-jobs gives the global download-jobs value (as it exists only in global configuration)
• opam option jobs=6 --global will set the number of parallel build jobs opam is allowed to run (along with the associated jobs variable)
• opam option depext-run-commands=false disables the use of sudo for handling system dependencies; it will be replaced by a prompt to run the installation commands
• opam option depext-bypass=m4 --global bypass m4 system package check globally, while opam option depext-bypass=m4 --switch myswitch will only bypass it in the selected switch

The command opam var is extended with the same format, acting on switch and global variables.

Hint: to revert your changes use opam option <field>=, it will take its default value.

CLI Versioning

A new --cli switch was added to the first beta release, but it's only now that it's being widely used. opam is a complex enough system that sometimes bug fixes need to change the semantics of some commands. For example:

• opam show --file needed to change behaviour
• The addition of new controls for setting global variables means that the opam config was becoming cluttered and some things want to move to opam var
• opam switch install 4.11.1 still works in opam 2.0, but it's really an OPAM 1.2.2 syntax.

Changing the CLI is exceptionally painful since it can break scripts and tools which themselves need to drive opam. CLI versioning is our attempt to solve this. The feature is inspired by the (lang dune ...) stanza in dune-project files which has allowed the Dune project to rename variables and alter semantics without requiring every single package using Dune to upgrade their dune files on each release.

Now you can specify which version of opam you expected the command to be run against. In day-to-day use of opam at the terminal, you wouldn't specify it, and you'll get the latest version of the CLI. For example: opam var --global is the same as opam var --cli=2.1 --global. However, if you issue opam var --cli=2.0 --global, you will told that --global was added in 2.1 and so is not available to you. You can see similar things with the renaming of opam upgrade --unlock-base to opam upgrade --update-invariant.

The intention is that --cli should be used in scripts, user guides (e.g. blog posts), and in software which calls opam. The only decision you have to take is the oldest version of opam which you need to support. If your script is using a new opam 2.1 feature (for example opam switch create --formula=) then you simply don't support opam 2.0. If you need to support opam 2.0, then you can't use --formula and should use --packages instead. opam 2.0 does not have the --cli option, so for opam 2.0 instead of --cli=2.0 you should set the environment variable OPAMCLI to 2.0. As with all opam command line switches, OPAMCLI is simply the equivalent of --cli which opam 2.1 will pick-up but opam 2.0 will quietly ignore (and, as with other options, the command line takes precedence over the environment).

Note that opam 2.1 sets OPAMCLI=2.0 when building packages, so on the rare instances where you need to use the opam command in a package build: command (or in your build system), you must specify --cli=2.1 if you're using new features.

Since 2.1.0~rc2, CLI versioning applies to opam environment variables. The previous behavior was to ignore unknown or wrongly set environment variable, while now you will have a warning to let you know that the environment variable won't be handled by this version of opam.

To ensure not breaking compatibility of some widely used deprecated options, a default CLI is introduced: when no CLI is specified, those deprecated options are accepted. It concerns opam exec and opam var subcommands.

There's even more detail on this feature in our wiki. We're hoping that this feature will make it much easier in future releases for opam to make required changes and improvements to the CLI without breaking existing set-ups and tools.

Note: For opam libraries users, since 2.1 environment variable are no more loaded by the libraries, only by opam client. You need to load them explicitly.

opam root portability

opam root format changes during opam life-cycle, new field are added or removed, new files are added ; an older opam version sometimes can no longer read an upgraded or newly created opam root. opam root format has been updated to allow new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots). It is a read-only best effort access, any attempt to modify the opam root fails.

Hint: for opam libraries users, you can safely load states with OpamStateConfig load functions.

Tremendous thanks to all involved people, who've developed, tested & retested, helped with issue reports, comments, feedback...

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0"

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

Feedback on this post is welcomed on Discuss!

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

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --…

Feedback on this post is welcomed on Discuss!

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

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --switch parameters in the package build [#4668]
• When built with opam-file-format 2.1.3+, opam-format 2.0.x displays better errors for newer opam files [#4394]

Bug fixes

• Linux sandbox now mounts host $TMPDIR read-only, then sets the sandbox $TMPDIR to a new separate tmpfs. Hardcoded /tmp access no longer works if TMPDIR points to another directory [#4589]
• Stop clobbering DUNE_CACHE in the sandbox script [#4535, fixing ocaml/dune#4166]
• Ctrl-C now correctly terminates builds with bubblewrap; sandbox now requires bubblewrap 0.1.8 or later [#4400]
• Linux sandbox script no longer makes PWD read-write on remove actions [#4589]
• Lint W59 and E60 no longer trigger for packages flagged conf [#4549]
• Reduce the length of temporary file names for pin caching to ease pressure on Windows [#4590]
• Security: correct quoting of arguments when removing switches [#4707]
• Stop advertising the removed option --compiler when creating local switches [#4718]
• Pinning no longer fails if the archive's opam file is malformed [#4580]
• Fish: stop using deprecated ^ syntax to fix support for Fish 3.3.0+ [#4736]

1. From binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.0.9"

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

Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The Wome…

Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The WomenHack event has a unique setup similar to 'speed dating,' but for prospective jobs. Each candidate is paired with a company, and they have 5 minutes to chat before moving on to the next company. This "rapid interview" is both fun and efficient for all involved, and it ensures each company will meet several talented candidates from diverse backgrounds, which increases their chance of finding that perfect fit for an open position!

From their website:

WomenHack is a community that empowers women in tech through events, jobs, and reviews. We aim to create a more inclusive and diverse workplace for all. Our diversity recruiting events target some of the most talented women in tech which include software developers, designers, and product talent. 

Join us tomorrow, July 21st, at WomenHack! You can get your ticket here.

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincen…

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincent Laviron as mentor, and we’re proud to let him show off what he has achieved in this post.

The problem at hand

OCaml’s strong typing system is one of its main perks: it allows to write safe code thanks to the abstraction it provides. Most of the basic design mistakes will directly result into a typing error and the user cannot mess up the memory as it is automatically handled by the compiler and runtime.

However, these perks keep a power-user from implementing some optimizations, in particular those linked to memory representation as they cannot be accessed directly.

A good example would be this piece of code:

type return = Ok of int | Failure
let id = function
| Some x -> Ok x
| None -> Failure

In terms of memory representation, this function is indeed the identity function. Some x and Ok x share the same representation (and so do None and Failure). However, this identity is invisible to the user. Even if the user knows the representation is the same, they would need to use this function to avoid a typing error.

Another good example would be this one:

type record = { a:int; b:int }
let id (x,y) = { a = x; b = y }

Even if those functions are the identity, they come with a cost: not only do they cost a function call, they reallocate the result instead of just returning their argument directly. Detecting those functions would allow us to produce interesting optimizations.

Hurdles

If we want to detect identities, we quickly hit the problem of recursive functions: how does one recognize identity in those cases? Can a function be an identity if it doesn’t always terminate, or if it never does?

Once we have a good definition of what exactly an identity function is, we still need to prove that an existing function fits the definition. Indeed, we want to ensure the user that this optimization will not change the observable behavior of the program.

We also want to avoid breaking type safety. As an example, the following function:

let rec fake_id = function
| [] -> 0
| t::q -> fake_id (t::q)

A naive induction proof would allow us to replace this function with the identity, as [] and 0 share the same memory representation. However, this is unsafe as applying this to a non-empty list would return a list even if this function has an int type (we’ll talk more about it later).

To tackle those challenges, we started the internship with a theoretical study that lasted for three fourths of the allocated time and lastly implemented a practical solution in the Flambda representation of the compiler.

Theoretical results

We worked on extensions of lambda-calculus (implemented in OCaml) in order to gradually test our ideas in a simpler framework than the full Flambda.

Pairs

We started with a lambda-calculus to which we only added the concept of pairs. To prove identities, every function has to be annotated as identity or not. We then prove these annotations by β-reducing the function bodies. After each recursive reduction, we apply a rule that states that a pair made of the first and second projection of a variable is equal to that variable. We do not reduce applications, but we replace them by the argument if the concerned function is annotated as identity.

Using this method, we maintain a reasonable complexity compared to a full β-reduction which would be unrealistic on a big program.

We then add higher-order capabilities by allowing annotations of the form Annotation → Annotation. Functions as List.map can that way be abstracted as Id → Id. Even though this solution doesn’t cover every case, most real-world usage are recognized by these patterns.

Tuple reconstruction

We then move from just pairs to tuples of arbitrary size. This adds a new problem: if we make a pair out of the first two fields of a variable, this is no longer necessarily that variable, as it may have more than two fields.

We then have two solutions: we can first annotate every projection with the size of the involved tuple to know if we are indeed reconstructing the entire variable. As an example, if we make a pair from the fields of a triplet, we know there is no way to simplify this reconstruction.

Another solution, more ambitious, is to adopt a less restrictive definition of equality and to allow the replacement of (x,y) by (x,y,z). Indeed, if the variable was typed as a pair, we are guaranteed that the third field will never be accessed. The behavior of the program will therefore never be affected by this extension.

Though this allows to avoid a lot of allocations, it may also increase memory usage in some cases: if the triplet ceases to be used, it won’t be deallocated by the Garbage Collector (GC) and the field z will be kept in memory as long as (x,y) is still accessible.

This approach remains interesting to us, as long as it is manually enabled by the user for some specific blocks.

Recursion

We now add recursive definitions to our language, through the use of a fixpoint operator.

To prove that a recursive function is the identity, we have to use induction. The main difficulty is to prove that the function indeed terminates to ensure the validity of the induction.

We can separate this into three different levels of safety. The first option is to not prove termination at all, and let the user state which function they know will return. We can then assume the function is the identity and replace its body on that hypothesis. This approach is enough for most practical cases, but its main problem lies in the fact that it allows to write unsafe code (as we’ve already seen).

Our second option is to limit our induction hypothesis to recursive applications on “smaller” elements than the argument. An element is defined as smaller if it is a projection of the argument or a projection of a smaller element. This is not enough to prove that the function will terminate (the argument might be cyclic, for example) but is enough to ensure type safety. The reason is that any possibly returned value is constructed (as it cannot directly come from a recursive call) and have therefore a defined type. Typing would fail if the function was to return a value that cannot be identified to its argument.

Finally, we may want to establish a perfect equivalence between the function and the identity function before simplifying it. In that case, we propose to create a special annotation for functions that are the identity when applied to a non-cyclical object. We can prove they have this property with the already described induction. The difficulty now lies into applying the simplification only to valid applications: if an object is immutable, wasn’t recursively defined and is made of components that also have that property, we can declare that object inductive and simplify applications on it. The inductive state of variables can be propagated during our recursive pass of optimization.

Block reconstruction

The representation of blocks in Flambda provides interesting challenges in terms of equality detection, which is often crucial to prove an identity. It is very hard to detect an identical block reconstruction.

Blocks in Flambda

Variants

The blocks in Flambda come from the existence of variants in OCaml: one type may have several different constructors, as we can see in

type choice = A of int | B of int

When OCaml is compiled to Flambda, the information used by the constructor is lost and replaced by a tag. The tag is a number contained in the header of the object’s memory representation between 0 and 255 that represents which constructor was used. As an example, an element of type choice would have tag 0 for the A constructor, and 1 for B.

That tag will be kept at runtime, which will allow for example to implement pattern matching as a simple switch in Flambda, that executes simple comparisons on the tag to know which branch to execute next.

This system complicates our task as Flambda’s typing doesn’t inform us which type the constructor is supposed to have, and therefore keeps us from easily knowing if two variants are indeed equal.

Tag generalization

To complicate things, tags are actually used for any block, meaning tuples, modules or functions (as a matter of fact, almost anything but constant constructors and integers). If the object doesn’t have variants, it will usually have tag 0. This tag is never read (as there are no variants to differentiate) but keeps us from simply comparing two tuples, because Flambda will simply see two blocks of unknown tag.

Inlining

Finally, this system is optimized by inlining tuples: if a variant has a shape Pair of int * int, it will be often be flattened into a tuple (tag Pair, int, int).

This also means that variants can have an arbitrary size, which is also unknown in Flambda.

Existing approach

A partial solution to the problem already existed in a Pull Request (PR) you can read here.

The chosen approach in this PR is the natural one: we use the switch to gain information on the tag of a block, depending on the branch taken. The PR also allows to know the mutability and size of the block in each branch, starting from OCaml (where this information is known as it is explicit in the pattern matching) and propagating the knowledge to Flambda.

This allows to register every block on which a switch is done with their tag, size and mutability. We can then detect if one of them is reconstructed with the use of a Pmakeblock primitive.

Unfortunately, this path has its limits as there are numerous cases where the tag and size could be known without performing a switch on the value. As an example, this doesn’t allow the simplification of tuple reconstruction.

New solution

Our new solution will have to propagate more information from OCaml into Flambda. This propagation is based on two PRs that already existed for Flambda 2, which annotated in the lambda representation each projection (Pfield) with typing informations. We add block mutability and tag and finally size.

Our first contribution was to translate these PRs to Flambda 1, and to propagate from lambda to Flambda correctly.

We then had access to every necessary information to detect and prove block reconstruction: not only we have a list of blocks that were pattern-matched, we can make a list of partially immutable blocks, meaning blocks for which we know that some fields are immutable.

Here’s how we use it:

Block discovery

As soon as we find a projection, we verify whether it is done on an immutable block of known size. If so, we add that block to the list of partial blocks. We verify that the information we have on the tag and size are compatible with the already known projections. If all of the fields of the block are known, the block is added to the list of simplifiable blocks.

Of course, we also keep track of known blocks though switches.

Simplification

This part is similar to the original PR: when an immutable block is met, we check whether this block is known as simplifiable. In that case we avoid a reallocation.

Compared to the original approach, we also reduced the asymptotic complexity (from quadratic to linear) by registering the association of every projection variable to its index and original block. We also modified some implementation details that could have triggered a bug when associated with our PR.

Example

Let’s consider this function:

type typ1 = A of int | B of int * int
type typ2 = C of int | D of {x:int; y:int}
let id = function
  | A n -> C n
  | B (x,y) -> D {x; y}

The current compiler would produce the resulting Flambda output:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.8
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0:
            (let
              (Pmakeblock_arg/11 (field 0<{../../test.ml:4,4-7}> param/7)
               Pmakeblock/12
                 (makeblock 0 (int)<{../../test.ml:4,11-14}>
                   Pmakeblock_arg/11))
              Pmakeblock/12)
           case tag 1:
            (let
              (Pmakeblock_arg/15 (field 1<{../../test.ml:5,4-11}> param/7)
               Pmakeblock_arg/16 (field 0<{../../test.ml:5,4-11}> param/7)
               Pmakeblock/17
                 (makeblock 1 (int,int)<{../../test.ml:5,17-23}>
                   Pmakeblock_arg/16 Pmakeblock_arg/15))
              Pmakeblock/17)))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Our optimization allows to detect that this function reconstructs a similar block and therefore can simplify it:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.7
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0 (1): param/7
           case tag 1 (2): param/7))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Possible improvements

Equality relaxation

We can use observational equality studied in the theoretical part for block equality in order to avoid more allocations. The implementation is simple:

When a block is created, to know if it will be allocated, the normal course of action is to check if all of its fields are the known projections of another block, with the same index, and if the block sizes are the same. We can just remove that last check.

Implementing this was a bit more tricky because of several practical details. First, we want that optimization to be only triggered on user-annotated blocks, we had to propagate that annotation to Flambda.

Additionally, if we only implement that optimization, numerous optimization cases will be ignored because unused variables are simplified before our optimization pass. As an example, if a function looks like

let loose_id (a,b,c) = (a,b)

The c variable will be simplified away before reaching Flambda, and there will be no way to prove that (a,b,c) is immutable as its third field could not be. This problem is being solved on Flambda2 thanks to a PR that propagates mutability information for every block, but we didn’t have the time necessary to migrate it on Flambda 1.

Detecting recursive identities

Now that we can detect block reconstruction, we’re left with solving the problem of recursive functions.

Unsafe approach

We began the implementation of a pass that contains no termination proof. The idea is to add the proof later, or to authorize non-terminating functions to be simplified as long as they type correctly (see previously in the theory part).

For now, we trust the user to verify these properties manually.

Hence, we modified the function simplification procedure: when a function with a single argument is modified, we first assume that this function is the identity before simplifying its body. We then check whether the result is equivalent to an identity by recursively going through it, so as to cover as many cases as possible (for example in conditional branchings). If it is the case, the function will be replaced by the identity ; otherwise, we go back to a normal simplification, without the induction hypothesis.

Constant propagation

We took some time to improve our code that checks whether the body of a function is an identity or not, so as to handle constant values. It propagates identity information we have on an argument during conditional branching.

This way, on a function like

type truc = A | B | C
let id = function
  | A -> A
  | B -> B
  | C -> C

or even

let id x = if x=0 then 0 else x

We can successfully detect identity.

Examples

Recursive functions

We can now detect recursive identities:

let rec listid = function
  | t::q -> t::(listid q)
  | [] -> []

Used to compile to:

End of middle end:
let_rec_symbol
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.11
        (listid/5 = fun param/7 ->
          (if param/7 then begin
            (let
              (apply_arg/13 (field 1<{../../test.ml:9,4-8}> param/7)
               apply_funct/14 camlTest__listid_5_closure
               Pmakeblock_arg/15
                 *(apply*[listid/5]<{../../test.ml:9,15-25}> apply_funct/14
                    apply_arg/13)
               Pmakeblock_arg/16 (field 0<{../../test.ml:9,4-8}> param/7)
               Pmakeblock/17
                 (makeblock 0<{../../test.ml:9,12-25}> Pmakeblock_arg/16
                   Pmakeblock_arg/15))
              Pmakeblock/17)
            end else begin
            (let (const_ptr_zero/27 Const(0a)) const_ptr_zero/27) end))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
let_symbol (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

But is now detected as being the identity:

End of middle end:
let_symbol
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.13 (listid/5 = fun param/7 -> param/7)
        free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

Unsafe example

However, we can use the unsafety of the feature to go around the typing system and access a memory address as if it was an integer:

type bugg = A of int*int | B of int
let rec bug = function
  | A (a,b) -> (a,b)
  | B x -> bug (B x)
  
let (a,b) = (bug (B 42))
let _ = print_int b

This function will be simplified to the identity even though the bugg type is not compatible with tuples; trying to project on the second field of variant b will access an undefined part of memory:

$ ./unsafe.out
47423997875612

Possible improvements – short term

Function annotation

A theoretically simple thing to add would be to let the choice of applying unsafe optimizations to the user. We lacked the time to do the work of propagating the information to Flambda, but it would not be hard to implement.

Order on arguments

For a safer optimization, we could use the idea developed in the theoretical part to make the optimization correct on non-cyclical objects and more importantly give us typing guarantees to avoid the problem we just saw.

To get this guarantee, we would have to change the simplification pass by adding an optional pair of function-argument to the environment. When this option exists, the pair indicates that we are in the body in the process of simplification and that applications on smaller elements can be simplified as identity. Of course, the pass would need to be modified to remember which elements are not smaller than the previous argument.

Possible improvements – long term

Exclusion of cyclical objects

As described in the theoretical part, we could recursively deduce which objects are cyclical and attempt to remove them from our optimization. The problem is then that instead of having to replace functions by the identity, we need to add a special annotation that represents IdRec.

This amounts to a lot of added implementation complexity when compiling over several files, as we need access to the interface of already compiled files to know when the optimization can be used.

A possibility would be to use .cmx files to store this information when the file is compiled, but that kind of work would have taken too long to be achieved during the internship. Moreover, the practicality of that choice is far from obvious: it would complexify the optimization pass for a small improvement with respect to a version that would be correct on non-cyclical objects and activated through annotations.

About OCamlPro:
OCamlPro is a company founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index, and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Introduction

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

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

Introduction

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

We provide at builds.robur.coop binary unikernel images (and supplementary software). Doing binary releases of MirageOS unikernels is challenging in two aspects: firstly to be useful for everyone, a binary unikernel should not contain any configuration (such as private keys, certificates, etc.). Secondly, the binaries should be reproducible. This is crucial for security; everyone can reproduce the exact same binary and verify that our build service did only use the sources. No malware or backdoors included.

This post describes how you can deploy MirageOS unikernels without compiling it from source, then dives into the two issues outlined above - configuration and reproducibility - and finally describes how to setup your own reproducible build infrastructure for MirageOS, and how to bootstrap it.

Deploying MirageOS unikernels from binary

To execute a MirageOS unikernel, apart from a hypervisor (Xen/KVM/Muen), a tender (responsible for allocating host system resources and passing these to the unikernel) is needed. Using virtio, this is conventionally done with qemu on Linux, but its code size (and attack surface) is huge. For MirageOS, we develop Solo5, a minimal tender. It supports hvt - hardware virtualization (Linux KVM, FreeBSD BHyve, OpenBSD VMM), spt - sandboxed process (a tight seccomp ruleset (only a handful of system calls allowed, no hardware virtualization needed), Linux only). Apart from that, muen (a hypervisor developed in Ada), virtio (for some cloud deployments), and xen (PVHv2 or Qubes 4.0) - read more. We deploy our unikernels as hvt with FreeBSD BHyve as hypervisor.

On builds.robur.coop, next to the unikernel images, solo5-hvt packages (FreeBSD 12.2, Ubuntu 20.04) are provided - download the binary and install it. A NixOS package is already available - please note that soon packaging will be much easier (and we will work on packages merged into distributions).

When the tender is installed, download a unikernel image (e.g. the traceroute described in an earlier post), and execute it:

$ solo5-hvt --net:service=tap0 -- traceroute.hvt --ipv4=10.0.42.2/24 --ipv4-gateway=10.0.42.1

If you plan to orchestrate MirageOS unikernels, you may be interested in albatross - we provide binary packages as well for this (albatross FreeBSD and albatross Ubuntu 20.04). An upcoming post will go into further details of how to setup albatross.

MirageOS configuration

A MirageOS unikernel has a specific purpose - composed of OCaml libraries - selected at compile time, which allows to only embed the required pieces. This reduces the attack surface drastically. At the same time, to be widely useful to multiple organisations, no configuration data must be embedded into the unikernel.

Early MirageOS unikernels such as mirage-www embed content (blog posts, ..) and TLS certificates and private keys in the binary (using crunch). The Qubes firewall (read the blog post by Thomas for more information) used to include the firewall rules until v0.6 in the binary, since v0.7 the rules are read dynamically from QubesDB. This is big usability improvement.

We have several possibilities to provide configuration information in MirageOS, on the one hand via boot parameters (can be pre-filled at development time, and further refined at configuration time, but those passed at boot time take precedence). Boot parameters have a length limitation.

Another option is to use a block device - where the TLS reverse proxy stores the configuration, modifiable via a TCP control socket (authentication using a shared hmac secret).

Several other unikernels, such as this website and our CalDAV server, store the content in a remote git repository. The git URI and credentials (private key seed, host key fingerprint) are passed via boot parameter.

Finally, another option that we take advantage of is to introduce a post-link step that rewrites the binary to embed configuration. The tool caravan developed by Romain that does this rewrite is used by our openvpn router (binary).

In the future, some configuration information - such as monitoring system, syslog sink, IP addresses - may be done via DHCP on one of the private network interfaces - this would mean that the DHCP server has some global configuration option, and the unikernels no longer require that many boot parameters. Another option we want to investigate is where the tender shares a file as read-only memory-mapped region from the host system to the guest system - but this is tricky considering all targets above (especially virtio and muen).

Behind the scenes: reproducible builds

To provide a high level of assurance and trust, if you distribute binaries in 2021, you should have a recipe how they can be reproduced in a bit-by-bit identical way. This way, different organisations can run builders and rebuilders, and a user can decide to only use a binary if it has been reproduced by multiple organisations in different jurisdictions using different physical machines - to avoid malware being embedded in the binary.

For a reproduction to be successful, you need to collect the checksums of all sources that contributed to the built, together with other things (host system packages, environment variables, etc.). Of course, you can record the entire OS and sources as a tarball (or file system snapshot) and distribute that - but this may be suboptimal in terms of bandwidth requirements.

With opam, we already have precise tracking which opam packages are used, and since opam 2.1 the opam switch export includes extra-files (patches) and records the VCS version. Based on this functionality, orb, an alternative command line application using the opam-client library, can be used to collect (a) the switch export, (b) host system packages, and (c) the environment variables. Only required environment variables are kept, all others are unset while conducting a build. The only required environment variables are PATH (sanitized with an allow list, /bin, /sbin, with /usr, /usr/local, and /opt prefixes), and HOME. To enable Debian's apt to install packages, DEBIAN_FRONTEND is set to noninteractive. The SWITCH_PATH is recorded to allow orb to use the same path during a rebuild. The SOURCE_DATE_EPOCH is set to enable tools that record a timestamp to use a static one. The OS* variables are only used for recording the host OS and version.

The goal of reproducible builds can certainly be achieved in several ways, including to store all sources and used executables in a huge tarball (or docker container), which is preserved for rebuilders. The question of minimal trusted computing base and how such a container could be rebuild from sources in reproducible way are open.

The opam-repository is a community repository, where packages are released to on a daily basis by a lot of OCaml developers. Package dependencies usually only use lower bounds of other packages, and the continuous integration system of the opam repository takes care that upon API changes all reverse dependencies include the right upper bounds. Using the head commit of opam-repository usually leads to a working package universe.

For our MirageOS unikernels, we don't want to stay behind with ancient versions of libraries. That's why our automated building is done on a daily basis with the head commit of opam-repository. Since our unikernels are not part of the main opam repository (they include the configuration information which target to use, e.g. hvt), and we occasionally development versions of opam packages, we use the unikernel-repo as overlay.

If no dependent package got a new release, the resulting binary has the same checksum. If any dependency was released with a newer release, this is picked up, and eventually the checksum changes.

Each unikernel (and non-unikernel) job (e.g. dns-primary outputs some artifacts:

• the binary image (in bin/, unikernel image, OS package)
• the build-environment containing the environment variables used for this build
• the system-packages containing all packages installed on the host system
• the opam-switch that contains all opam packages, including git commit or tarball with checksum, and potentially extra patches, used for this build
• a job script and console output

To reproduce such a built, you need to get the same operating system (OS, OS_FAMILY, OS_DISTRIBUTION, OS_VERSION in build-environment), the same set of system packages, and then you can orb rebuild which sets the environment variables and installs the opam packages from the opam-switch.

You can browse the different builds, and if there are checksum changes, you can browse to a diff between the opam switches to reason whether the checksum change was intentional (e.g. here the checksum of the unikernel changed when the x509 library was updated).

The opam reproducible build infrastructure is driven by:

• orb conducting reproducible builds (packages FreeBSD, Ubuntu 20.04)
• builder scheduling builds in contained environments (packages FreeBSD, Ubuntu 20.04)
• builder-web storing builds in a database and providing a HTTP interface (packages FreeBSD)

These tools are themselves reproducible, and built on a daily basis. The infrastructure executing the build jobs installs the most recent packages of orb and builder before conducting a build. This means that our build infrastructure is reproducible as well, and uses the latest code when it is released.

Conclusion

Thanks to NGI funding we now have reproducible MirageOS binary builds available at builds.robur.coop. The underlying infrastructure is reproducible, available for multiple platforms (Ubuntu using docker, FreeBSD using jails), and can be easily bootstrapped from source (once you have OCaml and opam working, getting builder and orb should be easy). All components are open source software, mostly with permissive licenses.

We also have an index over sha-256 checksum of binaries - in the case you find a running unikernel image where you forgot which exact packages were used, you can do a reverse lookup.

We are aware that the web interface can be improved (PRs welcome). We will also work on the rebuilder setup and run some rebuilds.

Please reach out to us (at team AT robur DOT coop) if you have feedback and suggestions.

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

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

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

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

Since digital transformation has become more and more dependent on cloud computing, it has increasing problems with high response latency, security risks, and resource inefficiencies—all which make these services ultimately unreliable. The demand for interconnected devices is ever increasing, but the security of these devices remain unchecked, making them susceptible to security vulnerabilities. This leaves consumers and businesses open to exploitation, as demonstrated in reports of tech devices violating users’ privacy, like sending audio recordings without their knowledge or consent.

Tarides addresses these issues with OSMOSE, a platform which combines hardware and software elements to invert the current cloud-centric model. OSMOSE securely connects with physical spaces to provide extremely low latency and high-bandwidth, local-area computation capabilities, which can turn a fleet of IoT devices into a local data-centre.

This innovative platform enables computer resources to be tracked efficiently and temporarily rented to users. This turns any IoT deployment into a local, private cloud, allowing a better utilization of local resources and improved security.

Major components of OSMOSE already have commercial applications. It’s been used to make existing cloud deployments more secure and efficient by companies such as Amazon, Citrix, and Docker.

Tarides applies a high-touch, mixed business strategy—using consultancy services to field test open source components under development. Tarides applies their research to real-world systems to build unikernels, a secure-by-design and resource-efficient application specialised to their run-time environments. If interested in using OSMOSE as a solution for your business, please reach out to Tarides for more information.

Register for OSIS to attend the OSMOSE presentation on 1 July 2021.

Feedback on this post is welcomed on Discuss!

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

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

Feedback on this post is welcomed on Discuss!

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

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots).

Please do take this release candidate for a spin! It is available in the Docker images at ocaml/opam on Docker Hub as the opam-2.1 command (or you can sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam in your Dockerfile to switch to it permanently). The release candidate can also be tested via our installation script (see the wiki for more information).

Thank you to anyone who noticed the unannounced first release candidate and tried it out. Between tagging and what would have been announcing it, we discovered an issue with upgrading local switches from earlier alpha/beta releases, and so fixed that for this second release candidate.

Assuming no showstoppers, we plan to release opam 2.1.0 next week. The improvements made in 2.1.0 will allow for a much faster release cycle, and we look forward to posting about the 2.2.0 plans soon!

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0~rc2"

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

We hope there won't be any, but please report any issues to the bug-tracker. Thanks for trying it out, and hoping you enjoy!

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

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

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

Given our investment in these technologies, we have been following closely the recent changes in ReScript, with its rebrand and renaming, and the split with the ReasonML project, explained in the project blog post.

ReScript: becoming its own language

We are excited about the way ReScript is unifying the experience and making it easier for developers who are getting started to find documentation in a single place, as well as continuing its strong focus on performance and readable JavaScript output.

On the other hand, we are trying to figure out the implications of this change in the mid- and long-term, especially regarding the integration with the OCaml ecosystem. And more importantly, what this evolution will mean for production users like us who rely on this integration.

ReScript integration with OCaml has historically been seamless, as BuckleScript started originally as a new backend for the OCaml compiler. However, in recent months, there have been several hints that ReScript wants to evolve towards becoming its own language:

• It has now its own parser, incompatible with OCaml native applications
• Official repository guidelines for technical writing mentions explicitly that no reference to OCaml should appear in docs
• Upgrades to the latest version of OCaml compiler, which used to be part of the roadmap, have been deprioritized recently.

So, even if officially ReScript has not announced that they will break backwards compatibility with OCaml, just the fact that it is sticking with an old version of the OCaml compiler poses some challenges for us in terms of tooling. The uncertainty about the future and the pace of changes add some risk to the high-level goals we have for our teams and codebase: we would like to share more code between frontend and backend, not less.

Melange: a fork of ReScript, focused on OCaml compatibility

When António Monteiro announced Melange, a fork of ReScript but with a strong focus on keeping compatibility with OCaml, we decided to try it out and see how it could work for us.

Ultimately, the experiment was successful. We managed to build all our frontend applications with Melange, while keeping the existing bundling setup, which currently uses Webpack.

Throughout this process, we had to modify some parts of the code. We will now go through the most relevant parts of the process:

• Upgrade to OCaml 4.12: the most relevant part was the deprecation of Pervasives module to use Stdlib.
• Use ppxlib in our ppxs: we had to upgrade the two ppxs that we use in the frontend codebase to the latest compiler version, bs-emotion-ppx and an in-house ppx for internationalization.
• Configure esy: we were already using esy to bring the editor tooling into scope of the developer environment, so we just had to make sure melange would also be included in the json configuration.
• Upgrade to Reason 3.7.0: a quite simple change too, as the whole process is automated by using refmt. As a side note, we ran into a small bug with some type annotations, that we were able to work around.
• “Lift” dune workspace to the root of our monorepo: this is probably the most intrusive change. Because we have shared code between backend and frontend, and Dune needs to have access to all sources under its workspace, we had to “lift” the Dune workspace from the backend directory to the root of monorepo.

The good

This experiment allowed us to experience what a project like Melange could offer for our use case. Here are some of the things we might be able to leverage in a codebase built with Melange:

• Recent version of the OCaml compiler: at some point, we could pin compiler version between backend and frontend teams, making upgrades more straightforward as they would happen atomically.
• Shared editor tooling: the official OCaml vscode extension works great with Melange, as well as any other OCaml editor integration. Having backend and frontend teams use similar editor setup removes a lot of maintenance work for us.
• Consuming ppxs from source: Melange allows to consume ppxs from source, which also removes issues with pre-compiled ppxs (like this issue with the recent M1 Macs).
• Melange allows to run all ppxs from a single executable file, which has some nice performance benefits.
• Use Dune for atd files generators: ReScript “generators” are unfortunately not documented anymore, but we use them extensively for atd file generation. Being able to share Dune rules in backend and frontend would make our build setup easier.
• Access to OCaml documentation tooling: Melange allows to leverage existing tooling for generating documentation, like odoc.
• Async syntax: the latest Reason version supports “let op” syntax, which is handy for client-side code.

The bad

While there are many things that are exciting about Melange, there are some other parts that can be improved.

• Build performance: We already knew that performance would be far worse than ReScript, as Melange uses Dune in a way that it was not designed for. In our tests, builds with Melange are roughly 1 order of magnitude slower than ReScript ones.
• First-class Dune support: if there was a deeper integration between Dune and Melange, we could explore features like shared libraries or shared rules between backend and frontend. As of today, Dune has no knowledge about Melange environment, so it can perform basic rules execution, but there is no access to high level stanzas like library in Melange.
• Two-headed goal: finally, we see a more strategic risk in Melange proposition. Right now it has two goals: keep compatibility with both ReScript and OCaml. But we don’t know how long these goals will be feasible. If at some point ReScript decides to move away from the OCaml compiler fully, then Melange users would not be able to consume any updates to the ReScript ecosystem anymore.

Alright, but are you migrating to Melange or ReScript?

With all the information available, the answer is: we don’t know yet. 😄 We want to keep exploring all the available options and have as much information as possible before committing further. So for now, we are upgrading the codebase to recent versions of ReScript, but we are holding up on features that only work one way. For example, we have not migrated our codebase to the ReScript syntax yet, as there is no way to translate back to Reason syntax.

In the meantime, we will keep exploring how far the limitations of Melange can be mitigated. To be continued! 🚀

Thanks to Igor and Feihong for reviewing and improving earlier versions of this post.

Building Ahrefs codebase with Melange was originally published in ahrefs on Medium, where people are continuing the conversation by highlighting and responding to this story.

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

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

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

Why formalize?

Most people formalize mathematics (in Automa…

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

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

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

Why formalize?

Most people formalize mathematics (in Automath, NuPrl, Coq, Agda, Lean, ...) to get confidence in the correctness of mathematics - or so they claim. The reality is that formalizing mathematics is intellectually fun.

Entertaining considerations aside, my initial motivation for computer formalization, about 10 years ago, was to write algorithms derived from work on game theory with Paulo Oliva. In particular, this had applications to proof theory, such as getting programs from classical proofs. Our first version of a (manually) extracted program from a classical proof was written in Haskell, in a train journey coming back from a visit to our collaborators Monika Seisenberger and Ulrich Berger in Swansea. The train journey was long enough for us to be able to complete the program. But when we ran it, it didn't work. I had been learning Agda for about one year by then, and I told Paulo that it would be easier to write the mathematics in Agda, and hence be sure it will work before we ran it, than to debug the Haskell program. And that was the case.

Before then I was the kind of person who dismissed formalization, and would say so to people who did formalization (it is probably too late to apologize now). I trusted my own mathematics, and if I wanted to derive programs from my mathematical work, I would just write them manually. Since then, my attitude has changed considerably.

I now use Agda as a "blackboard" to develop my work. For example, the following were conceived and developed directly in Agda before they were written in mathematical vernacular: Injective types in univalent mathematics, Compact, totally separated and well-ordered types in univalent mathematics, The Cantor-Schröder-Bernstein Theorem for ∞-groupoids, The Burali-Forti argument in HoTT/UF and Continuity of Gödel's system T functionals via effectful forcing.

Other people will have different reasons to formalize. For example, wouldn't it be wonderful if the whole undergraduate mathematical curriculum were formalized? Wouldn't it be wonderful to archive all mathematical knowledge not just as text but in a more structured way, so that it can be used by both people and computers? Wouldn't it be wonderful if when we submit a paper, the referee didn't need to check correctness, but only novelty, significance and so on? Did you ever woke up in the middle of the night after you submitted a paper, with doubts about the crucial lemma? Or worse, after it was published?

But for the purposes of this post, I will concentrate on only one aspect of formalization: a formalized piece of constructive mathematics is automatically a computer program that you can run in practice.

Constructive mathematics

Constructive mathematics begins by removing the principle of excluded middle, and therefore the axiom of choice, because choice implies excluded middle. But why would anybody do such an outrageous thing?

I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general.

When I say that I am interested in constructive mathematics, most of the time I mean that I am interested in neutral mathematics, so that we simply remove excluded middle and choice, and we don't add anything to replace them. So my constructive definitions and theorems are also definitions and theorems of classical mathematics.

Occasionally, I flirt with axioms that contradict the principle of excluded middle, such as Brouwerian intuitionistic axioms that imply that "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous", when we equip the set $2$ with the discrete topology and $\mathbb{N} \to 2$ with the product topology, so that we get the Cantor space. The contradiction with classical logic, of course, is that using excluded middle we can define non-continuous functions by cases. Brouwerian intuitionistic mathematics is analogous to hyperbolic or elliptic geometry in this respect. The "constructive" mathematics I am talking about in this post is like neutral geometry, and I would rather call it "neutral mathematics", but then nobody would know what I am talking about. That's not to say that the majority of mathematicians will know what I am talking about if I just say "constructive mathematics".

But it is not (only) the generality of neutral mathematics that I find attractive. Somehow magically, constructions and proofs that don't use excluded middle or choice are automatically programs. The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. We don't need to consider Turing machines to establish computability. What is a computable sheaf, anyway? I don't want to pause to consider this question in order to use a sheaf topos to compute a number. We only need to consider sheaves in the usual mathematical sense.

Sometimes people ask me whether I believe in the principle of excluded middle. That would be like asking me whether I believe in the parallel postulate. It is clearly true in Euclidean geometry, clearly false in elliptic and in hyperbolic geometries, and deliberately undecided in neutral geometry. Not only that, in the same way as the parallel postulate defines Euclidean geometry, the principle of excluded middle and the axiom of choice define classical mathematics.

The undecidedness of excluded middle in my neutral mathematics allows me to prove, for example, "if excluded middle holds, then the Cantor-Schröder-Bernstein Theorem for ∞-groupoids holds". If excluded middle were false, I would be proving a counter-factual - I would be proving that an implication is true simply because its premise is false. But this is not what I am doing. What I am really proving is that the CSB theorem holds for the objects of boolean ∞-toposes. And why did I use excluded middle? Because somebody else showed that there is no other way. But also sometimes I use excluded middle or choice when I don't know whether there is another way (in fact, I believe that more than half of my publications use classical logic).

So, am I a constructivist? There is only one mathematics, of which classical and constructive mathematics are particular branches. I enjoy exploring the whole landscape. I am particularly fond of constructive mathematics, and I wouldn't practice it, however useful it may be for applications, if I didn't enjoy it. But this is probably my bad taste.

Toposes as provinces of the mathematical world

Toposes are generalized (sober) spaces. But also toposes can be considered as provinces of the mathematical world.

Hyland's effective topos is a province where "everything is computable". This is an elementary topos, which is not a Grothendieck topos, built from classical ingredients: we use excluded middle and choice, with Turing machines to talk about computability. But, as it turns out, although everybody agrees which functions $\mathbb{N} \to \mathbb{N}$ are computable and which ones aren't, there is disagreement among classical mathematicians working on computability theory about what counts as "computable" for more general mathematical objects, such as functions $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. No problem. Just consider other provinces, called realizability toposes, which include the effective topos as an example.

Johnstone's topological topos is a topos of spaces. It fully embeds a large category of topological spaces, where the objects outside the image of the embedding can be considered as generalized spaces (which include the Kuratowski limit spaces and more). In this province of the mathematical world, "all functions are continuous".

There are also provinces where there are infinitesimals and "all functions are smooth".

A more boring, but important, province, is the topos of classical sets. This is where classical mathematics takes place.

These provinces of mathematics have an internal language. We use a certain subobject classifier to collect the things that count as truth values in the province, and we devise a kind of type theory whose types are interpreted as objects and whose mathematical statements are interpreted as truth values in the province. Then a mathematical statement in this type theory is true in some toposes, false in other toposes, and undecided in yet other toposes. This internal language, or type theory, is very rich. Starting from natural numbers we can construct the integers, the rationals, the real numbers, free groups etc., and then do e.g. analysis and group theory and so on. The internal language of the free topos can be considered as a type theory for neutral mathematics: whatever we prove in the free type theory is true in all mathematical provinces, including classical set theory.

In the above first three provinces, the principle of excluded middle fails, but for different reasons, with respectively computability, continuity and infinitesimals to blame.

Our topos

Now our plot has a twist: we work within neutral mathematics to build a province of "biased" constructive mathematics where Brouwerian principles hold, such as "all functions $(\mathbb{N} \to 2) → \mathbb{N}$ are uniformly continuous".

Johnstone's topological topos (1979) would do the job, except that it is built using classical ingredients. This topos has siblings by Mike Fourman (1982) and van der Hoeven and Moerdijk (1984) with aims similar to ours, as explained in our own 2013 and 2016 papers, which give a third sibling.

Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage. Van der Hoeven and Moerdijk's topos is similar: this time take the monoid of continuous endomaps of the Baire space, with the "open-cover coverage". Fourman's topos is constructed from a site of formal spaces or locales, with a similar coverage.

Our topos is also similar: we take the monoid of uniformly continuous endomaps of the Cantor space. Because it is not provable in neutral mathematics that continuous functions on the Cantor space are automatically uniformly continuous, we explicitly ask for uniform continuity rather than just continuity. As for our coverage, we initially considered coverings of finitely many jointly surjective maps. But an equivalent, smaller coverage makes the mathematics (and the formalization) simpler: for each natural number $n$ we consider a cover with $2^n$ functions, namely the concatenation maps $(\mathbb{N} \to 2) \to (\mathbb{N} \to 2)$ defined by $\alpha \mapsto s \alpha$ for each finite binary sequence $s$ of length $n$. These functions are jointly surjective, and, moreover, have disjoint images, considerably simplifying the checking of the sheaf condition. Moreover, the coverage axiom is not only satisfied, but also is equivalent to the fact that the morphisms in our site are uniformly continuous functions. So this is a sort of "uniform-continuity coverage". Our slides (2014) illustrate these ideas with pictures and examples.

The details of the mathematics can be found in the above paper, and the Agda formalization can be found at Chuangjie's page. A few years later, we ported part of this formalization to Cubical Agda to deal properly with function extensionality (which we originally dealt with in ad hoc ways).

The integer we compute

After we construct the sheaf topos, we define a simple type theory and we interpret it in the topos. We define a "function" $(\mathbb{N} \to 2) \to \mathbb{N}$ in this type theory, without proving that it is uniformly continuous, and apply the interpretation map to get a morphism of the topos, which amounts to a uniformly continuous function. From this morphism we get the modulus of uniform continuity, which is the integer we are interested in. The interested reader can find the details in the above paper and Agda code for the paper or the substantially more comprehensive Agda code for Chuangjie's thesis.

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

What is DAPSI?

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

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

What is DAPSI?

The Data Portability and Services Incubator (DAPSI) is an EU funded project, under the European Commission’s Next Generation Internet (NGI) initiative. The aim of this initiave is to empower top internet innovators to develop human-centric solutions. DAPSI addresses the challenge of personal data portability on the internet, as foreseen under the GDPR and make it significantly easier for citizens to have any data which is stored with one service provider transmitted directly to another provider.

Take a look at the DAPSI innovators portfolio to see more information about the selected projects.

What is our project?

Our project, called SCoP for Secure-by-design Communication Protocols, is taking part in the DAPSI to tackle data portability issues in communication services.

Over the past few decades, the usage of emails has been massively widespread by both individuals and companies. Billions of emails are sent every day and this number is expected to increase to reach 333 billion of emails exchanged daily in 2022. Moreover, as managing internet communication stacks have become increasingly complex, end-users have tended to entrust this task to third-party companies like Google and Microsoft. Furthermore, existing implementations of these communication services rely on ad-hoc methodologies and memory-unsafe languages, where minor developer errors can easily escalate into major security flaws. The centralization of these communication services means that a single successful attack leads to major personal data breaches.

To fix this issue, our project aims to engineer a modern basis for open messaging that supports existing protocols such as emails but is also extensible and customizable for emerging protocols such as matrix. We will be building trustable implementations of these open protocols using type-safe languages and we will deploy these implementations as specialized, secure and resource efficient unikernels. They will become the basis of the communication system of OSMOSE, Tarides’ commercial solution for secure-by-design IoT infrastructure.

Every component of that system will be carefully designed as independent libraries, using modern development techniques to avoid the common reported threats and flaws. For instance, the implementation of protocol parsers and serializers will be written in a type-safe language and will be using fuzzing, e.g state-of-the-art coverage-driven tests. The combination of these techniques will increase users’ trust to migrate their personal data to these new secure services.

Moreover, these techniques are also useful to produce a large and reusable corpus of test materials, which we plan to release separately for other implementations to use. It will give the tools to other developers to write the next generation of messaging applications by extending the existing protocols with more confidence.

Want to be part of it?

Would you like to hear more about the project? Or want to deploy our solution? This project will build on a number of existing components in MirageOS, such as MrMime and Irmin, so feel free to contribute to these existing components! Please reach out to contact@tarides.com.