Adrien Champion adrien.champion@ocamlpro.com This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License. These posts broadly discusses induction as a formal verification technique, which here really means formal program verification. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing directly with induction. The next chapters discuss the following notions: formal logics and formal fram ..read more

Distributing OCaml software on opam is great (if I dare say so myself), but sometimes you need to provide your tools to an audience outside of the OCaml community, or just without recompilations or in a simpler way. However, just distributing the locally generated binaries requires that the users have all the needed shared libraries installed, and a compatible libc. It’s not something you can assume in general, and even if you don’t need any C shared library or are confident enough it will be installed everywhere, the libc issue will arise for anyone using a distribution based on a different ..read more

We are happy to announce the release of opam 2.1.0. Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights. What’s new in opam 2.1? Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step Creation of lock files for reproducible installations (formerly the opam-lock plugin) Switch invariants, replacing the “base packages” in opam 2.0 and allowing for easier compiler upgrades Improved options configuration (see the new option and expanded var sub-c ..read more

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument. Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject. We welcomed Léo Boitel during three months to work on this topic, with Vincent Laviron as mentor, and we’re proud to let him show off what he has achieved in this post. The pr ..read more

We are pleased to announce the minor release of opam 2.0.8. This new version contains some backported fixes: Critical for fish users! Don’t add . to PATH. [#4078] Fix sandbox script for newer ccache versions. [#4079 and #4087] Fix sandbox crash when ~/.cache is a symlink. [#4068] User modifications to the sandbox script are no longer overwritten by opam init. [#4020 & #4092] macOS sandbox script always mounts /tmp read-write, regardless of TMPDIR [#3742, addressing ocaml/opam-repository#13339] pre- and post-session hooks can now print to the console [#4359] Switch-specific pre/post sessio ..read more

OCamlPro was created in 2011 to advocate the adoption of the OCaml language and formal methods in general in the industry. While building a team of highly-skilled engineers, we navigated through our expertise domains, delivering works on the OCaml language and tooling, training companies to the use of strongly-typed languages like OCaml but also Rust, tackling formal verification challenges with formal methods, maintaining the SMT solver Alt-Ergo, designing languages and tools for smart contracts and blockchains, and more! In this article, as every year, we review some of the work we did durin ..read more

A new release of Alt-Ergo (version 2.4.0) is available. You can get it from Alt-Ergo’s website. The associated opam package will be published in the next few days. This release contains some major novelties: Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard. We switched command line parsing to use cmdliner. You will need to use --<option name> instead of -<option name>. Some options have also been renamed, see the manpage or the documentation. We improved the online documentation of your solver, available here. This release also contains some minor novel ..read more

(This article is cross-posted by the Origin Labs team) We are happy to announce the first release of our Solidity parser, written in OCaml using Menhir. This is a joint effort with Origin Labs, the company behind Dune Network, to implement a full interpreter for the Solidity language directly in a blockchain. Solidity is probably the most popular language for smart-contracts, small pieces of code triggered when accounts receive transactions on a blockchain.Solidity is an object-oriented strongly-typed language with a Javascript-like syntax. Solidity was first implemented for th ..read more

Earlier, we dusted-off our Language and Stdlib cheatsheets, for teachers and students. With more time, we managed to design an Opam 2.0 cheat-sheet we are proud of. It is organized into two pages: The everyday average Opam use: Installation, Configuration, Switches, Allowed URL formats, Packages, Exploring, Package pinning, Working with local pins, Sharing a dev setup, Configuring remotes. Peculiar advanced use cases (opam-managed project, publishing, repository maintenance, etc.): Package definition files, Some optional fields, Expressions, External dependencies, Publishing, Repository a ..read more

We are pleased to announce the minor release of opam 2.0.7. This new version contains backported small fixes: Escape Windows paths on manpages [#4129 @AltGr @rjbou] Fix opam installer opam file [#4058 @rjbou] Fix various warnings [#4132 @rjbou @AltGr – fix #4100] Fix dune 2.5.0 promote-install-files duplication [#4132 @rjbou] 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, we keep uploading darwin & macos binaries, but from the 2.1.0 release, only macos ones will ..read more