[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

Alan Schmitt
2020-05-19T09:52:56Z

[-- Attachment #1: Type: text/plain, Size: 26620 bytes --]

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/

[-- Attachment #2: Type: text/html, Size: 42565 bytes --]