Features Download
From: Alan Schmitt <alan.schmitt-o/5/jSaJEHk+NdeTPqioyti2O/JbrIOy <at> public.gmane.org>
Subject: Attn: Development Editor, Latest Caml Weekly News
Newsgroups: gmane.comp.lang.ocaml.weekly-news
Date: Tuesday 28th February 2012 15:17:05 UTC (over 6 years ago)

Here is the latest Caml Weekly News, for the week of February 21 to 28, 

1) TypeRex release 1.0.0 candidate 1
2) Ocamlnet-3.5
3) findlib-1.2.8
4) post-doc position available at MSR-INRIA joint lab
5) llpp v11
6) Other Caml News

1) TypeRex release 1.0.0 candidate 1
** Tiphaine Turpin announced:

We are pleased to announce the first release candidate of TypeRex, a new
OCaml development environment, developed by OCamlPro and Inria Saclay.
This version of TypeRex only integrates with Emacs and brings a
collection of new features that programmers expect from a modern IDE.
Next versions will target more editors.

Downloads, screenshots, documentation, support and feedback
instructions are available on TypeRex website at:


Summary of TypeRex features:

     * Improved syntax coloring
     * Auto-completion of identifiers (experimental)
     * Browsing of identifiers: show type and comment, go to definition,
       cycle between alternate definitions, and semantic grep;
     * Strictly semantic-preserving, local and whole-program 
           o renaming identifiers and compilation units
           o open elimination and reference simplification
     * Robust /w.r.t./ not-recompiled, possibly unsaved buffers
     * Scalable (used regularly on a few hundreds of source files)

Auto-completion is disabled by default, since more testing is still
needed for this feature.

TypeRex is written in OCaml, communicating through a socket with the
OCaml mode of the editor (currently Tuareg for Emacs, OCAIDE for Eclipse

All the features of the Tuareg mode are also included, even when we
provide an equivalent for them.

2) Ocamlnet-3.5
** Gerd Stolpmann announced:

it is time for another version of Ocamlnet. The new release 3.5 focuses 
the system interface, and includes a long list of smaller improvements.

The system interface, Netsys_posix, is extended by:
  - Support for POSIX clocks and POSIX timers (with nanosecond 
  - Netsys_posix.spawn usses now the posix_spawn call if present on the 
  - Adding support for pollable events (as e.g. provided by Linux via
    eventfd). For other OS an emulation is available.
  - Support for epoll on Linux

Note that Netsys_posix covers now large parts of POSIX realtime.

Other improvements:

  - The code generator for XDR has been improved. A new switch -direct 
    ocamlrpcgen can be used to generate direct mappings between OCaml 
    and binary representation (in many cases). Speedups up to 50% are
    possible for large XDR values.
  - The new module Uq_mt allows it to access an event-driven resource 
    several kernel threads (e.g. use an RPC client commonly from several
  - The thread-safety of Netplex container functions has been improved.
  - Netmulticore condition variables can now be polled, for better
    integration into event-based programs.
  - Option greedy_accepts for Netplex to support servers that accept
    many connections per second. With this improvement, Netplex can
    now accept more than 5000 connections/s, and assign them to worker

Last but not least there is now a new tutorial for Equeue (event systems
and engines). In particular, the section about combining Ocamlnet with 
might be interesting.

For the full list of changes (especially bug fixes), see:


The download, manual, and other resources:


GODI has been updated.

3) findlib-1.2.8
** Gerd Stolpmann announced:

Findlib-1.2.8, a patch release, is out. It includes a fix for Win32, and
support for "ocamlfind ocamlmklib", mostly for completeness.


4) post-doc position available at MSR-INRIA joint lab
** 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 a proof 
environment for TLA+ developed in the Tools for Proofs project (see

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
and integrated it into the
TLA+ Toolbox, an IDE for the TLA+ tools

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 still lacking important features, TLAPS is
already a powerful tool and has been used for a few verification
projects, including a proof of the safety properties of a 
tolerant consensus algorithm

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

Description of the activity of the post-doc

You will work with other members of the project, including Leslie
Lamport, Damien Doligez, and Stephan Merz, on the extension of the
TLA+ proof language to temporal operators.  This extension poses
interesting conceptual and practical problems.  In particular, the new
translation must smoothly extend the existing one since temporal proof
steps rely on action-level subproofs.  You will have the primary
responsibility for designing and implementing algorithms to generate
corresponding proof obligations.

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;
- finding what improvements are needed by verifying real examples, 
   including liveness of the aforementioned consensus algorithm;
- integrating new backends to improve the automation of proofs;
- adding validation of proofs by backends whose proofs are not
   now checked.

Skills and profile of the candidate

You should have a solid knowledge of logic and set theory as well as
good implementation skills related to symbolic theorem proving.  Of
particular relevance are parsing and compilation techniques.  Our
tools are mainly implemented in OCaml.  Experience with temporal and
modal logics, Isabelle, Java or Eclipse would be a plus.

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.


The Microsoft Research-INRIA Joint Centre is located on the Campus of
INRIA Saclay south of Paris, near the Le Guichet RER station.

Starting date

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


Candidates should send a resume and the name and e-mail addresses of
one or two references to Damien Doligez
The deadline for application is April 15, 2012.

This announcement is available at

5) llpp v11
** malc announced:

