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

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

Announcing Signals and Threads, a new podcast from Jane Street — Jane Street, Aug 31, 2020

I’m excited (and slightly terrified) to announce that Jane Street is releasing a new podcast, called Signals and Threads, and I’m going to be the host.

BuckleScript Good and Bad News — Psellos, Aug 26, 2020

August 26, 2020

Since last year I’ve been using BuckleScript to build web apps in OCaml and have been enjoying it very much. However, when I went to the project’s home page recently I found that BuckleScript has been renamed to ReScript and that all reference to OCaml has been removed from the project (as far as I can tell).

In particular, there’s no documentation that describes how to use the standard OCaml syntax with the BuckleScript compiler. Previously there were paralle…

Read more...

What the interns have wrought, 2020 edition — Jane Street, Aug 17, 2020

It’s been an unusual internship season.

Coq 8.12.0 is out — Coq, Jul 27, 2020

We are happy to announce the release of Coq 8.12.0.

Some highlights from this release are:

  • a new binder notation for non-maximal implicit arguments;
  • an improved Search command which accepts more complex queries;
  • many additions to the standard library;
  • a restructured reference manual;
  • the deprecation of the omega tactic in favor the lia tactic.

Please see the changelog to learn more about this release.

The Jane Street Interview Process — 2020 Edition — Jane Street, Jul 24, 2020

We’re busy preparing for our software engineering fall hiring season. Over the years we’ve done our best to make our interview process more transparent to candidates. While many candidates show up knowing something about what our interviews look like, much of the information floating around on the internet is outdated or wrong. These past few months have also changed a lot about the process as we’ve adapted to working from home and other effects of COVID-19.

Frama-Clang 0.0.9 is out. Download it here. — Frama-C, Jul 15, 2020

Frama-C 21.1 (Scandium) is out. Download it here. — Frama-C, Jun 25, 2020

Really low latency multipliers and cryptographic puzzles — Jane Street, Jun 22, 2020

At Jane Street, we have some experience using FPGAs for low-latency systems–FPGAs are programmable hardware where you get the speed of an application-specific integrated circuit (ASIC) but without being committed to a design that’s burned into the chip. It wasn’t so long ago that FPGAs were expensive and rare, but these days, you can rent a $5,000 card on the Amazon AWS cloud for less than $3 an hour.

Every proof assistant: Cur - Designing a less devious proof assistant — Andrej Bauer, Jun 21, 2020

We shall finish the semester with a "Every proof assistant" talk by William Bowman. Note that we start an hour later than usual, at 17:00 UTC+2.

Cur: Designing a less devious proof assistant

Time: Thursday, June 25, 2020 from 17:00 to 18:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: William J. Bowman (University of British Columbia)
Proof assistant: Cur

Abstract:

Dijkstra said that our tools can have a profound and devious influence on o…

Read more...

Coq 8.12+beta1 is out — Coq, Jun 17, 2020

We are happy to announce the first beta release of Coq 8.12.

This new version integrates many usability improvements, in particular to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. See the changelog for details.

As usual, we are looking for feedback from beta testers. In addition, we are looking for beta readers of the updated reference manual.

The 8.12 improvements to the reference manual are the start of an effort to i…

Read more...

Frama-C 21.0 (Scandium) is out. Download it here. — Frama-C, Jun 11, 2020

Coq 8.11.2 is out — Coq, Jun 09, 2020

The 8.11.2 release of Coq is available.

This version brings in a few minor fixes. See the changelog for more details.

Every proof assistant: Epigram 2 - Autopsy, Obituary, Apology — Andrej Bauer, Jun 08, 2020

This week shall witness a performance by Conor McBride.

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2

Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted se…

Read more...

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

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

Coq 8.11.1 is out — Coq, Apr 24, 2020

The 8.11.1 release of Coq is available.

The most salient change in the 8.11.1 release is support for OCaml 4.10.0. See the changelog for more details.

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.

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

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

View older blog posts.