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

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

Bucket Sort — Shayne Fletcher, Jun 10, 2018

Bucket Sort

Bucket sort assumes input generated by a random process that distributes elements uniformly over the interval [0, 1).

The idea of bucket sort is to divide [0, 1) into n equal-sized subintervals or buckets, and then distribute the n input numbers into the buckets. To produce the output, sort the numbers in each bucket and then go through the buckets in order. Sorting a bucket can be done with insertion sort.

let rec insert x = function
| [] -> [x]
| h :: tl as ls ->
if x <…
Read more...

Frama-C 17 - Chlorine is out. Download ithere. — Frama-C, May 31, 2018

An OCaml quine | Drup's thingies — Gabriel Radanne, May 30, 2018

(fun x -> Printf.printf "%s %S" x x) "(fun x -> Printf.printf \"%s %S\" x x)"

Full Time: Compiler Engineer at Jane Street in New York & London — GitHub Jobs, May 29, 2018

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have …

Read more...

Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong — GitHub Jobs, May 29, 2018

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still…

Read more...

opam 2.0.0 Release Candidate 2 is out! — OCamlPro, May 22, 2018

We are pleased to announce the release of a second release candidate for OPAM 2.0.0.

This new version brings us very close to a final 2.0.0 release, and in addition to many fixes, features big performance enhancements over the RC1.

Among the new features, we have squeezed in full sandboxing of package commands for both Linux and Mac OS, to protect our users from any misbehaving scripts.

NOTE: if upgrading manually from 2.0.0~rc, you need to run opam init --reinit -ni to enable sandboxing.

The ne…

Read more...

simpl is less annoying than you think — GaGallium (Nathanaël Courant, Armaël Guéneau), May 22, 2018

In this blogpost we find out that it is possible to tweak the behavior of the Coq simpl tactic. We find it particularly useful when dealing with arithmetic goals on Z.

We just discovered an answer to a longstanding annoyance we faced when dealing with arithmetic Coq goals. Consider the following Coq goal, using integers on Z:

Require Import ZArith.
Open Scope Z_scope.

Goal forall a, 2 * a = 0 * a + a * 2.
  intros. simpl.

We call the simpl tactic to simplify 0 * a + ... into .... Unfort…

Read more...

Dijkstra's algorithm — Shayne Fletcher, May 20, 2018

Shortest Path

This article assumes familiarity with Dijkstra's shortest path algorithm. For a refresher, see [1]. The code assumes open Core is in effect and is online here.

The first part of the program organizes our thoughts about what we are setting out to compute. The signature summarizes the notion (for our purposes) of a graph definition in modular form. A module implementing this signature defines a type vertex_t for vertices, a type t for graphs and type extern_t

Read more...

Ann: Regenerate | Drup's thingies — Gabriel Radanne, May 08, 2018

I’m happy to announce the release of Regenerate, a library, tool and website to generate test cases for regular expression engines.

Release of Alt-Ergo 2.2.0 — OCamlPro, Apr 23, 2018

A new release of Alt-Ergo (version 2.2.0) is available.

You can get it from Alt-Ergo’s website. An OPAM package for it will be published in the next few days.

The major novelty of this release is a new experimental front-end that supports the SMT-LIB 2 language, extended prenex polymorphism. This extension is implemented as a standalone library, and is available here: https://github.com/Coquera/psmt2-frontend

The full list of CHANGES is available here. As usual, do not hesitate to report b…

Read more...

Visiting the camels - MirageOS spring hack retreat 2018 — MirageOS (Stefanie Schirmer), Apr 20, 2018

Original posted on linse's blog.

Jemaa El Fnaa Image by Luc Viatour / https://Lucnix.be

In March 2018, I attended my first MirageOS hack retreat in Morrocco. MirageOS is a library operating system which allows everyone to build very small, specialized operating system kernels that are intended to run directly on the virtualization layer. The application code itself is the guest operating system kernel, and can be deployed at scale without the need for an extra containerization step in between. It is written …

Read more...

The Bitcoin Piñata - no candy for you — Hannes Mehnert (hannes), Apr 18, 2018

History

