Hello
Here is the latest OCaml Weekly News, for the week of September 09 to 16, 2014.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-09/msg00072.html
Damien Doligez announced:
This is an announcement for a job opening that involves lots of
programming in OCaml...
-- Damien
Research team: Tools for Proofs, MSR-INRIA Joint Centre
=======================================================
The Microsoft Research-INRIA Joint Centre is offering a 14-month
position for a research engineer to contribute to the ADN4SE project.
We hope the position will be extended to 18 months, but are not yet
sure this will be possible.
The engineer will contribute to extending the TLA+ Proof System
(TLAPS, http://msr-inria.com/projects/tools-for-proofs) and will
assist domain experts in applying TLAPS for proving fundamental
properties of PharOS, a real-time operating system.
Research Context
================
TLA+ is a language for specifying and reasoning about systems,
including concurrent and distributed systems. It is based on
first-order logic, set theory, and temporal logic. TLA+ and its
tools have been used in industry for over a decade. More recently,
we have extended TLA+ by a language for writing structured formal
proofs and have developed TLAPS, a proof checker that contains an
interpreter for the proof language and integrates different back-end
provers. TLAPS is integrated into the TLA+ Toolbox, an IDE for TLA+
(http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).
Although it is still under active development, TLAPS is already quite
powerful and has been used for a few verification projects, in particular
in the realm of distributed algorithms
(e.g., http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html).
The current version of TLAPS handles the "action" part of TLA+:
first-order formulas with primed and unprimed variables that represent
the values of a variable before and after a transition. It also supports
the propositional fragment of temporal logic. This fragment is enough for
proving safety properties (invariants and step simulation). We are currently
refactoring the code base and preparing support for full temporal logic of
TLA+, which will allow us to prove liveness and refinement properties.
Description of the activity of the research engineer
====================================================
The research engineer (post-doctoral) position is funded by the PIA ADN4SE
project (http://www.systematic-paris-region.org/en/projets/adn4se) that
develops a real-time operating system and development tools for
embedded systems based on PharOS. The system aims at providing
certifiable correctness and performance guarantees, and fundamental
properties of the operating system, such as determinacy, are formally
verified using the TLA+ notation and tools.
Your work will make a key contribution to this verification effort.
In particular, you will work with members of the TLA+ project at the
Microsoft Research - INRIA Joint Centre, including Damien Doligez,
Leslie Lamport, and Stephan Merz on extending the TLA+ Proof System
and its libraries. You will also work with the project partners of
ADN4SE, and in particular members of CEA List, on modeling the
protocols subject to verification and on carrying out the proofs.
Your contributions will be conceptual, by identifying theories and
patterns that underly the verification of the operating system, and
practical, by implementing formal libraries and software in order to
carry out the verification task.
You will also have the opportunity to contribute to further improving
the proof checker, for example by adding support for certain TLA+ features
that are not yet handled by TLAPS, integrating new back-end provers, or
extending the capabilities for proof validation.
Skills and profile of the candidate
===================================
You should hold a PhD in computer science and have solid knowledge of
mathematical logic as well as implementation skills related to symbolic
theorem proving. Our tools are mainly implemented in OCaml. Some basic
familiarity with concepts of real-time systems is a plus. Experience
with temporal and modal logics, with interactive theorem provers or with
Eclipse could be valuable.
Working on the project provides the opportunity to learn about the
issues of using verification in practice, and it has in the past and
may continue in the future to produce published research. However,
the main focus is on practical applications and on the implementation
of components of our tool chain that are missing or need improvement.
Given the geographical distribution of the members of the team,
we highly value a good balance between the ability to work in a team
and the capacity to propose initiatives.
Location
========
The research engineer will be based at the INRIA research center in
Nancy (http://www.inria.fr/en/centre/nancy). Located in the North-East
of France, Nancy is a university town whose metropolitan area has
about 400,000 inhabitants. It is 1-1/2 hours from Paris by TGV.
Contact
=======
Candidates should send a resume and the names and e-mail addresses of
two references to Damien Doligez <damien.doligez@inria.fr>, preferably
by September 22, 2014.
We intend to hire the research engineer by November 2014, although the
exact date is negotiable.
This announcement is available at
http://www.msr-inria.com/open_positions/research-engineer-position-on-tla-tools/
Damien Doligez later added:
[updated: we got funding for 24 months instead of 14]
Research team: Tools for Proofs, MSR-INRIA Joint Centre
=======================================================
The Microsoft Research-INRIA Joint Centre is offering a 24-month
position for a research engineer to contribute to the ADN4SE project.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-09/msg00090.html
Yotam Barnoy asked:
It appears to me that every couple of months we hear of someone
implementing yet another build system in ocaml. Given the success of
opam, I think it's clear that sometimes a monolithic solution, behind
which the entire community can organize, is the best solution --
especially for infrastructure. Looking at haskell, having cabal as the
main build system has really helped them advance in terms of
supporting other platforms (such as windows), and since all community
efforts in this realm are focused on cabal, they can improve it
rapidly.
a. Is there any build system we can organize behind to crown as the
official build system?
b. What are the use-cases missing from specific build systems, that
have driven people to use other build systems?
c. To pick one possible candidate, if ocamlbuild were spun out of the
compiler, could it be enhanced to cover all the main use-cases so
(almost) everyone would be happy with it?
It's just such a shame to see the ocaml community re-inventing the
wheel over and over again, each time with some limitation so that the
next person needs to do the same thing yet again.
Richard Jones replied:
> b. What are the use-cases missing from specific build systems, that have
> driven people to use other build systems?
In a non-OCaml-centric world you need to fit into other projects. The
virt-* tools are a good example here, since they are mostly written in
C, and use automake/autoconf. And the OCaml virt tools have to link
with C and so are also built using only autotools.
Example of mixed C / OCaml program built using autotools:
https://github.com/libguestfs/libguestfs/tree/master/v2v
After many other replies, Yotam Barnoy summarized:
OK so here's my summary of what I've heard here so far:
- Ocaml does not yet have a (public) build system that the majority of
users can be happy with for all of their project needs.
- It seems difficult to have a build system that's simple enough to
use for small projects, flexible enough to handle the more complicated
projects, and that can scale.
- While declarative, dsl-based tools are appealing, they get bogged
down as you add features to them, making them become unwieldy.
- A better solution seems to be using a real programming language to
describe packages. In our case that should clearly be ocaml itself.
The trick is making the API simple.
Looking at some of the the available options:
- ocamlbuild (dsl-based) is a decent basic choice, but lacks advanced
features and has become weighed down by multiple file types (_tags,
myocamlbuild etc).
- OASIS (dsl-based) seems to be a good description layer for projects,
currently farming out the difficult work of building stuff to
ocamlbuild, but not really a contender in this race except as an
abstraction layer.
- omake (dsl-based) has some fans, but becomes overly-complex for more
complicated projects.
- ocp-build (dsl-based) has had nothing but criticism on this thread.
Is there any ongoing work to address these criticisms?
- Jenga (uses ocaml) seems promising but has heavy dependencies, and
is currently not geared towards light projects.
- assemblage (uses ocaml) seems promising as well, and seems focused
on simplicity. Any comment from assemblage contributors on its status?
Also, while I understand some of the windows hatred, the fact is, most
of the world uses windows. Even using cygwin as a translation layer
hurts ocaml's ability to reach people. Ideally, a windows programmer
could download opam, ocaml and perhaps a mingw compiler, and begin to
build projects without any need for a shell or anything POSIX-like.
This means that the build system needs to obviate the need for any
shell commands or makefiles.
Anil Madhavapeddy then said:
- assemblage (uses ocaml) seems promising as well, and seems
focused on simplicity. Any comment from assemblage contributors on
its status?
It's being actively developed, is still unreleased, and the build API
is still subject to change.
Early adopters and contributors are most welcome to get involved and
give feedback, as long as you understand the above caveats that it's a
moving target.
I'd suggest reading through some of the discussions and pull requests
on https://github.com/samoht/assemblage/issues to get a sense of the
outstanding tasks left before a public beta release.
Yaron Minsky then said:
Jenga, as I said, isn't currently ready for wide use. But I do think
it's a very promising tool. A few notes:
- Easy vs Sophisticated
We think Jenga provides a pretty good balance between easy and
sophisticated. Even though its core is quite powerful and so not
trivial to use, it is also amenable to using with other, simpler
build-declaration systems.
We ourselves use a simple s-expression config format for specifying
individual libraries, and there has been some talk of integrating
Assemblage into Jenga eventually as another such simple DSL. We've
even done some work making Jenga compile from Ninja build
descriptions.
- Bootstrapping
One concern with Jenga is boot-strapping, or other ways of exporting
packages to be built where Jenga itself is not available.
We have a pretty good solution to this in flight, and after talking
with Neil Mitchell, he's going to try the same trick out with Shake.
The idea is to be able to generate makefiles that can be used as
part of a package.
Systems like Jenga and Shake do well because they have rich, monadic
languages for expressing complex dependencies that are discovered
during a build. But we can use Jenga to do enough of the build to
discover the dependencies, and then export a makefile reflecting
those dependencies. This should make it possible to build all of
Jenga's dependencies using make, and indeed for any Jenga package to
be exported in a portable and dependency-free way.
(Windows make should be supportable this way too.)
- Dependencies
We're working on lightening the dependencies of Jenga. We are
planning to release a new version of Async in a couple of months
whose base (called Async_kernel) no longer depends on Core (which
depends on some Unix-isms) and instead only depends on the (highly
portable) Core_kernel.
That should bring us a good step closer to having Windows support.
I think we'd still need some work, in particular, someone to write
better windows support for Async, perhaps on top of libuv. But once
we release our cleaned up async, I think that's more approachable.
In the short term, I'm quite hopeful that Assemblage will provide
something that's easy to use right now. But I think Jenga is an
important part of the longer term plan for OCaml builds.
Adrien Nader also replied:
> Also, while I understand some of the windows hatred, the fact is, most of
> the world uses windows. Even using cygwin as a translation layer hurts
> ocaml's ability to reach people. Ideally, a windows programmer could
> download opam, ocaml and perhaps a mingw compiler, and begin to build
> projects without any need for a shell or anything POSIX-like. This means
> that the build system needs to obviate the need for any shell commands or
> makefiles.
I'm worried it my message which sounded like Windows hatred.
I don't hate Windows, really. I hate cmake and qt however because the
design they _chose_ was already a step back more than a decade ago. It's
similar to advocating static linking despite the current needs to
regularly update libraries because of security issues.
(NB: similar feelings towards people who do not use ocamlfind; hopefully
they're very uncommon nowadays)
As for using only cmd.exe. Well. You probably don't know cmd.exe. You
probably don't know how command-line argument parsing works on Windows.
I can't believe you would and not do your best to avoid them.
The main issue is that the newly-launched process does not receive its
arguments as an array of strings. Instead it receives them as a string.
When you call execv() on windows, it concatenates the string array
you've given and it will be the new process which will have to split
them back into a "char* []" for use with main().
So you have to prepare your arguments. But how? According to the spec of
course! Ah, easy! Except there is no real logic behind it: it's
completely ad-hoc stuff and while probably doable with only a few lines
of code (probably as many as this email), it's looks error-prone (and,
let's face it, boring). Oh and, it might well break compat and the issue
has been in OCaml since 1994.
This is the reason ocamlbuild depends on an sh.exe from msys/cygwin btw
(I'm actually wondering if cygwin's is fit for this task...).
It will receive a single string of arguments, parse it like it would do
on POSIX; in other words, its only purpose is to get back to well-known
and manageable parsing rules.
To be honest, OCamlbuild also has a large tendency to shell-out but in
90% of the cases, it's not a big issue although re-implementing "cp -r"
is annoying (did someone mention that if ocamlbuild moves out of the
compiler, it can depend on Fileutils which implements this kind of
operations?).
That said, ocamlbuild works well on Windows because besides these few
shell-outs, it's written in OCaml.
Btw, there are open bug reports on mantis about that. If you're
interested in getting these fixed, the links to the docs are already
there and the work is definitely manageable so speak up.
Btw2, there's a fairly recent "zsh for windows" (last release from 2011
or 2012) and which, if it works, and if it works for our use-case, could
maybe be integrated in the ocaml installers and could simplify the
process.
(note the number of "ifs" and conditionals used above)
In any case, if you plan on integrating with something else, and you
will, unless you don't want to use any C stubs, including the ones for
the OS, you will have to understand and integrate into the existing
C-building setups which already exist one way or another.
Fabrice Le Fessant also replied:
- ocp-build (dsl-based) has had nothing but criticism on this
thread. Is there any ongoing work to address these criticisms?
Yes, ocp-build is still alive. I would not advise anybody to use it
for anything complicated (no syntax extension, only predefined
compilation rules for .ml/.mli/.mll and .mly). My plan is to rewrite
the DSL to introduce better abstractions to allow cross-compilation,
composable package configuration and a better handling of META files.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-09/msg00147.html
Sylvain Conchon and Jean-Christophe Filliâtre announced:
(Note to non French-speaking users: this is an announcement for a new
book on OCaml, in French. We plan to translate it to English soon.)
Chers utilisateurs d'OCaml,
Nous sommes heureux d'annoncer la sortie d'un nouveau livre sur OCaml :
Apprendre à programmer avec OCaml
Algorithmes et structures de données
Éditions Eyrolles, 2014.
Ce livre s'accompagne d'un site web qui propose en téléchargement libre
les programmes contenus dans le livre :
http://programmer-avec-ocaml.lri.fr/
Ceci inclut un certain nombre de structures de données et d'algorithmes,
qui peuvent être directement réutilisés ou facilement adaptés. Ces
programmes sont distribués sous la même licence que ceux de la
bibliothèque standard d'OCaml.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2014-09/msg00165.html
Gerd Stolpmann announced:
a new minor version has been released. This is mostly about the
compatibility Bytes module. First, an installation problem has been
fixed (sometimes it wasn't honoring the install prefix). Second, Bytes
has been updated (by Gabriel Scherer) to also cover recent additions
(post-4.02).
As always, links for download can be found here:
http://projects.camlcity.org/projects/findlib.html
If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.
If you also wish to receive it every week by mail, you may subscribe online.