New version of llpp is now available (tagged v11) at


llpp a graphical PDF viewer which aims to superficially resemble


* Removed dependency on GLUT
   (consequently native Windows and OS X support is also gone)
   (There's a win32 a binary, built just before GLUT removal at:
- 3857425 bytes)
* User modifiable key mappings
* Keyboard link navigation
* Probably more, since:

llpp$ git diff --stat v10..v11 | tail -1
  14 files changed, 4203 insertions(+), 1461 deletions(-)

(That said: keysym2ucs.c |  849 +++++++++++++++++++
  IOW 849 added lines is keysym to unicode conversion code by by Markus 

How to build/run: <http://www.youtube.com/watch?v=9xtIqD_mHRw>

To run it one must have GLX capable X server, chances are good that if
the video card in ones machine is less than 10 years old things will 

Known to run with:
RV280 (aka Radeon 9200)           Mesa/linux/ppc
RV730 (aka Radeon HD 4650)        Mesa/freebsd/x86[_64?]
????  (aka ???)                   Mesa/x86[_64?] [1]
NV94  (aka GeForce 9600 GT)       nouveau (Gallium 0.4 on 
                                   binary blob by NVidia

(FWIW the card in this machine (rv280) is more than ten years old)

[1] 00:02.0 VGA compatible controller: Intel Corporation 2nd Generation 
Processor Family Integrated Graphics Controller (rev 09)

[2] Caveat emptor: with nouveau when window manager resizes windows 
     things might get garbled (same thing happens with GLUT based 
version too)
       a. Instruct the WM to not do opaque resizes
       b. LIBGL_ALWAYS_INDIRET=1 llpp [args]
diff --git a/link.c b/link.c
index 10a9eba..8a6f872 100644
--- a/link.c
+++ b/link.c
@@ -2725,7 +2725,7 @@ CAMLprim value ml_glx (value win_v)
          caml_failwith ("glXChooseVisual");

-    glx.ctx = glXCreateContext (glx.dpy, visual, NULL, True);
+    glx.ctx = glXCreateContext (glx.dpy, visual, NULL, False);
      if (!glx.ctx) {
          XCloseDisplay (glx.dpy);
          XFree (visual);

6) 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 

Opa 0.9.0: New syntax:

Debugging memory in OCaml: any advice?:

Spotlight on Opa app: OpaDo by Tristan Sloughter:

jingoo v1.0 release:

Dreaming of an ARM OCaml:

whenjobs - job lists, cancelling, algorithmic cleanup etc:

OCamlnet 3.5:

TypeRex 1.0.0rc1:

OCaml MySQL Protocol 0.3 available:

For the Right Hand:

Old cwn

If you happen to miss a CWN, you can send me a message
(alan.schmitt-o/5/jSaJEHk+NdeTPqioyti2O/[email protected]) and I'll
mail it to you, or go take a 
look at
the archive (<http://alan.petitepomme.net/cwn/>)
or the RSS feed of the
archives (<http://alan.petitepomme.net/cwn/cwn.rss>).
If you also wish
to receive it every week by mail, you may subscribe online at

CD: 4ms