• 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.

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

Coq 8.10.0 is out — Coq, Oct 07, 2019

The 8.10.0 release of Coq is available.

Main changes:

  • some quality-of-life bug fixes;
  • a critical bug fix related to template polymorphism;
  • native 63-bit machine integers;
  • a new sort of definitionally proof-irrelevant propositions: SProp;
  • private universes for opaque polymorphic constants;
  • string notations and numeral notations;
  • a new simplex-based proof engine for the tactics lia, nia, lra and nra;
  • new introduction patterns for SSReflect;
  • a tactic to rewrite under binders: under;
  • easy input of…
Read more...

OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

In our endeavour to encourage professional programmers to understand and use OCaml, OCamlPro will be giving two training sessions, in French, in our Paris offices:

  1. OCaml Beginner course for professional programmers (5-6 Nov)
  2. OCaml Expertise (7-8 Nov).

The “Expert” OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write “compiler-optimizable” code.

These sessions are …

Read more...

Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

We're glad to announce the first release of `mrmime`, a parser and a generator of emails. This library provides an OCaml way to analyze and craft an email. The eventual goal is to build an entire unikernel-compatible stack for email (such as SMTP or IMAP).

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the h…

Read more...

A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

As you already know if you’ve read our last blogpost, we have updated our OCaml cheat sheets starting with the language and stdlib ones. We know some of you have students to initiate in September and we wanted these sheets to be ready for the start of the school year! We’re working on more sheets for OCaml tools like opam or Dune and important libraries such as Obj Lwt or Core. Keep an eye on our blog or the repo on GitHub to follow all the updates.

Going through the documentation was a jour…

Read more...

Frama-C 19.1 (Potassium) is out. Download ithere. — Frama-C, Sep 17, 2019

Coq 8.10+beta3 is out — Coq, Sep 16, 2019

The third beta release of Coq 8.10 is available for testing.

This third β version includes various bug fixes and improvements, including:

  • improved warning on coercion path ambiguity;
  • support for OCaml extraction of primitive machine integers;
  • fix for the soundness issue with template polymorphism;
  • fix extraction of dependent record projections to OCaml.

More details are given in the user manual.

Feedback and bug reports are extremely welcome.

