OCaml Weekly News

I lead the formal methods team at Bedrock Systems (https://bedrocksystems.com) and we are looking to hire a full-time engineer working on automation in the Coq proof assistant (which is written in Ocaml). We're very interested in candidates with strong Ocaml background especially in topics related to automated theorem proving, e.g. SAT/SMT solvers, datalog, superposition, resolution, etc. While Coq experience is great, you do not need to be a Coq expert to apply to this position, we're happy to marry your Ocaml expertise with our Coq expertise.

Formal methods are at the core of BedRock's business and we are deeply committed to solving problems of system verification at industrial scale. We get FM techniques and insights into the code early on and use them to build, maintain, and evolve code. This includes developing more agile techniques to keep evolving verified systems once they're built.

We have eight folks on the formal methods team today, hailing from MPI-SWS, MIT CSAIL, Princeton, and other leading research groups. If you're interested, send me an email or you can inquire more broadly at jobs@bedrocksystems.com.

Company overview:

BedRock is building a trustworthy compute base for mission-critical applications . The foundation of the platform is an open source, multi-core, capability-based micro-hypervisor that we are developing and verifying. On top of these deep specifications we are writing and verifying applications to provide an extensible and configurable core.

Our contention is that the time is ripe for verifiably trustworthy systems, for everything from secure phones and industrial IoT to autonomous systems and financial infrastructure. With significant seed funding, great investors, and commercial projects underway, we are growing our team in Boston, the Bay Area, DC, and Germany.

I'm pleased to announce the release of ocaml-aws 1.2.

ocaml-aws aims to provide generated bindings to many AWS services using the botocore specifications. In this version we've bumped version bounds on a bunch of depedencies and also added new bindings for:

• RDS
• Route53
• SDB
• SQS

Please check it out and report any issues.

I am pleased to announce the second release (0.2.0) of fmlib, a functional library with managed effects.

The library has up to now 4 components:

• Some standard datatypes
• Pretty printing functions
• Parsing combinator library
• Primitives to compile to javascript

The last component is the new one in version 0.2.0. Internally it uses js_of_ocaml to compile to javascript. It is an easy to use library of primitive functions to access mainly browser functionality from ocaml and some rudimentary functions to access nodejs functionality.

It can be installed via opam by

opam update
opam install fmlib
opam install fmlib_js

It is located at github

Hint: fmlib is still a bundle of three libraries i.e. three toplevel modules Fmlib_std, Fmlib_pretty and Fmlib_parse. Therefore they have to be used in a dune file with

(libraries fmlib.fmlib_std fmlib.fmlib_pretty fmlib.fmlib_parse ...)

while the new library can be used with

(libraries fmlib_js ...)

This inconvenience will be corrected in the next release.

soupault 2.5.0 offers some features that are unique among SSGs.

There are two new built-in widgets for rewriting internal links, which is useful if you don't host your website at the server root. For example, if you host it at example.com/~user, you cannot just write <img src="/header.png">: it will point to example.com/header.png while you want example.com/~user/header.png instead.

The relative_links widget will convert all internal links to relative links according to their depth in the directory tree. For example, suppose you have <img src="/header.png"> in your page template. Then in about/index.html that link will become <img src="../header.png">; in books/magnetic-fields/index.html it will be <img src="../../header.png"> and so on. This way you can move the website to a subdirectory and it will still work.

The absolute_links widget prepends a prefix to every internal link. Conceptually similar to the site URL option in other SSGs and CMSes, but works for all links, not only links generated by the SSG itself.

I'm happy to announce the release of Timere-parse 0.0.2, the natural language parsing component of Timere, a date time handling and reasoning library. Both packages are under the Timere repo.

Timere-parse allows interpretation of common descriptions of date, time and duration.

there is now ocamlnet-4.1.9 available:

• compatibility with upcoming OCaml-4.12
• some fixes regarding TLS (https)
• a few build-related details

See the project page for download, documentation, a detailed changelog, and the mailing list: http://projects.camlcity.org/projects/ocamlnet.html

The repository is at

https://gitlab.com/gerdstolpmann/lib-ocamlnet3/

opam follows soon.

We are glad to announce the upcoming release of cohttp 4.0.0, a low-level OCaml library for HTTP clients and servers.

This release comes with a big update of the documentation and the examples, both in the README and in the codebase, and improvements and bug fixes from many contributors 🙇 which you will find listed below.

A huge thank you to all the people that helped to get this release ready by raising issues, participating in discussions, sending PRs, and otherwise using our library.

We are pleased to announce the new version of the Try Alt-Ergo website!

As a reminder, Try Alt-Ergo allows you to write and run your problems in your browser without any server computation. It was designed to be a powerful and simple tool to use.

Updates concern these parts of the site:

• A new back end in JavaScript
• Front end with news features (Ace editor, top panel, right panel, etc.)

Take a look at our blogpost to read how we have updated the Try Alt-Ergo website and what's new! You can also visit the Try Alt-Ergo website directly. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback.

Here are links from many OCaml blogs aggregated at OCaml Planet.

• New Try-Alt-Ergo
• TZComet's New Token Viewer