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

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

Using ASCII waveforms to test hardware designs — Jane Street, Jun 01, 2020

At Jane Street, an “expect test” is a test where you don’t manually write the output you’d like to check your code against – instead, this output is captured automatically and inserted by a tool into the testing code itself. If further runs produce different output, the test fails, and you’re presented with the diff.

Every proof assistant: redtt — Andrej Bauer, May 31, 2020

This week the speaker will be Jon Sterling, and we are getting two proof assistants for the price of one!

redtt and the future of Cartesian cubical type theory

Time: Thursday, June 4, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Jon Sterling (Carnegie Mellon University)
Proof assistant: redtt and cooltt

Abstract: redtt is an interactive proof assistant for Cartesian cubical type theory, a version of Martin-Löf type t…

Read more...

Every proof assistant: Beluga — Andrej Bauer, May 24, 2020

We are marching on with the Every proof assistant series!

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Brigitte Pientka (McGill University)
Proof assistant: Beluga

Abstract: Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will …

Read more...

TLS 1.3 support for MirageOS — MirageOS (Hannes Mehnert), May 20, 2020

We are pleased to announce that TLS 1.3 support for MirageOS is available. With mirage 3.7.7 and tls 0.12 the Transport Layer Security (TLS) Protocol Version 1.3 is available in all MirageOS unikernels, including on our main website. If you're reading this, you've likely established a TLS 1.3 connection already :)

Getting there was some effort: we now embed the Coq-verified fiat library (from fiat-crypto) for the P-256 elliptic curve, and the F*-verified hacl library (from Project Everest) for t…

Read more...

A Solidity parser in OCaml with Menhir — OCamlPro, May 19, 2020

(This article is cross-posted by the Origin Labs team)

We are happy to announce the first release of our Solidity parser, written in OCaml using Menhir. This is a joint effort with Origin Labs, the company behind Dune Network, to implement a full interpreter for the Solidity language directly in a blockchain.

Solidity is probably the most popular language for smart-contracts, small pieces of code triggered when accounts receive transactions on a blockchain.Solidity is an object-orien…

Read more...

vile 9.8u — Marc Simpson, May 18, 2020

vile 9.8u

# May 18, 2020

Tom Dickey released vile 9.8u yesterday (148 files changed, 13,530 insertions, 6,791 deletions).

Alongside the usual improvements and fixes, 9.8u includes a new smartcase mode1 for treating regex searches as case insensitive unless uppercase characters are included in the search string. This is similar to nvi’s iclower (when used in conjunction with ignorecase):

smartcase (scs)
       Overrides the setting of ignorecase when the pat…
Read more...

Every proof assistant: MMT — Andrej Bauer, May 14, 2020

I am happy to announce the next seminar in the "Every proof assistant" series.

MMT: A Foundation-Independent Logical System

Time: Thursday, May 21, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Florian Rabe (University of Erlangen)
Proof assistant: The MMT Language and System

Abstract: Logical frameworks are meta-logics for defining other logics. MMT follows this approach but abstracts even further: it avoids committin…

Read more...

Ocsigen Start 2.18 released — Ocsigen project (The Ocsigen Team), May 05, 2020

New release: Ocsigen Start 2.18

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 as a basis for your app.

Last features include:

  • Demo of new Ot_tongue widget

See live examples here:

Read more...

Ocsigen Start 2.18 released — Ocsigen blog (The Ocsigen Team), May 05, 2020

New release: Ocsigen Start 2.18

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 as a basis for your app.

Last features include:

  • Demo of new Ot_tongue widget

See live examples here:

Read more...

Ocsigen Toolkit 2.7 with new widget Ot_tongue — Ocsigen project (The Ocsigen Team), May 04, 2020

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

Read more...

Ocsigen Toolkit 2.7 with new widget Ot_tongue — Ocsigen blog (The Ocsigen Team), May 04, 2020

New release: Ocsigen Toolkit 2.7

Ocsigen Toolkit is a widget toolkit for developing mobile and Web apps with js_of_ocaml. It is designed to take advantage of Eliom’s multi-tier programming paradigm. All widgets can be created either on server or client side.

This version introduces a new widget: Ot_tongue. It is a swipable panel, coming from the bottom of the screen (or from another side). Try it online with a mobile phone in Ocsigen Start’s demo or on the app Mon club près de chez moi.

Read more...

Every proof assistant: Arend — Andrej Bauer, Apr 27, 2020

For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.

Getting the authors of proof assistants to travel to Ljubljana …

Read more...

opam 2.0.7 release — OCamlPro, Apr 21, 2020

We are pleased to announce the minor release of opam 2.0.7.

This new version contains backported small fixes:

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs &…

Read more...

opam 2.1.0 alpha is here! — OCamlPro, Apr 21, 2020

