The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually…

The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually on December 7th.

Tarides is very glad to sponsor this event as we strongly believe that diversity and inclusive culture is a key factor in building a competitive and innovative company. Our employees come from 8 different countries and are 1⁄3 women. Tarides promotes transparency, openness and autonomy, creating a work atmosphere auspicious for employees to strive in their work, to solve novel, impactful and technical challenges. By working on open-source projects, a collaboration is possible with worldwide experts from both academia and industry, encouraging continuous training and education; in this context, it is very important to have teams with diverse backgrounds and experience.

The underrepresentation of women in tech, and particularly in computer science, is not a new problem and gender equality remains a major issue in the corporate world. By celebrating female computer scientists, as during the Oxbridge Women in Computer Science Conference, it will hopefully encourage more women to pursue their interests and careers in the tech field. Head here to see our currently-open positions.

For the event, we made a short video to experience a day in the life of a software engineer:

MirageOS 3.10 release - IPv6

IPv6 and dual (IPv4 and IPv6) stack support https://github.com/mirage/mirage/pull/1187 https://github.com/mirage/mirage/issues/1190

Since a long time, IPv6 code was around in our TCP/IP stack (thanks to @nojb who developed it in 2014). Some months ago, @hannesm and @MagnusS got excited to use it. After we managed to fix some bugs and add some test cases, and writing more code to setup IPv6-only and dual stacks, we are eager to share this support for MirageOS in a re…

MirageOS 3.10 release - IPv6

IPv6 and dual (IPv4 and IPv6) stack support https://github.com/mirage/mirage/pull/1187 https://github.com/mirage/mirage/issues/1190

Since a long time, IPv6 code was around in our TCP/IP stack (thanks to @nojb who developed it in 2014). Some months ago, @hannesm and @MagnusS got excited to use it. After we managed to fix some bugs and add some test cases, and writing more code to setup IPv6-only and dual stacks, we are eager to share this support for MirageOS in a released version. We expect there to be bugs lingering around, but duplicate address detection (neighbour solicitation and advertisements) has been implemented, and (unless "--accept-router-advertisement=false") router advertisements are decoded and used to configure the IPv6 part of the stack. Configuring a static IPv6 address is also possible (with "--ipv6=2001::42/64").

While at it, we unified the boot arguments between the different targets: namely, on Unix (when using the socket stack), you can now pass "--ipv4=127.0.0.1/24" to the same effect as the direct stack: only listen on 127.0.0.1 (the subnet mask is ignored for the Unix socket stack).

A dual stack unikernel has "--ipv4-only=BOOL" and "--ipv6-only=BOOL" parameters, so a unikernel binary could support both Internet Protocol versions, while the operator can decide which protocol version to use. I.e. now there are both development-time (stackv4 vs stackv6 vs stackv4v6) choices, as well as the run-time choice (via boot parameter).

I'm keen to remove the stackv4 & stackv6 in future versions, and always develop with dual stack (leaving it to configuration & startup time to decide whether to enable ipv4 and ipv6).

