OCamlPro Highlights: Feb 2014
Here is a short report of some of our activities in February 2014 !
Displaying what OPAM is doing
After releasing version 1.1.1, we have been very busy preparing the next big things for OPAM. We have also steadily been improving stability and usability, with a focus on friendly messages: for example, there is a whole new algorithm to give the best explanations on what OPAM is going to do and why:
With OPAM 1.1.1, you currently get this information:
## opam install custom_printf.109.15.00 The following actions will be performed: – remove pa_bench.109.55.02 – downgrade type_conv.109.60.01 to 109.20.00 [required by comparelib, custom_printf] – downgrade uri.1.4.0 to 1.3.11 – recompile variantslib.109.15.03 [use type_conv] – downgrade sexplib.110.01.00 to 109.20.00 [required by custom_printf] – downgrade pa_ounit.109.53.02 to 109.18.00 [required by custom_printf] – recompile ocaml-data-notation.0.0.11 [use type_conv] – recompile fieldslib.109.20.03 [use type_conv] – recompile dyntype.0.9.0 [use type_conv] – recompile deriving-ocsigen.0.5 [use type_conv] – downgrade comparelib.109.60.00 to 109.15.00 – downgrade custom_printf.109.60.00 to 109.15.00 – downgrade cohttp.0.9.16 to 0.9.15 – recompile cow.0.9.1 [use type_conv, uri] – recompile github.0.7.0 [use type_conv, uri] 0 to install | 7 to reinstall | 0 to upgrade | 7 to downgrade | 1 to remove
With the next
trunk version of OPAM, you will get the much more informative output on real dependencies:
## opam install custom_printf.109.15.00 The following actions will be performed: – remove pa_bench.109.55.02 [conflicts with type_conv, pa_ounit] – downgrade type_conv from 109.60.01 to 109.20.00 [required by custom_printf] – downgrade uri from 1.4.0 to 1.3.10 [uses sexplib] – recompile variantslib.109.15.03 [uses type_conv] – downgrade sexplib from 110.01.00 to 109.20.00 [required by custom_printf] – downgrade pa_ounit from 109.53.02 to 109.18.00 [required by custom_printf] – recompile ocaml-data-notation.0.0.11 [uses type_conv] – recompile fieldslib.109.20.03 [uses type_conv] – recompile dyntype.0.9.0 [uses type_conv] – recompile deriving-ocsigen.0.5 [uses type_conv] – downgrade comparelib from 109.60.00 to 109.15.00 [uses type_conv] – downgrade custom_printf from 109.60.00 to 109.15.00 – downgrade cohttp from 0.9.16 to 0.9.14 [uses sexplib] – recompile cow.0.9.1 [uses type_conv] – recompile github.0.7.0 [uses uri, cohttp] 0 to install | 7 to reinstall | 0 to upgrade | 7 to downgrade | 1 to remove
Failsafe behaviour is being much improved as well, because things do happen to go wrong when you access the network to download packages and then compile them, and that was the biggest source of problems for our users: errors are now more tightly controlled in each stage of the opam command.
For example, nothing will be changed in case of a failed or interrupted download, and if you press
C-c in the middle of an action, you’ll get something like this:
[ERROR] User interruption while waiting for sub-processes [ERROR] Failure while processing typerex.1.99.6-beta =-=-= Error report =-=-= These actions have been completed successfully install conf-gtksourceview.2 upgrade cmdliner from 0.9.2 to 0.9.4 The following failed install typerex.1.99.6-beta Due to the errors, the following have been cancelled install ocaml-top.1.1.2 install ocp-index.1.0.2 install ocp-build.1.99.6-beta recompile alcotest.0.2.0 install ocp-indent.1.4.1 install lablgtk.2.16.0 The former state can be restored with opam switch import -f “<xxx>.export”
You also shouldn’t have to dig anymore to find the most meaningful error when something fails.
With the ever-increasing number of packages and versions, resolving requests becomes a real challenge and we’re glad we made the choice to rely on specialized solvers. The built-in heuristics may show its limits when attempting long-delayed upgrades, and everybody is encouraged to install an external solver (aspcud being the one supported at the moment).
Consequently, we have also been working more tightly with the Mancoosi team at IRILL to improve interaction with the solver, and how the user can get the best of it is now well documented, thanks to Roberto Di Cosmo.
Per-projects OPAM Switches with
At OCamlPro, we often use OPAM with multiple switches, to test whether our tools are working with different versions of OCaml, including the new ones that we are developing. Switching between versions is not always as intuitive as we would like, as we sometimes forget to call
$ eval `opam config env`
in the right location or at the good time, and end up compiling a project with a different version of OCaml that we would have liked.
It was quite surprising to discover that a tool that we had developed a long time ago, ocp-manager, would actually become a solution for us to a problem that appeared just now with OPAM:
was a tool we used to switch between different versions of OCaml before
OPAM. It would use a directory of wrappers, one for each OCaml tool,
and by adding this directory once and for all to the PATH, with:
$ eval `ocp-manager -config`
You would be able to switch to OPAM switch 3.12.1 (that needs to have been installed first with OPAM) immediatly by using:
[code language=”bash” gutter=”false”]
$ ocp-manager -set opam:3.12.1
Nothing much different from OPAM ? The nice thing with
is that wrappers also use environment variables and per-directory
information to choose the OCaml version of the tool they are going to
run. For example, if some top-directory of your project contains a file
with the line “opam:4.01.0”, your project will always be compiled with
this version of OCaml, even if you change the global per-user
configuration. You can also override the global and local configuration
by setting the
OCAML_VERSION environment variable.
Maybe ocp-manager can also be useful for you. Just install it with
opam install ocp-manager,
change your shell configuration to add its directory to your PATH, and
check if it also works for you (the manpage can be very useful!).
Optimization Patches for
ocamlopt under Reviewing Process
This month, we also spent a lot of time improving the optimization patches that we submitted for inclusion into OCaml, and that we have described in our previous blog posts. Mark Shinwell from Jane Street and Gabriel Scherer from INRIA kindly accepted to devote some of their time in a thorough reviewing process, leading to many improvements in the readability and maintenability of our optimization code. As this first patch is a prerequisite for our next patches, we also spent a lot of time propagating these modifications, so that we will be able to submit them faster once this one has been merged!
Displaying the Distribution of Block Sizes with
In our study to understand the memory behavior of OCaml applications, we have investigated the distribution of block sizes, both in the heap (live blocks) and in the free list (dead blocks). This information should help the programmer to understand which GC parameters might be the best ones for his application, by showing the fragmentation of the heap and the time spent searching in the free list. It is all the more important that improving the format of the free list with bins has been discussed lately in the Core team.
Here, we display the distribution of blocks at a snapshot during the execution of
why3replayer, a tool that we are trying to optimize during the Bware Project. The number of free blocks is displayed darker than live blocks, from size 21 to size 0.
It is interesting to notice that, for this applications, almost all allocations have a size smaller than 6. We are planning to use such information to simulate the cost of allocation for this application, and see which data structure for the free list would benefit the most to the performance of the application.
Whole Program Analysis
The static OCaml analyszer is going quite well. Our set of (working) test samples is growing in size and complexity. Our last improvement was what is called widening. What’s widening ? Well, the main idea is “when I go through a big loop 5000 times, I don’t want the analyzer to do that too”. If we take this sample test:
let () = for i = 0 to 5000 do () done
Without widening, the analysis would loop 5000 times through that
loop. That’s quite useless, not to mention that replacing 5000 by
Random.int () would make the analysis loop until max_int (2^62 times on a 64-bits computer) ! Worse, let’s take this code:
let () = let x = ref 0 in for i = 1 to 10 do x := !x + 1 done
Here, the analysis would not see that the increment on !x and i would be linked (that’s one of the aproximations we do to make the computation doable). So, the analyzer does not loop ten times, but again 2^62 times: we do not want that to happen.
The good news now: we can say to the analyzer “every time you go through a loop, check what integers you incremented, and suppose you’ll increment them again and again until you can’t”. This way we only go twice through our for-loop: first to discover it, then to propagate the widening approximation.
Of course this is not that simple, and we’ll often loose information by doing only two iterations. But in most cases, we don’t need it or we can get it in a quicker way than iterating billions of times through a small loop.
Hopefully, we’ll soon be able to analyze any simple program that uses only
Pervasives and the basic language features, but
while loops are already a good starting point !
SPARK 2014: a Use-Case of Alt-Ergo
The SPARK toolset, developped by the AdaCore company, targets the verification of programs written in the SPARK language; a subset of Ada used in the design of critical systems. We published this month a use-case of Alt-Ergo that explains the integration of our solver as a back-end of the next generation of SPARK.
Discussions with SPARK 2014 developpers were very important for us to understand the strengths of Alt-Ergo for them and what would be improved in the solver. We hope this use-case will be helpful for IT solutions providers that would need an automatic solver in their products.
Scilab 5 or Scilab 6 ?
We are still working at improving the Scilab environment with new
tools written in OCaml. We are soon going to release a new version of Scilint,
our style-checking tool for Scilab code, with a new parser compatible
with Scilab 5 syntax. Changing the parser of Scilint was not an easy
job: while our initial parser was partially based on the yacc parser of
the future Scilab 6, we had to write the new parser from scratch to
accept the more tolerant syntax of Scilab 5. It was also a good
opportunity to design a cleaner AST than the one copied from Scilab 6:
written in C++, Scilab 6 AST would for example have all AST nodes
inherit from the
Exp class, even instructions or the list of parameters of a function prototype !
We have also started to work on a type-system for Scilab. We want the result to be a type language expressive enough to express, say, the (dependent) sizes of matrices, yet simple enough for clash messages not to be complete black magic for Scilab programmers. This is not simple. In particular, there is the other constraint to build a versatile type system that could serve a JIT or give usable information to the programmer. Which means that the type environment is a mix of static information coming from the inference and of annotations, and dynamic information gotten by introspection of the dynamic interpreter.
In the mean time, we are also planning to write a simpler JIT, to mitigate the impatience of Scilab programmers expecting to feel the underlying power of OCaml!
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. Please reach out, we'll be delighted to discuss your challenges: email@example.com or book a quick discussion.