Hello
Here is the latest Caml Weekly News, for the week of June 04 to 11, 2013.
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
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/
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.gzFrancois 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.
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`.
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.
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.
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!
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
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
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/
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.