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

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

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 OCaml (with OPAM 2, flambda 2 etc.), of blockchains (Tezos and the Tezos ICO, Liquidity, etc.), of formal methods (Alt-Ergo etc.)

In the World of OCaml

Towards OPAM 2.0

OPAM was born at Inria/OCamlPro with Frederic, Thomas and Louis, and is still maintained here at OCamlPro. Now thanks to Louis Gesbert’s thorough effo…

Read more...

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

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…

Read more...

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:

Full Time: Tools & Compilers Engineer at Jane Street in New York & London — GitHub Jobs, Dec 22, 2017

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 …

Read more...

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

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…

Read more...

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 …

Read more...

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…

Read more...

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

Software Engineer (Haskell, Full Stack) at Capital Match (Full-time) — Functional Jobs (FunctionalJobs.com), Nov 24, 2017

About Us: Capital Match is a leading P2P lending platform based in Singapore, founded in 2014, backed by alternative investment management firm with more than US$ 5 bn AUM. We are looking for experienced developers to lead our tech growth in the Fintech space, expand into surrounding countries and develop new products on the platform.

Job Description: We are inviting developers with a minimum of 5 years coding experience. The candidate should have functional programming experience as well as…

Read more...

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…

Read more...

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…

Read more...

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…

Read more...

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

Quoting

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!";;
Hello…
Read more...

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…

Read more...

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

hero

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…

Read more...

Coq 8.7.0 is out — Coq, Oct 17, 2017

The final release of Coq 8.7.0 is available. Coq 8.7 includes:
  • A large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust.
  • New tactics:
    • Variants of tactics supporting existential variables eassert, eenough, etc. by Hugo Herbelin;
    • Tactics extensionality i…
Read more...

How to render trees like the Unix tree command — Shayne Fletcher, Oct 14, 2017

How to render trees like Unix 'tree'

The Unix tree utility produces a pretty rendering of a filesystem. Implementing an algorithm to produce output like tree is a little harder than one might expect! This short example program illustrates one way of doing it.

(* A type of non-empty trees of strings. *)
type tree = [
|`Node of string * tree list
]
;;

(* [print_tree tree] prints a rendering of [tree]. *)
let rec print_tree
?(pad : (string * string)= ("", ""))
(tree :…
Read more...

"More OCaml" updated to support OCaml 4.06 immutable strings — OCaml Book, Oct 14, 2017

OCaml 4.06 has, by default, immutable strings. This necessitates some changes to "More OCaml" ("OCaml from the Very Beginning" is unaffected).

The paper and kindle books (on Amazon), as well as the PDF e-book here, have been updated, together with the online resources. The new code works on any version of OCaml starting from 4.02.0.

If you are an existing customer, and have not received an update email, please contact the author using the form on this website.

Implementing the PowerPC backend for BAP - Part 0 — The BAP Blog, Oct 13, 2017

On this week we started to work on the PowerPC backend. We are planning a series of blog posts that will describe the process and probably will help others, who will pursue the task of implementing a backend for BAP, by either suggesting the right way or discouraging by showing an example of how one shouldn’t do this.

As you may know, BAP is a platform for program analysis that works with compiled binaries. In a sense, BAP is dual to a compiler, since we move in the opposite direction – we …

Read more...

NAT your own packets — Mindy Preston, Oct 09, 2017

I’ve been talking about network address translation here for a while, including instructions on building your own NAT device with MirageOS. The library behind those posts, mirage-nat, went on to back talex5’s unikernel firewall for QubesOS, but was unreleased and essentially unmaintained between late 2015 and early 2017. At the March 2017 MirageOS hack retreat in Marrakesh, talex5 convinced me to do some much-needed maintenance on this library. After having let it age between March and Octob…Read more...

Coq 8.7+beta2 is out — Coq, Oct 06, 2017

The second beta release of Coq 8.7 is available for testing. Coq 8.7 includes:
  • A large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin writers and making the code more robust.
  • New tactics:
    • Variants of tactics supporting existential variables eassert, eenough, etc. by Hugo Herbelin;
    • Tactics
Read more...

The BAP Tutorial — The BAP Blog, Oct 03, 2017

It was a lasting issue that BAP didn’t have a tutorial. We have an extensive reference documentation that can even be considered as a manual, we have wiki and chats, but still it was necessary to read lots of stuff even for writing the simplest analysis. That’s why people kept asking us for the tutorial. So, today we are happy to announce the first true tutorial.

The target auditory of the tutorial is expected to be more or less advanced, as the tutorial will cover not only the basics, but …

Read more...

View older blog posts.