• en

OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

1012 blog posts are available. You can read the 30 more recent ones below or view older ones.

MirageOS 4 Released! — Tarides, Mar 29, 2022

Tarides is delighted to announce that MirageOS 4 is finally released! As core contributors to the project, we are proud to have been part of the journey to 4.0.

What is MirageOS? MirageOS is a library operating system that constructs unikernels for fast and secure network applications that work across a variety of cloud computing and mobile platforms. The goal of MirageOS is to give the individual control of their own data and take back control of their privacy.

It achieves these goals in severa…

Read more...

PhD Position at CEA LIST - LSL — Frama-C, Mar 28, 2022

All your metrics belong to influx — Hannes Mehnert (hannes), Mar 08, 2022

Introduction to monitoring

At robur we use a range of MirageOS unikernels. Recently, we worked on improving the operations story thereof. One part is shipping binaries using our reproducible builds infrastructure. Another part is, once deployed we want to observe what is going on.

I first got into touch with monitoring - collecting and graphing metrics - with MRTG and munin - and the simple network management protocol SNMP. From the whole system perspective, I find it crucial that the monitoring…

Read more...

Secure Virtual Messages in a Bottle with SCoP — Tarides, Mar 08, 2022

People love to receive mail, especially from loved ones. It’s heartwarming to read each word as their thoughts touch our deepest feelings. Now imagine someone else reading those private sentiments, like a postal worker. Imagine how violated they’d feel if their postal carrier handed them an open letter with a knowing smile. Of course, people trust that postal employees won’t read their personal correspondence; however, they regularly risk their privacy when sending emails, images, and mess…

Read more...

Research internships in our Tools and Compilers group — Jane Street, Mar 04, 2022

We are excited to announce research internships in our Tools and Compilers group.

Segfault Systems Joins Tarides — Tarides, Mar 01, 2022

We are delighted to announce that Segfault Systems, a spinout from IIT-Madras, is joining Tarides. Tarides has worked closely with Segfault Systems over the last couple of years, most notably on the award-winning Multicore OCaml project and the upstreaming plans for OCaml 5.0. This alliance furthers the goals of Tarides, bringing the compiler and benchmarking expertise of the Segfault team directly into the Tarides organisation.

KC Sivaramakrishnan, CEO & CTO of Segfault Systems says that …

Read more...

OCaml from the Very Beginning now free in HTML and PDF formats — OCaml Book, Feb 18, 2022

Thanks to a grant from the OCaml Software Foundation (ocaml-sf.org), I am able to release my 2013 book OCaml from the Very Beginning free-of-charge in the existing PDF format, and in a new HTML format:

https://johnwhitington.net/ocamlfromtheverybeginning/

The book continues to be available in paperback and Kindle formats from Amazon.

The book has been updated for OCaml 4.14 in all formats.

Permanent Computer Scientist Position at CEA LIST - LSL — Frama-C, Feb 01, 2022

OCaml Labs Joins Tarides — Tarides, Jan 27, 2022

Today I am incredibly delighted to announce that OCaml Labs, a spinout from the University of Cambridge, is joining Tarides. After successfully collaborating on many OCaml projects over the last four years, this alliance will combine the expertise of both groups and enable us to bring OCaml, one of the most advanced programming languages in the world, into mainstream use. Combining forces will accelerate OCaml development and its broader adoption. Furthermore, it will bring the security, portabi…

Read more...

How Jane Street Pairs Interns to Projects and Teams During the Software Engineering Internship — Jane Street, Jan 14, 2022

Software engineering intern candidates often ask how team placement works and how much input incoming interns have over their teams and projects. We know team placement is an important factor for many students when deciding which internship to accept. We’ve spent considerable time and thought on this process in recent years and hope to demystify the experience with this post. 1

  1. This process is used in New York and London. Due to their smaller size Hong Kong’s process is slig…

Read more...

Is every projective setoid isomorphic to a type? — Andrej Bauer, Jan 11, 2022

Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.

We are going to work in pure Martin-Löf type theory and the straightforward propostions-as-types interpretation of logic, so no univalence, propostional truncation and other goodies are available. Our primary objects of interest are setoids, and Agda's…

Read more...

Two new doctors! — Andrej Bauer, Jan 11, 2022

