OCamlPro Highlights, Sept-Oct 2013

---

Here is a short report of our activities in September-October 2013.

OCamlPro at OCaml’2013 in Boston

We were very happy to participate to OCaml’2013, in Boston. The event was a great success, with a lot of interesting talks and many participants. It was a nice opportunity for us to present some of our recent work:

• Fabrice presented his work on the design of the wxOCaml library. Although the wxOCaml library itself is an interesting project, the goal of his talk was to show that binding thousands of functions from a C++ library can be automated very easily in OCaml, and make the bindings easy to maintain and to improve.
• The work of Thomas and Louis on OPAM was presented in a talk by Anil on the OCaml Platform v0.1. The OCaml Platform is a set of tools, including OPAM, to provide an ever increasing set of packages for OCaml developers, including high-quality documentation and broad portability. Some statistics showed how OPAM, in less than a year, grew from 200 packages to more than 1400 packages, and from 2-3 contributors to about 130 contributors in September. Another talk, Ocamlot: OCaml Online Testing presented how sets of packages will now be automatically tested, to give immediate feedback to contributors, and an evaluation of packages quality to users.
• Pierre presented his work on Improving OCaml high level optimisations that he also presented in a recent blog post.
• Grégoire presented his work with Jacques Garrigue on Runtime types in OCaml. In particular, he showed how abstraction is hard to deal with, as there is a dilemma between the ability to write powerful polytipic functions and the preservation of the abstraction wanted by the developer for code modularity.
• Finally, Çagdas presented his work on Profiling the Memory Usage of OCaml Applications without Changing their Behavior. This new profiler will be able to provide precise memory information on production OCaml software, by snapshoting the memory and recovering type information. It is currently being tested on several projects, such as the Why3 verification tool.

Of course, the day was full of interesting talks, and we can only advise to see all of them on the complete program that is now online.

CUFP’2013 Program was also very dense. For OCaml users, Dave Thomas, first keynote, reminded us how important it is to build two-way bridges between OCaml and other languages: we have the bad habit to only build one-way bridges to just use other languages from OCaml, and forget that new users will have to start by using small OCaml components from their existing software written in another language. Then, Julien Verlaguet presented the use of OCaml at Facebook to type-check and compile a typed version of PhP, HipHop, that is now used for a large part of the code at Facebook.

Software Projects

The period of September-October was also very busy trying to find some funding for our projects. Fortunately, we still managed to make a lot of progress in the development of these projects:

OPAM

Lots has been going on regarding OPAM, as the 1.1 release is being pushed forward, with a beta and a RC available already. This release focuses on stability improvements and bug-fixes, but is nonetheless a large step from 1.0, with an enhanced update mechanism, extended metadata, an enhanced ‘pin’ workflow for developers, and much more.

We are delighted by the success met by OPAM, which was mentioned again and again at the OCaml’2013 workshop, where we got a warming lot of positive feedback. To be sure that this belongs to the community, after licensing all metadata of the repository under CC0 (as close to public domain as legally possible), we have worked hand in hand with OCamlLabs to migrate it to opam.ocaml.org. External repositories for Windows, Android and so on are appearing, which is a really good thing, too.

The Alt-Ergo SMT Solver

In September, we officially announced the distribution and the support of Alt-Ergo by OCamlPro and launched its new website. This site allows to download public releases and to discover available support offerings. We have also published a new public release (version 0.95.2) of the prover. The main changes in this minor release are: source code reorganization, simplification of quantifier instantiation heuristics, GUI improvement to reduce latency when opening large files, as well as various bug fixes.

During September, we also re-implemented and simplified other parts of Alt-Ergo. In addition, we started the integration of a new SAT-solver based on miniSAT (implemented as a plug-in) and the development of a new tool, called Ctrl-Alt-Ergo, that automates the most interesting strategies of Alt-Ergo. The experiments we made during October are very encouraging as shown by our previous blog post.

Multi-runtime

Luca Saiu completed his work at Inria and on the multi-runtime branch, fixing the last bugs and leaving the code in a shape not too far removed from permitting its eventual integration into the OCaml mainline.

Now, the code has a clean configuration-time facility for disabling the multi-runtime system, and compatibility is restored with architectures not including the required assembly support to at least compile and work using a single runtime. A crucial optimization permits to work in this mode with extremely little overhead with respect to stock OCaml. Testing on an old PowerPC 32-bit machine revealed a few minor portability problems related to word size and endianness.

Compiler optimisations

We have been working on allowing cross module inlining. We wanted to be able to show a version generating strictly better code than the current compiler. This milestone being reached, we are now preparing a patch series for upstreaming the base parts. We are also working on polishing the remaining problems: the passes were written in an as simple as possible way, so compilation time is still a bit high. And there are a few difficulties remaining with cross module inlining and packs.

The INRIA-OCamlPro Lab Team

The team is also evolving, and some of us are now leaving the team to join other projects:

• After two years with us, Thomas Gazagnaire has left OCamlPro in October to work most of his time on Mirage in Cambridge (UK). Thomas was OCamlPro’s first employee, and OCamlPro probably wouldn’t exist without him. Thomas has also been the main architect of OPAM, and was involved in the design of many of our projects. Louis Gesbert will continue his work on developing and maintaining OPAM.
• After one year with us, Luca Saiu has left Inria in October. Luca has made a tremendous work on the implementation of a multicore-OCaml, where every runtime runs in a different memory space with its own garbage collector. We hope to be able to upstream his work soon to the official OCaml distribution.
• After an internship with us, Pierrick Couderc, Souhire Kenawi and David Maison are back to their masters’ studies since September. Souhire worked on testing the development of iOS applications on Linux with OCaml, a very challenging task ! Pierrick and David developed an online editor for OCaml that we are going to release very soon.

This blog post was about departures, but stay connected, next month, we are going to announce some newcomers who decided to join the team for the winter !

---

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

• We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
• We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
• We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
• We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.