This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type t…

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type theory featuring computational versions of function extensionality, higher inductive types, and univalence. Building on ideas from Epigram, Agda, and Idris, redtt introduces a new cubical take on interactive proof development with holes. We will first introduce the basics of cubical type theory and then dive into an interactive demonstration of redtt’s features and its mathematical library.

After this we will catch a first public glimpse of the future of redtt, a new prototype that our team is building currently code-named “cooltt”: cooltt introduces syntax to split on disjunctions of cofibrations in arbitrary positions, implementing the full definitional eta law for disjunction. While cooltt is still in the early stages, it already has full support for univalence and cubical interactive proof development.

The talk will be recorded and published online.

Upcoming talks:

• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will …

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions.

Our experience demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.

The video recording of the talk.

Upcoming talks:

• June 4, 2020: Jon Sterling - redtt
• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

We are pleased to announce that TLS 1.3 support for MirageOS is available. With mirage 3.7.7 and tls 0.12 the Transport Layer Security (TLS) Protocol Version 1.3 is available in all MirageOS unikernels, including on our main website. If you're reading this, you've likely established a TLS 1.3 connection already :)

Getting there was some effort: we now embed the Coq-verified fiat library (from fiat-crypto) for the P-256 elliptic curve, and the F*-verified hacl library (from Project Everest) for t…

We are pleased to announce that TLS 1.3 support for MirageOS is available. With mirage 3.7.7 and tls 0.12 the Transport Layer Security (TLS) Protocol Version 1.3 is available in all MirageOS unikernels, including on our main website. If you're reading this, you've likely established a TLS 1.3 connection already :)

Getting there was some effort: we now embed the Coq-verified fiat library (from fiat-crypto) for the P-256 elliptic curve, and the F*-verified hacl library (from Project Everest) for the X25519 elliptic curve to establish 1.3 handshakes with ECDHE.

Part of our TLS 1.3 stack is support for pre-shared keys, and 0 RTT. If you're keen to try these features, please do so and report any issues you encounter to our issue tracker.

We are still lacking support for RSA-PSS certificates and EC certificates, post-handshake authentication, and the chacha20-poly1305 ciphersuite. There is also a minor symbol clash with the upstream F* C bindings which we are aware of. We will continue to work on these, and patches are welcome.

(This article is cross-posted by the Origin Labs team)

We are happy to announce the first release of our Solidity parser, written in OCaml using Menhir. This is a joint effort with Origin Labs, the company behind Dune Network, to implement a full interpreter for the Solidity language directly in a blockchain.

Solidity is probably the most popular language for smart-contracts, small pieces of code triggered when accounts receive transactions on a blockchain.Solidity is an object-orien…

(This article is cross-posted by the Origin Labs team)

We are happy to announce the first release of our Solidity parser, written in OCaml using Menhir. This is a joint effort with Origin Labs, the company behind Dune Network, to implement a full interpreter for the Solidity language directly in a blockchain.

Solidity is probably the most popular language for smart-contracts, small pieces of code triggered when accounts receive transactions on a blockchain.Solidity is an object-oriented strongly-typed language with a Javascript-like syntax. Solidity was first implemented for the Ethereum blockchain, with a compiler to the EVM, the Ethereum Virtual Machine.

Dune Network takes a different approach, as Solidity smart-contracts will be executed natively, after type-checking. Solidity will be the third native language on Dune Network, with Michelson, a low-level strongly-typed language inherited from Tezos, and Love, an higher-level strongly-typed language, also implemented jointly by OCamlPro and Origin Labs.

A first step has been accomplished, with the completion of the Solidity parser and printer, written in OCaml with Menhir.

This parser (and its printer companion) is now available as a standalone library under the LGPLv3 license with Linking Exception, allowing its integration in all projects. The source code is available at https://gitlab.com/o-labs/solidity-parser-ocaml.

Our parser should support all of Solidity 0.6, with the notable exception of inline assembly (may be added in a future release).

