OCamlPro Highlights, August 2013
Here is a short report on the different projects we have been working on in August.
News from OCamlPro
Compiler Optimizations
After our reports on better inlining have raised big expectations, we have been working hard on fixing the few remaining bugs. An enhanced alias/constant analysis was added, to provide the information needed to lift some constraints on the maintained invariants, and simplifying some other passes quite a lot in the process. We are now working on reestablishing cross-module inlining, by exporting the new information between compilation units.
Memory Profiling
On the memory profiling front, now that the compiler patch is well tested and quite stable, we started some cleanup to make it more modular, easier to understand and extend. We also worked on improving the performance of the profiler (the tool that analyzes the heap snapshots), by caching some expensive computations, such as extracting type information from ‘cmt’ files associated with each location, in files that are shared between executions. We have started testing the profiler on the Why3 verification platform, and these optimizations proved very useful to analyze longer traces.
OPAM Package Manager
On OPAM, we are still preparing the release of version 1.1. The release date has shifted a little bit — it is now planned to happen mid-September, before the OCaml’2013 meeting — because we are focusing on getting speed and stability improvements in a very good shape. We are now relying on opam-rt, our new regression testing infrastructure, to be sure to get the best level of quality for the release.
Regarding the package and compiler metadata, we are very proud to announce that our community has crossed an important line, with more than 100 contributors and 500 different packages ! In order to ensure that these hours of packaging efforts continue to benefit everyone in the OCaml community in the future, we are (i) clarifying the license for all the metadata in the package repository to use CC0 and (ii) discussing with OCamlLabs and the different stakeholders to migrate all the metadata to the ocaml.org infrastructure.
Simple Build Manager
We also made progress on the design of our simple build-manager for OCaml, ocp-build. The next branch in the GIT repository features a new, much more expressive package description language : ocp-build can now be used to build arbitrary files, for example to generate new source files, or to compile files in other languages than OCaml. We successfully used the new language to build Try-ocaml and wxOCaml, completely avoiding the use of “make”.
It can also automatically generate basic HTML documentation for libraries using ocamldoc with “ocp-build make -doc”. There are still some improvements on our TODO list before an official release, for example improving the support of META files, but we are getting very close ! ocp-build is very efficient: compiling Merlin with ocp-build takes only 4s on a quad-core while ocamlbuild needs 13s in similar conditions and with the same parallelisation settings.
Graphics on Try-OCaml
Try-OCaml has been improved with a dedicated implementation of the Graphics module: type “lesson 19”, and you will get some fun examples, including a simple game by Sylvain Conchon.
Alt-Ergo Theorem Prover
We are also happy to welcome Mohamed Iguernelala in the team, starting at the beginning of September. Mohamed is a great OCaml programmer, and he will be working on the Alt-Ergo theorem prover, an SMT-solver in OCaml developed by Sylvain Conchon, and heavily used in the industry for safety-critical software (aircrafts, trains, etc.).
News from the INRIA-OCamlPro Lab
Multi-runtime OCaml
After thorough testing, the multi-runtime branch is getting stable enough for being submitted upstream. The build system has been fixed to enable the modified OCaml to run, in single-runtime mode, on architectures for which no multi-runtime port exists yet, while maintaining API compatibility with mainline OCaml. Thanks to some clever preprocessor hacks, the performance impact in single-runtime mode will be negligible.
Whole-Program Analysis
Our work on whole program analysis, while still in the early stages, is quickly getting forward, and we managed to generate well-formed graphs representing a whole OCaml program. The tool can be fed sources and .cmt files, and at each point of the program, will compute all of the plausible values every variable can take, plus the calculations that allowed to get those values. We hope to have it ready for testing the detection of uncaught exceptions soon.
Editing OCaml Online
We also made a lot of progress in our Online IDE for OCaml, with code generation within the browser. The prototype is now quite robust, and some tricky bugs with the representation of integers and floats in Javascript have been fixed, so that the generated code is always the same as the one generated by a standalone compiler. Also, the interface now allows the user to have a full hierarchy of files and projects in his workspace. There is still some work to be done on improving the design, but we are very exited with the possibility to develop in OCaml without installing anything on the computer !
Scilab Code Analysis
For the Richelieu project, after testing some type inference analysis on Scilab code in the last months, we have now started to implement a new tool, Scilint, to perform some of this analysis on whole Scilab projects and report warnings on suspect code. We hope this tool will soon be used by every Scilab user, to avoid wasting hours of computation before reaching an easy-to-catch error, such as a misspelled — thus undefined — variable.
Meeting with the Community
Some of us are going to present part of this work at OCaml’2013, the OCaml Users and Developers Workshop in Boston. We expect it to be a good opportunity to get some feedback on these projects from the community!
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.
Most Recent Articles
2024
- opam 2.3.0 release!
- Optimisation de Geneweb, 1er logiciel français de Généalogie depuis près de 30 ans
- Alt-Ergo 2.6 is Out!
- Flambda2 Ep. 3: Speculative Inlining
- opam 2.2.0 release!
- Flambda2 Ep. 2: Loopifying Tail-Recursive Functions
- Fixing and Optimizing the GnuCOBOL Preprocessor
- OCaml Backtraces on Uncaught Exceptions
- Opam 102: Pinning Packages
- Flambda2 Ep. 1: Foundational Design Decisions
- Behind the Scenes of the OCaml Optimising Compiler Flambda2: Introduction and Roadmap
- Lean 4: When Sound Programs become a Choice
- Opam 101: The First Steps
2023
- Maturing Learn-OCaml to version 1.0: Gateway to the OCaml World
- The latest release of Alt-Ergo version 2.5.1 is out, with improved SMT-LIB and bitvector support!
- 2022 at OCamlPro
- Autofonce, GNU Autotests Revisited
- Sub-single-instruction Peano to machine integer conversion
- Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
- Release of ocplib-simplex, version 0.5