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

Weekly News — Caml Weekly News, Jul 22, 2014

  1. proposal for finding, loading and composing ppx preprocessors
  2. Existential row types
  3. Immutable strings
  4. Article on why they use Ocaml: "Why We Use OCaml | Esper Tech Blog"
  5. Lablqt 0.3 is out
  6. A proposal of a standard support for Unicode string
  7. Other OCaml News

Mirage v2.0: a recap of the new features — Open Mirage, Jul 22, 2014

The first release of Mirage back in December 2013 introduced the prototype of the unikernel concept, which realised the promise of a safe, flexible mechanism to build highly optimized software stacks purpose-built for deployment in the public cloud (more background on this). Since then, we've been hard at work using and extending Mirage for real projects and the community has been steadily growing.

We're thrilled to announce the release of Mirage OS v2.0 today! Over the past few weeks the team

Read more...

Building an ARMy of Xen unikernels — Open Mirage, Jul 22, 2014

Mirage has just gained the ability to compile unikernels for the Xen/arm32 platform, allowing Mirage guests to run under the Xen hypervisor on ARM devices such as the Cubieboard 2 and CubieTruck.

Introduction

The ARMv7 architecture introduced the (optional) Virtualization Extensions, providing hardware support for running virtual machines on ARM devices, and Xen's ARM Hypervisor uses this to support hardware accelerated ARM guests.

Mini-OS is a tiny OS kernel designed specifically for running un…

Read more...

Merge sort — Shayne Fletcher, Jul 19, 2014

Merge sort

Here's another divide and conquer algorithm. This one is for sorting a sequence.

Conceptually, a merge sort works like this (see http://en.wikipedia.org/wiki/Merge_sort):

  • Divide the unsorted list into n sub-lists, each containing one element (a list of one element is trivially sorted);
  • Repeatedly merge sublists to produce new sorted sub-lists until there is only one sub-list remaining : this will be the sorted list.

In the following OCaml, we are drawing on inspiration from the the Haske…

Read more...

Reductions in computability theory from a constructive point of view — Andrej Bauer, Jul 19, 2014

Here are the slides from my Logic Coloquium 2014 talk in Vienna. This is joint work with Kazuto Yoshimura from Japan Advanced Institute for Science and Technology.

Abstract: In constructive mathematics we often consider implications between non-constructive reasoning principles. For instance, it is well known that the Limited principle of omniscience implies that equality of real numbers is decidable. Most such reductions proceed by reducing an instance of the consequent to an instance of the a…

Read more...

Simple top-down development in OCaml — Jane Street, Jul 18, 2014

Often when writing a new module, I want to write the interface first and save the implementation for later. This lets me use the module as a black box, extending the interface as needed to support the rest of the program. When everything else is finished, I can fill in the implementation, knowing the full interface I need to support. Of course sometimes the implementation needs to push back on the interface – this pattern isn't an absolute – but it's certainly a useful starting point. The tr…

Read more...

Coq is hiring a specialized engineer for 2 years — Coq, Jul 18, 2014

As part of the ADT Coq-API, we are now offering a 2-year position for a specialized engineer.
For more details, see http://www.pps.univ-paris-diderot.fr/~letouzey/coq-api-position.html

OCamlPro Highlights: May-June 2014 — OCamlPro, Jul 16, 2014

Here is a short report on some of our public activities in May and June 2014.

Towards OPAM 1.2

After a lot of discussions and work on OPAM itself, we are now getting to a clear workflow for OCaml developpers and packagers: the preliminary document for OPAM 1.2 is available here. The idea is that you can now easily create and test the metadata locally, before having to get your package included in any repo: there is less administrative burden and it's much quicker to start, fix it, test it and g…

Read more...

Weekly News — Caml Weekly News, Jul 15, 2014

  1. ocaml-tls (and ocaml-nocrypto / ocaml-x509 / ocaml-asn1-combinators)
  2. proposal for finding, loading and composing ppx preprocessors
  3. llpp v19
  4. OCaml-Java is going alpha, to github
  5. Core Suite 111.21.00
  6. Other OCaml News

Try Alt-Ergo in Your Browser — OCamlPro, Jul 15, 2014

Recently, we worked on an online Javascript-based serverless version of the Alt-Ergo SMT solver. In what follows, we will explain the principle of this version of Alt-Ergo, show how it can be used on a realistic example and compare its performances with bytecode and native binaries of Alt-Ergo.

Compilation

"Try Alt-Ergo" is a Javascript-based version of Alt-Ergo that can be run on compatible browsers (eg. Firefox, Chromium) without requiring a server for computations. It is obtained by compilin…

Read more...