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.htmlDamien 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 <firstname.lastname@example.org>, 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.htmlYotam 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/v2vAfter 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.htmlSylvain 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.htmlGerd 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.