Previous week Up Next week

Hello

Here is the latest Caml Weekly News, for the week of June 04 to 11, 2013.

  1. Ocamlnet-3.6.5
  2. post-doc position at MSR-Inria
  3. ocaml-ctypes, a library for calling C functions directly from OCaml
  4. Core Suite 109.27.00 + core_kernel
  5. OCaml on zLinux
  6. Use-site variance in OCaml
  7. New Book: OCaml from the Very Beginning
  8. Deadline extension: OCaml 2013, new deadline on June 18 (anywhere on earth)
  9. Findlib-1.4
  10. Other Caml News

Ocamlnet-3.6.5

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00043.html

Amending the announcement from last week, Gerd Stolpmann said:
Well, things go wrong...

There was a build problem in 3.6.4 so that netstring-pcre did not work
properly. This is fixed in the new versiopn 3.6.5 I just released.

Gerd

> Hi,
>
> I've just released Ocamlnet-3.6.4. This is a maintenance release
> including:
>
> - New configure options for PCRE (-enable-full-pcre, -enable-pcre).
> There is also documentation about the PCRE issue in Regexp.html
> (remember that PCRE is no longer the default regexp engine).
> - More documentation for Netmulticore: Netmcore_basics
> - New Netplex module for mailboxes: Netplex_mbox.
> - netcgi2-apache builds against apache-2.4
>
> plus various smaller fixes and additions.
>
> For a full description, see the ChangeLog.
>
> Get Ocamlnet, read the manual etc. from
> http://projects.camlcity.org/projects/ocamlnet.html
      

post-doc position at MSR-Inria

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00042.html

Damien Doligez announced:
Research team: Tools for Proofs, MSR-INRIA Joint Centre
=======================================================

