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

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

Full Time: Compiler Engineer at Jane Street in New York & London — GitHub Jobs, Mar 24, 2018

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have …


Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong — GitHub Jobs, Mar 24, 2018

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still…


Coq 8.8+beta1 is out — Coq, Mar 19, 2018

The first beta release of Coq 8.8 is available for testing. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Release of Alt-Ergo 2.1.0 — OCamlPro, Mar 14, 2018

A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon.
In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of CHANGES is available here.
Despite our various tests, you may still encounter some issues with this new solver.  Please, don&…


New updates on TzScan — OCamlPro, Mar 14, 2018

Update – TZScan.io can now work on top of the zeronet (zeronet.tzscan.io), we hope it can help the developers community monitor the network. You can now switch between the alphanet & zeronet networks!

OCamlPro is pleased to announce an update of TzScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network.

In addition to some minor bugfixes, the main novelties are:

  • Health of the network with stats about the blocks, endorsements, bakers, etc.
  • Display of futu…

frama-clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out. Download ithere. — Frama-C, Feb 19, 2018

Coq 8.7.2 is out — Coq, Feb 17, 2018

Version 8.7.2 of Coq is available. It fixes a critical bug in the VM handling of universes. This bug affected all releases since 8.5.

Other changes include improved support for building with OCaml 4.06.0 and external num package, many other bug fixes, documentation improvements, and user message improvements (for details, see the 8.7.2 milestone).

Release of a first version of TzScan.io, a Tezos block explorer — OCamlPro, Feb 14, 2018