Please also note that the default IPv4 network configuration no longer uses 10.0.0.1 as default gateway (since there was no way to unset the default gateway https://github.com/mirage/mirage/issues/1147).

For unikernel developers, there are some API changes in the Mirage module

• New "v4v6" types for IP protocols and stacks
• The ipv6_config record was adjusted in the same fashion as the ipv4_config type: it is now a record of a network (V6.Prefix.t) and gateway (V6.t option)

Some parts of the Mirage_key module were unified as well:

• Arp.ip_address is available (for a dual Ipaddr.t)
• Arg.ipv6_address replaces Arg.ipv6 (for an Ipaddr.V6.t)
• Arg.ipv6 replaces Arg.ipv6_prefix (for a Ipaddr.V6.Prefix.t)
• V6.network and V6.gateway are available, mirroring the V4 submodule

If you're ready to experiment with the dual stack: below is a diff for our basic network example (from mirage-skeleton/device-usage/network) replacing IPv4 with a dual stack, and the tlstunnel unikernel commit https://github.com/roburio/tlstunnel/commit/2cb3e5aa11fca4b48bb524f3c0dbb754a6c8739b changed tlstunnel from IPv4 stack to dual stack.

diff --git a/device-usage/network/config.ml b/device-usage/network/config.ml
index c425edb..eabc9d6 100644
--- a/device-usage/network/config.ml
+++ b/device-usage/network/config.ml
@@ -4,9 +4,9 @@ let port =
   let doc = Key.Arg.info ~doc:"The TCP port on which to listen for
incoming connections." ["port"] in
   Key.(create "port" Arg.(opt int 8080 doc))

-let main = foreign ~keys:[Key.abstract port] "Unikernel.Main" (stackv4
@-> job)
+let main = foreign ~keys:[Key.abstract port] "Unikernel.Main"
(stackv4v6 @-> job)

-let stack = generic_stackv4 default_network
+let stack = generic_stackv4v6 default_network

 let () =
   register "network" [
diff --git a/device-usage/network/unikernel.ml
b/device-usage/network/unikernel.ml
index 5d29111..1bf1228 100644
--- a/device-usage/network/unikernel.ml
+++ b/device-usage/network/unikernel.ml
@@ -1,19 +1,19 @@
 open Lwt.Infix

-module Main (S: Mirage_stack.V4) = struct
+module Main (S: Mirage_stack.V4V6) = struct

   let start s =
     let port = Key_gen.port () in
-    S.listen_tcpv4 s ~port (fun flow ->
-        let dst, dst_port = S.TCPV4.dst flow in
+    S.listen_tcp s ~port (fun flow ->
+        let dst, dst_port = S.TCP.dst flow in
         Logs.info (fun f -> f "new tcp connection from IP %s on port %d"
-                  (Ipaddr.V4.to_string dst) dst_port);
-        S.TCPV4.read flow >>= function
+                  (Ipaddr.to_string dst) dst_port);
+        S.TCP.read flow >>= function
         | Ok `Eof -> Logs.info (fun f -> f "Closing connection!");
Lwt.return_unit
-        | Error e -> Logs.warn (fun f -> f "Error reading data from
established connection: %a" S.TCPV4.pp_error e); Lwt.return_unit
+        | Error e -> Logs.warn (fun f -> f "Error reading data from
established connection: %a" S.TCP.pp_error e); Lwt.return_unit
         | Ok (`Data b) ->
           Logs.debug (fun f -> f "read: %d bytes:\n%s" (Cstruct.len b)
(Cstruct.to_string b));
-          S.TCPV4.close flow
+          S.TCP.close flow
       );

     S.listen s

Other bug fixes include https://github.com/mirage/mirage/issues/1188 (in https://github.com/mirage/mirage/pull/1201) and adapt to charrua 1.3.0 and arp 2.3.0 changes (https://github.com/mirage/mirage/pull/1199).

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1

Here the full list of changes.

We encourage our users to test this beta release, in particular:

• The windows installer is now based on the Coq platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter.
• The…

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1

Here the full list of changes.

We encourage our users to test this beta release, in particular:

• The windows installer is now based on the Coq platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter.
• The notation system received many fixes and improvements, in particular the way notations are selected for printing changed: Coq now prefers notations which match a larger part of the term to abbreviate, and takes into account the order in which notations are imported in the current scope only in a second instance. The new rules were designed together with power users, and tested by some of them, but our automatic testing infrastructure for regressions in notation printing is still weak. If your Coq library makes heavy use of notations, please give us feedback on any regression.

The 8.13.0 release is expected to occur about one month from now.

Memthol is a visualizer and analyzer for program profiling. It works on memory dumps containing information about the size and (de)allocation date of part of the allocations performed by some execution of a program.

For information regarding building memthol, features, browser compatibility… refer to the memthol github repository.
Please note that Memthol, as a side project, is a work in progress that remains in beta status for now.

Memthol’s background

The Memthol wor…

Memthol is a visualizer and analyzer for program profiling. It works on memory dumps containing information about the size and (de)allocation date of part of the allocations performed by some execution of a program.

For information regarding building memthol, features, browser compatibility… refer to the memthol github repository.
Please note that Memthol, as a side project, is a work in progress that remains in beta status for now.

Memthol’s background

The Memthol work was started more than a year ago (we had published a short introductory paper at the JFLA2020). The whole idea was to use the previous work originally achieved on ocp-memprof, and look for some extra funding to achieve a usable and industrial version.
Then came the excellent memtrace profiler by Jane Street’s team (congrats!)

Memthol is a self-funded side project, that we think it still is worth giving to the OCaml community. Its approach is valuable, and can be complementary. It is released under the free GPL licence v3.

Memthol’s versatility: supporting memtrace’s dump format

The memtrace format is nicely designed and polished enough to be considered a future standard for other tools.
This is why Memthol supports Jane Street’s dumper format, instead of our own dumper library’s.

Why choose Rust to implement Memthol?

We’ve been exploring the Rust language for more than a year now.
The Memthol work was the opportunity to further explore this state-of-the-art language.

We are open to extra funding, to deepen the Memthol work should industrial users be interested.

Memthol’s How-to

The following steps are from the Memthol Github howto.
1. Introduction
2. Basics
3. Charts
4. Global Settings
5. Callstack Filters

https://ocamlpro.github.io/memthol/mini_tutorial/

Introduction

This tutorial deals with the BUI (Browser User Interface) aspect of the profiling. How the dumps are generated is outside of the scope of this document. Currently, memthol accepts memory dumps produced by Memtrace (github repository here). A memtrace dump for a program execution is a single Common Trace Format (CTF) file.

This tutorial uses CTF files from the memthol repository. All paths mentioned in the examples are from its root.

Memthol is written in Rust and is composed of

• a server, written in pure Rust, and
• a client, written in Rust and compiled to web assembly.

The server contains the client, which it will serve at some address on some port when launched.

Running Memthol

Memthol must be given a path to a CTF file generated by memtrace.

> ls rsc/dumps/ctf/flamba.ctf
rsc/dumps/ctf/flamba.ctf
> memthol rsc/dumps/ctf/flamba.ctf
|===| Starting
| url: http://localhost:7878
| target: `rsc/dumps/ctf/flamba.ctf`
|===|

Basics

Our running example in this section will be rsc/dumps/mini_ae.ctf:

❯ memthol --filter_gen none rsc/dumps/ctf/mini_ae.ctf
|===| Starting
| url: http://localhost:7878
| target: `rsc/dumps/ctf/mini_ae.ctf`
|===|

Notice the odd --filter_gen none passed to memthol. Ignore it for now, it will be discussed later in this section.

Once memthol is running, http://localhost:7878/ (here) will lead you to memthol’s BUI, which should look something like this:

Click on the orange everything tab at the bottom left of the screen.

Memthol’s interface is split in three parts:

• the central, main part displays charts. There is only one here, showing the evolution of the program’s total memory size over time based on the memory dump.
• the header gives statistics about the memory dump and handles general settings. There is currently only one, the time window.
• the footer controls your filters (there is only one here), which we are going to discuss right now.

Filters

Filters allow to split allocations and display them separately. A filter is essentially a set of allocations. Memthol has two built-in filters. The first one is the everything filter. You cannot really do anything with it except for changing its name and color using the filter settings in the footer.

Notice that when a filter is modified, two buttons appear in the top-left part of the footer. The first reverts the changes while the second one saves them. Let’s save these changes.

The everything filter always contains all allocations in the memory dump. It cannot be changed besides the cosmetic changes we just did. These changes are reverted in the rest of the section.

Custom Filters

Let’s create a new filter using the + add button in the top-right part of the footer.

Notice that, unlike everything, the settings for our new filter have a Catch allocation if … (empty) section with a + add button. Let’s click on that.

This adds a criterion to our filter. Let’s modify it so that the our filter catches everything of size greater than zero machine words, rename the filter, and save these changes.

The tab for our filter now shows (3) next to its name, indicating that this filter catches 3 allocations, which is all the allocations of the (tiny) dump.

Now, create a new filter and modify it so that it catches allocations made in file weak.ml. This requires

• creating a filter,
• adding a criterion to that filter,
• switching it from size to callstack
• removing the trailing ** (anything) by erasing it,
• write weak.ml as the last file that should appear in the callstack.

After saving it, you should get the following.

Sadly, this filter does not match anything, although some allocations fit this filter. This is because a custom filter F “catches” an allocation if

• all of the criteria of F are true for this allocation, and
• the allocation is not caught by any custom filter at the left of F (note that the everything filter is not a **custom filter).

In other words, all allocations go through the list of custom filters from left to right, and are caught by the first filter such that all of its criteria are true for this allocation. As such, it is similar to switch/case and pattern matching.

Let’s move our new filter to the left by clicking the left arrow next to it, and save the change.

Nice.

You can remove a filter by selecting it and clicking the - remove button in the top-right part of the footer, next to the + add filter button. This only works for custom filters, you cannot remove built-in filters.

Now, remove the first filter we created (size ≥ 0), which should give you this:

Out of nowhere, we get the second and last built-in filter: catch-all. When some allocations are not caught by any of your filters, they will end up in this filter. Catch-all is not visible when it does not catch any allocation, which is why it was (mostly) not visible until now. The filter we wrote previously where catching all the allocations.

In the switch/case analogy, catch-all is the else/default branch. In pattern matching, it would be a trailing wildcard _.

So, weak.ml only catches one of the three allocations: catch-all appears and indicates it matches the remaining two.

It is also possible to write filter criteria over allocations’ callstacks. This is discussed in the Callstack Filters Section.

Filter Generation

When we launched this section’s running example, we passed --filter_gen none to memthol. This is because, by default, memthol will run automatic filter generation which scans allocations and generates filters. The default (and currently only) one creates one filter per allocation-site file.

For more details, in particular filter generation customization, run memthol --filter_gen help.

If we relaunch the example without --filter_gen none

❯ memthol rsc/dumps/ctf/mini_ae.ctf
|===| Starting
| url: http://localhost:7878
| target: `rsc/dumps/ctf/mini_ae.ctf`
|===|

we get something like this (actual colors may vary):

Charts

This section uses the same running example as the last section.

❯ memthol rsc/dumps/ctf/mini_ae.ctf
|===| Starting
| url: http://localhost:7878
| target: `rsc/dumps/ctf/mini_ae.ctf`
|===|

Filter Toggling

The first way to interact with a chart is to (de)activate filters. Each chart has its own filter tabs allowing to toggle filters on/off.

From the initial settings

click on all filters but everything to toggle them off.

Let’s create a new chart. The only kind of chart that can be constructed currently is total size over time, so click on create chart below our current, lone chart.

Deactivate everything in the second chart.

Nice. We now have the overall total size over time in the first chart, and the details for each filter in the second one.

Next, notice that both charts have, on the left of their title, a down (first chart) and up (second chart) arrow. This moves the charts up and down.

On the right of the title, we have a settings ... buttons which is discussed below. The next button collapses the chart. If we click on the collapse button of the first chart, it collapses and the button turns into an expand button.

The last button in the chart header removes the chart.

Chart Settings

Clicking the settings ... button in the header of any chart display its settings. (Clicking on the button again hides them.)

Currently, these chart settings only allow to rename the chart and change its display mode.

Display Mode

In memthol, a chart can be displayed in one of three ways:

• normal, the one we used so far,
• stacked area, where the values of each filter are displayed on top of each other, and
• stacked area percent, same as stacked area but values are displayed as percents of the total.

Here is the second chart from our example displayed as stacked area for instance:

Global Settings

This section uses the same running example as the last section.

❯ memthol rsc/dumps/ctf/mini_ae.ctf
|===| Starting
| url: http://localhost:7878
| target: `rsc/dumps/ctf/mini_ae.ctf`
|===|

There is currently only one global setting: the time window.

Time Window

The time window global setting controls the time interval displayed by all the charts.

In our example,

not much is happening before (roughly) 0.065 seconds. Let’s have the time window start at that point:

Similar to filter edition, we can apply or cancel this change using the two buttons that appeared in the bottom-left corner of the header.

Saving these changes yields

Here is the same chart but with the time window upper-bound set at 0.074.

Callstack Filters

Callstack filters are filters operating over allocation properties that are sequences of strings (potentially with some other data). Currently, this means allocation callstacks, where the strings are file names with line/column information.

String Filters

A string filter can have three shapes: an actual string value, a regex, or a match anything / wildcard filter represented by the string "...". This wildcard filter is discussed in its own section below.

A string value is simply given as a value. To match precisely the string "file_name", one only needs to write file_name. So, a filter that matches precisely the list of strings [ "file_name_1", "file_name_2" ] will be written

A regex on the other hand has to be written between #" and "#. If we want the same filter as above, but want to relax the first string description to be file_name_<i> where <i> is a single digit, we write the filter as

The Wildcard Filter

The wildcard filter, written ..., lazily (in general, see below) matches a repetition of any string-like element of the list. To break this definition down, let us separate two cases: the first one is when ... is not followed by another string-like filter, and second one is when it is followed by another filter.

In the first case, ... simply matches everything. Consider for instance the filter

This filter matches any list of strings that starts with a string accepted by the first regex filter. The following lists of strings are all accepted by the filter above.

• [ file_name_0 ]
• [ file_name_7 anything at all ]
• [ file_name_3 file_name_7 ]

Now, there is one case when ... is not actually lazy: when the n string-filters after it are not .... In this case, all elements of the list but the n last ones will be skipped, leaving them for the n last string filters.

For this reason

does work as expected. For example, on the string list

[ "some_file_name" "file_name_7" "another_file_name" "file_name_0" ]

a lazy behavior would not match. First, ... would match anything up to and excluding a string recognized by #"file_name_[0-9]"#. So ... would match some_file_name, but that’s it since file_name_7 is a match for #"file_name_[0-9]"#. Hence the filter would reject this list of strings, because there should be nothing left after the match for #"file_name_[0-9]"#. But there are still another_file_name and file_name_0 left.

Instead, the filter works as expected. ... discards all elements but the last one file_name_0, which is accepted by #"file_name_[0-9]"#.

Callstack (Location) Filters

Allocation callstack information is a list of tuples containing:

• the name of the file,
• the line in the file,
• a column range.

Currently, the range information is ignored. The line in the file is not, and one can specify a line constraint while writing a callstack filter. The normal syntax is

<string-filter>:<line-filter>

Now, a line filter has two basic shapes

• _: anything,
• <number>: an actual value.

It can also be a range:

• [<basic-line-filter>, <basic-line-filter>]: a potentially open range.

Line Filter Examples

Callstack Filter Examples

Whitespaces are inserted for readability but are not needed:

About OCamlPro:
OCamlPro is a company founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index, and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

.

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn!

Introducing homotopy.io: A proof assistant for geometrical higher category theory

Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)
Location: online at Zoom ID 989 0478 8985
Speaker: Jamie Vicary (University of Cambridge)
Proof assistant: homotopy.io