The Microsoft Research-INRIA Joint Centre is offering a 2-year
position for a post-doctoral researcher to contribute to the ADN4SE
project aiming at extending the proof development environment for TLA+
developed in the Tools for Proofs project
(http://msr-inria.com/projects/tools-for-proofs) and applying it for
the verification of key components of 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, temporal logic, and a module system.
TLA+ and its tools have been used in industry for over a decade. More
recently, we have extended TLA+ to include hierarchically structured
formal proofs that are independent of any proof checker. We have
released several versions of the TLAPS proof checker
(http://tla.msr-inria.inria.fr/tlaps) and integrated it into the
TLA+ Toolbox, an IDE for the TLA+ tools
(http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

TLAPS and the Toolbox support the top-down development of proofs and
the checking of individual proof steps independently of the rest of
the proof. This helps users focus on the part of the proof they are
working on. Although it is still under active development, TLAPS is
already a powerful tool 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).

TLAPS consists of the Proof Manager (PM, an interpreter for the
proof language that computes the proof obligations corresponding to
each proof step) and an extensible list of backend provers. Current backends
include the tableau prover Zenon, an encoding of TLA+ as an object logic
in the Isabelle proof assistant, and a generic backend for SMT solvers.
When possible, we expect backend provers to produce a detailed proof that
is then checked by Isabelle. In this way, we can obtain high assurance
of correctness as well as satisfactory automation.

The current version of the PM handles only the "action" part of TLA+:
first-order formulas with primed and unprimed variables, where a
variable v is considered to be unrelated to its primed version v'.
This allows us to translate non-temporal proof obligations to standard
first-order logic, without the overhead associated with an encoding of
temporal logic into first-order logic. An extension for handling full
TLA+, including its temporal logic for verifying liveness properties,
is currently being developed.


Description of the activity of the post-doc
===========================================

The 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 core protocols
of the operating system will be formally verified using the TLA+
notation and tools.

Your research will make a key contribution to this verification effort.
In particular, you will work with other members of the project,
including Damien Doligez, Leslie Lamport, Tomer Libal, 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,
to model the protocols subject to verification. 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.

As time permits and depending on your interests, you will have the
opportunity to contribute to further improving the proof checker.
This may include:
- adding support for certain TLA+ features that are not yet handled by
the PM, such as recursive operator definitions and elaborate patterns
for variable bindings;
- integrating new backends to improve the automation of proofs;
- adding validation of proofs by backends whose proofs are not
yet checked in the current version.

Skills and profile of the candidate
===================================

You should have a solid knowledge of mathematical logic as well as
good implementation skills related to symbolic theorem proving.
Experience with developing real-time systems are a plus. Our tools
are mainly implemented in OCaml. Experience with temporal and
modal logics, with interactive theorem provers or with Eclipse could
be valuable.

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 Microsoft Research-INRIA Joint Centre is located on the Campus of
Ecole Polytechnique south of Paris, France.

Starting date
=============

The normal starting date of the contract would be November 2013, but
we can arrange for an extremely well-qualified candidate to start
sooner.

Contact
=======

Candidates should send a resume and the name and e-mail addresses of
one or two references to Damien Doligez
<damien.doligez AT inria.fr>.
The deadline for application is July 10, 2013.

This announcement is available at
http://www.msr-inria.com/open_positions/post-doc-research-position-on-tla-tools/
      

ocaml-ctypes, a library for calling C functions directly from OCaml

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00046.html

Jeremy Yallop announced:
I'm happy to announce the initial release of ocaml-ctypes.

The ocaml-ctypes library makes it possible to call C functions
directly from OCaml without writing or generating C code.  The core of
the library is a set of combinators for describing C types -- scalars,
functions, structs, unions, arrays, and pointers to values and
functions.  Type descriptions can then be used to bind native
functions and values.  Here's a simple example:

    # let puts = foreign "puts" (string @-> returning int);;
    val puts : string -> int = <fun>
    # puts "Hello, world!";;
    Hello, world!

Here's a more substantial example that shows how to describe a C
structure type, map the type to an OCaml record, and call a function
that returns the structure.

    (* Describe the C struct.  There are two fields, both ints. *)
    let div_t = structure "div_t";;
    let q = div_t *:* int
    let r = div_t *:* int
    let () = seal div_t

    (* Define the OCaml record that we'll use to view the C structure. *)
    type div_result = { quot : int; rem: int }

    (* Define the conversions between the C struct and the OCaml record. *)
    let div_result_of_div_t d = { quot = getf d q; rem = getf d r }
    let div_t_of_div_result {quot; rem} =
        let d = make div_t in (setf d q quot; setf d r rem; d)

    (* Create a "view type" for that looks like div_result and behaves
like div_t *)
    let div_result = view ~read:div_result_of_div_t
~write:div_t_of_div_result div_t

    (* Bind to the standard C `div' function *)
    let div = foreign "div" (int @-> int @-> returning div_result)

    (* Try it out *)
    # div 17 2;;
    - : div_result = {quot = 8; rem = 1}

The distribution contains larger examples and a fairly extensive test
suite, showing how to use other features of the library, such as
binding to functions that accept callback arguments.  Among the
examples is Anil Madhavapeddy's port of the `curses' example from the
OCaml documentation; it's instructive to compare the two
implementations:

    OCaml manual curses example
    http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html#toc147

    ocaml-ctypes curses example
    https://github.com/ocamllabs/ocaml-ctypes/blob/master/examples/ncurses/ncurses.ml

Detailed installation instructions for ocaml-ctypes can be found in
the tutorial.  (Briefly: ensure libffi is installed, then 'opam
install ctypes'.)

Comments, bug reports, and other feedback are most welcome.

Tutorial:
https://github.com/ocamllabs/ocaml-ctypes/wiki/ctypes-tutorial
Examples:
https://github.com/ocamllabs/ocaml-ctypes/tree/master/examples
API documentation: http://ocamllabs.github.io/ocaml-ctypes/
Github repository: https://github.com/ocamllabs/ocaml-ctypes
Direct download:
https://github.com/ocamllabs/ocaml-ctypes/archive/ocaml-ctypes-0.1.tar.gz
      
Francois Berenger asked and Jeremy Yallop replied:
> How about the cost of exchanging values between C and OCaml?
> Is there a trick in ocaml-ctypes like there is for bigarrays?

Array and struct memory in ocaml-ctypes is managed similarly to the
way bigarray does things, i.e. objects are allocated on the C heap, so
both C and OCaml functions can safely access them without copying.
However, there's no special compiler support for ocaml-ctypes as there
is for bigarrays, so it's likely that array access will be slower for
the moment.

Of course, arrays in ocaml-ctypes also have some advantages over
bigarrays. For example, they can hold a broader range of data --
structs, pointers, and so on.

I'm hoping to add bigarray integration to ocaml-ctypes at some point.
      

Core Suite 109.27.00 + core_kernel

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00052.html

Jeremie Dimino announced:
I am pleased to announce the 109.27.00 release of the Core suite.

The following packages were upgraded:

- async
- async_core
- async_extra
- async_parallel
- async_unix
- comparelib
- core
- core_bench
- core_extended
- custom_printf
- jenga
- pa_ounit
- zero

Starting with this release the "core" package is split into two
packages: "core_kernel" and "core". core_kernel is a lightweight
subset of core. It contains all the non-Unix parts, it should be
easier to use with js_of_ocaml for example.

We couldn't make it C-free since there is a strong depency to bin_prot
which has C stubs. In addition core_kernel still contains a few C
stubs for bigstrings and also arrays.

Files and documentation for this release are available on our website
and all packages are in opam:

  https://ocaml.janestreet.com/ocaml-core/109.27.00/individual/
  https://ocaml.janestreet.com/ocaml-core/109.27.00/doc/

Here is the changelog since version 109.24.00:

## async_core

- Fixed `Monitor.catch_stream` to prevent missing a synchronous
  exception.

## async_extra

- Added function `Versioned_typed_tcp.Client.shutdown`.
- Added new module `Sequencer_table`, which is a table of
  `Throttle.Sequencer`'s indexed by keys.

## async_unix

- Fixed a performance problem in the scheduler due to repeated calls
  of `Timing_wheel.min_elt`.

  `Timing_wheel.min_elt` is an important part of async, since the
  scheduler calls it once per cycle to know when to timeout for
  `epoll` or `select`.  This causes a problem if `min_elt` is slow and
  called repeatedly, which happens in an application where the next
  clock event is a second out, and yet there are lots of cycles per
  second.

  `Timing_wheel.min_elt` now caches the minimum element, which
  eliminates the problem.
- Fixed async's clock to work on 32-bit machines.

  With the change to `Timing_wheel` in 109.22, async no longer worked
  on 32-bit machines, due to the clock overflowing.  This is because
  it is initialized to `Time.epoch`, and can only handle 6 days.

  The fix now in place is to start the clock at `Time.now ()` rather
  than `Time.epoch`.
- Added many functions to `Async.Sys` so that it looks more like
  `Core.Sys`.
- Changed `Reader.read_one_chunk_at_a_time_until_eof` to not destroy
  the reader buffer.

  Destroying the buffer failed if user code held on to the buffer.

## comparelib

- Changed how `with compare` treats `option`'s so that `None < Some`,
  like `Pervasives.compare`.

  Previously, `with compare` had treated `Some < None`.

## core

- Disabled use of `recvmmssg`, which isn't available on CentOS 5
  machines.
- Defined `Option.compare` using `with compare` so that their
  comparisons are consistent.
- Cleaned up the `Dequeue` module's interface and implementation.

  The interface now matches the conventions used elsewhere in `Core`.
  The new implementation is also cleaner and more efficient.
- Reimplemented the `Stack` module to improve performance, and renamed
  the old implementation as `Linked_stack`.

  The new `Stack` is implemented with this type:

  ```ocaml
  type 'a t `
    { dummy : 'a;
      mutable length : int;
      mutable elts : 'a array;
    }
  ```

  `Linked_stack` is implemented with this type:

  ```ocaml
  type 'a t `
    { mutable length : int;
      mutable elts : 'a list;
    }
  ```

  Using an array rather than a linked list is a more efficient and
  traditional implementation.  Pushing to the stack now does not
  require allocation, except in the rare case when the stack grows.

  One downside is that `Stack.clear` is now O(n) rather than O(1).

  This change also eliminates the `Stack.Empty` exception, so any code
  matching on that exception should fail to compile, and should be
  changed to depend on option-returning `top` and `pop` operations.
- Improved `Lock_file.Nfs`.
  * Allowed an arbitrary message to be stored and retreived.
  * Fixed a case where `create` might throw an exception.
  * Delete both files used for locking when we unlock.
- Split `Core` into `Core_kernel` and `Core`.
- `Core_kernel` is composed of all modules of `Core` that do not
  depend on unix or threads, and `Core` contains the rest and depends
  on `Core_kernel`.

  The goal is to have a very portable standard library that can
  especially run on exotic environment such as Javascript.

  So that code that directly refers to `Core` (rather than `Core.Std`)
  for modules that have moved to `Core_kernel`, we included "proxy"
  modules in `Core` that simply include the corresponding module from
  `Core_kernel`.

- Fixed `Core.Flags` to build on 32-bit machines.

  It had contained a unit test with an integer literal too large to be
  accepted by the compiler when building on a 32-bit machine.

## core_bench

- Added R^2 error estimation.

  Adding this metric should give us a sense of how closely the given
  values fit a line.  Even dots that are fairly scattered can give
  tight confidence intervals.  We would like to have to number to have
  a sense of how much noise we have.

## core_extended

- In module `Sexp`, changed and renamed `load_includes_in_sexp`.

  From:

  ```ocaml
  val load_includes_in_sexp : ?max_depth:int -> Sexp.t -> Sexp.t
  ```

  to:

  ```ocaml
  val load_sexp_with_includes: ?max_depth:int -> ?buf:string -> string -> Sexp.t
  ```
- Added function `Sexp.Diff.to_string`.
- Previously the only option was to print to `Out_channel`.

## custom_printf

- Added missing registration of `custom_printf`'s Camlp4 filter so
  that it works in the toplevel.

## pa_ounit

- Removed comments from test names displayed by `pa_ounit`.

  Before:
  ```
  File "iobuf.ml", line 141, characters 0-34: <<(** WHEN YOU CHANGE
THIS, CHANGE iobuf_fields `...`>> threw ("Iobuf.create got nonpositive
len" 0).
  ```

  After:
  ```
  File "iobuf.ml", line 141, characters 0-34: <<ignore (create ~len:
0)>> threw ("Iobuf.create got nonpositive len" 0).
  ```

## zero

- Added new hashtable module, `Pooled_hashtbl`.

  `Pooled_hashtbl` is a drop-in replacement for `Core_hashtbl`, and
  has the same interface.

  `Pooled_hashtbl` is a linked-chain hashtbl implemented using the
  pooling features of `Zero`.  In addition to pooling, by using
  `Flat_tuple_array` (and therefore `Obj_array`) it has much improved
  performance when working with immediate keys or values, as a test is
  performed and the `caml_modify` skipped when possible.

  The algorithm is a straightforward implementation, and as such will
  not perform well under heavy collisions that come from poor hash
  functions.  Additionally, since the pool of Key/Data nodes are
  created up front, rapidly creating and releasing `Pooled_hashtbl`s
  will not perform well.

  For a well-thought-out hash with a long-lived table and immediate
  values as keys (or data), `Pooled_hashtbl` will very likely
  outperform `Core_hashtbl`.
- Made pointers in `Pool.Obj_array` contain the unique id of the
  object they point to.

  This allows one to check in constant time check whether a pointer is
  valid.
- Improved the performance of `Timing_wheel` by internally exposing
  `Priority_queue.Elt_.t ` private int`.

  This allows the compiler to eliminate some `caml_modify`'s.  This
  made `nanoseconds_per_step` in the timing-wheel benchmark go from
  96ns to 79ns.
- Changed `Timing_wheel` to cache its minimum element.

  This is an important optimization for how async uses `Timing_wheel`.
      

OCaml on zLinux

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00053.html

Alain Frisch asked and Stéphane Glondu replied:
> Does anyone have any experience running OCaml on the zLinux operating
> system (i.e. Linux on IBM System z)? I suspect that the bytecode system
> would work fine, but it would be great to get confirmation of it.

It compiles, and the test suite seems to pass on the Debian s390 and
s390x ports. Build logs are available at:

https://buildd.debian.org/status/package.php?p=ocaml&suite=experimental

Same for most of the software written in OCaml that is packaged in Debian.
      

Use-site variance in OCaml

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00055.html

Jeff Meister asked and Jacques Garrigue replied:
> I don't often use subtyping in OCaml, but I was recently reading a paper
> about a mixture of declaration-site and use-site variance annotations in a
> Java-like language
> (http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed-site-tate-2013.pdf),
> and it occurred to me that OCaml might be able to express the same
> concepts.
>
> If I have a type parameter that appears in both covariant and contravariant
> positions, then it is invariant, and OCaml will not allow me to annotate
> the parameter with + or -. For example, this class of mutable references:
>
> class ['a] rw (init : 'a) = object
>   val mutable v = init
>   method get = v
>   method set x = v <- x
> end
>
> This code will not compile with [+'a] or [-'a]. However, the class can be
> (manually) decomposed into separate covariant and contravariant parts:
>
> class [+'a] ro (init : 'a) = object val mutable v = init method get = v end
> class [-'a] wo (init : 'a) = object val mutable v = init method set x = v <- x end
> class ['a] rw init = object inherit ['a] ro init inherit! ['a] wo init end
> 
> I can always coerce from 'a rw to 'a ro or 'a wo, when I want to restrict access
> to the reference as read-only or write-only. Those types will then allow
> coercions that would not be permitted on 'a rw. For example, given this pair of
> classes:
> 
> class super = object end
> class sub = object method foo = () end
> 
> The compiler will accept (new ro (new sub) :> super ro) as well as (new wo (new
> super) :> sub wo).
> 
> However, I didn't actually need to annotate the type parameters in my
> definitions of 'a ro and 'a wo; OCaml would have inferred them. And these
> coercions are all compile-time operations.
> 
> So, it seems that the OCaml type checker knows which methods of my first
> definition of 'a rw use 'a in a covariant or contravariant position. Would
> it be possible to implement use-site variance in OCaml based on this?
>
> I'm imagining an expression like (new rw 0 :> +'a rw) that would give an
> object of type 'a ro, without the programmer having to declare any such
> type, or decompose his class manually. OCaml would automatically select
> only those methods where 'a appears only in covariant positions. Similarly,
> -'a rw would produce an object of type 'a wo.
>
> Is this feasible, or is the situation more complicated than I've described?

This is technically doable.
Maybe the most painful part would be to extend the syntax to allow variance
annotations inside type expressions.
Also, OCaml and Java differ in that OCaml allows binary methods, which being
contravariant in the type of self
introduce some ambiguity in the meaning of "+":
  class type ['a] cell = object ('self) inherit ['a] rw method eq : 'self -> bool end
In that case, +'a cell could either keep only method get, or only eq, but
keeping both would be invariant.

And as always the question is rather how useful it would be in practice.

Also, an intermediate form seems possible too: rather than doing this on the
fly inside coercions,
one could use it in declarations:

  class type ['a] ro = [+'a] rw

or

  class type ['a] c = object
    inherit [+'a] rw
    method set x = {< v = x >}
  end

The change in syntax is much more modest: we just allow variance annotations
in the bracket, and we are sure that rw must be a class type.
      

New Book: OCaml from the Very Beginning

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00064.html

John Whitington announced:
I've written a concise but self-contained introduction to writing computer
programs with OCaml, suitable for the talented beginner to programming, or
someone trying functional programming or OCaml for the first time.

On your local Amazon: http://asin.info/a/0957671105

E-book: http://www.ocaml-book.com

Sample chapters also at http://www.ocaml-book.com

Thanks to all those who reviewed and proof-read earlier drafts.

Reviews on Amazon are always very useful - my understanding is that if you have
an amazon account, you can review the book based on having read the e-book,
without buying a printed copy. Do please consider adding a review, especially if
you like the book!
      

Deadline extension: OCaml 2013, new deadline on June 18 (anywhere on earth)

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00070.html

Michel Mauny announced:
OCaml 2013 extends its submission deadline. The new deadline is June
18, anywhere on earth.

Let me remind you that the scope of OCaml 2013 is rather broad, and
includes experience reports, libraries, bindings, extensions,
optimizations, and virtually everything concerning about. The only
requirement is a short description of what you'd like to address, and
what you'd like to present. The description does not have to be long,
but should be explicit enough for the PC members to understand what
your presentation is about.

Some travel grants shall be available for students or people having
financial difficulties for attending OCaml 2013.

If you missed time for meeting the original deadline, if you use OCaml
in your company and would like to share your experience with OCaml
users and developers, if you have something cool to present, don't
hesitate!

Please forward this message to whoever could be interested, and redirect
questions to <michel DOT mauny AT ensta-paristech.fr>

Submissions are at:

https://www.easychair.org/conferences/?conf=ocaml2013
      

Findlib-1.4

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00072.html

Gerd Stolpmann announced:
I just released findlib-1.4:

- Fixed performance bug when many arguments need to be processed.
- Auto-configuring ocamldoc.opt if it is found.
- New config switch -no-custom to prevent that "ocamlfind" is linked in
custom-runtime mode (bytecode only)
- The library dbm is no longer part of OCaml, and now optional in
findlib
- Support for ocamloptp.
- New function Topfind.log for controlling the verbosity.
- Rewritten Fl_metascanner without camlp4 (patch from Gabriel Scherer)

Thanks to all supporters - I got a lot of patches for this release.

More documentation and download:
http://projects.camlcity.org/projects/findlib.html
      

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

New book: OCaml from the Very Beginning:
  http://coherentpdf.com/blog/?p=56

Now available on Amazon:
  http://ocaml-book.com/blog/2013/6/6/now-available-on-amazon

OCaml?Scope : a new OCaml API search by names and types:
  http://camlspotter.blogspot.com/2013/06/ocamlscope-new-ocaml-api-search-by.html

Flowing faster: foundations:
  http://scattered-thoughts.net/blog/2013/06/04/flowing-faster-foundations/
      

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