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

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

How We Lost at The Delphi Oracle Challenge — Sebastien Mondet, Dec 23, 2020

Because the method — some messing around with the tezos-crypto library — could be useful to others. Also, some code annotated in SVG.

Tarides sponsors the Oxbridge Women in Computer Science Conference 2020 — Tarides, Dec 14, 2020

The Oxbridge Women in Computer Science conference is an annual one-day event hosted by the Universities of Oxford and Cambridge (UK). The conference is free and open to everyone from any discipline, regardless of gender identity. Its purpose is to spotlight the successes of women within computer science and strengthen the network of women in computer science within a supportive and friendly environment.

This year, the conference was organised by the University of Cambridge and was held virtually…

Read more...

Coq 8.12.2 is out — Coq, Dec 11, 2020

We are happy to announce the release of Coq 8.12.2.

This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the exists tactic). See the changelog for details.

First release of MetAcsl plugin — Frama-C, Dec 09, 2020

Announcing MirageOS 3.10 — MirageOS (Hannes Mehnert), Dec 08, 2020

MirageOS 3.10 release - IPv6

IPv6 and dual (IPv4 and IPv6) stack support https://github.com/mirage/mirage/pull/1187 https://github.com/mirage/mirage/issues/1190

Since a long time, IPv6 code was around in our TCP/IP stack (thanks to @nojb who developed it in 2014). Some months ago, @hannesm and @MagnusS got excited to use it. After we managed to fix some bugs and add some test cases, and writing more code to setup IPv6-only and dual stacks, we are eager to share this support for MirageOS in a re…

Read more...

ReScript 8.4 — Reason Documentation Blog, Dec 07, 2020

Coq 8.13+beta1 is out — Coq, Dec 07, 2020

The Coq development team is proud to announce the immediate availability of Coq 8.13+beta1

Here the full list of changes.

We encourage our users to test this beta release, in particular:

  • The windows installer is now based on the Coq platform: This greatly simplifies its build process and makes it easy to add more packages. At the same time this new installer was only tested by two people, so if you use Windows please give us feedback on any problem you may encounter.
  • The…
Read more...

Memthol: exploring program profiling — OCamlPro, Dec 01, 2020

Memthol is a visualizer and analyzer for program profiling. It works on memory dumps containing information about the size and (de)allocation date of part of the allocations performed by some execution of a program.

For information regarding building memthol, features, browser compatibility… refer to the memthol github repository.
Please note that Memthol, as a side project, is a work in progress that remains in beta status for now.

Memthol’s background

The Memthol wor…

Read more...

Growing the Hardcaml toolset — Jane Street, Dec 01, 2020

I am pleased to announce that we have recently released a slew of new Hardcaml libraries!

Editor Plugin for VSCode and Vim Officially Released! — Reason Documentation Blog, Nov 26, 2020

Type hints, jump to definition, error diagnostics, and more.

Announcing Our Market Prediction Kaggle Competition — Jane Street, Nov 24, 2020

Jane Street is running a Kaggle contest based on a real problem with real financial data. If you like ML projects, or think you might, head over and check it out. We think it’s a pretty fun one. The prizes are pretty good too, with a total $100K being paid out.

Every proof assistant: introducing homotopy.io – a proof assistant for geometrical higher category theory — Andrej Bauer, Nov 23, 2020

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn!

Introducing homotopy.io: A proof assistant for geometrical higher category theory

Time: Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)
Location: online at Zoom ID 989 0478 8985
Speaker: Jamie Vicary (University of Cambridge)
Proof assistant: homotopy.io

Abstract:

Weak higher categories can be difficult to wo…

Read more...

“Universal” Dune Tip: Rebuild Stuff, Sometimes — Sebastien Mondet, Nov 21, 2020

Quick hack to make “at most every n seconds” dune targets.

Release of Frama-C 22.0 (Titanium) — Frama-C, Nov 20, 2020

Editor Support, Custom Operators and More — Reason Documentation Blog, Nov 17, 2020

Update on what we're doing around the end of 2020 and early next year.

Coq 8.12.1 is out — Coq, Nov 16, 2020

We are happy to announce the release of Coq 8.12.1.

This release contains numerous bug fixes and documentation improvements. Some bug fix highlights:

  • Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency.
  • Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim.
  • Several bugs with Search.
  • The de…
Read more...

Beta release of Frama-C 22.0-beta (Titanium) — Frama-C, Oct 28, 2020

