Commit a914b2e7 authored by Dario Pinto's avatar Dario Pinto
Browse files

Merge branch 'master' into 'master'

add an article, update, rm duplicate articles

See merge request OCamlPro/www!55
parents 4e74d75d 1b147701
title=An Overview of our Current Activities
authors=Çagdas Bozman
From the early days of OCamlPro, people have been curious about our plans; they were asking how we worked at OCamlPro and what we were doing exactly. Now that we have started releasing projects more regularly, these questions come again. They are very reasonable questions, and have resolved to be more public and communicate more regularly. This post covers our activities from the beginning of 2013 and updates are scheduled on a monthly basis.
## OCamlPro ?
OCamlPro has been created to promote the use of OCaml in the industry. In order to do so, we provide a wide range of services targeted at all stages of typical software projects: we train engineers and we improve the efficiency and usability of the OCaml compiler and tools, we help design new projects, advise on which open-source software components to use and how, we help deliver OCaml software projects and we do custom software development. One extra focus is the increase of the accessibility of OCaml for beginners and students.
Our customers are well-known industrial users such as [Jane-Street](, [Citrix]( and [Lexifi]( but we also help individual developers lost in the wild of non-OCaml environments inter-operate OCaml with other components. We also believe that collaborative R&D projects are a great opportunity to make existing companies discover OCaml and its benefits to their products and we are involved in several of them (see below).
Our engineering team is steadily growing (currently 9 full-time engineers in a joint lab between OCamlPro and INRIA) located in Paris and Nice. We gather a wide range of technical skills and industrial world expertise as we are all coming from major academic and industrial actors such as [INRIA](, [text](Dassaut Systèmes), [MLstate]( and [Citrix]( We also love the OCaml open-source ecosystem: we have been participating to the development of [ocsigen](, [mirage](, [XCP](, [mldonkey](, [marionet]( and so on. By the way, OCamlPro has some open [positions](/jobs) and we are still looking to hire excellent software engineers!
## OCaml Distribution
The first of our technical activities is related to work on the OCaml distribution itself. We are part of the OCaml compiler development team - our INRIA members are part of the [Gallium]( project which develops OCaml at INRIA - and we regularly contribute patches to improve the usability and performance of the compiler itself.
We have recently proposed [a series of patches]( to improve the performance of functions with float arguments and we have started developing a [framework]( to benchmark the efficiency of compiler optimizations.
We are also actively exploring the design-space for concurrency and distribution in OCaml, with an implementation of
- reentrant runtime
- way to instantiate different runtimes in separate system threads in the same process
- efficient multi-scale communication library, between threads and between processes.
We call this **multi-runtime OCaml** and a prototype is available on [github](
Last, we are also making progress with the memory profiling tools. We work on a modified OCaml runtime which can store the location of each allocated block in the heap, with hooks to dump that heap on demand. External tools can then use that dump to produce useful statistics about memory usage of the program. The good news is that we now have a working and usable bytecode runtime and an external tool that produces basic memory information. We are preparing an alpha release in the next month, so stay tuned!
## Development Tools
Our efforts to make OCaml more usable go further than looking at the compiler. We are improving the development tools already existing in the community, such as the recently released [indentation tool]( which was initially coming from an experiment from [Jun Furuse](, and creating new ones when the lack is blatant.
Most recent news on that front concern [OPAM](, the package manager for OCaml that we are developing since mid-2012. For people not familiar with it yet, OPAM is a source-based package manager for OCaml. It supports resolution of complex dependency constraints between packages, multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow. The beta release was announced in January, and we expect the first official release to happen in the next weeks. The OCaml community has gratefully welcomed OPAM, and the [repository of its package metadata]( has already become the most forked OCaml project on github! Interestingly, two meetups have gathered more than fifty OPAM users in [Paris]( and Cambridge in January. We really hope this kind of meetup can be generalized: if you want to help us organize one in your area, feel free to contact us!
The other major part of our work around development tools for OCaml is TypeRex. TypeRex is a collection of tools which focus on improving developer efficiency, and lowering the entry barrier for experienced developers who are used to shiny IDEs in other languages. The first version of [TypeRex](, that was released last year, was a first step in this direction: it provided an enhanced emacs mode for OCaml code, with colorization, indentation, refactoring facilities, completion, code-navigation, documentation tooltips, etc. The next version of TypeRex (simply dubbed **typerex2**) is underway, with more independent tools (like ocp-indent), less tightly coupled to Emacs, and focused on better integration with various IDEs. If you are interested in following the progress of these tools, you can check the **typerex2** OPAM packages with 1.99.X+beta version numbers, which we release on a regular basis.
## R&D projects
The idea that OCaml is the right choice to create new innovative products is at the core of OCamlPro. We are very involved in the research community, especially on Functional Languages, with participation into the Program Committees of various conferences such as [the OCaml User and Developer (OUD)]( workshop and [the Commercial User of Functional Programming (CUFP)]( conference. We also joined two collaborative R&D projects in 2012, the [Richelieu FUI]( and [BWare ANR]( As part of the Richelieu project, we are developing a JIT compiler for the [Scilab language]( As part of the Bware project, we improve the efficiency of automatic theorem provers, with a specific focus on [Alt-Ergo](, an SMT solver particularly suited to program verification. We are always interested in bringing our expertise in compiler technologies and knowledge of complex and distributed systems to new R&D projects: contact us if you are interested!
In the Richelieu project, our combined technical and theoretical expertise proved particularly effective. The research consortium is led by [Scilab Entreprises]( which needed a safer and more efficient execution engine for Scilab in order to compete with Matlab. We joined the consortium to implement the early analysis required by the JIT compiler. The project started last December, and we have since specified the semantics of the language and implemented a working prototype of an interpreter that is already as fast as the current C++ engine of Scilab 6.
## Growing the Community
Our last important domain of activity is geared towards the OCaml community. It is important to us that the community grows bigger, and to achieve this goal there are some basic blocks that we need to help build, together with the other main actors of the community.
The first missing block is a good reference documentation. This year will end with (at least) one new important book for the language: [Real-World OCaml]( which targets experienced software engineers who do not know OCaml yet. We collaborate with [OCamlLabs]( to make the technical experience of this book a success. We also work to improve the general experience of using OCaml for complete beginners by creating a stable [replacement]( to the broken **ocamlwin**, the simple editor distributed with OCaml on Windows.
It is also important to us that OCaml uses the web as a platform to attract new users, as is becoming the norm for modern programming languages. We are members of the []( building effort and have created [tryocaml]( to let newcomers easily discover the language directly from their browser. TryOcaml has been welcomed as a great tool, already adopted and adapted: see for instance [tryrtt]( or [try ReactiveML]( We are in the process of simplifying the integration with other compiler variants.
Last, but not least, we collaborate very closely with OCamlLabs to create the OCaml Plateform: a consistent set of libraries, thoroughly tested and integrated, with a rolling release schedule of 6 months. The platform will be based on [OPAM]( and we are currently designing and prototyping a testing infrastructure to improve and guarantee the quality of packages.
title=April Monthly Report
authors=Çagdas Bozman
This post aims at summarizing the activities of OCamlPro for the past month. As usual, we worked in three main areas: the OCaml toolchain, development tools for OCaml and R&D projects.
## The toolchain
Our multi-runtime implementation of OCaml had gained stability. [Luca]( fixed a lot of low-level bugs in the “master” branch of [his OCaml repository](, which were mainly related to the handling of signals. There are still some issues, which seem to be related to thread-switching (ie. when using OS level mutli-threading).
We made great progress on improved inlining strategy. In the current OCaml compiler, inlining, closure conversion and constant propagation are done in a single pass interleaved with analysis. It has served well until now, but to improve it in a way which is easily extensible in the future, it needs a complete rewrite. After a few prototypes, [Pierre]( is now coming up with a suitable intermediate language (IR) more suited for the job, using a dedicated value analysis to guide the simplification and inlining passes. This IR will stand between the lambda code and the C-lambda and is designed such that future specialized optimization can be easily be added. There are two good reasons for this IR: First, it is not as intrusive and reduces the extent of the modifications to the compiler, as it can be plugged between two existing passes and turned on or off using a command-line flag. Second, it can be tweaked to make the abstract interpretation more precise and efficient. For instance, we want the inlining to work with higher-order functions as well as modules and functors, performing basic defunctorization. It is still in an experimentation phase, but we are quickly converging on the API and hope to have something we can demo in the next months.
Our [frame-pointer patch]( has also been accepted. Note that, as this patch changes the calling sconvention of OCaml programs, you cannot link together libraries compiled with and without the patch. Hence, this option will be provided as a configuration switch (`./configure --with-frame-pointer`).
Regarding memory profiling, we released a preliminary prototype of the memory profiler for native code. It is available in [Çagdas]( repository. We are still in the process of testing and evaluating the prototype before making it widely available through OPAM. As the previous bytecode prototype, you need to compile the libraries and the program you want to profile as usual in order to build a table associating unique identifier to program locations (.prof file). Then, for each allocated block, we have then patched the runtime of OCaml to encode in the header the identifier of the line which allocated it. To be able to dump the heap, you can either instrument your program, or send a signal, or set the appropriate environment variable (`OCAMLRUNPARAM=m`). Finally, you can use the profiler which will read the .prof and .cmt files in order to generate a pdf file which is the amount of memory use by type. More details on this will come soon, you can already read the [README]( file available on github.
Finally, we organized a new meeting with the core-team to discuss some of the bugs in the [OCaml bug tracker]( It was the first of the year, but we are now going to have one every month, as it has a very positive impact on the involvement of everybody in fixing bugs and helps focus work on the most important issues.
## Development Tools for OCaml
Since the latest release of [ocp-indent](, [Louis]( continued to improve the tool. We plan to release version 1.2.0 in the next couple of days, with some bug fixes (esp. related to the handling of records) and the following new features: operators are now aligned by default (as well as opened parentheses not finishing a line) and indentation can be bounded using the `max_indent` parameter. We are also using the great [cmdliner]( which means `ocp-indent` now has nice manual pages.
We are also preparing a new minor release of [OPAM](, with a few bug fixes, an improved solver heuristic and improved performance. OPAM statistics seem to converge towards round numbers, as [OcamlPro/opam]( repository has recently reached 100 “stars” on Github, [OCamlPro/opam-repository]( is not very far from being forked 100 times, while the number of unique packages on []( is almost 400\. We are also preparing the platform release, with a cleaner and simpler client API to be used by the upcoming “Ocamlot”, the automated infrastructure which will test and improve the quality and consistency of OPAM packages.
Last, we released a very small – but already incredibly useful tool: [ocp-index]( This new tool provides completion based on what is installed on your system, with type and documentation when available. Similarly to `ocp-indent`, the main goal of this tool is to make it easy to integrate in your editor of choice. As a proof of concept, we also distribute a small curses-based tool, called `ocp-browser`, which lets you browse interactively the libraries installed on your system, as well as an emacs binding for `auto-complete.el`. Interestingly enough, behind the scene `ocp-index` uses a [lazy immutable prefix tree]( with merge operations to efficiently store and load cmis and cmt files.
## Other R&D Projects
We continued to work on the [Richelieu]( project. We are currently adding basic type-inference for Scilab programs to our tool [scilint](, to be able to print warnings on possible programers mistakes. A first part of the work was to understand how to automatically get rid of some of the `eval` constructs, especially `deff` and `evalstr` primitives that are often used. After this, [Michael]( manually analyzed some real-world Scilab programs to understand how typing should be done, and he is now implementing the type checker and a table of types for primitive functions.
We are also submitting a new project, called SOCaml, for funding by the French government. In 2010, [ANSSI](, the French agency for the security of computer systems, commanded a study, called LAFOSEC, to understand the advantages of using functional languages in the domain of security. Early results of the study were presented in [JFLA’2013](, with in particular recommandations on how to improve OCaml to use it for security applications. The goal of the SOCaml project would be to implement these recommandations, to improve OCaml, to provide additional tools to detect potential errors and to implement libraries to verify marshaled values and bytecode. We hope the project will be accepted, as it opens a new application domain for OCaml, and would allow us to work on this topic with our partners in the project, such as [LexiFi]( and [Michel Mauny](‘s team at ENSTA Paristech (the project would also contribute to their [ocamlcc]( bytecode-to-c compiler).
\ No newline at end of file
title=Private Release of Alt-Ergo 1.00
authors=Mohamed Iguernlala
category=Formal Methods
![altergo logo](/blog/assets/img/logo_alt_ergo.png)
After the public release of Alt-Ergo 0.99.1 last December, it's time to announce a new major private version (1.00) of our SMT solver. As usual:
- we freely provide a JavaScript version on Alt-Ergo's website
- we provide a private access to our internal repositories for academia users and our clients.
### Quick Evaluation
A quick comparison between this new version and the previous releases is given below. Timeout is set to 60 seconds. The benchmark is made of 19044 formulas: (a) some of these formulas are known to be invalid, and (b) some of them are out of scope of current SMT solvers. The results are obtained with Alt-Ergo's native input language.
<table class="tableau" style="font-size: 90%; width: 100%;">
<th>public release<br />
<th>public release<br />
<th>private release<br />
<th>Proved Valid</th>
<th>Proved Valid (%)</th>
<td>84,01 %</td>
<td>85,77 %</td>
<td>92,62 %</td>
<th>Required time (seconds)</th>
<th>Average speed<br />
(valid formulas per second)</th>
### Main Novelties of Alt-Ergo 1.00
#### General Improvements
- theories data structures: semantic values (internal theories representation of terms) are now hash-consed. This enables the use of hash-based comparison (instead of structural comparison) when possible
- theories combination: the dispatcher component, that sends literals assumed by the SAT solver to different theories depending on whether these literals are equalities, disequalities or inequalities, has been re-implemented. The new code is much more simpler and enables some optimizations and factorizations that could not be made before
- case-split analysis: we made several improvements in the heuristics of the case-split analysis mechanism over finite domains
- explanations propagation: we improved explanations propagation in congruence closure and linear arithmetic algorithms. This makes the proofs faster thanks to a better back-jumping in the SAT solver part
- linear integer arithmetic: we re-implemented several parts of linear arithmetic and introduced important improvements in the Fourier-Motzkin algorithm to make it run on smaller sub-problems and avoid some useless executions. These optimizations allowed a significant speed up on our internal benchmarks
- data structures: we optimized hash-consing and some functions in the "formula" and "literal" modules
- SAT solving: we made a lot of improvements in the default SAT-solver and in the SatML plugin. In particular, the solvers now send lists of facts (literals) to "the decision procedure part" instead of sending them one by one. This avoids intermediate calls to some "expensive" algorithms, such as Fourier-Motzkin
- Matching: we extended the E-matching algorithm to also perform matching modulo the theory of records. In addition, we simplified matching heuristics and optimized the E-matching process to avoid computing the same instances several times
- Memory management: thanks to the ocp-memprof tool (, we identified some parts of Alt-Ergo that needed some improvements in order to avoid useless memory allocations, and thus unburden the OCaml garbage collector
- the function that retrieves the used axioms and predicates (when option 'save-used-context' is activated) has been improved
#### Bug Fixes
- 6 in the "inequalities" module of linear arithmetic
- 4 in the "formula" module
- 3 in the "ty" module used for types representation and manipulation
- 2 in the "theories front-end" module that interacts with the SAT solvers
- 1 in the "congruence closure" algorithm
- 1 in "existential quantifiers elimination" module
- 1 in the "type-checker"
- 1 in the "AC theory" of associative and commutative function symbols
- 1 in the "union-find" module
#### New OCamlPro Plugins
- profiling plugin: when activated, this plugin records and prints some information about the current execution of Alt-Ergo every 'x' seconds: In particular, one can observe a module being activated, a function being called, the amount of time spent in every module/function, the current decision/instantiation level, the number of decisions/instantiations that have been made so far, the number of case-splits, of boolean/theory conflicts, of assumptions in the decision procedure, of generated instances per axiom, ….
- fm-simplex plugin: when activated, this plugin is used instead of the Fourier-Motzkin method to infer bounds for linear integer arithmetic affine forms (which are used in the case-split analysis process). This module uses the Simplex algorithm to simulate particular runs of Fourier-Motzkin, which makes it scale better on linear integer arithmetic problems containing a lot of inequalities
#### New Options
- version-info: prints some information about this version of Alt-Ergo (release and compilation dates, release commit ID)
- no-theory: deactivate theory reasoning. In this case, only the SAT-solver and the matching parts are working
- inequalities-plugin: specify a plugin to use, instead of the "default" Fourier-Motzkin algorithm, to handle inequalities of linear arithmetic
- tighten-vars: when this option is set, the Fm-Simplex plugin will try to infer bounds for integer variables as well. Note that this option may be very expensive
- profiling-plugin: specify a profiling plugin to use to monitor an execution of Alt-Ergo
- profiling <freq>: makes the profiling module prints its information every <freq> seconds
- no-tcp: deactivate constraints propagation modulo theories
#### Removed Capabilities
- the pruning module used in the frontend is now removed
- the SMT and SMT2 front-ends are removed. We plan to implement a new front-end for SMT2 in upcoming releases
......@@ -8,8 +8,6 @@ let old_to_new =
; ("/fr/recrutement-ocamlpro/", "/jobs")
; ( ""
, "/" )
; ( ""
, "/" )
; ( ""
, "/" )
; ( ""
......@@ -159,6 +157,8 @@ let old_to_new =
, "/blog/2014_03_05_ocamlpro_highlights_feb_2014" )
; ( "/2014/04/01/the-generic-syntax-extension/"
, "/blog/2014_04_01_the_generic_syntax_extension" )
; ( "/2015/01/29/private-release-of-alt-ergo-1-00/"
, "/blog/2015_01_29_private_release_of_alt_ergo_1_00" )
; ( "/2015/04/13/yes-ocp-memprof-scanf/"
, "/blog/2015_04_13_yes_ocp_memprof_scanf" )
; ( "/2015/05/07/opam-1-2-2-released/"
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment