Hello

Here is the latest OCaml Weekly News, for the week of May 12 to 19,
2020.

Table of Contents
─────────────────

ocamlformat 0.14.2
ML Family Workshop 2020: Call for presentations
memprof-limits preview (and a guide to handle asynchronous exceptions)
Tezos 7.0 is now available on opam
Official OCaml bindings for verified Everest cryptography
nmea and sail-gadgets
Is there specialized math library for statistics?
New OCaml books?
Other OCaml News
Old CWN


ocamlformat 0.14.2
══════════════════

  Archive: [https://discuss.ocaml.org/t/ann-ocamlformat-0-14-2/5754/1]


Guillaume Petiot announced
──────────────────────────

  We are pleased to announce the release of `ocamlformat' 0.14.2.  This
  minor release improves the recent 0.14.0 and 0.14.1 releases regarding
  the `doc-comments' option.


How to migrate from 0.13.0
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  Here are the changes of the `doc-comments' options compared to
  ocamlformat 0.13.0:
  • `after' has been renamed to `after-when-possible' to take into
    account the technical limitations of ocamlformat;
  • a new value `before-except-val' has been added, placing doc-comments
    before the corresponding code, but placing doc-comments of val and
    external declarations after the corresponding declaration;
  • `before' is unchanged.

  Here is the full list of changes made by the 0.14.0 release:
  [https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435]


How to migrate from 0.14.0
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  The 0.14.0 release lead to some regression of the `doc-comments'
  behavior that (although intended for us) lead to some surprise from a
  lot of users.  The behavior of `doc-comments' has thus been reverted
  to it's 0.13.0 state with the following changes:

  The `doc-comments-val' option has been removed and merged with
  `doc-comments'. The placement of documentation comments on `val' and
  `external' items is now controlled by `doc-comments' .

  • `doc-comments=after' becomes `doc-comments=after-when-possible' to
    take into account the technical limitations of ocamlformat;
  • `doc-comments=before' is unchanged;
  • `doc-comments-val' is now replaced with `doc-comments'

  To reproduce the former behaviors
  • `doc-comments=before' + `doc-comments-val=before' : now use
    `doc-comments=before' ;
  • `doc-comments=before' + `doc-comments-val=after' : now use
    `doc-comments=before-except-val' ;
  • `doc-comments=after' + `doc-comments-val=before' : this behavior did
    not make much sense and is not available anymore;
  • `doc-comments=after' + `doc-comments-val=after' : now use
    `doc-comments=after-when-possible'.


How to migrate from 0.14.1
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  The 0.14.1 release was preserving the behavior of 0.13.0 regarding
  `doc-comments', it added a `unset' value to the `doc-comments-val'
  option.  This option has been removed with the following changes:

  The `doc-comments-val' option has been removed and merged with
  `doc-comments'. The placement of documentation comments on `val' and
  `external' items is now controlled by `doc-comments' .

  • `doc-comments=after' becomes `doc-comments=after-when-possible' to
    take into account the technical limitations of ocamlformat;
  • `doc-comments=before' is unchanged;
  • `doc-comments-val' is now replaced with `doc-comments'

  To reproduce the former behaviors
  • `doc-comments=before' + `doc-comments-val=before' : now use
    `doc-comments=before' ;
  • `doc-comments=before' + `doc-comments-val=after' : now use
    `doc-comments=before-except-val' ;
  • `doc-comments=after' + `doc-comments-val=before' : this behavior did
    not make much sense and is not available anymore;
  • `doc-comments=after' + `doc-comments-val=after' : now use
    `doc-comments=after-when-possible'.


Thank you
╌╌╌╌╌╌╌╌╌

  We would like to thank our early users to help us on the road of a
  stable 1.0.0 release of ocamlformat.


ML Family Workshop 2020: Call for presentations
═══════════════════════════════════════════════

  Archive:
  [https://discuss.ocaml.org/t/ml-family-workshop-2020-call-for-presentations/5441/4]


Leo White announced
───────────────────

  ICFP, and by extension the ML workshop, will be now officially be held
  online with a significantly reduced fee. Due to the change in official
  status we decided to extend the submission deadline to the end of May.


Important Dates (updated)
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  • Friday 29th May (any time zone): Abstract submission deadline
  • Friday 17th July: Author notification
  • Thursday 27th August: ML Family Workshop


memprof-limits preview (and a guide to handle asynchronous exceptions)
══════════════════════════════════════════════════════════════════════

  Archive:
  [https://discuss.ocaml.org/t/ann-memprof-limits-preview-and-a-guide-to-handle-asynchronous-exceptions/5756/1]


Guillaume Munch-Maccagnoni announced
────────────────────────────────────

  Dear OCamlers, I am happy to pre-announce [memprof-limits], an
  implementation of per-thread global memory limits, and per-thread
  allocation limits à la Haskell, compatible with systhreads.

  Memprof-limits interrupts the execution by raising an _asynchronous
  exception_, an exception that can arise at almost any location in the
  code. I also announce [a guide on how to recover from asynchronous
  exceptions and other unexpected exceptions] that you find in the
  documentation. It summarises knowledge acquired in OCaml by the Coq
  proof assistant as well as in other programming languages. To my
  knowledge, this has never been told in OCaml textbooks, so I thought
  it might be of general interest to you. This research is part of a
  wider work aiming to regulate the use of asynchronous exceptions in
  OCaml in coordination with multicore language designers.

  _Global memory limits_ let you bound the memory consumption inside
  specific parts of your program, in terms of memory used by the whole
  program. It is inspired by [this other post], but in a form readily
  available for use with systhreads.

  _Allocation limits_ let you bound the execution of parts of the
  program measured in number of allocations, analogous to the same
  feature in Haskell advocated in [a nice post by Simon
  Marlow]. Allocation limits count allocations but _not_ deallocations,
  and is therefore a measure of the work done, which can be more
  suitable than execution time.

  Memprof-limits, as the name tells, uses the upcoming Memprof engine
  from OCaml 4.11, with a low sampling rate that does not affect
  performance. A reimplementation of the Memprof interface compatible
  with memprof-limits running at the same time is provided for profiling
  needs.

  Memprof-limits is available on the public opam repository, but depends
  on OCaml 4.11 which at the moment is available from the beta opam
  repository only. It is _experimental_ for reasons explained in the
  manual.


[memprof-limits] https://gitlab.com/gadmm/memprof-limits

[a guide on how to recover from asynchronous exceptions and other
unexpected exceptions] https://gitlab.com/gadmm/memprof-limits#recover

[this other post]
https://discuss.ocaml.org/t/todays-trick-memory-limits-with-gc-alarms/4431

[a nice post by Simon Marlow]
https://simonmar.github.io/posts/2017-01-24-asynchronous-exceptions.html

FAQ
╌╌╌

◊ “Is it wise to rely on the statistical nature of Memprof? If I set an allocation limit of 100 KB, and run a function that allocates exactly 50 KB, then the function might fail, due to the random nature of Memprof.”

  Memprof-limits is provided with a [statistical analysis] meant to help
  you chose appropriate values for the limit depending on a target safe
  allocation value. (Nice pictures omitted because this discuss does not
  support svg.)

  Long story short, memprof-limits starts being accurate-enough starting
  around a safe allocation value of 100 KB with the default sampling
  rate (meaning a limit of 1 to 3 MB depending on chosen precision),
  with the ratio between the maximal safe allocation and the limit
  dropping very quickly for higher values. Correctly, the analysis shows
  that limits under 500 KB are unreliable.

  I have found that the statistical nature of Memprof makes it very easy
  to reason about its application and not have to factor in runtime
  implementation details. In addition, Memprof is nevertheless
  deterministic, which is (essential and) useful for reproducing runs in
  test scenarios.


  [statistical analysis]
  https://gitlab.com/gadmm/memprof-limits#statistical


◊ “But can we really program with memprof-limits, that is, not only write programs but also reason about them, given the probabilistic nature of the guarantees?”

  Yes, if we make two additional hypotheses:

  1. Allocation limits (as used in Haskell) are used by determining peak
     reasonable allocation usage empirically and picking a limit at a
     comfortable margin over it, rather than computing a precise memory
     bound to be used as a limit. In very controlled environments where
     the latter would be possible, there probably would be better
     solutions, and the language this is inspired from makes it very
     hard to make predictions on memory use.
  2. The programmer is fine with a very unlikely possibility of a false
     positive; indeed the program is already designed to let true
     positives fail without bringing down mission-critical parts of the
     program. For instance they can prefer to see a legitimate client
     having a connexion closed once every 10ⁿ year for *n* of their
     choosing, if that is the price to pay for avoiding being subject to
     DOS on maliciously-crafted requests.

  Under these hypotheses, the statistical limit is just as reliable as
  the precise limits à la Haskell.


◊ “Is it possible to also implement _local memory limits_, to bound the memory consumption of a particular function?”

  Yes but read on.

  [Yang & Mazières (2014)] advocates in favour of an _allocator-pays_
  model of cost attribution, and note its similarity with memory
  profiling. In this model, it is possible for instance to process
  untrusted user input under some memory limit, before the result is
  distributed to the rest of the program.

  Implementing memory limits based on the allocator-pays model, by
  adapting allocation limits to take into account deallocations, would
  be very easy thanks to the facilities provided by Memprof. Moreover,
  the statistical analysis of allocation limits can be transposed, and
  guarantees similarly accuracy at a low runtime cost for limits greater
  than 100KB.

  There is one surprising difficulty, though, which has to do with the
  way the GC works. The GC has a space overhead: memory that is wasted
  because unreachable values are not collected immediately. This
  overhead has to be taken into account when choosing the
  limit. However, this overhead is non-local and dependent on the
  _total_ major heap size: one cannot just say “take the double of the
  desired limit”. Indeed, active threads will pay for memory that has
  been allocated in the past and kept alive. More experimentation is
  needed to provide guidance on how to take the space overhead into
  account.


  [Yang & Mazières (2014)]
  https://dl.acm.org/doi/10.1145/2594291.2594341


◊ “Can this be used to bound the consumption of lightweight threads in Lwt and Async?”

  It is straightforward to make memprof-limits parametric in the notion
  of _thread id_ used to track per-thread limits.  However, to the best
  of my knowledge, Lwt and Async are not meant to play well when the
  computation is interrupted by asynchronous exceptions. If you have
  more information about this limitation or are interested in
  experimenting, please get in touch.


Thanks
╌╌╌╌╌╌

  Thank you to Jacques-Henri Jourdan for his explanations about Memprof
  and Stephen Dolan for his feedback.


Tezos 7.0 is now available on opam
══════════════════════════════════

  Archive:
  [https://discuss.ocaml.org/t/ann-tezos-7-0-is-now-available-on-opam/5764/1]


Pierre Boutillier announced
───────────────────────────

  Tezos executables and libraries have just been released on `opam'. You
  can thus build them from source with a simple `opam install tezos' and
  build your own projects upon them.


What is Tezos
╌╌╌╌╌╌╌╌╌╌╌╌╌

  Tezos is a distributed consensus platform with meta-consensus
  capability. Tezos not only comes to consensus about the state of its
  ledger, like Bitcoin or Ethereum. It also comes to consensus about how
  the protocol and the nodes should adapt and upgrade. For more
  information about the project, see [https://tezos.com].

  Our implementation of Tezos is written in OCaml. It is split into
  several libraries (command-line interface `tezos-clic', peer-to-peer
  library `tezos-p2p', cryptographic primitives `tezos-crypto~…) and
  executables (node ~tezos-node', client ~tezos-client~…).


Useful Links
╌╌╌╌╌╌╌╌╌╌╌╌

  Source code for this particular implementation can be found at
  [https://gitlab.com/tezos/tezos/]. Developer documentation is
  available at [https://tezos.gitlab.io/]. In particular, documentation
  for this specific release (version 7.0) is available at
  [http://tezos.gitlab.io/releases/version-7.html].


Installation Instructions
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  Tezos (internal compiler in order to self amend itself) requires a
  specific version of the compiler (OCaml 4.09.1):

  ┌────
  │ opam switch 4.09.1
  └────

  Tezos also requires some external libraries:

  ┌────
  │ opam depext tezos
  └────

  Finally, to install all binaries:

  ┌────
  │ opam install tezos
  └────


Replying to Nick Betteridge, Raphaël Proust said
────────────────────────────────────────────────

  Tezos has a soft-updating mechanism that works (roughly) as follows:

  The network starts with a genesis protocol (“protocol” here means
  “economic protocol”: the rules according to which smart contracts are
  initiated and acted upon, transactions take place, etc.) in which a
  single public key is specified.

  The genesis protocol has no notion of coin, currency, smart-contract,
  etc. Instead, the genesis protocol knows a single operation: a
  protocol injection.

  The protocol injection for genesis requires the operation to be signed
  by the private key that matches the public key of the genesis
  block. And the protocol injection changes, irreversibly, the genesis
  protocol to a new protocol. This new protocol specifies what
  constitutes a valid block to add to the chain.

  In the Tezos blockchain, the protocol injected on top of genesis
  included a notion of coins and an in-protocol voting system to inject
  new protocols based on consensus amongst coin-holders. There is even a
  system to obtain the protocol sources over the blockchain network so
  they can be compiled by each node and dynlinked directly in: you don't
  need to update/restart your node to get the protocol updates. However,
  this is arbitrary: you can start a new block-chain with a different
  protocol.

  For example, you could re-implement Bitcoin (proof-of-work,
  coins+transfer, etc.) as a protocol that you inject on top of
  genesis. Your block chain would have a tezos genesis block, then a
  block that activate your own version of bitcoin, and then the blocks
  would be similar to what you would find on the bitcoin block-chain.

  Of particular interest to you, the protocol you inject can have
  entirely different on-chain notions (e.g., a TCG/CCG with no coins at
  all but a notion of ownership over cards) and different soft-updating
  mechanism (e.g., the new protocol can accept genesis-style updates (a
  “dictatorship” where a single person controls the protocol) or even no
  soft-updating mechanism at all (a “stale” protocol where you need to
  hard-fork if you want to make significant changes)).

  For this use case (of starting your own chain with a different
  protocol), you might be better off cloning the git repository, doing
  some minimal clean up, etc. This is because the tezos binaries include
  the sources for all protocols that have been used on the chain (so you
  don't *need* to get them over the network even if you can).

  You might be interested in the following blog post about how to write
  your own protocol:
  [https://blog.nomadic-labs.com/how-to-write-a-tezos-protocol.html]


Official OCaml bindings for verified Everest cryptography
═════════════════════════════════════════════════════════

  Archive:
  [https://sympa.inria.fr/sympa/arc/caml-list/2020-05/msg00017.html]


Jonathan Protzenko announced
────────────────────────────

  The Everest team is pleased to announce the release of official OCaml
  bindings for all of our verified cryptographic algorithms, now
  available through OPAM as packages hacl-star and hacl-star-raw.

  We provide bindings for the following:
  • HACL*, a library of pure C algorithms
  • Vale, a collection of optimized core assembly routines for maximum
    performance
  • EverCrypt, an agile, multiplexing API with CPU auto-detection that
    brings together HACL* and Vale.

  Our code is compiled from the F* programming language to C via the
  KReMLin compiler ("K&R meets ML"). We offer two OPAM packages:
  • hacl-star-raw consists of low-level ocaml-ctypes bindings generated
    by KReMLin
  • hacl-star is a hand-written OCaml idiomatic API that uses much more
    pleasant signatures, types and abstractions and is also safer, as it
    checks all static preconditions at run-time

  We support AES{128,256}-GCM, Chacha20-Poly1305, Curve25519 / Ed25519,
  P256, MD5, SHA-{1,2,3} (all variants), Blake2 (s&b), HMAC/HKDF, and
  the HPKE and SecretBox high-level APIs. Some algorithms are optimized
  for Intel chips, notably AES-GCM – see
  [https://hacl-star.github.io/Supported.html] for full details.

  General documentation about the project is available at
  [https://hacl-star.github.io/index.html] – sample code for the OCaml
  API is provided as part of the test suite
  [https://github.com/project-everest/hacl-star/tree/master/bindings/ocaml/tests]

  This work was performed by Victor Dumitrescu from Nomadic Labs, one of
  the teams responsible for the core development of the Tezos
  blockchain.


nmea and sail-gadgets
═════════════════════

  Archive: [https://discuss.ocaml.org/t/ann-nmea-sail-gadgets/5773/1]


Davide Gessa announced
──────────────────────

  Ahoy developers, few days ago I published a new ocaml library called
  *nmea*, which is essentially a parser for NMEA0183 sentences, a format
  for encoding instruments data in boats. There are many sentences,
  regarding GPS, compass data, wind, air pressure, water temperature,
  waypoints handling, ais, autopilot and more; at the moment the library
  is able to decode GPS sentences and compass data, but I'll implement
  more sentences in the spare time. I tested it with my boat GPS and
  with a gps usb dongle.

  After that, I started a new tiny experiment called *sail-gadgets*,
  which is a Gtk program that elaborates and displays NMEA data received
  from various boat instruments (wind vane, autopilot, gps, radar, ais,
  etc). Sail-gadgets can be extended with "gadgets" modules, each one
  providing new functionalities and new tabs to the main interface.

  Data from sensors are handled using /React/ signals, so in every
  gadget we can compose data from various sensor to obtain new reactive
  values.

  The gadgets I'm planning to write:
  • dashboard: shows current position, speed, heading, tripdist, compass
  • satview: shows current connected gps satellites (partially done)
  • wind: shows wind indicator with true / apparent speed and direction
  • radar: shows AIS and Radar targets in range
  • mob: allows to drop a marker in the current position, and drive you
    to that point
  • startline: helper for regatta start
  • track: shows current track in a vector map

  The hard thing in my opinion is writing new custom widget with cairo
  (compass, radar, and things like that).

  Finally, the project is intended to run over *gtk-broadway*, so every
  html5 enabled device can access the application.

  [https://raw.githubusercontent.com/dakk/sail-gadgets/master/media/broadway.jpg]

  Hope there are some sailor here that want to join writing some gadgets
  :) Repos are:

  • [https://github.com/dakk/nmea]
  • [https://github.com/dakk/sail-gadgets]


Is there specialized math library for statistics?
═════════════════════════════════════════════════

  Archive:
  [https://discuss.ocaml.org/t/is-there-specialized-math-library-for-statistics/5778/1]


hss asked
─────────

  I searched to find math library which is written in OCaml, but there
  are only few repositories.

  I'd like to use some function like coefficient correlation,
  covariance, etc.

  I found Lacaml but it seems not to support them.

  Could you give some link if you know?


bnguyenvanyen replied
─────────────────────

  Hi, you can take a look at Owl : [https://ocaml.xyz/]

  There are stat functions and also a lot more


UnixJunkie also replied
───────────────────────

  There is also this one:
  [https://github.com/superbobry/pareto]
  GSL powered OCaml statistics library
  [http://superbobry.github.io/pareto/0.2]

  And probably even some more:
  ┌────
  │ opam search statistic
  │ # Packages matching: match(*statistic*)
  │ # Name            # Installed # Synopsis
  │ [...]
  │ gsl               --          GSL - Bindings to the GNU Scientific Library
  │ oml               --          Math Library
  │ owl               --          OCaml Scientific and Engineering Computing
  │ owl-plplot        --          OCaml Scientific and Engineering Computing
  │ pareto            --          GSL powered OCaml statistics library.
  │ statsd-client     --          StatsD client library
  │ [...]
  └────


New OCaml books?
════════════════

  Archive: [https://discuss.ocaml.org/t/new-ocaml-books/5789/1]


Axel Wintermann asked
─────────────────────

  I wonder, why there are no new OCaml books since 2014 year? Many books
  are published on Haskell, Scala, F# themes, but no OCaml. I think we
  need new books for learning and for rising interest in our beautiful
  language.


Takuma Ishikawa replied
───────────────────────

  • There is an ongoing work for 2nd edition of Real World OCaml:
    [http://dev.realworldocaml.org/].
  • OCaml Scientific Computing is also ongoing:
    [https://ocaml.xyz/book/].
  • A Japanese book "コンピュータを操る", published in Feb. 2020 for
    beginners of programming, uses OCaml Blockly:
    [https://www.saiensu.co.jp/search/?isbn=978-4-7819-1470-1&y=2020#detail].


Weng Shiwei also replied
────────────────────────

  A Chinese book [OCaml语言编程基础教程] ([an introduction to OCaml
  language programming]) is published in 2018.


[OCaml语言编程基础教程] https://e.jd.com/30417662.html

[an introduction to OCaml language programming]
https://caml.inria.fr/about/books.en.html#idm277


Other OCaml News
════════════════

From the ocamlcore planet blog
──────────────────────────────

  Here are links from many OCaml blogs aggregated at [OCaml Planet].

  • [Every proof assistant: MMT]


[OCaml Planet] http://ocaml.org/community/planet/

[Every proof assistant: MMT]
http://math.andrej.com/2020/05/15/mmt-a-foundation-independent-logical-system/


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]


[send me a message] mailto:alan.schmitt@polytechnique.org

[the archive] http://alan.petitepomme.net/cwn/

[RSS feed of the archives] http://alan.petitepomme.net/cwn/cwn.rss

[online] http://lists.idyll.org/listinfo/caml-news-weekly/

[Alan Schmitt] http://alan.petitepomme.net/