Announcing MirageOS 3.9.0 — MirageOS (Martin Lucina), Oct 27, 2020

MirageOS 3.9.0 release

We are pleased to announce the release of MirageOS 3.9.0.

Our last release announcement was for MirageOS 3.6.0, so we will also cover changes since 3.7.x and 3.8.x in this announcement.

New features:

  • The Xen backend has been re-written from scratch to be based on Solo5, and now supports PVHv2 on Xen 4.10 or higher, and QubesOS 4.0.
  • As part of this re-write, the existing Mini-OS based implementation has been retired, and all non-UNIX backends now use a unified OCaml runtime…
Read more...

SmartPy@OCaml2020: The Making Of — Sebastien Mondet, Oct 26, 2020

A quick experience report … Tools used for the paper, the slides, and the video.

Qrc — Daniel Bünzli, Oct 22, 2020

First release of Qrc, a QR code encoder for OCaml.

Brr — Daniel Bünzli, Oct 14, 2020

First release of Brr, a toolkit for programming browsers in OCaml.

A Short Review of 4th Generation Cryptocurrencies — Eray Özkural, Oct 07, 2020

In the course of designing Cypher, our home-brewed cryptoken infrastructure, I have witnessed the emergence of a new generation of cryptocurrency designs I can name 4th generation cryptocurrencies owing my lack of imagination in naming things, but also because a …

Finding memory leaks with Memtrace — Jane Street, Oct 06, 2020

Memory issues can be hard to track down. A function that only allocates a few small objects can cause a space leak if it’s called often enough and those objects are never collected. Even then, many objects are supposed to be long-lived. How can a tool, armed with data on allocations and their lifetimes, help sort out the expected from the suspicious?

Rehabilitating packs using functors and recursivity, part 2. — OCamlPro, Sep 30, 2020

This blog post and the previous one about functor packs covers two RFCs currently developed by OCamlPro and Jane Street. We previously introduced functor packs, a new feature adding the possiblity to compile packs as functors, allowing the user to implement functors as multiple source files or even parameterized libraries.

In this blog post, we will cover the other aspect of the packs rehabilitation: allowing anyone to implement recursive compilation units using packs (as described formally …

Read more...

What's new in ReScript 8.3 (Part 2) — Reason Documentation Blog, Sep 26, 2020

What's new in ReScript 8.3 (Part 1) — Reason Documentation Blog, Sep 25, 2020

Rehabilitating Packs using Functors and Recursivity, part 1. — OCamlPro, Sep 24, 2020

OCamlPro has a long history of dedicated efforts to support the development of the OCaml compiler, through sponsorship or direct contributions from Flambda Team. An important one is the Flambda intermediate representation designed for optimizations, and in the future its next iteration Flambda 2. This work is funded by JaneStreet.

Packs in the OCaml ecosystem are kind of an outdated concept (options -pack and -for-pack in the OCaml manual), and their main utility has been overtaken by the in…

Read more...

Building portable user interfaces with Nottui and Lwd — Tarides, Sep 24, 2020

At Tarides, we build many tools and writing UI is usually a tedious task. In this post we will see how to write functional UIs in OCaml using the Nottui & Lwd libraries.

These libraries were developed for Citty, a frontend to the Continuous Integration service of OCaml Labs.

In this recording, you can see the lists of repositories, branches and jobs monitored by the CI service, as well as the result of job execution. Most of the logic is asynchronous, with all the contents…

Read more...

Tarides is now a sponsor of the OCaml Software Foundation — Tarides, Sep 17, 2020

Tarides is pleased to provide support for the OCaml Software Foundation, a non-profit foundation hosted by the Inria Foundation. The OCaml Software Foundation's mission is to promote the OCaml programming language and its ecosystem by supporting the growth of a diverse and international community of OCaml users.

Tarides develops secure-by-design solutions in which OCaml's memory and type-safety guarantees play a major role. Hence, most of the software development that is done at Tarides is in OC…

Read more...

Memory allocator showdown — Jane Street, Sep 15, 2020

Since version 4.10, OCaml offers a new best-fit memory allocator alongside its existing default, the next-fit allocator. At Jane Street, we've seen a big improvement after switching over to the new allocator. This post isn't about how the new allocator works. For that, the best source is these notes from a talk by its author. Instead, this post is about just how tricky it is to compare two allocators in a reasonable way, especially for a garbage-collected system.

View older blog posts.