OCaml Developer at Ahrefs Pte Ltd (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 14, 2019

What We Need

Ahrefs is looking for a backend developer with deep understanding of networks, distributed systems, OS fundamentals and taste for simple and efficient architectural designs. Our backend is mostly implemented in OCaml with some C++ and Rust.

In this role, be prepared to deal with 25 petabytes of live data, OCaml and Linux on a daily basis.

Basic Requirements:

  • Proficiency in OCaml
  • Knowledge of C++ and/or Rust is a plus

The ideal candidate is expected to:

  • Independently deal wi…
Read more...

Compiler Engineer at Axoni (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 13, 2019

Compiler Engineer

Headquartered in New York City, we are currently working intensely on what we expect to become the most widely used programming language for blockchain smart contracts: AxLang. Based on Scala, AxLang enables secure and full featured smart contract development by supporting both functional programming and formal verification. Its design is driven by the rigorous requirements for solutions serving the world's largest financial institutions.

AxLang is part of Axoni's b…

Read more...

Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

In 2011, we shared several cheat sheets for OCaml. Cheat sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. We hope they will help you out when your rubber duck is rubbish at debugging your code!

Since we first shared them, OCaml and its related tools have evolved. We decided to refresh them and started…

Read more...

Frama-Clang 0.0.7 is out. Download ithere. — Frama-C, Sep 13, 2019

Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

In our first article we mostly discussed the API design of decompress and did not talk too much about the issue of optimizing performance. In this second article, we will relate our experiences of optimizing decompress.

As you might suspect, decompress needs to be optimized a lot. It was used by several projects as an underlying layer of some formats (like Git), so it can be a real bottleneck in those projects. Of course, we start with a footgun by using a garbage-collected language; comparing t…

Read more...

On complete ordered fields — Andrej Bauer, Sep 08, 2019

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

  1. A complete ordered field is archimedean.
  2. Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in …

Read more...

An introduction to fuzzing OCaml with AFL, Crowbar and Bun — Tarides (Nathan Rebours), Sep 04, 2019

American Fuzzy Lop or AFL is a fuzzer: a program that tries to find bugs in other programs by sending them various auto-generated inputs. This article covers the basics of AFL and shows an example of fuzzing a parser written in OCaml. It also introduces two extensions: the Crowbar library which can be used to fuzz any kind of OCaml program or function and the Bun tool for integrating fuzzing into your CI.

All of the examples given in this article are available on GitHub at ocaml-afl-examples. Th…

Read more...

What is algebraic about algebraic effects? — Andrej Bauer, Sep 02, 2019

Published as arXiv:1807.05923.

Abstract: This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra.…

Read more...

The blog moved from Wordpress to Jekyll — Andrej Bauer, Sep 02, 2019

You may have noticed that lately I have had trouble with the blog. It was dying periodically because the backend database kept crashing. It was high time I moved away from Wordpress anyway, so I bit the bullet and ported the blog.

All in all, it was a typical system administration experience: lots of installing Ruby and Node.js packages, figuring out which of several equivalent tools actually is worth using, dealing with scarce and obsolete documentation (a blog post is not a good substitute …

Read more...

OCamlPro’s compiler team work update — OCamlPro, Aug 30, 2019

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

A lot of work has been done towards a new framework for optimizations in the compiler, called Flambda2, aiming at solving the shortcomings that became apparent in the Flambda optimization framework (see below for more details). While that work is in progress, the team also worked on some more short-term improvements, notably on the current Flambda optimization framework, a…

Read more...

What the interns have wrought, 2019 edition — Jane Street, Aug 30, 2019

Jane Street’s intern program yet again is coming to an end, which is a nice opportunity to look back over the summer and see what they’ve accomplished.

Decompress: The New Decompress API — Tarides (Romain Calascibetta), Aug 26, 2019

RFC 1951 is one of the most used standards. Indeed, when you launch your Linux kernel, it inflates itself according zlib standard, a superset of RFC 1951. Being a widely-used standard, we decided to produce an OCaml implementation. In the process, we learned many lessons about developing OCaml where we would normally use C. So, we are glad to present `decompress`.

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress

Read more...

Derivations as computations (ICFP 2019 slides) — Andrej Bauer, Aug 21, 2019

I gave a keynote talk "Derivations as Computations" at ICFP 2019.

Abstract: According to the propositions-as-types reading, programs correspond to proofs, i.e., a term t of type A encodes a derivation D whose conclusion is t : A. But to be quite precise, D may have parts which are not represented in t, such as subderivations of judgmental equalities. In general, a term does not record an e…

Read more...

Deriving Slowly — Rudi Grinberg, Aug 20, 2019

There’s been some recent grumbling about the usability of ppx in OCaml, and instead of just letting it slide again, I’ve decided to do something constructive about this and write a little tutorial on how to write a deriving plugin.

Using OCaml to drive a Raspberry Pi robot car — Jane Street, Aug 19, 2019

Back when the Raspberry Pi was first released in 2012 Michael Bacarella wrote a blog post on using OCaml and Async on this little device. Since then installing OCaml via opam has become a pretty smooth experience and everything works out of the box when using Raspbian – the default Raspberry Pi distribution.

Do applied programming languages research at Jane Street! — Jane Street, Aug 16, 2019

As our Tools & Compilers team has grown, the kinds of projects we work on has become more ambitious. Here are some of the major things we’re currently working on:

X509 0.7 — Hannes Mehnert (hannes), Aug 15, 2019

Cryptographic material

Once a private and public key pair is generated (doesn't matter whether it is plain RSA, DSA, ECC on any curve), this is fine from a scientific point of view, and can already be used for authenticating and encrypting. From a practical point of view, the public parts need to be exchanged and verified (usually a fingerprint or hash thereof). This leads to the struggle how to encode this cryptographic material, and how to embed an identity (or multiple), capabilities, …

Read more...

BAP Knowledge Representation - Part 1 — The BAP Blog, Aug 15, 2019

An important part of BAP 2.0 is the new knowledge representation system, which drives all the new code. Given how important it is for understanding and using modern BAP, I decided to introduce it informally in a series of blog posts. This series is by no means a substitution for documentation or a tutorial, which will (I hope) follow. The intention is to describe the system in a friendly manner like I would describe it to my colleague in front of a whiteboard.

All information in BAP 2.0 is stor…

Read more...

Down — Daniel Bünzli, Jul 23, 2019

First release of Down, an unintrusive OCaml toplevel experience upgrade.

Ocsigen Start and Ocsigen Server updated — Ocsigen project (The Ocsigen Team), Jul 18, 2019

New releases:

  • Ocsigen Start 2.2
  • Ocsigen Server 2.13

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or to quickly create your own Minimum Viable Product. See an online demo.

Last features include:

  • Demo of “Pull to refresh page” feature (mobile apps)
  • Updated template

Ocsigen Server is a full fea…

Read more...

Ocsigen Start and Ocsigen Server updated — Ocsigen blog (The Ocsigen Team), Jul 18, 2019

New releases:

  • Ocsigen Start 2.2
  • Ocsigen Server 2.13

Ocsigen Start is a template for client-server Web and/or mobile app in OCaml or ReasonML. It contains many standard features like user management, notifications, and many code examples. Use it to learn Web/mobile development in OCaml or to quickly create your own Minimum Viable Product. See an online demo.

Last features include:

  • Demo of “Pull to refresh page” feature (mobile apps)
  • Updated template

Ocsigen Server is a full fea…

Read more...

A look at OCaml 4.08 — Jane Street, Jul 12, 2019

Now that OCaml 4.08 has been released, let’s have a look at what was accomplished, with a particular focus on how our plans for 4.08 fared. I’ll mostly focus on work that we in the Jane Street Tools & Compilers team were involved with, but we are just some of the contributors to the OCaml compiler, and I’ll have a quick look at the end of the post at some of the other work that went into 4.08.

opam 2.0.5 release — OCamlPro, Jul 11, 2019

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

This new version contains build update and small fixes:

  • Bump src_ext Dune to 1.6.3, allows compilation with OCaml 4.08.0. [#3887 @dra27]
  • Support Dune 1.7.0 and later [#3888 @dra27 – fix #3870]
  • Bump the ocaml_mccs lib-ext, to include latest changes [#3896 @AltGr]
  • Fix cppo detection in configure [#3917 @dra27]
  • Read jobs variable from OpamStateConfig [#3916 @dra27]
  • Linting:
    • add check upstream option [#3758 @rjbou]
    • add warning for w…
Read more...

opam 2.0.5 release — OCaml Platform (Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Jul 11, 2019

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

This new version contains build update and small fixes:

  • Bump src_ext Dune to 1.6.3, allows compilation with OCaml 4.08.0. [#3887 @dra27]
  • Support Dune 1.7.0 and later [#3888 @dra27 - fix #3870]
  • Bump the ocaml_mccs lib-ext, to include latest changes [#3896 @AltGr]
  • Fix cppo detection in configure [#3917 @dra27]
  • Read jobs variable from OpamStateConfig [#3916 @dra27]
  • Linting:
    • add check upstream option [#3758 @rjbou]
    • add warning for with-test in r…
Read more...

View older blog posts.