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!
Au sujet d'OCamlPro :
OCamlPro développe des applications à haute valeur ajoutée depuis plus de 10 ans, en utilisant les langages les plus avancés, tels que OCaml et Rust, visant aussi bien rapidité de développement que robustesse, et en ciblant les domaines les plus exigeants (méthodes formelles, cybersécurité, systèmes distribués/blockchain, conception de DSLs). Fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique) que pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (OCaml, Rust, Cobol, Python, Scilab, C/C++, etc.) et appliquée à de multiples domaines. Nous dispensons également des [formations sur mesure certifiées Qualiopi sur OCaml, Rust, et les méthodes formelles] (https://training.ocamlpro.com/) Pour nous contacter : contact@ocamlpro.com.
Articles les plus récents
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