Previous week Up Next week

Hello

Here is the latest Caml Weekly News, for the week of October 08 to 15, 2013.

  1. equivalent checking of ocaml program?
  2. Procord 0.1.0: Delegate tasks to other processes
  3. OCaml 2013: papers and slides are available
  4. OPAM 1.1.0 Release Candidate
  5. Marshalling: automatic discard of unmashalable data via ephemerons
  6. Developper position: designing a C front-end in OCaml
  7. Other Caml News

equivalent checking of ocaml program?

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00073.html

Continuing 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.
      

Procord 0.1.0: Delegate tasks to other processes

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00078.html

Romain 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 [1].
> 
> I also had to handle sending a SIGINT to the ocaml toplevel, which wasn't very fun,
> 
> 
> [1] 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.
      

OCaml 2013: papers and slides are available

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00080.html

Michel 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.
      

OPAM 1.1.0 Release Candidate

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00112.html

Louis 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 formulas
      
Nicolas Braud-Santoni then added:
This feel like a good occasion to annouce that, since today[1], OPAM is
available directly as a package on Exherbo[2].
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

[1] https://github.com/nbraud/nicoo_exherbo/commits/master/packages/dev-ocaml/opam
[2] http://exherbo.org/
      

Marshalling: automatic discard of unmashalable data via ephemerons

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00113.html

Enrico 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.
      

Developper position: designing a C front-end in OCaml

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00118.html

Xavier 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 (rival@di.ens.fr).
      

Other Caml News

From the ocamlcore planet blog:
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
      

Old cwn

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.


Alan Schmitt