Here is the latest Caml Weekly News, for the week of October 08 to 15, 2013.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00073.htmlContinuing the thread from last week, Gabriel Scherer said:
Shortly after writing my email, I found out that Ong had co-written a recent article (CAV'12) on using those techniques precisely for equivalence checking: Hector: An Equivalence Checker for a Higher-Order Fragment of ML David Hopkins' Andrzej S. Murawski and C.-H Luke Ong 2012 http://www.cs.ox.ac.uk/files/4786/cav12.pdf They restrict themselves to a order-bounded fragment of higher-order function types (and only allow ground reference types) suggested by game-semantics considerations, on which equivalence checking is decidable, and leave extensions to more complex settings where equivalence becomes indecidable to future work. You probably know more about this than I do (this is not my field at all), but my understanding is that whether the problems are decidable or not is not an actual concern with model checking, as even in decidable cases the tools most often run out of time; actual feasability on concrete examples seems the most useful way to evaluate those, so I don't think going to undecidable fragments would be a problem in principle. Of course, the more complex the fragment, the more expansive the computations.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00078.htmlRomain Bardou announced:
I am happy to announce the first release of Procord, a portable library to delegate tasks to other processes. Obtain it with opam: opam install procord Or, download the tarball: https://github.com/cryptosense/procord/archive/v0.1.0.tar.gz View a minimal, commented example: https://github.com/cryptosense/procord/blob/master/examples/minimal.ml You can browse the API at: http://cryptosense.github.io/procord/api/index.html Procord can spawn local worker processes or communicate using sockets to a remote worker server. Workers will receive an input, execute a function on this input, and send back the result. Meanwhile, the main program can continue to run while waiting for the results. Not relying on threads, Procord is robust - a segmentation fault in the worker will not kill the main program. Not relying on fork, Procord is portable - it has been tested on Linux and Windows. Procord provides an easy way to have the same executable act as a worker - local or remote - or as the main program. The actual behavior can be specified on the command-line. The default is to run as the main program, which delegates tasks by running itself. I will present Procord at the OUPS meeting of this evening.Arnaud Spiwack asked and Romain Bardou replied:
> I see you are using Unix.kill to kill processes. But I was under the > impression that it didn't work properly on Windows. Am I mistaken? Indeed. In fact I made a feature request about this: http://caml.inria.fr/mantis/view.php?id=6146 So, just waiting for OCaml 4.02 will solve the issue. If waiting is not an option I can of course add this in Procord. I should at least provide a way to get the PID / Process Handle so that one can call TerminateProcess using his own binding. While we are discussing the differences between Windows and Linux, there is actually another one: the Windows server does not fork and, thus, only accepts one task at a time. This could be solved by having the server execute himself to run the tasks. But before actually implementing this I prefer to wait and see whether there is a real need (Windows servers are less common).Louis Gesbert then suggested and Jacques Garrigue added:
> You may find the bindings for Terminate_process in ocaml-top useful . > > I also had to handle sending a SIGINT to the ocaml toplevel, which wasn't very fun, > > >  https://github.com/OCamlPro/ocaml-top/blob/master/src/sigint_win.c If you're just trying to kill an ocaml toplevel that you have spawned yourself, you can have a look at labltk/browser/shell.ml. By setting the environment variable OCAMLSIGPIPE and sending T or C to this pipe you can kill or interrupt the ocaml toplevel asynchronously. (At the time I implemented that, there was basically no other way to do that in windows than having a child thread kill its parent.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00080.htmlMichel Mauny announced:
The presentations that have been given at OCaml 2013 in Boston on september 24 are now online: http://ocaml.org/meetings/ocaml/2013/program.html The presentations have been video recorded. I'll let you know if and when they are online. Don't forget to submit a presentation to OCaml 2014 which should again be co-located with ICFP 2014.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00112.htmlLouis Gesbert announced:
OPAM 1.1.0 is ready, and we are shipping a release candidate for packagers and all interested to try it out. This version features several bug-fixes over the September beta release, and quite a few stability and usability improvements. Thanks to all beta-testers who have taken the time to file reports, and helped a lot tackling the remaining issues. # OPAM OPAM is a source-based package manager for OCaml. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow. OPAM is edited and maintained by OCamlPro, with continuous support from OCamlLabs and the community at large (including its main industrial users such as Jane-Street and Citrix). # Repository change to opam.ocaml.org This release is synchronized with the migration of the main repository from ocamlpro.com to ocaml.org. A redirection has been put in place, so that all up-to-date installation of OPAM should be redirected seamlessly. OPAM 1.0 instances will stay on the old repository, so that they won't be broken by incompatible package updates. We are very happy to see the impressive amount of contributions to the OPAM repository, and this change, together with the licensing of all metadata under CC0 (almost pubic domain), guarantees that these efforts belong to the community. # If you are upgrading from 1.0 The internal state will need to be upgraded at the first run of OPAM 1.1.0. THIS PROCESS CANNOT BE REVERTED. We have tried hard to make it fault- resistant, but failures might happen. In case you have precious data in your ~/.opam folder, it is advised to backup that folder before you upgrade to 1.1.0. # Installing Using the binary installer: - download and run http://www.ocamlpro.com/pub/opam_installer.sh You can also get the new version either from Anil's unstable PPA: add-apt-repository ppa:avsm/ppa-testing apt-get update sudo apt-get install opam or build it from sources at : - http://www.ocamlpro.com/pub/opam-full-1.1.0.tar.gz - https://github.com/OCamlPro/opam/releases/tag/1.1.0-RC # Changes Too many to list here, see https://raw.github.com/OCamlPro/opam/1.1.0-RC/CHANGES For packagers, some new fields have appeared in the OPAM description format: - `depexts` provides facilities for dealing with system (non ocaml) dependencies - `messages`, `post-messages` can be used to notify the user or help her troobleshoot at package installation. - `available` supersedes `ocaml-version` and `os` constraints, and can contain more expressive formulasNicolas Braud-Santoni then added:
This feel like a good occasion to annouce that, since today, OPAM is available directly as a package on Exherbo. I will endeavour to provide up-to-date packages for both “stable releases” and “testing releases” (such as -beta or -RC). Regards, Nicolas Braud-Santoni  https://github.com/nbraud/nicoo_exherbo/commits/master/packages/dev-ocaml/opam  http://exherbo.org/
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00113.htmlEnrico Tassi said:
(Editor note: please see the archive link for the attached files.) Hello caml-list. I'm new here, It's my fist post, and I want to share an hack I came up with to systematically solve some marshalling problems I have in the context of Coq development. I hope the hack is of general interest, maybe it is folklore, maybe not... The Coq architecture is switching to a multi process one, where slave processes are fed a system state, a portion of the proof script (an entire proof at the moment) and are expected to return the resulting proof term. Data is marshalled using the standard Marshal module. The system state is made of pretty much anything, and is also user extensible via plugins. Nothing prevents someone to stick in there values that can hardly be marshalled, like callbacks, file descriptors, lazy_t, and the like. Of course it is nice to be able to store callbacks or lazy values in the system state, so forbidding all that is not nice. Luckily enough, I don't need this data in the slave processes. Hence I could pre-process the system state and throw it away. But the system state is big, and traversing it to prune out some bits is likely to be expensive. Moreover I'm lazy, I don't want to code that pruning function, hence the following solution. Values that can't, or should not, be marshalled are stored in the system state using a unique key, and given a key one can retrieve the corresponding value. These (key,value) pairs are ephemeron, if the key is not reachable, the value (if it has no extra references) will be eventually collected too. When a key is marshalled, no error occurs (keys are just doubly boxed integers). When a key is unmarshalled it becomes invalid, i.e. the associated value cannot be retrieved anymore. In some sense it is like if marshalling was forgetting the part of the marshalled value that is stored as a key. All automatically, no need to pre/post process the marshalled value and no extra memory management hassle. Thanks to Damien Doligez for his preliminary comments on the attached files.
Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00118.htmlXavier Rival announced:
We are looking for an experienced OCaml developper in order to design front-end components for a static analyzer developped as part of the MemCAD ERC project (http://www.di.ens.fr/~rival/memcad.html). The position is offered at INRIA Paris Rocquencourt center, in the Abstraction Research Team (located in Ecole Normale Supérieure, Paris, 5th Arrondissement). It will be funded on the MemCAD project, for a one or two years duration (if the candidate opts for a one year contact, an extension to two years will be possible). Hiring could be done as soon as December 2013 (later starting dates are feasible). The task that will be undertaken consists in developping front-end components for the MemCAD static analyzer, including a C front-end, syntax tree simplification, and possibly pre-analyses to be used in the MemCAD tool (the goal of this tool is to infer program invariants for codes manipulating complex memory data-structures). The components that shall be designed as part of this effort have the potential to be used by other research groups in the static analysis area. The candidate should be familiar with functional programming (expertise in OCaml is very appreciated) and should preferably have some knowledge in compilation (lexers, parsers, representation and transformation of abstract syntax trees). The ability to design interfaces with external libraries in C/C++ will also be useful. No knowledge in static analysis is required. This position requires a Master Degree (or equivalent). For additional details, please contact Xavier Rival (email@example.com).
Thanks to Alp Mestan, we now include in the Caml Weekly News the links to the recent posts from the ocamlcore planet blog at http://planet.ocaml.org/. dlnasync: https://forge.ocamlcore.org/projects/dlnasync/ Batsh: https://forge.ocamlcore.org/projects/batsh/ OCaml MySQL Protocol 0.9 available: https://forge.ocamlcore.org/forum/forum.php?forum_id=888
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.