We are happy to announce the alpha release of Opam 2.1.0, one year and a half after Opam 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependencies handling (a.k.a. …

Read more...

opam 2.0.7 release — OCaml Platform (Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Apr 21, 2020

We are pleased to announce the minor release of opam 2.0.7.

This new version contains backported small fixes:

Note: To homogenise macOS name on system detection, we decided to keep macos, and convert darwin to macos in opam. For the moment, in order to avoid breaking jobs & CIs…

Read more...

opam 2.1.0 alpha is here! — OCaml Platform (Raja Boujbel - OCamlPro, Louis Gesbert - OCamlPro), Apr 21, 2020

We are happy to announce a alpha for opam 2.1.0, one year and a half in the making after the release of 2.0.0.

Many new features made it in (see the complete changelog or release note for the details), but here are a few highlights of this release.

Release highlights

The two following features have been around for a while as plugins and are now completely integrated in the core of opam. No extra installs needed anymore, and a more smooth experience.

Seamless integration of System dependenci…

Read more...

Chrome extensions: Finding the missing proof — Jane Street, Apr 17, 2020

Web browsers have supported custom plug-ins and extensions since the 1990s, giving users the ability to add their own features and tools for improving workflow or building closer integration with applications or databases running on back-end servers.

An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy — OCamlPro, Mar 23, 2020

The Garbage Collector probably is OCaml’s greatest unsung hero. Its pragmatic approach allows us to allocate without much fear of efficiency loss. In a way, the fact that most OCaml hackers know little about it is a good sign: you want a runtime to gracefully do its job without having to mind it all the time.

But as OCaml 4.10.0 has now hit the shelves, a very exciting feature is in the changelog:

- #8809, #9292: Add a best-fit allocator for the major heap; still
experimental, it should be…
Read more...

Sliding Tile Puzzle, Self-Contained OCaml Webapp — Psellos, Mar 21, 2020

March 21, 2020

I just finished coding up another webapp in OCaml. I thought it would be cool to publish the sources of a small, completely self-contained app. It’s a sliding tile puzzle coded entirely in OCaml, using a few of the BuckleScript extensions. There are no dependencies on any frameworks or the like aside from the Js modules of BuckleScript. The app itself consists of just one JavaScript file—no images, nothing else.


You can try out the puzzle or get the sources a…

Read more...

New version of Try OCaml in beta! — OCamlPro, Mar 16, 2020

We are happy to announce that our venerable “Try Ocaml” service is being retired and replaced by a new, modern version based upon our work on Learn-OCaml.

Try it here

The new interface provides an editor panel besides the familiar top-level, error and warning positions highlighting, the latest OCaml release (4.10.0), local storage of your session, and more.

The service is still in beta, so it would be helpful if you could tell us about any hiccups you may encounter on the Dis…

Read more...

Frama-Clang 0.0.8 is out. Download it here. — Frama-C, Mar 10, 2020

A reasonable TyXML release | Drup's thingies — Gabriel Radanne, Mar 06, 2020

I have the pleasure to announce the release of TyXML 4.4.0, with special Reason support!

Alt-Ergo Users’ Club Annual Meeting — OCamlPro, Mar 03, 2020

The second annual meeting of the Alt-Ergo Users’ Club was held in mid-February. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements.

Alt-Ergo is an automatic mathematical formula checker, jointly developed by LRI and OCamlPro (since 2014). For more information or to join the club, visit https://alt-ergo.ocamlpro.com.

Read more...

OCaml iOS Apps Ported to Browser — Psellos, Feb 24, 2020

February 24, 2020

Something like ten years ago we produced two iOS card game apps written in OCaml, partly as a proof of concept for compiling OCaml to iOS and partly because we enjoy card games. Unfortunately we weren’t able to spark a worldwide craze for writing iOS apps in OCaml or for playing Schnapsen, as we had hoped. Consequently there was very little financial return and we all had to move on to other projects.

Both apps play a very good two-player card game. The apps are essenti…

Read more...

Watch all of Jane Street's tech talks — Jane Street, Feb 20, 2020

Jane Street has been posting tech talks from internal speakers and invited guests for years—and they’re all available on our YouTube channel:

Mercurial: prettyconfig extension — Marc Simpson, Feb 16, 2020

Mercurial: prettyconfig extension

# February 16, 2020

Since the Bitbucket migration, I’ve found myself tinkering1 with Mercurial and its extensions system again (after a long hiatus).

One byproduct of this was a simple, single function extension for listing aliases in a user-friendly way. I subsequently realised that the same behaviour would be useful for arbitrary config sections (aliases, paths, schemes)… and so, the prettyconfig fork.

The prettyconfig

Read more...

Mercurial extensions (update) — Marc Simpson, Feb 05, 2020

Mercurial extensions (update)

# February 5, 2020

In my previous post, I mentioned that a couple of old Mercurial extensions are archived on this server: hg-prettypaths and hg-persona.

Both have now been lightly tidied and updated to work with newer versions of Mercurial (tested on 4.5.3, 5.3).


comments powered by Disqus

2019 at OCamlPro — OCamlPro, Feb 04, 2020

OCamlPro was created to help OCaml and formal methods spread into the industry. We grew from 1 to 21 engineers, still strongly sharing this ambitious goal! The year 2019 at OCamlPro was very lively, with fantastic accomplishments all along!

Let’s quickly review the past years’ works, first in the world of OCaml (flambda2 & compiler optimisations, opam 2, our Rust-based UI for memprof, tools like tryOCaml, ocp-indent, and supporting the OCaml Software Foundation), then in the wor…

Read more...

Bitbucket repository migration — Marc Simpson, Feb 03, 2020

Bitbucket repository migration

# February 3, 2020

Since Bitbucket are discontinuing Mercurial support in a few months’ time (see here), I’ve started migrating a few old repositories:

Read more...

Troubleshooting systemd with SystemTap — Jane Street, Feb 03, 2020

When we set up a schedule on a computer, such as a list of commands to run every day at particular times via Linux cron jobs, we expect that schedule to execute reliably. Of course we’ll check the logs to see whether the job has failed, but we never question whether the cron daemon itself will function. We always assume that it will, as it always has done; we are not expecting mutiny in the ranks of the operating system.

View older blog posts.