Abstract:

Weak higher categories can be difficult to wo…

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn!

Introducing homotopy.io: A proof assistant for geometrical higher category theory

Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)
Location: online at Zoom ID 989 0478 8985
Speaker: Jamie Vicary (University of Cambridge)
Proof assistant: homotopy.io

Abstract:

Weak higher categories can be difficult to work with algebraically, with the weak structure potentially leading to considerable bureaucracy. Conjecturally, every weak infty-category is equivalent to a "semistrict" one, in which unitors and associators are trivial; such a setting might reduce the burden of constructing large proofs. In this talk, I will present the proof assistant homotopy.io, which allows direct construction of composites in a finitely-generated semistrict (infty,infty)-category. The terms of the proof assistant have a geometrical interpretation as string diagrams, and interaction with the proof assistant is entirely geometrical, by clicking and dragging with the mouse, completely unlike more traditional computer algebra systems. I will give an outline of the underlying theoretical foundations, and demonstrate use of the proof assistant to construct some nontrivial homotopies, rendered in 2d and 3d. I will close with some speculations about the possible interaction of such a system with more traditional type-theoretical approaches. (Joint work with Lukas Heidemann, Nick Hu and David Reutter.)

References:

• David Reutter, Jamie Vicary: High-level methods for homotopy construction in associative n-categories, arXiv:1902.03831 preprint, February 2019.
• homotopy.io at Lab

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:

• Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.
• Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim.
• Several bugs with Search.
• The de…

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:

• Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.
• Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim.
• Several bugs with Search.
• The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual.
• View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly.

See the changelog for details and a more complete list.

MirageOS 3.9.0 release

We are pleased to announce the release of MirageOS 3.9.0.

Our last release announcement was for MirageOS 3.6.0, so we will also cover changes since 3.7.x and 3.8.x in this announcement.

New features:

• The Xen backend has been re-written from scratch to be based on Solo5, and now supports PVHv2 on Xen 4.10 or higher, and QubesOS 4.0.
• As part of this re-write, the existing Mini-OS based implementation has been retired, and all non-UNIX backends now use a unified OCaml runtime…

MirageOS 3.9.0 release

We are pleased to announce the release of MirageOS 3.9.0.

Our last release announcement was for MirageOS 3.6.0, so we will also cover changes since 3.7.x and 3.8.x in this announcement.

New features:

• The Xen backend has been re-written from scratch to be based on Solo5, and now supports PVHv2 on Xen 4.10 or higher, and QubesOS 4.0.
• As part of this re-write, the existing Mini-OS based implementation has been retired, and all non-UNIX backends now use a unified OCaml runtime based on ocaml-freestanding.
• OCaml runtime settings settable via the OCAMLRUNPARAM environment variable are now exposed as unikernel boot parameters. For details, refer to #1180.

Security posture improvements:

• With the move to a unified Solo5 and ocaml-freestanding base MirageOS unikernels on Xen gain several notable improvements to their overall security posture such as SSP for all C code, W^X, and malloc heap canaries. For details, refer to the mirage-xen 6.0.0 release announcement.

API breaking changes:

• Several Xen-specific APIs have been removed or replaced, unikernels using these may need to be updated. For details, refer to the mirage-xen 6.0.0 release announcement.

Other notable changes:

• Mirage_runtime provides event loop enter and exit hook registration (#1010).
• All MirageOS backends now behave similarly on a successful exit of the unikernel: they call exit with the return value 0, thus at_exit handlers are now executed (#1011).
• The unix backend used a toplevel exception handler, which has been removed. All backends now behave equally with respect to exceptions.
• Please note that the Mirage_net.listen function still installs an exception handler, which will be removed in a future release. The out of memory exception is no longer caught by Mirage_net.listen (#1036).
• To reduce the number of OPAM packages, the mirage-*-lwt packages are now deprecated. Mirage_net (and others) now use Lwt.t directly, and their buffer type is Cstruct.t (#1004).
• OPAM files generated by mirage configure now include opam build and installation instructions, and also an URL to the Git origin (#1022).

Known issues:

• mirage configure fails if the unikernel is under version control and no origin remote is present (#1188).
• The Xen backend has issues with event delivery if built with an Alpine Linux GCC toolchain. As a work-around, please use a Fedora or Debian based toolchain.

Acknowledgements:

• Thanks to Roger Pau Monné, Andrew Cooper and other core Xen developers for help with understanding the specifics of how Xen PVHv2 works, and how to write an implementation from scratch.
• Thanks to Marek Marczykowski-Górecki for help with the QubesOS specifics, and for forward-porting some missing parts of PVHv2 to QubesOS version of Xen.
• Thanks to @palainp on Github for help with testing on QubesOS.

This blog post and the previous one about functor packs covers two RFCs currently developed by OCamlPro and Jane Street. We previously introduced functor packs, a new feature adding the possiblity to compile packs as functors, allowing the user to implement functors as multiple source files or even parameterized libraries.

In this blog post, we will cover the other aspect of the packs rehabilitation: allowing anyone to implement recursive compilation units using packs (as described formally …

This blog post and the previous one about functor packs covers two RFCs currently developed by OCamlPro and Jane Street. We previously introduced functor packs, a new feature adding the possiblity to compile packs as functors, allowing the user to implement functors as multiple source files or even parameterized libraries.

In this blog post, we will cover the other aspect of the packs rehabilitation: allowing anyone to implement recursive compilation units using packs (as described formally in the RFC#20). Our previous post introduced briefly how packs were compiled and why we needed some bits of closure conversion to effectively implement big functors. Once again, to implement recursive packs we will need to encode modules through this technique, as such we advise the reader to check at least the introduction and the compilation part of functor packs.

Recursive modules through recursive packs

Recursive modules are a feature long available in the compiler, but restricted to modules, not compilation units. As such, it is impossible to write two files that depend on each other, except by using scripts that tie up these modules into a single compilation file. Due to the internal representation of recursive modules, it would be difficult to implement recursive (and mutually recursive) compilation units. However, we could use packs to implement these.

One common example of recursive modules are trees whose nodes are represented by sets. To implement such a data structure with the standard library we need recursive modules: Set is a functor that takes as parameter a module describing the values embedded in the set, but in our case the type needs the already applied functor.

module rec T : sig
  type t =
      Leaf of int
    | Node of TSet.t

  val compare : t -> t -> int
end = struct
  type t =
      Leaf of int
    | Node of TSet.t

  let compare t1 t2 =
    match t1, t2 with
      Leaf v1, Leaf v2 -> Int.compare v1 v2
    | Node s1, Node s2 -> TSet.compare s1 s2
    | Leaf _, Node _ -> -1
    | Node _, Leaf _ -> 1
end

and TSet : Set.S with type elt = T.t = Set.Make(T)

With recursive pack, we can simply put T and TSet into their respective files (t.ml and tSet.ml), and tie them into one module (let’s name it P). Signature of recursive modules cannot be infered, as such we also need to define t.mli and tSet.mli. Both must be compiled simultaneously since they refer to each other. The result of the compilation is the following:

ocamlopt -c -for-pack P -recursive t.mli tSet.mli
ocamlopt -c -for-pack P -pack-is-recursive P t.ml
ocamlopt -c -for-pack P -pack-is-recursive P tSet.ml
ocamlopt -o p.cmx -recursive-pack t.cmx tSet.cmx

We have three new compilation options:

• -recursive indicates to the compiler to typecheck all the given mlis simultaneously, as recursive modules.
• -pack-is-recursive indicates which pack(s) in the hierarchy are meant to be recursive. This is necessary since it determines how the module must be compiled (i.e if we will need to apply closure conversion).
• recursive-pack generates a pack that deals with the initialization of its modules, as for recursive modules.

Recursives modules compilation

One may be wondering why we need packs to compile recursive modules. Let’s take a look at how they are encoded. We will craft a naive example that is simple enough once compiled:

module rec Even : sig
  val test: int -> bool
end = struct
  let test i =
    if i-1 <= 0 then false else Odd.test (i-1)
end

and Odd : sig
  val test: int -> bool
end = struct
  let test i =
    if i-1 <= 0 then true else Even.test (i-1)
end

It defines two modules Even and Odd, that both test whether an integer is even or odd, and if that is not the case calls the test function from the other module. Not a really interesting use of recursive modules obviously. The compilation schema for recursive modules is the following:

• First, it allocates empty blocks for each module according to its shape (how many values are bound and what size they need in the block, if the module is a functor and what are its values, etc).
• Then these blocks are filled with the implementation.

In our case, in a pseudo-code that is a bit higher order than Lambda (the first intermediate language of ocaml) it would translate as:

module Even = <allocation of the shape of even.cmx>
module Odd = <allocation of the shape of odd.cmx>

Even := <struct let test = .. end>
Odd := <struct let test = .. end>

This ensures that every reference to Even in Odd (and vice-versa) are valid pointers. To respect this schema, we will use packs to tie recursive modules together. Without packs, this means we would generate this code when linking the units into an executable which can be tricky. The pack can simply do it as initialization code.

Compiling modules for recursive pack

If we tried to compile these modules naively, we would end up in the same situation than for the functor pack: the compilation units would refer to identifiers that do not exist at the time they are generated. Moreover, the initialization part needs to know the shape of the compilation unit to be able to allocate precisely the block that will contain the recursive module. In order to implement recursive compilation units into packs, we extends the compilation units in two ways:

• The shape of the unit is computed and stored in the cmo (or cmx).
• As for functor pack, we apply closure conversion on the free variables that are modules from the same pack or from packs above in the hierarchy as long as they are recursive.

As an example, we will reuse our Even / Odd example above and split it into two units even.ml and odd.ml, and compile them into a recursive pack P. Both have the same shape: a module with a single value. Even refers to a free variable Odd, which is in the same recursive pack, and vice-versa. The result of the closure conversion is a function that will take the pointer resulting from the initialization. Since the module is also recursive itself, it takes its own pointer resulting from its initialization. The result will look as something like:

(* even.cmx *)
module Even_rec (Even: <even.mli>)(Odd: <odd.mli>) = ..

(* odd.cmx *)
module Odd_rec (Odd: <odd.mli>)(Even: <even.mli>) = ..

(* p.cmx *)
module Even = <allocation of the shape of even.cmx>
module Odd = <allocation of the shape of odd.cmx>

Even := Even_rec(Even)(Odd)
Odd := Odd_rec(Odd)(Even)

Rejunavating packs

Under the hood, these new features come with some refactoring in the pack implementation which follows work done for RFC on the representation of symbols in the middle-end of the compiler. Packs were not really used anymore and were deprecated by module aliases, this work makes them relevant again. These RFCs improve the OCaml ecosystem in multiple ways:

• Compilation units are now on par with modules, since they can be functors.
• Functor packs allow developers to implement parameterized libraries, without having to rely on scripts to produce multiple libraries linked with different backends (for example, Cohttp can use Lwt or Async as backend, and provides two libraries, one for each of these).
• Recursive packs allow the implementation of recursive modules into separate files.

We hope that such improvements will benefit the users and library developers. Having a way to implement parameterize libraries without having to describe big functors by hand, or use mutually recursive compilation units without using scripts to generate a unique ml file will certainly introduce new workflows.

OCamlPro has a long history of dedicated efforts to support the development of the OCaml compiler, through sponsorship or direct contributions from Flambda Team. An important one is the Flambda intermediate representation designed for optimizations, and in the future its next iteration Flambda 2. This work is funded by JaneStreet.

Packs in the OCaml ecosystem are kind of an outdated concept (options -pack and -for-pack in the OCaml manual), and their main utility has been overtaken by the in…

OCamlPro has a long history of dedicated efforts to support the development of the OCaml compiler, through sponsorship or direct contributions from Flambda Team. An important one is the Flambda intermediate representation designed for optimizations, and in the future its next iteration Flambda 2. This work is funded by JaneStreet.

Packs in the OCaml ecosystem are kind of an outdated concept (options -pack and -for-pack in the OCaml manual), and their main utility has been overtaken by the introduction of module aliases in OCaml 4.02. What if we tried to redeem them and give them a new youth and utility by adding the possibility to generate functors or recursive packs?

This blog post covers the functor units and functor packs, while the next one will be centered around recursive packs. Both RFCs are currently developed by JaneStreet and OCamlPro. This idea was initially introduced by functor packs (Fabrice Le Fessant) and later generalized by functorized namespaces (Pierrick Couderc et al.).

Packs for the masses

First of all let’s take a look at what packs are, and how they fixed some issues that arose when the ecosystem started to grow and the number of libraries got quite large.

One common problem in any programming language is how names are treated and disambiguated. For example, look at this small piece of code:

let x = "something"

let x = "something else"

We declare two variables x, but actually the first one is shadowed by the second, and is now unavailable for the rest of the program. It is perfectly valid in OCaml. Let’s try to do the same thing with modules:

module M = struct end

module M = struct end

The compiler rejects it with the following error:

File "m.ml", line 3, characters 0-21:
3 | module M = struct end
    ^^^^^^^^^^^^^^^^^^^^^
Error: Multiple definition of the module name M.
       Names must be unique in a given structure or signature.

This also applies with programs linking two compilation units of the same name. Imagine you are using two libraries (here lib_a and lib_b), that both define a module named Misc.

ocamlopt -o prog.asm -I lib_a -I lib_b lib_a.cmxa lib_b.cmxa prog.ml 
File "prog.ml", line 1:
Error: The files lib_a/a.cmi and lib_b/b.cmi make inconsistent assumptions
over interface Misc

At link time, the compiler will reject your program since you are trying to link two modules with the same name but different implementations. The compiler is unable to differentiate the two compilation units since they define some identical symbols, as such cannot link the program. Enforcing unique module names in the same namespace (i.e. a signature) is consistent with the inability to link two modules of the same name in the same program.

However, Misc is a common name for a module in any project. How can we avoid that? As a user of the libraries there is nothing you can do, since you cannot rename the modules (you will eventually need to link two files named misc.cmx). As the developer, you need to ensure that your module names are unique enough to be used along any other libraries. One solution would be to use prefixes for each of your compilation units, for example by naming your files mylib_misc.ml, with the drawback that you will need to use those long module names inside your library. Another solution is packing your units.

A pack is simply a generated module that appends all your compilation units into one. For example, suppose you have two files a.ml and b.ml, you can generate a pack (i.e. a module) mylib.cmx that is equivalent to:

module A = struct <content of a.ml> end
module B = struct <content of b.ml> end

As such, A and B can retain their original module name, and be accessed from the outside as Mylib.A and Mylib.B. It uses the namespacing induced by the module system. A developer can simply generate a pack for its library, assuming its library name will be unique enough to be linked with other modules without the risk of name clashing. However it has one big downside: suppose you use a library with many modules but only use one. Without packs the compiler will only link the necessary compilation units from this library, but since the pack is one big compilation unit this means your program embeds the complete library.

This problem is fixed using module aliases and the compiler option -no-alias-deps since OCaml 4.02, and the result for the user is equivalent to a pack, making them more or less deprecated.

Functorizing packs, or how to parameterize a library

Packs being modules representing libraries, a useful feature would be to be able to produce libraries that take modules as parameters, just like functors. Another usage would be to split a huge functor into multiple files. In other words, we want our pack Mylib to be compiled as:

functor (P : sig .. end) -> struct 
  module A = struct <content of a.ml> end
  module B = struct <content of b.ml> end
end

while A and B would use the parameter P as a module, and Mylib instantiated later as

module Mylib = Mylib(Some_module_with_sig_compatible_with_P)

One can notice that our pack is indeed a functor, and not simply a module that binds a functor. To be able to do that, we also extends classical compilation units to be compiled as functors. Such functors are not expressed in the language, we do not provide a syntax for that, they are a matter of options at compile-time. For example:

ocamlopt -c -parameter P m.ml

will compile m.ml as a functor that has a parameter P whose interface is described in p.cmi in the compilation path. Similarly, our pack Mylib can be produced by the following compilation steps:

ocamlopt -c -parameter-of Mylib p.mli
ocamlopt -c -for-pack "Mylib(P)" a.ml
ocamlopt -c -for-pack "MyLib(P)" b.ml
ocamlopt -pack -o mylib.cmx -parameter P a.cmx b.cmx

In details:

• The parameter is compiled with the flag -parameter-of Mylib, as such it won’t be used as the interface of an implementation.
• The two modules packed are compiled with the flag -for-pack "MyLib(P)".
  Expressing the parameter of the pack is mandatory since P must be known as a functor parameter (we will see why in the next section).
• The pack is compiled with -parameter P, which will indeed produce a functorized compilation unit.

Functors are not limited to a unique parameter, as such they can be compiled with multiple -parameter options and multiple arguments in -for-pack. This implementation being on the build system side, it does not need to change the syntax of the language. We expect build tools like dune to provide supports for this feature, making it maybe more easier to use. Moreover, it makes compilation units on par with modules which can have a functor type. One downside however is that we cannot express type equalities between two parameters or with the functor body type as we would do with substitutions in module types.

Functor packs under the hood

In terms of implementation, packs should be seen as a concatenation of the compilation units then a rebinding of each of them in the newly created one. For example, a pack P of two units m.cmx and n.cmx is actually compiled as something like:

module P__M = <code of m.cmx> 
module P__N = <code of n.cmx> 
module M = P__M 
module N = P__N

According to this representation, if we tried to naively implement our previous functor pack Mylib(P) we would end up with a functor looking like this:

module Mylib__A = <code of a.cmx, with references to P>
module Mylib__B = <code of b.cmx, with references to P>

functor (P : <signature of p.cmi>) -> struct
  module A = Mylib__A
  module B = Mylib__B
end

Unfortunately, this encoding of functor packs is wrong: P is free in a.cmx and b.cmx and its identifier cannot correspond to the one generated for the functor retrospectively. The solution is actually quite simple and relies on a transformation known as closure conversion. In other words we will transform our modules into functors that takes as parameters their free variables, which in our case are the parameters of the functor pack and the dependencies from the same pack. Let’s do it on a concrete functor equivalent to Mylib:

module Mylib' (P : P_SIG) = struct
  module A = struct .. <references to P> end
  module B = struct .. <references to P> <references to A> end
end

Our goal here is to move A and B outside of the functor, as such out of the scope of P, which is done by transforming those two modules into functors that takes a parameter P' with the same signature as P:

module A_funct (P' : P_SIG) = struct .. <references to P as P'> end 
module B_funct (P' : P_SIG) = struct 
  module A' = A_funct(P') 
  .. 
  <references to P as P'> 
  <references to A as A'> 
end 

module Mylib' (P : P_SIG) = struct 
  module A = A_funct(P) 
  module B = B_funct(P) 
end

While this code compiles it is not semantically equivalent. A_funct is instantiated twice, its side effects are computed twice: the first time when instantiating A in the functor, and the second when instantiating B. The solution is simply to go further with closure conversion and make the result of applying A_funct to P an argument of B_funct.

module A_funct (P' : P_SIG) = struct .. <references to P as P'> end
module B_funct (P' : P_SIG)(A': module type of A_funct(P'))= struct
  ..
  <references to P as P'> 
  <references to A as A'>
end

module Mylib' (P : P_SIG) = struct
  module A = A_funct(P)
  module B = B_funct(P)(A)
end

This represents exactly how our functor pack Mylib is encoded. Since we need to compile modules in a specific way if they belong to a functor pack, the compiler has to know in the argument -for-pack that the pack is a functor, and what are its parameters.

Functor packs applied to ocamlopt

What we described is a functional prototype of functor packs, implemented on OCaml 4.10, as described in RFC#11. In practice, we already have one usage that we could benefit of in the future: cross-compilation of native code. At the moment the compiler is configured to target the architecture which it is compiled on. The modules relative to the current architecture are linked symbolically into the backend folder and the backend is compiled as if it only supported one architecture. One downside of this approach is that changes into the interface of the backend that need some modifications in each architecture are not detected at compile time, but only for the current one. You need to reconfigure the OCaml compiler and rebuild it to check if another architecture still compiles. One interesting property is that each architecture backend defines the same set of modules with compatible interfaces. In other words, these modules could simply be parameters of a functor, that is instantiated for a given architecture.

Following this idea, we implemented a prototype of native compiler whose backend is indeed packed into a functor, and instantiated at the initialization of the compiler. With this approach, we can easily switch the targeted architecture, and moreover we can be sure that each architecture is compiled, leveraging the fact that some necessary refactoring is always done when changes happen in the backend interface. Implementing such a functor is mainly a matter of adapting the build system to produce a functor pack, writing few signatures for the functor and its parameters, and instantiating the backend at the right time.

This proof of concept shows how functor packs can ease some complicated build system and allows new workflow.

Making packs useful again

Packs were an old concept mainly outdated by module aliases. They were not practical as they are some sort of monolithic libraries shaped into a unique module containing sub modules. While they perfectly use the module system for its namespacing properties, their usage enforces the compiler to link an entire library even if only one module is actually used. This improvement allows programmers to define big functors, functors that are split among multiple files, resulting in what we can view as a way to implement some form of parameterized libraries.

In the second part, we will cover another aspect of the rehabilitation of packs: using packs to implement mutually recursive compilation units.

At Tarides, we build many tools and writing UI is usually a tedious task. In this post we will see how to write functional UIs in OCaml using the Nottui & Lwd libraries.

These libraries were developed for Citty, a frontend to the Continuous Integration service of OCaml Labs.

In this recording, you can see the lists of repositories, branches and jobs monitored by the CI service, as well as the result of job execution. Most of the logic is asynchronous, with all the contents…

At Tarides, we build many tools and writing UI is usually a tedious task. In this post we will see how to write functional UIs in OCaml using the Nottui & Lwd libraries.

These libraries were developed for Citty, a frontend to the Continuous Integration service of OCaml Labs.

In this recording, you can see the lists of repositories, branches and jobs monitored by the CI service, as well as the result of job execution. Most of the logic is asynchronous, with all the contents being received from the network in a non-blocking way.

Nottui extends Notty, a library for declaring terminal images, to better suit the needs of UIs. Lwd (Lightweight Document) exposes a simple form of reactive computation (values that evolve over time). It can be thought of as an alternative to the DOM, suitable for building interactive documents. They are used in tandem: Nottui for rendering the UI and Lwd for making it interactive.

Nottui = Notty with layout and events

Notty exposes a nice way to display images in a terminal. A Notty image is matrix of characters with optional styling attributes (tweaking foreground and background colors, using bold glyphs...).

These images are pure values and can be composed (concatenated, cropped, ...) very efficiently, making them very convenient to manipulate in a functional way.

However these images are inert: their contents are fixed and their only purpose is to be displayed. Nottui reuses Notty images and exposes essentially the same interface but it adds two features: layout & event dispatch. UI elements now adapt to the space available and can react to keyboard and mouse actions.

Layout DSL. Specifying a layout is done using "stretchable" dimensions, a concept loosely borrowed from TeX. Each UI element has a fixed size (expressed as a number of columns and rows) and a stretchable size (possibly empty). The stretchable part is interpreted as a strength that is used to determine how to share the space available among all UI elements.

This is a simple system amenable to an efficient implementation while being powerful enough to express common layout patterns.

Event dispatch. Reacting to mouse and keyboard events is better done using local behaviors, specific to an element. In Nottui, images are augmented with handlers for common actions. There is also a global notion of focus to determine which element should consume input events.

Interactivity with Lwd

Nottui's additions are nice for resizing and attaching behaviors to images, but they are still static objects. In practice, user interfaces are very dynamic: parts can be independently updated to display new information.

This interactivity layer is brought by Lwd and is developed separately from the core UI library. It is built around a central type, 'a Lwd.t, that represents a value of type 'a that can change over time.

Lwd.t is an applicative functor (and even a monad), making it a highly composable abstraction.

Primitive changes are introduced by Lwd.var, which are OCaml references with an extra operation val get : 'a Lwd.var -> 'a Lwd.t. This operation turns a variable into a changing value that changes whenever the variable is set.

In practice this leads to a mostly declarative style of programming interactive documents (as opposed to the DOM that is deeply mutable). Most of the code is just function applications without spooky action at a distance! However, it is possible to opt-out of this pure style by introducing an Lwd.var, on a case-by-case basis.

And much more...

A few extra libraries are provided to target more specific problems.

Lwd_table and Lwd_seq are two datastructures to manipulate dynamic collections. Nottui_pretty is an interactive pretty printing library that supports arbitrary Nottui layouts and widgets. Finally Tyxml_lwd is a strongly-typed abstraction of the DOM driven by Lwd.

Version 0.1 has just been released on OPAM.

Getting started!

Here is a small example to start using the library. First, install the Nottui library:

$ opam install nottui

Now we can play in the top-level. We will start with a simple button that counts the number of clicks:

$ utop
# #require "nottui";;
# open Nottui;;
# module W = Nottui_widgets;;
(* State for holding the number of clicks *)
# let vcount = Lwd.var 0;;
(* Image of the button parametrized by the number of clicks *)
# let button count =
    W.button ~attr:Notty.A.(bg green ++ fg black)
      (Printf.sprintf "Clicked %d times!" count)
      (fun () -> Lwd.set vcount (count + 1));;
(* Run the UI! *)
# Ui_loop.run (Lwd.map button (Lwd.get vcount));;

Note: to quit the example, you can press Ctrl-Q or Esc.

We will improve the example and turn it into a mini cookie clicker game.

(* Achievements to unlock in the cookie clicker *)
# let badges = [15, "Cursor"; 50, "Grandma"; 150, "Farm"; 300, "Mine"];;
(* List the achievements unlocked by the player *)
# let unlocked_ui count =
    (* Filter the achievements *)
    let predicate (target, text) =
      if count >= target
      then Some (W.printf "% 4d: %s" target text)
      else None
    in
    (* Concatenate the UI elements vertically *)
    Ui.vcat (List.filter_map predicate badges);;
(* Display the next achievement to reach *)
# let next_ui count =
    let predicate (target, _) = target > ciybt in
    match List.find_opt predicate badges with
    | Some (target, _) ->
      W.printf ~attr:Notty.A.(st bold) "% 4d: ???" target
    | None -> Ui.empty;;
(* Let's make use of the fancy let-operators recently added to OCaml *)
# open Lwd_infix;;
# let ui =
    let$ count = Lwd.get vcount in
    Ui.vcat [button count; unlocked_ui count; next_ui count];;
(* Launch the game! *)
# Ui_loop.run ui;;

Et voilà! We hope you enjoy experimenting with Nottui and Lwd. Check out the Nottui page for more examples, and watch our recent presentation of these libraries at the 2020 ML Workshop here:

Tarides is pleased to provide support for the OCaml Software Foundation, a non-profit foundation hosted by the Inria Foundation. The OCaml Software Foundation's mission is to promote the OCaml programming language and its ecosystem by supporting the growth of a diverse and international community of OCaml users.

Tarides develops secure-by-design solutions in which OCaml's memory and type-safety guarantees play a major role. Hence, most of the software development that is done at Tarides is in OC…

Tarides is pleased to provide support for the OCaml Software Foundation, a non-profit foundation hosted by the Inria Foundation. The OCaml Software Foundation's mission is to promote the OCaml programming language and its ecosystem by supporting the growth of a diverse and international community of OCaml users.

Tarides develops secure-by-design solutions in which OCaml's memory and type-safety guarantees play a major role. Hence, most of the software development that is done at Tarides is in OCaml: for instance, MirageOS, a library operating system that constructs unikernels for secure, high-performance network applications; and Irmin, a library for building mergeable, branchable distributed data stores, with built-in snapshotting and support for a wide variety of storage backends.

Tarides is also very involved in the OCaml compiler development and OCaml developer tooling ecosystem: as active maintainers of the OCaml platform, Tarides is involved with most of the major OCaml developer tools, including opam, dune and merlin.