Example contract

Here is an example of a very simple contract that stores an integer value and allows the contract’s owner to add an arbitrary value to this value, and any other contract to read this value:

pragma solidity >=0.6.0 <0.7.0;

contract C {

    address owner;
    int x;

    constructor() public {
        owner = msg.sender;
        x = 0;
    }

    function add(int d) public {
        require(msg.sender == owner);
        x += amount;
    }

    function read() public view returns(int) {
        return x;
    }

}

Parser Usage

Executable

Our parser comes with a small executable that demonstrates the library usage. Simply run:

./solp contract.sol

This will parse the file contract.sol and reprint it on the terminal.

Library

To use our parser as a library, add it to your program’s dependencies and use the following function:

Solidity_parser.parse_contract_file : string -> Solidity_parser.Solidity_types.module_

It takes a filename and returns a Solidity AST.

If you wish to print this AST, you may turn it into its string representation by sending it to the following function:

Solidity_parser.Printer.string_of_code : Solidity_parser.Solidity_types.module_ -> string

Conclusion

Of course, all of this is Work In Progress, but we are quite happy to share it with the OCaml community. We think there is a tremendous work to be done around blockchains for experts in formal methods. Do not hesitate to contact us if you want to use this library!

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 etc. and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch with Jane Street. 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 provide consulting and 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.

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committin…

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committing to any foundational features like function types or propositions. All MMT algorithms are parametric in a set of rules, which are self-contained objects plugged in by the language designer. That results in a framework general enough to develop many formal systems including other logical frameworks in it, enabling the rapidly prototyping of new language features.

Despite this high level of generality, it is possible to develop sophisticated results in MMT. The current release includes, e.g., parsing, type reconstruction, module system, IDE-style editor, and interactive library browser. MMT is systematically designed to be extensible, providing multiple APIs and plugin interfaces, and thus provides a versatile infrastructure for system development and integration.

This talk gives an overview of the current state of MMT and its future challenges. Examples are drawn from the LATIN project, a long-running project of building a modular, highly inter-related suite of formalizations of logics and related formal systems.

The video recording of the talk.

The spring schedule of talks is planned as follows:

• May 28, 2020: Brigitte Pientka - Beluga
• June 4, 2020: Jon Sterling - redtt (to be confirmed)
• June 11, 2020: Conor McBride - Epigram 2
• June 25, 2020: William J. Bowman, Cur
• July 2, 2020: Anders Mörtberg - Cubical Agda

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start Web / Android / iOS

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start

New release: Ocsigen Start 2.18

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or as a basis for your app.

Last features include:

• Demo of new Ot_tongue widget

See live examples here:

• See an online demo of the default template
• The same, as a mobile app for Android
• Be Sport is based on Ocsigen Start Web / Android / iOS

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

You can also test it on mobile apps:

• Ocsigen Start demo
• Be Sport Android / iOS

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

You can also test it on mobile apps:

• Ocsigen Start demo
• Be Sport Android / iOS

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

Getting the authors of proof assistants to travel to Ljubljana …

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

Getting the authors of proof assistants to travel to Ljubljana and giving talks at our Foundations of mathematics and theoretical computer science seminar has largely become impossible. But luckily research seminars world-wide are rapidly moving online, and so is our Foundations seminar. I am therefore delighted to announce the first "Every proof assistant" seminar:

Arend proof assistant

Time: Thursday, April 30, 2020 from 18:00 to 19:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 965 4439 5816
Speaker: Valery Isaev (JetBrains research) Proof assistant: Arend proof assistant

Abstract: I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with a convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures.

Video recording of the talk is available.

I have a couple more in the pipeline, so follow this blog, the Foundations seminar announcements or my Twitter account @andrejbauer.

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

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr – fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs &…

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

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr – fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

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

Installation instructions (unchanged):

1. From binaries: run

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

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