Within a month two of my students defended their theses: Dr. Anja Petković Komel just before Christmas, and Dr. Philipp Haselwarter just yesterday. I am very proud of them. Congratulations!

Philipp's thesis An Effective Metatheory for Type Theory has three parts:

  1. A formulation and a study of the notion of finitary type theories and standard type theories. These are closely related to the general type theories that were developed with Peter Lumsdaine, but are tailored for implementatio…

Read more...

Magic-trace: Diagnosing tricky performance issues easily with Intel Processor Trace — Jane Street, Jan 11, 2022

Intel Processor Trace is a hardware technology that can record all program execution flow along with timing information accurate to around 30ns. As far as I can tell almost nobody uses it, seemingly because capturing the data is tricky and, without any visualization tools, you’re forced to read enormous text dumps.

Monorobot: a Slack bot for monorepos — Ahrefs, Dec 09, 2021

Monorobot: a notification bot for monorepos

Monorobot enables configurable directory tree notifications for your monorepo.

A few years ago, we decided to move most of our code into a monorepo. Many advocates have highlighted its upsides, which include better cross-project coordination and simpler dependency management.

But one problem remained: none of the available GitHub integrations for Slack work nicely with monorepos. Slack is vital for day to day communication among Ahrefs’ globally distrib…

Read more...

