Hello

Here is the latest OCaml Weekly News, for the week of January 24 to 31, 2017.

1. mSAT 0.6
2. visitors
3. Memory Usage
4. Celebrating a round number of pull requests for the compiler distribution
5. Ocaml Github Pull Requests

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00139.html

I have the pleasure to announce the release of mSAT 0.6 [0], a modular
SAT-solver library in pure OCaml. SAT solvers are useful for NP-complete
constraint solving, and are commonly used directly in many tools
(including the package manager of eclipse), or indirectly as part of
SMT solvers (Satisfiability Modulo Theory).

mSAT is a modernized fork of alt-ergo-zero[1] that can be used both as a
pure SAT solver, and as a building block for writing SMT solvers.
To write a SMT solver based on mSAT, there is a functor that can be
instantiated with a custom term structure and a custom theory
responsible for propagation, following the Lazy SMT framework.  The
functor also provides an interface for MCSat-style solvers.
mSAT is also proof-producing (it can output boolean resolution proofs),
model-producing, and can output unsat-cores.
Its flexibility and availability as an OCaml library make it useful for
writing SMT solvers that feature experimental theories or theory
implementations. The documentation can be found online [2].

Performance-wise, mSAT should be in the fast end of what OCaml makes
possibles. Obviously, state of the art C solvers (minisat, picosat,
etc.) are still much better.

mSAT is developed by Guillaume Bury and Simon Cruanes, and available
on opam as "msat", under the permissive Apache license.

[0] https://github.com/Gbury/mSAT
[1] http://cubicle.lri.fr/alt-ergo-zero/
[2] https://gbury.github.io/mSAT/
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00144.html

I would like to announce the first release of the "visitors" package.
It is a syntax extension for OCaml, or more accurately, a plugin for
the "ppx_deriving" syntax extension.

By annotating a type definition with [@@deriving visitors { ... }],
one requests the automatic generation of visitor classes, which make
it easy to traverse and transform a data structure.

The documentation (which contains many examples) is here:

  http://gallium.inria.fr/~fpottier/visitors/manual.pdf

To install the package via opam, use the following commands:

  opam update
  opam install visitors

The project's repository is public:

  git clone git@gitlab.inria.fr:fpottier/visitors.git

Comments and feedback are welcome.
      

> Very nice! I wanted this for quite a while and the documentation is
> excellent.

Thanks! And thanks for your comments and pointers.

> A big difference is that it load type definition from .cmi files directly.

Indeed, a limitation of the ppx approach is that it is purely syntatic:
a syntax tree (the type definition) is turned into a syntax tree (the
definition of the visitor classes). In particular, at the moment, "visitors"
cannot generate visitor classes for a pre-existing type. Perhaps one could
write a tool that reads a .cmi file, but I suppose it would have to be
explicitly invoked as an external tool. I will think about it.

> What do you think of visitor that translates one datatype into another ?

Well, the current package already allows this.

If the two data types are just two distinct instances of a single
parameterized data type, then a "map" visitor can do this, with very little
effort. See the examples in the manual when "ordinary expressions" are
converted to "hash-consed expressions" and back.

If the two data types are unrelated, then, in order to translate the type
"foo" to the type "bar", you need a "fold" visitor for the type "foo". You
then have to manually implement each of the "build_" methods, so as to explain
how each data constructor of the type "foo" should be translated.

> I wonder if, given some annotations, it would be doable to use similar
> techniques to generate visitors between different datatypes.

I think you have it already, but instead of placing "annotations" in the
type definition, you have to implement the "build_" methods.
      

> If the two data types are unrelated, then, in order to translate the type
> "foo" to the type "bar", you need a "fold" visitor for the type "foo". You
> then have to manually implement each of the "build_" methods, so as to
> explain how each data constructor of the type "foo" should be translated.

I forgot to add that the manual has an example of converting between two
entirely unrelated types: a user-defined type "crowd" is converted to
"(string * string) list".
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00148.html

I am wondering what is the best way to find the time and memory usage (in words
or bytes) of an Ocaml function, e.g., Factorial) on MAC?
      

One option is using a profiling tool, for example the following one
http://memprof.typerex.org
      

I have to also point out: https://caml.inria.fr/pub/docs/manual-ocaml/spacetime.html
      

Archive: https://sympa.inria.fr/sympa/arc/caml-list/2017-01/msg00148.html

The number of pull requests (change proposals) on the
github/ocaml/ocaml repository reached a nice round number in the
favorite number base of some of you during this month of January 2016:

  https://github.com/ocaml/ocaml/pull/1000
    (Improvements to afl-fuzz support, Stephen Dolan)

  https://github.com/ocaml/ocaml/pull/1024
    (Extend the testsuite to test installations, David Allsopp)

We started accepting github Pull Requests on January 30, 2014, as part
of a general effort by the developers of the OCaml compiler
distribution to encourage and better handle external contributions. It
is of course difficult (and not terribly important) to judge the
impact of Github in particular in enabling the diverse contributions
we received since then, but having round numbers is a good reason to
celebrate.

(I should point out that any help reviewing the pull requests is
appreciated, and the accelerated rate of changes also came with a few
irritating regressions in the last couple major releases. We are
trying to fight back against regressions; any help in testing the new
releases during their alpha and beta periods are much appreciated.)

Many thanks to the contributors to the compiler distribution (through
patches but also the equally important, bug reports, documentation,
communication, etc.), and to any of the nice and interesting projects
built within our friendly OCaml community.

Happy hacking.
      

Here is a sneak peek at some potential future features of the Ocaml
compiler, discussed by their implementers in these Github Pull Requests.

- add resource-handling IO functions in pervasives
  https://github.com/ocaml/ocaml/pull/640
      

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