2020_02_04_2019_at_ocamlpro.md 16.2 KB
Newer Older
1
title=2019 at OCamlPro
Dario Pinto's avatar
Dario Pinto committed
2
authors=Muriel,OCamlPro
3 4 5 6 7
date=2019-02-04
category=OCamlPro
tags=compiler,cheat sheet,OCamlPro,opam,Rust,Try-OCaml,OCaml,Alt-Ergo,blockchains,Flambda2

![2019 at OCamlPro](assets/img/logo_ocp_2019.png)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
8 9 10 11 12 13 14

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](#ocaml) ([flambda2](#compilation) & compiler optimisations, [opam](#opam) 2, our [Rust-based](#rust) UI for [memprof](#memthol), tools like tryOCaml, ocp-indent, and supporting the [OCaml Software Foundation](#ocsf)), then in the world of [formal methods](#formalmethods) (new versions of our SMT Solver [Alt-Ergo](#altergo), launch of the [Alt-Ergo Users' Club](#altergoclub), the [Love language](#love), etc.).

## In the World of OCaml

15
![ocaml](assets/img/logo_ocaml.png)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
16 17 18 19 20 21 22 23 24 25 26

### 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](https://github.com/ocaml/RFCs/pull/11) for OCaml (a [similar idea](https://github.com/ocaml/ocaml/issues/5283) was suggested and implemented in 2011 by Fabrice Le Fessant).
* The implementation is available on GitHub for both [functorized packs](https://github.com/OCamlPro-Couderc/ocaml/tree/functorized-packs) and [recursive packs](https://github.com/OCamlPro-Couderc/ocaml/tree/recursive-units+pack-cleanup). 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.
27
* See also Vincent's [OCamlPro’s compiler team work update](https://ocamlpro.com/2019/08/30/ocamlpros-compiler-team-work-update/) of August 2019.
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
28 29 30 31 32 33 34 35 36 37 38 39 40

*This work is allowed thanks to Jane Street's funding.*

### Work on a formalized type system for OCaml

*Work of Pierrick Couderc*

At the end of 2018, Pierrick defended his PhD on "[Checking type inference results of the OCaml language](https://pastel.archives-ouvertes.fr/tel-02100717/)", leading to a formalized type systems and semantics for a large subset of OCaml, or at least its unique typed intermediate language: the Typedtree. This work led us to work on new aspects of the OCaml compiler as recursive and functorized packs described earlier, and we hope this proves useful in the future for the evolution of the language.

### The OPAM package manager

*Work of Raja Boujbel and Louis Gesbert*

41
![opam](assets/img/logo_opam_300_261.png)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
42

43
[OPAM](https://opam.ocaml.org) is maintained and developed at OCamlPro by Louis and Raja. Thanks to their thorough efforts the opam 2.1 first release candidate is soon to be published!
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
44 45 46 47 48 49 50 51 52

Back in 2018, the long-awaited opam 2.0 version was finally released. It embedded many changes, in opam itself as well as for the community. The opam file format was redefined to simplify and add new features. With the close collaboration of OCamlLabs and opam repository maintainers, we were able to manage a smooth transition of the repository and whole ecosystem from opam 1.2 format to the new – and richer – opam 2.0 format. Other emblematic features are e.g. for practically integrated mccs solver, sandboxing builds, for security issues (we care about your filesystem!), for usability reworking of the pin' command, etc.

While the 2.1.0 version is in preparation, the 2.0.0 version is still updated with minor releases to fix issues. The lastest 2.0.6 release is fresh from January.

In the meantime, we continued to improve opam by integrating some opam plugins (opam lock, opam depext), recursively discover opam files in the file tree when pinning, new definition of a switch compiler, the possibility to use z3 backend instead of mccs, etc.

All these new features – among others – will be integrated in the 2.1.0 release, that is betaplanned for February. The best is yet to come!

53
* More details: on [https://opam.ocaml.org](https://opam.ocaml.org)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
54 55 56 57 58 59 60 61
* Releases on Releases on [https://github.com/ocaml/opam/releases](https://github.com/ocaml/opam/releases) & [our blog](https://opam.ocaml.org/blog/opam-2-0-6/)

*This work is allowed thanks to Jane Street's funding.*

### Encouraging OCaml adoption

#### OCaml Expert trainings for professional programmers

62
We proposed in 2019 some [OCaml expert training](https://ocamlpro.com/course-ocaml-expert/) specially designed for developers who want to use advanced features and master all the open-source tools and libraries of OCaml.
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
63 64 65

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

66
Next session: 3-4 March 2020, Paris [(registration)](https://ocamlpro.com/forms/preinscriptions-formation-ocaml/)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
67 68 69 70 71

#### Our cheat-sheets on OCaml, the stdlib and opam

*Work of Thomas Blanc, Raja Boujbel and Louis Gesbert*

72
Thomas announced the release of our up-to-date cheat-sheets for the [OCaml language, standard library](https://ocamlpro.com/2019/09/13/updated-cheat-sheets-ocaml-language-and-ocaml-standard-library/) and [opam](https://ocamlpro.com/wp-content/uploads/2019/11/ocaml-opam.pdf). Our original cheat-sheets were dating back to 2011. This was an opportunity to update them after the [many changes](https://ocamlpro.com/2019/09/13/updated-cheat-sheets-ocaml-language-and-ocaml-standard-library/) in the language, library and ecosystem overall.
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
73 74 75

>Cheat-sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. *They come in handy when your [rubber duck](https://rubberduckdebugging.com/) is rubbish at debugging your code!*

76
More details on [Thomas' blog post](https://ocamlpro.com/2019/09/13/updated-cheat-sheets-ocaml-language-and-ocaml-standard-library/)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
77 78 79 80 81 82 83

#### Open Source Tooling and Web IDEs

And let's not forget the other tools we develop and maintain! We have tools for education such as our interactive editor OCaml-top and [Try-OCaml](https://try.ocamlpro.com/new.html) (from the previous work on the learn-OCaml platform for the OCaml Fun MOOC) which you can use to code in your browser. Developers will appreciate tools like our indentation tool ocp-indent, and ocp-index which gives you easy access to the interface information of installed OCaml libraries for editors like Emacs and Vim.

### Supporting the OCaml Software Foundation

84
OCamlPro was proud to be one of the first supporters of the new Inria's [OCaml Software Foundation.](https://ocaml-sf.org/) We keep committed to the adoption of OCaml as an industrial language:
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
85 86 87

>"[…] As a long-standing supporter of the OCaml language, we have always been committed to helping spread OCaml's adoption and increase the accessibility of OCaml to beginners and students. […] We value close and friendly collaboration with the main actors of the OCaml community, and are proud to be contributing to the OCaml language and tooling." (August 2019, Advisory Board of the OCSF, ICFP Berlin)

88
More information on the [OCaml Software Foundation](https://ocaml-sf.org/)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
89 90 91 92 93 94 95 96 97

## In the World of Formal Methods

*By Mohamed Iguernlala, Albin Coquereau, Guillaume Bury*

In 2018, we welcomed five new engineers with a background in formal methods. They consolidate the department of formal methods at OCamlPro, in particular help develop and maintain our SMT solver Alt-Ergo.

### Release of Alt-Ergo 2.3.0, and version 2.0.0 (free)

98
After the release of [Alt-Ergo 2.2.0](https://ocamlpro.com/2018/04/23/release-of-alt-ergo-2-2-0/) (with a new front-end that supports the SMT-LIB 2 language, extended prenex polymorphism, implemented as a standalone library) came the version 2.3.0 in 2019 with new features : dune support, ADT / algebraic datatypes, improvement of the if-then-else and let-in support, improvement of the data types.
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
99 100 101

* More information on the [Alt-Ergo SMT Solver](https://alt-ergo.ocamlpro.com/)
* Albin Coquereau defended his PhD thesis in Decembre 2019 "Improving performance of the SMT solver Alt-Ergo with a better integration of efficient SAT solver"
102
* We participated in the SMT-COMP 2019 during the 22nd SAT conference. The results of the competition are detailed [here.](https://ocamlpro.com/2019/07/09/alt-ergo-participation-to-the-smt-comp-2019/)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
103 104 105 106 107

### The launch of the Alt-Ergo Users' Club

Getting closer to our users, gathering industrial and academic supporters, collecting their needs into the Alt-Ergo roadmap is key to Alt-Ergo's development and sustainability.

108
The [Alt-Ergo Users' Club](https://alt-ergo.ocamlpro.com/#club) was officially launched beginning of 2019. The first yearly meeting took place in February 2019. We were happy to welcome our first members [Adacore](https://www.adacore.com), [CEA List](https://www-list.cea.fr/en/), [Trust-In-Soft](https://trust-in-soft.com), and now Mitsubishi MERCE.
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
109 110 111

More information on the [Alt-Ergo Users' Club](https://alt-ergo.ocamlpro.com/#club)

112
![Love-language](assets/img/logo_love_couleur.png)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127

## Harnessing our language-design expertise: Love

*Work by David Declerck & Steven de Oliveira*

Following the launch of Dune network, the Love language for smart-contracts was born from the collaboration of OCamlPro and Origin Labs. This new language, whose syntax is inspired from OCaml and Liquidity, is an alternative to the Dune native smart contract language Michelson. Love is based on system-F, a type system requiring no type inference and allowing polymorphism. The language has successfully been integrated on the network and the first smart contracts are being written.

[LOVE: a New Smart Contract Language for the Dune Network](https://medium.com/dune-network/love-a-new-smart-contract-language-for-the-dune-network-a217ab2255be)
[The Love Smart Contract Language: Introduction & Key Features — Part I](https://medium.com/dune-network/the-love-smart-contract-language-introduction-key-features-part-i-949d8a4e73c3)


## Rust-related activities

The OCaml & Rust combo *should* be a candidate for any ambitious software project!

128 129 130
* A Rust-based UI for memprof: we started in 2019 to work in collaboration with the memprof developer team on a Rust based UI for memprof. See Pierre and Albin's exposé at the [JFLA2020](https://jfla.inria.fr/jfla2020.html)'s "Gardez votre mémoire fraiche avec Memthol" (Pierre Chambart , Albin Coquereau and Jacques-Henri Jourdan)
* [Rust training](https://ocamlpro.com/rust-vocational-training/) : *Rust borrows heavily from functional programming languages to provide very expressive abstraction mechanisms. Because it is a systems language, these mechanisms are almost always zero-cost. For instance, polymorphic code has no runtime cost compared to a monomorphic version.This concern for efficiency also means that Rust lets developers keep a very high level of control and freedom for optimizations. Rust has no Garbage Collection or any form of runtime memory inspection to decide when to free, allocate or re-use memory. But because manual memory management is almost universally regarded as dangerous, or at least very difficult to maintain, the Rust compiler has a borrow-checker which is responsible for i) proving that the input program is memory-safe (and thread-safe), and ii) generating a safe and “optimal” allocation/deallocation strategy. All of this is done at compile-time.*
* Next sessions: April 20-24th 2020 [(registration)](https://ocamlpro.com/forms/preinscriptions-formation-ocaml/)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
131 132 133 134 135 136 137 138

## OCamlPro around the world

OCamlPro's team members attended many events throughout the world:

* [ICFP 2019](https://icfp19.sigplan.org/) (Berlin)
* The [JFLA’2019](https://dpt-info.u-strasbg.fr/~magaud/JFLA2019/lieu.html) (Les Rousses, Haut-Jura)
* The[ POSS'2019 ](https://www.opensourcesummit.paris/)(Paris)
139
* [MirageOS Retreat](https://retreat.mirage.io/) (Marrakech)
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
140 141 142 143 144 145 146 147 148

As a committed member of the OCaml ecosystem's animation, we've organized OCaml meetups too (see the famous [OUPS](https://www.meetup.com/fr-FR/ocaml-paris/) meetups in Paris!).

Now let's jump into the new year 2020, with a team keeping expanding, and new projects ahead: keep posted!

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

Many people ask us about what happened in 2018! That was an incredibly active year on blockchain-related achievements, and at that time we were hoping to attract clients that would be interested in our blockchain expertise.

149
But that is [history](https://ocamlpro.com/wp-content/uploads/2020/01/Flyer_Blockchains_OSIS2017ok.pdf) now! Still interested? Check the [Origin Labs](https://www.origin-labs.com/) team and their partner [The Garage](https://www.thegara.ge/) on [Dune Network](https://dune.network)!
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
150

151
For the [record](https://ocamlpro.com/2019/04/29/blockchains-at-ocamlpro-an-overview/):
Muriel Shan Sei Fan's avatar
Muriel Shan Sei Fan committed
152 153

* (April 2019) We had started Techelson: a testing framework for Michelson and Liquidity
154 155
* (Nov 2018) [An Introduction to Tezos RPCs: Signing Operations](https://ocamlpro.com/2018/11/21/an-introduction-to-tezos-rpcs-signing-operations/) / [An Introduction to Tezos RPCs: a Basic Wallet](https://ocamlpro.com/2018/11/15/an-introduction-to-tezos-rpcs-a-basic-wallet/) / [Liquidity Tutorial: A Game with an Oracle for Random Numbers](https://ocamlpro.com/2018/11/06/liquidity-tutorial-a-game-with-an-oracle-for-random-numbers/) / [First Open-Source Release of TzScan](https://ocamlpro.com/2018/11/08/first-open-source-release-of-tzscan/)
* (Oct 2018) [OCamlPro’s TZScan grant proposal accepted by the Tezos Foundation – joint press release ](https://ocamlpro.com/2018/10/17/ocamlpros-tzscan-grant-proposal-accepted-by-the-tezos-foundation-joint-press-release/)
156
* (Jul 2018) [OCamlPro’s Tezos block explorer TzScan’s last updates](/blog/2018_07_20_new_updates_on_tzscan_2)
157 158
* (Feb 2018) [Release of a first version of TzScan.io, a Tezos block explorer](https://ocamlpro.com/2018/02/14/release-of-a-first-version-of-tzscan-io-a-tezos-block-explorer/) / [OCamlPro’s Liquidity-lang demo at JFLA2018 – a smart-contract design language](https://ocamlpro.com/2018/11/06/liquidity-tutorial-a-game-with-an-oracle-for-random-numbers/) . We were developing [Liquidity](https://www.liquidity-lang.org/), a high level smart contract language, human-readable, purely functional, statically-typed, which syntax was very close to the OCaml syntax.
* To garner interest and adoption, we also developed the online editor [Try Liquidity](https://www.liquidity-lang.org/edit). Smart-contract developers could design contracts interactively, directly in the browser, compile them to Michelson, run them and deploy them on the alphanet network of Tezos. Future plans included a full-fledged web-based IDE for Liquidity. Worth mentioning was a neat feature: decompiling a Michelson program back to its Liquidity version, whether it was generated from Liquidity code or not.