2. From source, using opam:

   opam update; opam install opam-devel

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

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

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

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

 

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.

We are happy to announce the alpha release of Opam 2.1.0, one year and a half after Opam 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependencies handling (a.k.a. …

We are happy to announce the alpha release of Opam 2.1.0, one year and a half after Opam 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

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

A number of opam packages depend on tools or libraries installed on the system, which are out of the scope of opam itself. Previous versions of opam added a specification format, and opam 2.0 already handled checking the OS and extracting the required system package names.

However, the workflow generally involved letting opam fail once, then installing the dependencies and retrying, or explicitely using the opam-depext plugin, which was invaluable for CI but still incurred extra steps.

With opam 2.1.0, depexts are seamlessly integrated, and you basically won’t have to worry about them ahead of time:

• Before applying its course of actions, opam 2.1.0 checks that external dependencies are present, and will prompt you to install them. You are free to let it do it using sudo, or just run the provided commands yourself.
• It is resilient to depexts getting removed or out of sync.
• Opam 2.1.0 detects packages that depend on stuff that is not available on your OS version, and automatically avoids them.

This is all fully configurable, and can be bypassed without tricky commands when you need it (e.g. when you compiled a dependency yourself).

Dependency locking

To share a project for development, it is often necessary to be able to reproduce the exact same environment and dependencies setting — as opposed to allowing a range of versions as opam encourages you to do for releases.

For some reason, most other package managers call this feature “lock files”. Opam can handle those in the form of [foo.]opam.locked files, and the --locked option.

With 2.1.0, you no longer need a plugin to generate these files: just running opam lock will create them for existing opam files, enforcing the exact version of all dependencies (including locally pinned packages).

If you check-in these files, new users would just have run opam switch create . --locked on a fresh clone to get a local switch ready to build the project.

Pinning sub-directories

This one is completely new: fans of the Monorepo rejoice, opam is now able to handle projects in subtrees of a repository.

• Using opam pin PROJECT_ROOT --subpath SUB_PROJECT, opam will look for PROJECT_ROOT/SUB_PROJECT/foo.opam. This will behave as a pinning to PROJECT_ROOT/SUB_PROJECT, except that the version-control handling is done in PROJECT_ROOT.
• Use opam pin PROJECT_ROOT --recursive to automatically lookup all sub-trees with opam files and pin them.

Opam switches are now defined by invariants

Previous versions of opam defined switches based on base packages, which typically included a compiler, and were immutable. Opam 2.1.0 instead defines them in terms of an invariant, which is a generic dependency formula.

This removes a lot of the rigidity opam switch commands had, with little changes on the existing commands. For example, opam upgrade ocaml commands are now possible; you could also define the invariant as ocaml-system and have its version change along with the version of the OCaml compiler installed system-wide.

Configuring opam from the command-line

The new opam option command allows to configure several options, without requiring manual edition of the configuration files.

For example:

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

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

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

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

   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

This is still a alpha, so a few glitches or regressions are to be expected. Please report them to the bug-tracker. Thanks for trying it out, and hoping you enjoy!

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

 

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.

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

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr - fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs…

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

This new version contains backported small fixes:

• Escape Windows paths on manpages [#4129 @AltGr @rjbou]
• Fix opam installer opam file [#4058 @rjbou]
• Fix various warnings [#4132 @rjbou @AltGr - fix #4100]
• Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou]

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

1. From binaries: run

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

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

2. From source, using opam:

   opam update; opam install opam-devel

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

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

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

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

We are happy to announce a alpha for opam 2.1.0, one year and a half in the making after the release of 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependenci…

We are happy to announce a alpha for opam 2.1.0, one year and a half in the making after the release of 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

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

A number of opam packages depend on tools or libraries installed on the system, which are out of the scope of opam itself. Previous versions of opam added a specification format, and opam 2.0 already handled checking the OS and extracting the required system package names.

However, the workflow generally involved letting opam fail once, then installing the dependencies and retrying, or explicitely using the opam-depext plugin, which was invaluable for CI but still incurred extra steps.

With opam 2.1.0, depexts are seamlessly integrated, and you basically won't have to worry about them ahead of time:

• Before applying its course of actions, opam 2.1.0 checks that external dependencies are present, and will prompt you to install them. You are free to let it do it using sudo, or just run the provided commands yourself.
• It is resilient to depexts getting removed or out of sync.
• Opam 2.1.0 detects packages that depend on stuff that is not available on your OS version, and automatically avoids them.

This is all fully configurable, and can be bypassed without tricky commands when you need it (e.g. when you compiled a dependency yourself).

Dependency locking

To share a project for development, it is often necessary to be able to reproduce the exact same environment and dependencies setting — as opposed to allowing a range of versions as opam encourages you to do for releases.

For some reason, most other package managers call this feature "lock files". Opam can handle those in the form of [foo.]opam.locked files, and the --locked option.

With 2.1.0, you no longer need a plugin to generate these files: just running opam lock will create them for existing opam files, enforcing the exact version of all dependencies (including locally pinned packages).

If you check-in these files, new users would just have run opam switch create . --locked on a fresh clone to get a local switch ready to build the project.

Pinning sub-directories

This one is completely new: fans of the Monorepo rejoice, opam is now able to handle projects in subtrees of a repository.

• Using opam pin PROJECT_ROOT --subpath SUB_PROJECT, opam will look for PROJECT_ROOT/SUB_PROJECT/foo.opam. This will behave as a pinning to PROJECT_ROOT/SUB_PROJECT, except that the version-control handling is done in PROJECT_ROOT.
• Use opam pin PROJECT_ROOT --recursive to automatically lookup all sub-trees with opam files and pin them.

Opam switches are now defined by invariants

Previous versions of opam defined switches based on base packages, which typically included a compiler, and were immutable. Opam 2.1.0 instead defines them in terms of an invariant, which is a generic dependency formula.

This removes a lot of the rigidity opam switch commands had, with little changes on the existing commands. For example, opam upgrade ocaml commands are now possible; you could also define the invariant as ocaml-system and have its version change along with the version of the OCaml compiler installed system-wide.

Configuring opam from the command-line

The new opam option command allows to configure several options, without requiring manual edition of the configuration files.

For example:

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

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

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

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

   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

This is still a alpha, so a few glitches or regressions are to be expected. Please report them to the bug-tracker. Thanks for trying it out, and hoping you enjoy!

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

The Garbage Collector probably is OCaml’s greatest unsung hero. Its pragmatic approach allows us to allocate without much fear of efficiency loss. In a way, the fact that most OCaml hackers know little about it is a good sign: you want a runtime to gracefully do its job without having to mind it all the time.

But as OCaml 4.10.0 has now hit the shelves, a very exciting feature is in the changelog:

- #8809, #9292: Add a best-fit allocator for the major heap; still
experimental, it should be…

The Garbage Collector probably is OCaml’s greatest unsung hero. Its pragmatic approach allows us to allocate without much fear of efficiency loss. In a way, the fact that most OCaml hackers know little about it is a good sign: you want a runtime to gracefully do its job without having to mind it all the time.

But as OCaml 4.10.0 has now hit the shelves, a very exciting feature is in the changelog:

- #8809, #9292: Add a best-fit allocator for the major heap; still
experimental, it should be much better than current allocation
policies (first-fit and next-fit) for programs with large heaps,
reducing both GC cost and memory usage.
This new best-fit is not (yet) the default; set it explicitly with
OCAMLRUNPARAM="a=2" (or Gc.set from the program). You may also want
to increase the `space_overhead` parameter of the GC (a percentage,
80 by default), for example OCAMLRUNPARAM="o=85", for optimal
speed.
(Damien Doligez, review by Stephen Dolan, Jacques-Henri Jourdan,
Xavier Leroy, Leo White)

At OCamlPro, some of the tools that we develop, such as the package manager Opam, the Alt-Ergo SMT solver or the Flambda optimizer, can be quite demanding in memory usage, so we were curious to better understand the properties of this new allocator.

Minor heap and Major heap: the GC in a nutshell

Not all values are allocated equal. Some will only be useful for the span of local calculations, some will last as long as the program lives. To handle those two kinds of values, the runtime uses a Generational Garbage Collector with two spaces:

• The minor heap uses the Stop-and-copy principle. It is fast but has to stop the computation to perform a full iteration.
• The major heap uses the Mark-and-sweep principle. It has the perk of being incremental and behaves better for long-lived data.

Allocation in the minor heap is straightforward and efficient: values are stored sequentially, and when there is no space anymore, space is emptied, surviving values get allocated in the major heap while dead values are just forgotten for free. However, the major heap is a bit more tricky, since we will have random allocations and deallocations that will eventually produce a scattered memory. This is called fragmentation, and this means that you’re using more memory than necessary. Thankfully, the GC has two strategies to counter that problem:

• Compaction: a heavyweight reallocation of everything that will remove those holes in our heap. OCaml’s compactor is cleverly written to work in constant space, and would be worth its own specific article!
• Free-list Allocation: allocating the newly coming data in the holes (the free-list) in memory, de-scattering it in the process.

Of course, asking the GC to be smarter about how it allocates data makes the GC slower. Coding a good GC is a subtle art: you need to have something smart enough to avoid fragmentation but simple enough to run as fast as possible.

Where and how to allocate: the 3 strategies

OCaml used to propose 2 free-list allocation strategies: next-fit, the default, and first-fit. Version 4.10 of OCaml introduces the new best-fit strategy. Let’s compare them:

Next-fit, the original and remaining champion

OCaml’s original (and default) “next-fit” allocating strategy is pretty simple:

1. Keep a (circular) list of every hole in memory ordered by increasing addresses;
2. Have a pointer on an element of that list;
3. When an allocation is needed, if the currently pointed-at hole is big enough, allocate in it;
4. Otherwise, try the next hole and so-on.

This strategy is extremely efficient, but a big hole might be fragmented with very small data while small holes stay unused. In some cases, the GC would trigger costly compactions that would have been avoidable.

First-fit, the unsuccessful contender

To counteract that problem, the “first-fit” strategy was implemented in 2008 (OCaml 3.11.0):

• Same idea as next-fit, but with an extra allocation table.
• Put the pointer back at the beginning of the list for each allocation.
• Use the allocation table to skip some parts of the list.

Unfortunately, that strategy is slower than the previous one. This is an example of making the GC smarter ends up making it slower. It does, however, reduce fragmentation. It was still useful to have this strategy at hand for the case where compaction would be too costly (on a 100Gb heap, for instance). An application that requires low latency might want to disable compaction and use that strategy.

Best-fit: a new challenger enters!

This leads us to the brand new “best-fit” strategy. This strategy is actually composite and will have different behaviors depending on the size of the data you’re trying to allocate.

• On small data (up to 32 words), segregated free lists will allow allocation in (mostly) constant time.
• On big data, a general best-fit allocator based on splay trees.

This allows for the best of the two worlds, as you can easily allocate your numerous small blocks in the small holes in your memory while you take a bit more time to select a good place for your big arrays.

How will best-fit fare? Let’s find out!

Try it!

First, let us remind you that this is still an experimental feature, which from the OCaml development team means “We’ve tested it thoroughly on different systems, but only for months and not on a scale as large as the whole OCaml ecosystem”.

That being said, we’d advise you don’t use it in production code yet.

Why you should try it

Making benchmarks of this new strategy could be beneficial for you and the language at large: the dev team is hoping for feedback, the more quality feedback you give means the more the future GC will be tuned for your needs.

In 2008, the first-fit strategy was released with the hope of improving memory usage by reducing fragmentation. However, the lack of feedback meant that the developers were not aware that it didn’t meet the users’ needs. If more feedback had been given, it’s possible that work on improving the strategy or on better strategies would have happened sooner.

Choosing the allocator strategy

Now, there are two ways to control the GC behavior: through the code or through environment variables.

First method: Adding instructions in your code

This method should be used by those of us who have code that already does some GC fine-tuning. As early as possible in your program, you want to execute the following lines:

let () =
Gc.(set
  { (get()) with
    allocation_policy = 2; (* Use the best-fit strategy *)
    space_overhead = 100; (* Let the major GC work a bit less since it's more efficient *)
  })

You might also want to add verbose = 0x400; or verbose = 0x404; in order to get some GC debug information. See here for more details on how to use the GC module.

Of course, you’ll need to recompile your code, and this will apply only after the runtime has initialized itself, triggering a compaction in the process. Also, since you might want to easily switch between different allocation policies and overhead specifications, we suggest you use the second method.

Second method: setting $OCAMLRUNPARAM

At OCamlPro, we develop and maintain a program that any OCaml developer should want to run smoothly. It’s called Opam, maybe you’ve heard of it? Though most commands take a few seconds, some administrative-heavy commands can be a strain on our computer. In other words: those are perfect for a benchmark.

Here’s what we did to benchmark Opam:

$ opam update
$ opam switch create 4.10.0
$ opam install opam-devel # or build your own code
$ export OCAMLRUNPARAM='b=1,a=2,o=100,v=0x404'
$ cd my/local/opam-repository
$ perf stat ~/.opam/4.10.0/lib/opam-devel/opam admin check --installability # requires right to execute perf, time can do the trick

If you want to compile and run your own benchmarks, here are a few details on OCAMLRUNPARAM:

• b=1 means “print the backtrace in case of uncaught exception”
• a=2 means “use best-fit” (default is 0, first-fit is 1)
• o=100 means “do less work” (default is 80, lower means more work)
• v=0x404 means “have the gc be verbose” (0x400 is “print statistics at exit”, 0x4 is “print when changing heap size”)

See the manual for more details on OCAMLRUNPARAM

You might want to compare how your code fares on all three different GC strategies (and fiddle a bit with the overhead to find your best configuration).

Our results on opam

Our contribution in this article is to benchmark opam with the different allocation strategies:

A quick word on these results. Most of opam‘s calculations are done by dose and rely heavily on small interconnected blocks. We don’t really have big chunks of data we want to allocate, so the strategy won’t give us the bonus you might have as it perfectly falls into the best-case scenario of the next-fit strategy. As a matter of fact, for every strategy, we didn’t have a single GC compaction happen. However, Best-fit still allows for a lower memory footprint!

Conclusions

If your software is highly reliant on memory usage, you should definitely try the new Best-fit strategy and stay tuned on its future development. If your software requires good performance, knowing if your performances are better with Best-fit (and giving feedback on those) might help you in the long run.

The different strategies are:

• Next-fit: generally good and fast, but has very bad worst cases with big heaps.
• First fit: mainly useful for very big heaps that must avoid compaction as much as possible.
• Best-fit: almost the best of both worlds, with a small performance hit for programs that fit well with next-fit.

Remember that whatever works best for you, it’s still better than having to malloc and free by hand. Happy allocating!

About OCamlPro

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users harness the OCaml state-of-the art programming language.

We design, create and implement custom ad-hoc software for our clients in state-of-the-art languages (OCaml, Rust…). We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam and ocp-indent, 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 reach out by email: contact@ocamlpro.com.

I just finished coding up another webapp in OCaml. I thought it would be cool to publish the sources of a small, completely self-contained app. It’s a sliding tile puzzle coded entirely in OCaml, using a few of the BuckleScript extensions. There are no dependencies on any frameworks or the like aside from the Js modules of BuckleScript. The app itself consists of just one JavaScript file—no images, nothing else.

You can try out the puzzle or get the sources a…

I just finished coding up another webapp in OCaml. I thought it would be cool to publish the sources of a small, completely self-contained app. It’s a sliding tile puzzle coded entirely in OCaml, using a few of the BuckleScript extensions. There are no dependencies on any frameworks or the like aside from the Js modules of BuckleScript. The app itself consists of just one JavaScript file—no images, nothing else.

You can try out the puzzle or get the sources at the Slide24 page.

I also tried to make a clean DOM interface based on experience with the Cassino and Schnapsen apps. I think it came out well, at least for these self-contained webapps.

The idea for the DOM interface is that it should expose only abstract types, but that there should be a subtype relation based on the JavaScript DOM. It turns out that you can do this pretty easily using private declarations. Types for contents of a document look like this:

type node
type text = private node
type element = private node
type canvas = private element
type box = private element
type div = private box
type span = private box
type button = private box

So, the interface reveals nothing whatsoever about the types except that they participate in a subtype relation. text and element are subtypes of node, canvas is a subtype of element, and so on. node is the supertype of all the document content types.

What this means is that you can pass a canvas or a button to a function that expects an element, and so on. I don’t find the necessity to use explicit supertype coercion to be too much trouble when working with non-parameterized types.

let style = Pseldom.(element_style (mybutton :> element)) in
. . .

It seems to me this captures pretty much everything that I want from the object-oriented approach without the usual complicated baggage. I think inheritance is more often a hindrance than a help. It’s too dependent on implementation details, and is associated with too many informal (unenforceable) descriptions of how to write subclasses of each class without messing up the semantics.

I’ve never used private declarations before, but they seem to have created exactly the structure I was hoping for.

Posted by: Jeffrey

We are happy to announce that our venerable “Try Ocaml” service is being retired and replaced by a new, modern version based upon our work on Learn-OCaml.

→ Try it here ←

The new interface provides an editor panel besides the familiar top-level, error and warning positions highlighting, the latest OCaml release (4.10.0), local storage of your session, and more.

The service is still in beta, so it would be helpful if you could tell us about any hiccups you may encounter on the Dis…

We are happy to announce that our venerable “Try Ocaml” service is being retired and replaced by a new, modern version based upon our work on Learn-OCaml.

→ Try it here ←

The new interface provides an editor panel besides the familiar top-level, error and warning positions highlighting, the latest OCaml release (4.10.0), local storage of your session, and more.

The service is still in beta, so it would be helpful if you could tell us about any hiccups you may encounter on the Discuss thread.

Let’s read the testimony of Sylvain Conchon about our new version of TryOCaml:

“Try OCaml saved our lives in Paris Saclay in these times of social distancing. I teach functional programming with OCaml to my Y2 Bachelor’s Degree students. With the quarantine in place, we weren’t able to host the practical assignment in the machine room as usual, so we decided the students would do the exam at home. However, many of our students use Windows on which setting up OCaml is a hassle, or otherwise encountered problems while setting up the OCaml environment. We invited our students to use try-ocaml instead! Many have and the exam went really smoothly.”

The second annual meeting of the Alt-Ergo Users’ Club was held in mid-February. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements.

Alt-Ergo is an automatic mathematical formula checker, jointly developed by LRI and OCamlPro (since 2014). For more information or to join the club, visit https://alt-ergo.ocamlpro.com.

The second annual meeting of the Alt-Ergo Users’ Club was held in mid-February. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements.

Alt-Ergo is an automatic mathematical formula checker, jointly developed by LRI and OCamlPro (since 2014). For more information or to join the club, visit https://alt-ergo.ocamlpro.com.

Our club has several goals, the first of which is to ensure the sustainability of Alt-Ergo by fostering collaboration among club members and strengthening collaboration with formal method communities such as Why3. One of our priorities is to increase our user community by extending our tool to new sectors such as Model Checking. Participation in international competitions is also a way to gain visibility. Finally, the last objective of the club is to find new projects or contracts for the development of long-term functionalities.

We thank all our members for their support and bid a warm welcome Mitsubishi Electric R&D Centre Europe as they join AdaCore and the CEA list as a member of the club this year. We would also like to highlight the Why3 development team with whom we are working to improve our tools.

Our members are particularly interested in:

• Better generation of models and counter-examples.
• The addition of sequence theory.
• The improvement of non-linear arithmetic support in Alt-Ergo.

These features are now top priorities for us. For more information, you can read our articles on this blog.

Something like ten years ago we produced two iOS card game apps written in OCaml, partly as a proof of concept for compiling OCaml to iOS and partly because we enjoy card games. Unfortunately we weren’t able to spark a worldwide craze for writing iOS apps in OCaml or for playing Schnapsen, as we had hoped. Consequently there was very little financial return and we all had to move on to other projects.

Both apps play a very good two-player card game. The apps are essenti…

Something like ten years ago we produced two iOS card game apps written in OCaml, partly as a proof of concept for compiling OCaml to iOS and partly because we enjoy card games. Unfortunately we weren’t able to spark a worldwide craze for writing iOS apps in OCaml or for playing Schnapsen, as we had hoped. Consequently there was very little financial return and we all had to move on to other projects.

Both apps play a very good two-player card game. The apps are essentially a kind of solitaire where you play against the app as your opponent. The games are:

• Cassino, a classic fishing game said without substantiation to be of Italian origin (per Wikipedia).

• Schnapsen, a kind of miniature Pinochle very popular in the territories of the former Austro-Hungarian Empire (again per Wikipedia).

The Schnapsen app also plays a closely related game called Sixty-Six, named after this number in many different languages.

The images and layout algorithms for the apps quickly fell behind the formats and display capabilities of later iOS devices, so I was thinking we might just as well release the apps as is, for free. However there is a lot of rigamarole (and some cost) associated with the App Store if all you want to do is release some free apps.

Cassino

Master Schnapsen/66

Recently I wondered if it wouldn’t be possible to revive the apps in a browser environment. These days you can compile OCaml to JavaScript using BuckleScript or Js_of_ocaml. The HTML 5 canvas element has an interface a lot like the two-dimensional graphics used by the apps. It seems like it should be possible.

So, in fact, that’s what I did. I ported the two card game apps to run as webapps. Visually they run in a smallish rectangle exactly the size of the original iPhone screen. I was able to retain the iPhone behavior almost unchanged. Computationally they run completely in the browser, and make no further contact with psellos.com (unless you want to access the game pages at psellos.com).

The OCaml code is compiled to JavaScript using the BuckleScript compiler. Because the target language is JavaScript, there’s no need for any stubs or supporting code (as there was in iOS). All of the code for the apps is in OCaml.

Once the basic graphics primitives were in place, a lot of the code worked without any change. The part of the code that actually plays the game (the “engine”) didn’t change at all.

As an unexpected and very welcome side effect, two of the old iOS app team members got interested in the project again. They’re working on making the Schnapsen app into an even better player. I added some extra features to the Schnapsen GUI to make it easier to keep track of what’s happened in a hand.

Neither of the webapps is quite finished yet. But they both are already playable and in fact quite enjoyable. You can try them by clicking on the icons above. You can also read about the apps and the games they play on their own separate pages.

• Cassino Page
• Schnapsen Page

If you have any comments, suggestions, or encouragement, leave them below or email me at jeffsco@psellos.com.

Posted by: Jeffrey

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

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

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

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

Flambda & Compilation Team

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

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

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

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

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

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

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

Encouraging OCaml adoption

OCaml Expert trainings for professional programmers

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

The “Expert” OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write “compiler-optimizable” code. These sessions are also an opportunity to come discuss with our OPAM & Flambda lead developers and core contributors in Paris.

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

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