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

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

Derivations as computations — Andrej Bauer, Aug 21, 2019

I have a keynote talk "Derivations as Computations" at ICFP 2019. Slides with speaker notes: derivations-as-computations-icfp-2019.pdf Demo file: demo-icfp2019.m31 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 … Continue reading Derivations as computations

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

OCaml Developer at Ahrefs Pte Ltd (Full-time) — Functional Jobs (FunctionalJobs.com), Jul 13, 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...

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

The Alt-Ergo SMT Solver’s results in the SMT-COMP 2019 — OCamlPro, Jul 09, 2019

The results of the SMT-COMP 2019 were released a few days ago at the SMT whorkshop during the 22nd SAT conference. We were glad to participate in this competition for the second year in a row, especially as Alt-Ergo now supports the SMT-LIB 2 standard.

Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro and partially funded by R&D projects. If you’re interested, please consider joining the Alt-Ergo User’s Club! Its history goes back in 2006 from early aca…

Read more...

Of Pythons and Camels — Jane Street, Jul 09, 2019

Welcome to another post in our series of how to use OCaml for machine learning. In previous posts we’ve discussed artistic style-transfer and reinforcement learning. If you haven’t read these feel free to do so now, we’ll wait right here until you’re done. Ready? Ok, let’s continue …

Summer 2019 — Hannes Mehnert (hannes), Jul 08, 2019

Working at robur

As announced previously, I started to work at robur early 2018. We're a collective of five people, distributed around Europe and the US, with the goal to deploy MirageOS unikernels. We do this by developing bespoke MirageOS unikernels which provide useful services, and deploy them for ourselves. We also develop new libraries and enhance existing ones and other components of MirageOS. Example unikernels include our website which uses Canopy, a CalDAV server that stores ent…

Read more...

i-Lab 2019 — Tarides (Céline Laplassotte), Jul 05, 2019

We are thrilled to announce that Tarides is laureate of the 21st edition of the i-Lab innovation contest for its innovative technological solution: OSMOSE.

Organized by the French Ministry of Higher Education, Research and Innovation in partnership with Bpifrance, the objective of this competition is to identify and support innovative technology-based projects. This year, over 700 applications have been registered and 75 projects rewarded. The jury was composed of fifty experts (business leaders…

Read more...

What is an explicit bijection? (FPSAC 2019 slides) — Andrej Bauer, Jul 04, 2019

Here are the slides with speaker notes for the talk What is an explicit bijection which I gave at the 31st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2019). It was the "outsider" talk, where they invite someone to tell them something outside of their area. So how does one sell homotopy … Continue reading What is an explicit bijection? (FPSAC 2019 slides)

Release of OCamlFormat 0.10 — Tarides (Guillaume Petiot), Jun 27, 2019

We are pleased to announce the release of OCamlFormat 0.10 (available on opam).

There have been numerous changes since the last release, so here is a comprehensive list of the new features and breaking changes to help the transition from OCamlFormat 0.9.

ocamlformat-0.10 now works on the 4.08 AST, although the formatting should not differ greatly from the one of ocamlformat-0.9 in this regard. Please note that it is necessary to build ocamlformat with 4.08 to be able to parse new features like…

Read more...

Compiler Engineer at Axoni (Full-time) — Functional Jobs (FunctionalJobs.com), Jun 26, 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...

Learn Eliom - Graffiti tutorial updated — Ocsigen project (The Ocsigen Team), Jun 25, 2019

Graffiti tutorial explains step by step how to write a multi-user client-server drawing application with Eliom.

It is the best starting point for beginners!

An updated version of this tutorial is now online, thanks to corentinjuvigny and chrismamo1.

Learn Eliom - Graffiti tutorial updated — Ocsigen blog (The Ocsigen Team), Jun 25, 2019

Graffiti tutorial explains step by step how to write a multi-user client-server drawing application with Eliom.

It is the best starting point for beginners!

An updated version of this tutorial is now online, thanks to corentinjuvigny and chrismamo1.

Frama-C 19.0 (Potassium) is out. Download ithere. — Frama-C, Jun 21, 2019

Coq 8.10+beta2 is out — Coq, Jun 20, 2019

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

This second β version includes many bug fixes and documentation improvements; more details are given in the reference manual.

Feedback and bug reports are extremely welcome.

Moved to GitHub — OCamlCore Forge News (Jacques Garrigue), Jun 01, 2019

This Project has moved to GitHub. The new project page is: https://github.com/garrigue/labltk

LablGTK moved to GitHub — OCamlCore Forge News (Jacques Garrigue), Jun 01, 2019

New address is https://github.com/garrigue/lablgtk

Coq 8.9.1 is out — Coq, May 20, 2019

The 8.9.1 release of Coq is available.

Main changes:

  • some quality-of-life bug fixes,
  • many improvements to the documentation,
  • a critical bug fix related to primitive projections and native_compute,
  • several additional Coq libraries shipped with the Windows installer.

Feedback and bug reports are extremely welcome.

Coq 8.10+beta1 is out — Coq, May 15, 2019

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

Coq version 8.10 contains two major new features: support for a native machine integer type and a new sort SProp, a definitionally proof irrelevant universe. It is also the result of refinements and stabilization of previous features, deprecations or removals of deprecated features, cleanups of the internals of the system and API, and many documentation improvements. This release includes many user-visible changes, including deprecat…

Read more...

Thoughts from AAAI 2019 — Jane Street, May 13, 2019

At Jane Street, for the last several years, we have been increasingly interested in machine learning and its many use cases. This is why it was exciting when earlier this year myself and a few of my colleagues had the opportunity to attend the AAAI 2019 conference. We’d like to take this space to share with you some of the interesting projects and themes we saw at the conference.

On the road to Irmin v2 — Tarides (Thomas Gazagnaire), May 13, 2019

Over the past few months, we have been heavily engaged in release engineering the Irmin 2.0 release, which covers multiple years of work on all of its constituent elements. We first began Irmin in late 2013 to act as a Git-like distributed and branchable storage substrate that would let us escape the perils of POSIX filesystems.

The Irmin libraries provide snapshotting, branching and merging operations over storage and can communicate via Git both on-disk and remotely. Irmin today therefore cons…

Read more...

View older blog posts.