OCaml Weekly News

I'm happy to announce mwt 0.1.0, a library providing preemptive thread pools for use from Lwt.

mwt supports interaction between Lwt and OCaml's native Thread.t threads. It is similar to Lwt_preemptive, but with user-managed pools of threads. A program may create an arbitrary number of pools. Each thread in a pool has a (potentially unit/meaningless) state which persists for the life of the thread. This state can be useful, for example, when working with bindings to a C library which requires initialization, use and disposal of some value withing a single system thread.

API documentation is available here.

---

Two great OPAM articles by @Khady:

https://khady.info/opam-sandbox.html
https://khady.info/opam-npm.html

---

I'm cleaning up an older piece of OCaml code as I work on it. The author included a huge personal library (basically their own giant stdlib++) and it isn't obvious what parts of it are and aren't relevant to the code I'm actually using.

Are there any good tools for figuring out what code is and isn't live in a program?

I haven’t used it but this looks promising: Dead Code Analyzer.

There was a presentation at ICFP17 about a refactoring tool for ocaml : https://icfp17.sigplan.org/event/ocaml-2017-papers-rotor-first-steps-towards-a-refactoring-tool-for-ocaml

---

It is my pleasure to announce the new release for FoCaLiZe (the 0.9.2 version).

As for previous releases, some bugs have been fixed in the focalizec compiler. This version introduces the Dedukti backend written by Raphaël Cauderlier, taking benefits from Zenon_modulo to ease proofs. The Coq backend now generates Coq code compatible with Coq 8.8. A complete description of changes / new features can in found in the CHANGES file of the distribution. A complete description of changes / new features can in found in the CHANGES file of the distribution.

The 0.9.2 release is available from http://focalize.inria.fr at http://focalize.inria.fr/download/focalize-0.9.2.tgz Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.9.2 and follow the simple instructions written there.

A public GIT repository is also available on GitHub (https://github.com/pessaux-f/focalize), allowing to fetch the latest development state of FoCaLiZe. However, its content is not bullet-proof and may be unstable at some times. It reflects the real-time state of FoCaLiZe and may bring fixes and features not available in previous releases and that will be part of the next release. To join people and discussions write to focalize-users@inria.fr. Implementors also listen to suggestions (and compliments if some ^_^) at the mail address: focalize-devel@inria.fr.

Enjoy.

For the entire FoCaLiZe implementation group,

François Pessaux.

September 2018

What is it FoCaLiZe ?

---

FoCaLiZe is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLiZe provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of properties them from within the program source code.

The FoCaLiZe compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator to produce Coq proof terms that are then formally verified.

The FoCaLiZe compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developed in FoCaLiZe can be efficiently compiled to native code on a large variety of architectures.

Last but not least, FoCaLiZe automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance.

The FoCaLiZe system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation, while proving that their implementation meets its specification or design requirements. The FoCaLiZe language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically generated ultimately relies on Coq formal proof verification.

FoCaLiZe is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantics, featuring a rock-solid infrastructure and greatly improved capabilities.

---

Quick update: converting between ReasonML and OCaml has been deployed to main website. Now when changing language, the code will be converted automatically.

---

I have completed the implementation of parsers and serializers for HTTP/2 frame types. It uses Angstrom/Faraday for the implementation. My first goal was to just focus on a working implementation, so there will be room for improvement for the API when it comes to simplicity, good OCaml style and/or performance, so feedback is welcome about that.

https://github.com/anuragsoni/h2

---

Here is a sneak peek at some potential future features of the Ocaml compiler, discussed by their implementers in these Github Pull Requests.

• Improve stdlib support for bool
• Improve stdlib support for int
• Private items in structures and signatures

---

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

• Full Time: Compiler Engineer at Jane Street in New York & London
• Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong

---