OCamlPro is proud to release a first version of TzScan (http://tzscan.io), its Tezos
block explorer to ease the use of the Tezos network.

What TzScan can do for you :

– Several charts on blocks, operations, network, volumes, fees, and more,
– Marketcap and Futures/IOU prices from coinmarket.com,
– Blocks, operations, accounts and contracts detail pages,
– Public API to get information about blocks, operations, accounts and more,
– Documentation on different concept…


OCamlPro’s Liquidity-lang demo at JFLA2018 – a smart-contract design language — OCamlPro, Feb 08, 2018

As a tradition, we took part in this year’s Journées Francophones des Langages Applicatifs (JFLA 2018) that was chaired by LRI’s Sylvie Boldo and hosted in Banyuls the last week of January. That was a nice opportunity to present a live demo of a multisignature smart-contract entirely written in the #Liquidity language designed at OCamlPro, and deployed live on the Tezos alphanet (the slides are now available, see at the end of the post).

Tezos is the only blockchain to use a strong…


OCaml Engineer for PL/distributed-systems cryptocurrency project at O(1) Labs (Full-time) — Functional Jobs (FunctionalJobs.com), Jan 23, 2018

O(1) Labs is a small, well-funded startup aiming to develop the first cryptocurrency protocol that can deliver on the promise of supporting real-world applications and widespread use. Our team is based in San Francisco, and we are funded by top investors (including Polychain, Metastable, and Naval Ravikant).

Cryptocurrency is a domain where correctness really counts. As such, a cornerstone of our approach is a focus on building reliable software through the use of statically-typed functional pr…


2017 at OCamlPro — OCamlPro, Jan 15, 2018

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

In the World of Blockchains

The Liquidity Language for smart contracts

* Work of Alain Mebsout, Fabrice Le Fessant, Çagdas Bozman, Michaël Laporte

LiquidityOCamlPro dev…


My 2018 contains robur and starts with re-engineering DNS — Hannes Mehnert (hannes), Jan 11, 2018


At the end of 2017, I resigned from my PostDoc position at University of Cambridge (in the rems project). Early December 2017 I organised the 4th MirageOS hack retreat, with which I'm very satisfied. In March 2018 the 5th retreat will happen (please sign up!).

In 2018 I moved to Berlin and started to work for the (non-profit) Centre for the cultivation of technology with our robur.io project "At robur, we build performant bespoke minimal operating systems for high-assurance se…


MacOS package updated — Coq, Jan 09, 2018

The macOS installer for Coq 8.7.1 was updated on 2018-01-08 to fix frequent crashes of CoqIDE due to the use of an outdated dependency. Direct link to the new version: coq-8.7.1-1-installer-macos.dmg.

OCaml internships at LexiFi — LexiFi, Jan 08, 2018

LexiFi has great internship topics for OCaml hackers!

No prior knowledge of finance is required. If you are interested, please send your resume to careers@lexifi.com.

Posts and Talks Elsewhere — Mindy Preston, Dec 23, 2017

I’ve done a lot of stuff in the last half of 2017, but not much of it has made it here. Here’s a roundup of things published/spoken/embroidered/etc in other places:

frama-clang 0.0.4, compatible with Frama-C 16 is out. Download ithere. — Frama-C, Dec 21, 2017

Coq 8.7.1 is out — Coq, Dec 15, 2017

Version 8.7.1 of Coq is available. It brings compatibility with OCaml 4.06.0, many bug fixes, documentation improvements, and user message improvements (for details see the 8.7.1 milestone).

testing ocaml-migrate-parsetree with `ppx_deriving_crowbar` — OCaml Labs, Dec 14, 2017

testing ocaml-migrate-parsetree with ppx_deriving_crowbar

Early feedback on Crowbar suggested that some automated method of constructing generators might be useful. It wasn’t necessary to do this immediately for the demonstration of testing the OCaml standard library’s Map and Set functors with Crowbar, but what about more complicated types? Like, say, the complicated and heavily mutually recursive types that compose OCaml parsetrees?

With an eye to solving this problem, I looked into a …


Spartan type theory — Andrej Bauer, Dec 11, 2017

The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.

Download slides with speaker notes: Spartan Type Theory [PDF]

How to migrate your ppx to OCaml migrate parsetree — Shayne Fletcher, Dec 09, 2017

OCaml migrate parse tree

OCaml migrate parse tree

Earlier this year, this blog post [2] explored the implementation of a small preprocessor extension (ppx).

The code of the above article worked well enough at the time but as written, exhibits a problem : new releases of the OCaml compiler are generally accompanied by evolutions of the OCaml parse tree. The effect of this is, a ppx written against a specific version of the compiler will "break" in the presence o…


Frama-C 16 - Sulfur is out. Download ithere. — Frama-C, Nov 28, 2017

Eighteenth OCaml compiler hacking evening at Pembroke, Cambridge — OCaml Labs compiler hacking, Nov 21, 2017

Our next OCaml Compiler Hacking event will be on Thursday 7th December in The Thomas Gray Room at Pembroke College, Cambridge.

If you're planning to come along, it'd be helpful if you could indicate interest via Doodle and sign up to the mailing list to receive updates.

When: Thursday 7 December 2017, 19:00 - 22:30

Where: The Thomas Gray Room, Pembroke College, Cambridge CB2 1RF

Who: anyone interested in improving OCaml. Knowledge of OCaml programming will obviously be helpful, but p…


Migration to GitHub is complete — Coq, Nov 21, 2017

After several years of using GitHub specifically for its pull request system, the Coq development team has migrated the Coq bug tracker and Cocorico, the Coq wiki to GitHub as well.

More information about the migration of the Coq bug tracker may be found in this blog post.

More information about the migration of Cocorico, the Coq wiki, may be found on this wiki page.

Finally, the GitHub repository is now the repository we push to (as opposed to a mirror). Make sure that your git clone is tra…


PhD Thesis: Tierless Web programming in ML | Drup's thingies — Gabriel Radanne, Nov 15, 2017

I’m happy to announce that I successfully defended my PhD Thesis!

Towers of Hanoi — Shayne Fletcher, Nov 11, 2017

Towers of Hanoi

The "towers of Hanoi" problem is stated like this. There are three pegs labelled a, b and c. On peg a there is a stack of n disks of increasing size, the largest at the bottom, each with a hole in the middle to accomodate the peg. The problem is to transfer the stack of disks to peg c, one disk at a time, in such a way as to ensure that no disk is ever placed on top of a smaller disk.

The problem is amenable to a divide and conquer strategy : "Move the top n - 1 disk…


OCaml 4.06.0 released — Caml INRIA, Nov 03, 2017

Windows Unicode Support - A Bug-Fix 12 Years in the Making — OCaml Labs, Oct 30, 2017

(Only) 12 years after the initial Mantis issues - and with thanks to a huge community effort - we now have Windows support in the OCaml 4.06.0 release candidate! Read more in David’s detailed blog post and follow the conversation on our Discuss forum.

Nesting quoted strings in OCaml — Shayne Fletcher, Oct 28, 2017


According to the lexical conventions of OCaml, characters different from \ and " can be enclosed in single quotes and appear in strings. The special characters \ and " are represented in these contexts by their escape sequences. The escape sequence \\ denotes the character \ and \" denotes the character ".

Here we print the string "Hello world!". The quotes delimit the string and are not themselves part of the string.

utop[0]> Caml.Printf.printf "Hello world!";;

Fuzzing for CI Workflows — OCaml Labs, Oct 24, 2017

Stephen Dolan recently presented crowbar at the 2017 OCaml Workshop. Crowbar bridges a gap between property-based testing frameworks and instrumentation-based automated testing techniques. Tests written in Crowbar can be executed by the wildly popular and successful American Fuzzy Lop fuzzer. (For more on testing OCaml code with AFL, see the afl-persistent README, Crowbar’s examples, or a user’s DHCP library tests.)

American Fuzzy Lop provides a command-line tool for running tests, afl-fu…


Pearl No.4 - Kth Smallest in the Union of 2 Sorted Collections — Xinuo Chen, Oct 19, 2017


Here is the Pearl No.4:

Let A and B be two disjoint ordered collections with distinct elements inside. Their combined size is greater than k.

  1. A and B are sorted, but the underlying data structures are not specified as they are collections.
  2. A and B do not have common elements, since they are disjoint
  3. All elements in A and B are distinct
  4. The total number of all elements is larger than k

Find the kth smallest element of A ∪ B.

By definition, the kth smallest elem…


View older blog posts.