On February 10th 2015 David Kaloper-Meršinjak and Hannes Mehnert launched (read also Amir's description) our bug bounty program in the form of our Bitcoin Piñata MirageOS unikernel. Thanks again to IPredator for both hosting our services and lending us the 10 Bitcoins! We analysed a bit more in depth after running it for five months. Mindy recently wrote about whacking the Bitcoin Piñata.

On March 18th 2018, after more than three years, IPredator, the lender of the Bitcoins,…

Read more...

Whacking the Bitcoin Piñata — Mindy Preston, Apr 17, 2018

@yomimono or @hannesm surely know if people have tried crowbar on the BTC Piñata. – @kensan@mastodon.social

tl;dr - yes, and it seems that ocaml-x509 is not trivially easy to trick.

Background

The Bitcoin Piñata

In 2015 David Kaloper-Mersinjak and Hannes Mehnert released ocaml-tls, an implementation of TLS (formerly known as SSL) written fully in OCaml. A full writeup of the stack is available in their Usenix Security 2015 paper, and as a series of blog posts on mirage.io. To acc…

Read more...

Coq 8.8.0 is out — Coq, Apr 17, 2018

The final release of Coq 8.8.0 is available. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Taskforce on the Tezos Protocol, and Tzscan evolution — OCamlPro, Apr 13, 2018

As we are preparing to work on the Tezos Protocol, we’re still actively keeping the pace on the block explorer TZScan.io, adding cool information for baking accounts. We’d like to allow people to see who is contributing to the network and to understand the distribution of rolls, rights, etc.

For starters, we are showing the roll balance used for baking in the current cycle and the rolls history of a baker.

http://tzscan.io/tz1MqVR7hnZwH1FoQ7swjamanNxrXtNVAQ7v?default=baking

Enjoy, mo…

Read more...

How to quantify quantifiers: an Ltac puzzle — GaGallium (Armaël Guéneau), Apr 05, 2018

In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.

Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.

In this blog-post, I would li…

Read more...

OCaml JTRT — OCamlPro, Apr 01, 2018

This time of the year is, just like Christmas time, a time for laughs and magic… although the magic we are talking about, in the OCaml community, is not exactly nice, nor beautiful. Let’s say that we are somehow akin to many religions: we know magic does exist , but that it is satanic and shouldn’t be introduced to children.

Introducing Just The Right Time (JTRT)

Let me first introduce you to the concept of ‘Just The Right Time’ [1]. JTRT is somehow a ‘Just In…

Read more...

Announcing the Sound Static Analysis for Security Workshop (2018-06-27 and 28 at NIST). See the whole programhere. — Frama-C, Mar 22, 2018

Coq 8.8+beta1 is out — Coq, Mar 19, 2018

The first beta release of Coq 8.8 is available for testing. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Release of Alt-Ergo 2.1.0 — OCamlPro, Mar 14, 2018

A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon.
In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of CHANGES is available here.
Despite our various tests, you may still encounter some issues with this new solver.  Please, don&…

Read more...

New updates on TzScan — OCamlPro, Mar 14, 2018

Update – TZScan.io can now work on top of the zeronet (zeronet.tzscan.io), we hope it can help the developers community monitor the network. You can now switch between the alphanet & zeronet networks!

OCamlPro is pleased to announce an update of TzScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network.

In addition to some minor bugfixes, the main novelties are:

  • Health of the network with stats about the blocks, endorsements, bakers, etc.
  • Display of futu…
Read more...

frama-clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out. Download ithere. — Frama-C, Feb 19, 2018

Coq 8.7.2 is out — Coq, Feb 17, 2018

Version 8.7.2 of Coq is available. It fixes a critical bug in the VM handling of universes. This bug affected all releases since 8.5.

Other changes include improved support for building with OCaml 4.06.0 and external num package, many other bug fixes, documentation improvements, and user message improvements (for details, see the 8.7.2 milestone).

Release of a first version of TzScan.io, a Tezos block explorer — OCamlPro, Feb 14, 2018

OCamlPro is proud to release a first version of TzScan (http://tzscan.io), its Tezos
block explorer to ease the use of the Tezos network.

What TzScan can do for you :

– Several charts on blocks, operations, network, volumes, fees, and more,
– Marketcap and Futures/IOU prices from coinmarket.com,
– Blocks, operations, accounts and contracts detail pages,
– Public API to get information about blocks, operations, accounts and more,
– Documentation on different concept…

Read more...

OCamlPro’s Liquidity-lang demo at JFLA2018 – a smart-contract design language — OCamlPro, Feb 08, 2018

As a tradition, we took part in this year’s Journées Francophones des Langages Applicatifs (JFLA 2018) that was chaired by LRI’s Sylvie Boldo and hosted in Banyuls the last week of January. That was a nice opportunity to present a live demo of a multisignature smart-contract entirely written in the #Liquidity language designed at OCamlPro, and deployed live on the Tezos alphanet (the slides are now available, see at the end of the post).

Tezos is the only blockchain to use a strong…

Read more...

MirageOS running on the ESP32 embedded chip — MirageOS (Anil Madhavapeddy), Jan 26, 2018

Now that the winter holiday break is over, we are starting to see the results of winter hacking among our community.

The first great hack for 2018 is from Sadiq Jaffer, who got OCaml booting on a tiny and relatively new CPU architecture -- the Espressif ESP32. After proudly demonstrating a battery powered version to the folks at OCaml Labs, he then proceeded to clean it up enough tha it can be built with a Dockerfile, so that others can start to do a native code port and get bindings to the net…

Read more...

2017 at OCamlPro — OCamlPro, Jan 15, 2018

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

In the World of Blockchains

The Liquidity Language for smart contracts

* Work of Alain Mebsout, Fabrice Le Fessant, Çagdas Bozman, Michaël Laporte

LiquidityOCamlPro dev…

Read more...

My 2018 contains robur and starts with re-engineering DNS — Hannes Mehnert (hannes), Jan 11, 2018

2018

At the end of 2017, I resigned from my PostDoc position at University of Cambridge (in the rems project). Early December 2017 I organised the 4th MirageOS hack retreat, with which I'm very satisfied. In March 2018 the 5th retreat will happen (please sign up!).

In 2018 I moved to Berlin and started to work for the (non-profit) Center for the cultivation of technology with our robur.io project "At robur, we build performant bespoke minimal operating systems for high-assurance se…

Read more...

MacOS package updated — Coq, Jan 09, 2018

The macOS installer for Coq 8.7.1 was updated on 2018-01-08 to fix frequent crashes of CoqIDE due to the use of an outdated dependency. Direct link to the new version: coq-8.7.1-1-installer-macos.dmg.

Posts and Talks Elsewhere — Mindy Preston, Dec 23, 2017

View older blog posts.