opam 2.1.2 release — OCaml Platform (Kate Deplaix - OCaml Labs, David Allsopp - OCaml Labs, Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Dec 08, 2021

We are pleased to announce the minor release of opam 2.1.2.

This opam release consists of backported fixes, including:

  • Fallback on dnf if yum does not exist on RHEL-based systems (#4825)
  • Use --no-depexts in CLI 2.0 mode. This further improves the use of opam 2.1 as a drop-in replacement for opam 2.0 in CI, for example with setup-ocaml in GitHub Actions. (#4908)


Opam installation instructions (unchanged):
  1. From binaries: run

    bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/oc…
Read more...

Release of Frama-C 24.0 (Chromium) — Frama-C, Nov 30, 2021

'Signals and Threads' Podcast: What is an Operating System? — Tarides, Nov 23, 2021

November has become MirageOS month! Between the upcoming official MirageOS 4.0 release, making custom Christmas Tree garlands with MirageOS on a Raspberry Pi, and now this "What is an Operating System?" podcast (featuring Tarides advisor and core MirageOS maintainer Anil Madhavapeddy), it truly is MirageOS month!

MirageOS can do much more than program a Raspberry Pi for Christmas decor. From agricultural monitoring to smart buildings, its applications cover a wide range of needs. For example, it…

Read more...

The proposal for a proof assistants StackExchange site — Andrej Bauer, Nov 19, 2021

Proof assistant communities have grown quite a bit lately. They have active Zulip chats: Lean, Coq, Agda, Isabelle. These are good for discussions, but less so for knowledge accumulation and organization, and are not indexed by the search engines.

I have therefore created a proposal for a new “Proof assistants” StackExchange site. I believe that such a site would complement very well various Zulips dedicated to specific proof assistants. If you favor the idea, please support it by visiting …

Read more...

Tarides & Hyper: Partners in Agricultural Innovation — Tarides, Nov 18, 2021

We are thrilled to announce a partnership between Tarides and Hyper, a technology provider in the agritech space who’s building an "operating system for high-performing farms." Indoor and vertical farms are becoming tech businesses that require scalable, flexible, and easy-to-use tools to facilitate data analysis and thereby increase productivity. According to the State of Indoor Farming 2020 Report, “40% of vertical and indoor farms are implementing data analytics and control automation to …

Read more...

opam releases: 2.0.10, 2.1.1, & opam depext 1.2! — OCaml Platform (David Allsopp - OCamlLabs, Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Nov 15, 2021

Feedback on this post is welcomed on Discuss!

We are pleased to announce several minor releases: opam 2.0.10, opam 2.1.1, and opam-depext 1.2.

The opam releases consist of backported fixes, while opam-depext has been adapted to be compatible with opam 2.1, to allow for workflows which need to maintain compatibility with opam 2.0. With opam 2.1.1, if you export OPAMCLI=2.0 into your environment then workflows expecting opam 2.0 should now behave even more equivalently.

opam-depext 1.2

Previous…

Read more...

MirageOS Workshop: Working with the Raspberry Pi 4 — Tarides, Nov 11, 2021

Earlier this week, Romain Calascibetta hosted an in-house MirageOS workshop for employees, both locally and remotely around the world. This interactive workshop taught participants how to build an operating system on a Raspberry Pi 4 using MirageOS. They got to create their own OS and play with projects, like one they dubbed GuirlandeOS for which they programmed an LED garland to trim their Christmas tree, creating their own customized light show! There will be a dedicated blog to GuirlandeOS so…

Read more...

MirageOS 4.0 Preview Live Presentation — Tarides, Nov 09, 2021

The official release of MirageOS 4.0 quickly approaches! Learn about some general MirageOS concepts and get a sneak park at the forthcoming changes in MirageOS 4.0 during a LIVE presentation today at 15h CET.

Lucas Pluvinage will lead you through a live-streaming presentation to acquaint you with MirageOS 4.0. You’ll learn what kinds of problems MirageOS can solve and about Functoria, the compilation model. Then Lucas will also discuss the switch to the Dune build system and how that enables…

Read more...

Beta release of Frama-C 24.0-beta (Chromium) — Frama-C, Nov 04, 2021

Isolating Xwayland in a VM — Thomas Leonard, Oct 30, 2021

In my last post, Qubes-lite with KVM and Wayland, I described setting up a Qubes-inspired Linux system that runs applications in virtual machines. A Wayland proxy running in each VM connects its applications to the host Wayland compositor over virtwl, allowing them to appear on the desktop alongside normal host applications. In this post, I extend this to support X11 applications using Xwayland.

Table of Contents

Read more...

Hiring a Developer Educator — Jane Street, Oct 21, 2021

We spend a lot of time on education at Jane Street. Like, really a lot.

SCoP Passed Phase 1 of the DAPSI Initiative! — Tarides, Oct 14, 2021

In April, we announced that the DAPSI initiative accepted the proposal for our Secure-by-Design Communication Protocols (SCoP) project. Today, we are thrilled to announce that SCoP has passed the initiative’s Phase 1, and we are now on our way to Phase 2!

SCoP is an open, secure, and resource-efficient infrastructure to engineer a modern basis for open messaging (for existing and emerging protocols) using type-safe languages and unikernels—to ensure your private information remains secure. A…

Read more...

The New Replaying Benchmark in Irmin — Tarides, Oct 04, 2021

As mentioned in our Tezos Storage / Irmin Summer 2021 Update on the Tezos Agora forum, the Irmin team's goal has been to improve Irmin's performance in order to speed up the Baking Account migration process in Octez, and we managed to make it 10x faster in the first quarter of 2021. Since then, we've been working on a new benchmark program for Irmin that's based on the interactions between Irmin and Octez. This won't just help make Irmin even faster, it will also help speed up the Tezos blockcha…

Read more...

Announcing Tezos’ 8th protocol upgrade proposal: Hangzhou — Tarides, Sep 21, 2021

The last upgrade of the Tezos protocol, Granada, activated on August 6th, 2021. We are now glad to announce a new protocol proposal, Hangzhou, the result of a collaborative work from various teams.

This is a joint post with Nomadic Labs, Marigold, Oxhead Alpha and DaiLambda.

Measuring OCaml compilation speed after a refactoring — GaGallium (Florian Angeletti), Sep 17, 2021

It can be tricky to evaluate the effect of invidual commits or pull requests on the speed of the OCaml compiler. In this blog post, I (Florian Angeletti) report my experience on measuring such impact with some degree of statistical significance.

The OCaml typechecker is an important piece of the OCaml compiler pipeline which accounts for a significant portion of time spent on compiling an OCaml program (see the appendices).

The code of the typechecker is also quite optimised, sometime…

Read more...

Writing Lifters Using Primus Lisp — The BAP Blog, Sep 15, 2021

Defining instructions semantics using Primus Lisp (Tutorial)

Introduction

So you found a machine instruction that is not handled by BAP and you wonder how to add it to BAP. This is the tutorial that will gently guide you through the whole process of discovering the instruction, studying its semantics, encoding it, testing, and finally submitting to BAP. The latter is optional but highly appreciated.

In modern BAP, the easiest option is to use Primus Lisp to define new instructions. The idea i…

Read more...

View older blog posts.