OCamlPro Highlights, Sept-Oct 2013

Authors: Çagdas Bozman
Date: 2013-11-01
Category: OCamlPro
Tags: highlights



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:

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:

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