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

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

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

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

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

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

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!

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

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.

Ocsigen Start updated — Ocsigen project (The Ocsigen Team), Jan 20, 2020

New release: Ocsigen Start 2.15

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:

  • Get rid of all remaining Camlp4 code
  • compatibility with OCaml 4.09

Ocsigen Start updated — Ocsigen blog (The Ocsigen Team), Jan 20, 2020

New release: Ocsigen Start 2.15

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:

  • Get rid of all remaining Camlp4 code
  • compatibility with OCaml 4.09

View older blog posts.