[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

Alan Schmitt
2025-01-28T13:24:40Z

[-- Attachment #1: Type: text/plain, Size: 33038 bytes --]

Hello

Here is the latest OCaml Weekly News, for the week of January 21 to 28,
2025.

Table of Contents
─────────────────

Google Summer of Code
Merlin and OCaml-LSP support experimental project-wide renaming
qcheck-lin and qcheck-stm 0.2
Dune 3.17
Odoc 3 Beta Release
2024 at OCamlPro
Old CWN

Google Summer of Code
═════════════════════

Archive: <https://discuss.ocaml.org/t/google-summer-of-code/3196/12>

Anton Kochkov announced
───────────────────────

Hi everyone! If you plan to apply this year for the Google Summer of
Code, it starts on January 27 and ends on Februrary 11:
<https://opensource.googleblog.com/2025/01/google-summer-of-code-2025-is-here.html>

Merlin and OCaml-LSP support experimental project-wide renaming
═══════════════════════════════════════════════════════════════

Archive:
<https://discuss.ocaml.org/t/ann-merlin-and-ocaml-lsp-support-experimental-project-wide-renaming/16008/1>

vds announced
─────────────

I am delighted to announce that the latest releases of Merlin
(`5.4.1-503') and OCaml-LSP (`1.22.0') for OCaml 5.3 provide
experimental support for _project-wide_ renaming of symbols.

Users of [vscode-ocaml-platform], [ocaml-eglot] or any generic LSP
client can experiment with the new feature right now via the standard
`Rename' feature of their favorite editors. (This is not enabled in
the standard Emacs and Vim modes yet.)

All project-wide features require [the indexer] to be installed and an
up-to date index built with `dune build @ocaml-index --watch' (we only
ship rules for Dune, but the indexer itself is agnostic).

This is a complex feature in an experimental state, please report any
issue you might encounter to [Merlin's issue tracker].

<https://us1.discourse-cdn.com/flex020/uploads/ocaml/original/2X/a/a1bf8be427da9f11d2e65717eb0100778eec9ac3.gif>

*Complete changelog*

[vscode-ocaml-platform]
<https://github.com/ocamllabs/vscode-ocaml-platform/>

[ocaml-eglot]
<https://discuss.ocaml.org/t/ann-release-of-ocaml-eglot-1-0-0/15978>

[the indexer] <https://ocaml.org/p/ocaml-index/latest>

[Merlin's issue tracker] <https://github.com/ocaml/merlin/issues>

merlin 5.4.1
╌╌╌╌╌╌╌╌╌╌╌╌

⁃ merlin binary
• Support for OCaml 5.3
• Use new 5.3 features to improve locate behavior in some
cases. Merlin no longer confuses uids from interfaces and
implementations. (#1857)
• Perform less merges in the indexer (#1881)
• Add initial support for project-wide renaming: occurrences can now
return all usages of all related definitions. (#1877)
⁃ ocaml-index
• Bump magic number after index file format change (#1886)
⁃ vim plugin
• Added support for search-by-type (#1846) This is exposed through
the existing `:MerlinSearch' command, that switches between
search-by-type and polarity search depending on the first
character of the query.

Ocaml-LSP 1.22.0
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

• Enable experimental project-wide renaming of identifiers (#1431)

qcheck-lin and qcheck-stm 0.2
═════════════════════════════

Archive:
<https://discuss.ocaml.org/t/ann-qcheck-lin-and-qcheck-stm-0-2/12301/5>

Jan Midtgaard announced
───────────────────────

Version 0.7 of `qcheck-lin', `qcheck-stm', and
`qcheck-multicoretests-util' is now available on the opam repository:
<https://github.com/ocaml-multicore/multicoretests/releases/tag/0.7>

This release contains two contributions from @polytypic, incl. an
`STM' feature to help testing of ~cmd~s that may raise an effect:

• [#509]: Change/Fix to use a symmetric barrier to synchronize domains
• [#511]: Introduce extended specs to allow wrapping command sequences
• [#517]: Add `Lin' combinators `seq_small', `array_small', and
`list_small'

Happy testing! :smiley:

[#509] <https://github.com/ocaml-multicore/multicoretests/pull/509>

[#511] <https://github.com/ocaml-multicore/multicoretests/pull/511>

[#517] <https://github.com/ocaml-multicore/multicoretests/pull/517>

Dune 3.17
═════════

Archive: <https://discuss.ocaml.org/t/ann-dune-3-17/15770/5>

Etienne Marais announced
────────────────────────

The Dune team is releasing Dune `3.17.2'! :wrench:

This patch release includes some bug fixes. It mostly brings some
fixes for Melange and Wasm_of_ocaml. It also fixes a bug that prevents
the experimental feature, package management, to build with
`ocaml.5.3.0'.

If you encounter a problem with this release, you can report it on the
[ocaml/dune] repository.

[ocaml/dune] <https://github.com/ocaml/dune/issues>

Changelog
╌╌╌╌╌╌╌╌╌

◊ Fixed

• Fix a crash in the Melange rules that would prevent compiling public
library implementations of virtual libraries. (@amonteiro, #11248)
• Pass `melange.emit''s `compile_flags' to the JS emission
phase. (@amonteiro, #11252)
• Disallow private implementations of public virtual libs in `melange'
mode. (@amonteiro, #11253)
• Wasm_of_ocaml: fix the execution of tests in a sandbox. (#11304,
@vouillon)

Odoc 3 Beta Release
═══════════════════

Archive: <https://discuss.ocaml.org/t/ann-odoc-3-beta-release/16043/1>

Jon Ludlam announced
────────────────────

On behalf of the odoc team, I'm thrilled the announce the release of
odoc 3.0.0 beta 1!

This release has been cooking for a long time - it's been more than a
year since odoc 2.4 landed, and a huge amount of work has gone into
this. Thanks to the many others who contributed, either by code or by
comments: @juloo, @panglesd, @EmileTrotignon, @gpetiot, @trefis,
@sabine, @dbuenzli, @yawaramin, and more.

With this release we're including a driver that knows how to use all
of the exciting new features of odoc. This driver has been used to
create the [docs site for the various odoc tools].

Here are a selected set of features:

• :droplet: Rendered source! Jump from any item in the documentation
straight to its rendered source; no matter how much of OCaml's
complex module system you are using.
• :mag: Search by type! Our detective sherlodoc will find your lost
value given its type.
• :warning: Convenient warnings! Warnings are now clearly visible and
useful, no longer buried among your dependencies’ warnings.
• :arrow_heading_up: Self host your documentation, but [link to
ocaml.org] for your dependencies.
• :100: More sidebars! Odoc 3 features a [global sidebar], allowing
you to discover the most hidden corner of underground documentation.
• :exploding_head: Image support! This cutting-edge feature now allows
you to [add images] to your documentation. Video and audio come for
free.
• :spider_web: [Fully cross-package links]! The OCaml docs are now a
true spider web. Prepare to catch bugs, and eat them.
• :cop: Hierarchical documentation pages! We use a modular
language. We don't want a flat namespace for pages.
• :building_construction: The build dependencies are friendlier with
incremental build systems, allowing better shared build caches.
• :heart: Quality of life improvements! Many improvements have been
piling up since we started odoc 3. For instance: `Add clock emoji
before @since tag (@yawaramin, #1089)'!

More explanation of these features is available at the odoc site,
where we have documentation [for authors], for [users of
`odoc_driver'], a [cheatsheet], and [differences from ocamldoc].

[docs site for the various odoc tools] <https://ocaml.github.io/odoc/>

[link to ocaml.org]
<https://ocaml.github.io/odoc/odoc-driver/#remapping-dependencies>

[global sidebar]
<https://ocaml.github.io/odoc/odoc/odoc_for_authors.html#page-tags>

[add images]
<https://ocaml.github.io/odoc/odoc/odoc_for_authors.html#media>

[Fully cross-package links]
<https://ocaml.github.io/odoc/odoc/odoc_for_authors.html#links_and_references>

[for authors] <https://ocaml.github.io/odoc/odoc/odoc_for_authors.html>

[users of `odoc_driver']
<https://ocaml.github.io/odoc/odoc-driver/index.html>

[cheatsheet] <https://ocaml.github.io/odoc/odoc/cheatsheet.html>

[differences from ocamldoc]
<https://ocaml.github.io/odoc/odoc/ocamldoc_differences.html>

How can you help?
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

We need your feedback, both as authors and as users of documentation!
Try things out using the new driver:

┌────
│ $ opam install odoc-driver # don't forget to ~opam update~
│ $ odoc_driver <package list> # For instance: ~$ odoc_driver brr odoc~
│ $ $YOUR_BROWSER _html/index.html
└────

Many of those features' implementations are not set in stone, but
first versions. Please leave comments, either in this thread or as
issues in the repository.

So, navigate already written documentation, and update your own docs
to use the new features!

2024 at OCamlPro
════════════════

Archive: <https://discuss.ocaml.org/t/2024-at-ocamlpro/16046/1>

OCamlPro announced
──────────────────

*2024 at OCamlPro*

At OCamlPro, we like to solve issues that have an impact in the real
world, so we focus most of our efforts on projects that our customers
bring from their domains. We often like to work in the shadows,
focusing on the hardest tasks. Fabrice, OCamlPro’s founder, used to
say that we are the Commandos of OCaml (and now of Rust too), a team
of highly skilled professionals jumping into the most demanding
projects. That ability was illustrated several times in the past, from
the birth of Opam, the development of the Flambda compilers for Jane
Street, the design and development of the Tezos prototype and ICO
platform, to the adventurous extension of the GnuCOBOL open-source
compiler for French DGFiP, even the port of Flow and Hack to Windows
for Meta. Of course, we are always happy to be entrusted with more
common projects and tasks also, building a team and training the
talents required to master all tasks, from the simplest to the hardest
ones. And the hardest ones are often hidden in the middle of the
simplest ones, too.

The OCaml language is the greatest tool at hand to fulfil our
missions, and we try to contribute back to the OCaml ecosystem when
possible. We are always attracted to issues met by OCaml industrial
users, as it gives us the opportunity to directly work for the OCaml
community. Would you be having such issues, do not hesitate to contact
us and discuss what we can do for you!

The beginning of a new year is always a good time to look back at the
previous year, and see what we have achieved with OCaml, and sometimes
for OCaml, in 2024.

Contributions to the OCaml ecosystem
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

◊ Sharing Knowledge

In 2024, we made efforts to dedicate more time to write blog posts to
share our knowledge on the OCaml tools we work on, so that OCaml
developers can use this knowledge in their daily tasks. We wrote a
series of articles on mastering Opam from the ground up ( [Opam 101:
The First Steps], [Opam 102: Pinning Packages]), on the internals of
the Flambda2 compiler ( [Behind the Scenes of the OCaml Optimising
Compiler Flambda2: Introduction and Roadmap], [Flambda2 Ep. 2:
Loopifying Tail-Recursive Functions], [Flambda2 Ep. 3: Speculative
Inlining] ) and one on OCaml backtraces ( [OCaml Backtraces on
Uncaught Exceptions] ). More are coming!

Of course, if you are not patient enough to wait for our next
articles, you may register for one of [our trainings] , we have [OCaml
Beginner] , [OCaml Expert] , [Mastering Opam] , [OCaml Code
Optimization] and we can build new ones on demand. To be honest, in
2024, we received many more requests for our sessions on Rust
(Beginner, Expert and Embedded) than for OCaml, but more for OCaml
ones than for COBOL ones 🙂

[Opam 101: The First Steps]
<https://ocamlpro.com/fr/blog/2024_01_23_opam_101_the_first_steps>

[Opam 102: Pinning Packages]
<https://ocamlpro.com/fr/blog/2024_03_25_opam_102_pinning_packages>

[Behind the Scenes of the OCaml Optimising Compiler Flambda2:
Introduction and Roadmap]
<https://ocamlpro.com/fr/blog/2024_03_18_the_flambda2_snippets_0>

[Flambda2 Ep. 2: Loopifying Tail-Recursive Functions]
<https://ocamlpro.com/fr/blog/2024_05_07_the_flambda2_snippets_2>

[Flambda2 Ep. 3: Speculative Inlining]
<https://ocamlpro.com/fr/blog/2024_08_09_the_flambda2_snippets_3>

[OCaml Backtraces on Uncaught Exceptions]
<https://ocamlpro.com/fr/blog/2024_04_25_ocaml_backtraces_on_uncaught_exceptions>

[our trainings] <https://training.ocamlpro.com>

[OCaml Beginner]
<https://training.ocamlpro.com/en/formation-ocaml-debutant-2022.html>

[OCaml Expert]
<https://training.ocamlpro.com/en/formation-ocaml-expert-2022.html>

[Mastering Opam]
<https://training.ocamlpro.com/en/formation-mastering-opam-2022.html>

[OCaml Code Optimization]
<https://training.ocamlpro.com/en/formation-ocaml-optimisation-2022.html>

◊ Opam, Maintenance and Evolution

Since we created Opam in 2012, we have always had at least one full
time engineer in the Opam team, to maintain it, add new features and
review contributions by other members. This was made possible thanks
to a partnership with Jane Street, and, since 2024, to a partnership
with Tarides.

In 2024, opam had two major releases, [opam 2.3.0 release!] and [opam
2.2.0 release!] . The most ground-breaking change is the *official
native support for Windows*, with access to either mingw-w64 gcc
compilers or Visual Studio MSVC compilers with automatic
detection. This native support is tremendous news for OCaml adoption
in general, and it was built thanks to a lot of work from all the
community, especially on the opam-repository and packages. An
interesting next step to consider for OCaml on Windows would be to
have a single OCaml toolchain for all Windows compilers, using an
integrated assembler for x86/x64 with elf/coff support, something that
we had implemented and tested in OcpWin a long time ago.

Among many fixes and updates, there is the addition of opam tree
<package> to get a nice display of the dependencies of an installed
package, `opam pin –recursive' to look deeper into sub-directories
when searching for opam files and many more small improvements. Check
the blog posts for more details !

[opam 2.3.0 release!]
<https://ocamlpro.com/fr/blog/2024_11_13_opam_2_3_0_releases>

[opam 2.2.0 release!]
<https://ocamlpro.com/fr/blog/2024_07_01_opam_2_2_0_releases>

◊ Work on the OCaml Compiler

We have had a long partnership with Jane Street to improve the
performance of the code generated by the OCaml compiler. The first
outcome of this work was the Flambda backend, which was merged into
OCaml 4.03 in 2016. Since then, we have started a new backend,
[Flambda2] , that is included in the Jane Street OCaml compiler.

In 2024, our team focused its efforts on several new optimizations,
like match in match (simplify pattern-matching appearing in another
pattern-matching after inlining), unbox free vars of closures
(shortcut chains of pointers stored in closures) or the reaper (do not
allocate unused fields of blocks). Such optimizations are often much
more complex than you would think, as guaranteeing that they can be
applied safely is not obvious, requiring escape analysis and other
checks. We were also very active at helping the compiler team at Jane
Street by reviewing their code and adapting our backend to their
needs. If you are interested in this subject, read our blog series on
the topic that was mentioned earlier.

In 2024, we also had an intern working on *modular explicits*, an
extension of OCaml first-class modules with module-dependent
functions, functions taking first-class modules as arguments. This
work can be seen as a first step towards modular implicits, and was
presented [at the OCaml workshop] with Didier Rémy. The [main
pull-request] is still under review, while other smaller ones have
already been merged, leading to interesting extensions inside the
compiler such as new forms of dependent types.

[Flambda2] <https://github.com/ocaml-flambda/flambda-backend>

[at the OCaml workshop]
<https://icfp24.sigplan.org/details/ocaml-2024-papers/1/On-the-design-and-implementation-of-Modular-Explicits>

[main pull-request] <https://github.com/ocaml/ocaml/pull/13275>

◊ Optimizing Geneweb, a Webserver for Genealogy

Last year, we also started working on [Geneweb], a webserver in OCaml
that is used to store family trees by genealogists. Geneweb is a very
old piece of OCaml, initially written around 1996 by Daniel De
Rauglaudre at Inria. It is used both by [Geneanet] , a genealogy
company recently acquired by Ancestry, and the [Roglo association], a
French association that administrates a single family tree of more
than 10 million persons. One of the issues faced by the Roglo
association was that their branch of the software had diverged from
the official one maintained by Geneanet, as Roglo had to use specific
features on their branch to cope with the huge size of their unique
family tree. We helped them by optimizing the official branch, so that
it could host the tree while providing the same latencies for requests
as before. It required optimizing the representation of stored data
(both in OCaml and on disk), how it was accessed through system calls,
and a good understanding of the complex algorithms used by Geneweb,
typically to traverse family members using various relationships.

[Geneweb] <https://github.com/geneweb/geneweb>

[Geneanet] <https://en.geneanet.org/legal/geneanet/>

[Roglo association] <https://asso.roglo.eu/page/350795-accueil>

Contributions to other languages
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

◊ Compiling to Wasm and Wasm Symbolic Execution

Since 2021, OCamlPro has actively contributed to the W3C's efforts on
bringing a dedicated Garbage Collector to WebAssembly - an essential
feature that has now become reality with the increased use of Wasm
(See [How Prime Video updates its app for more than 8,000 device
types] or [Introducing the Disney+ Application Development Kit (ADK)]
).

Our work ensured the official [WasmGC proposal] remained fully
compatible with the needs of OCaml. Crucial to this success was
[Wasocaml], our Flambda-based backend targeting WebAssembly, which
helped drive the proposal's release and subsequent implementation in
2023 across all major browsers.

One of our biggest contributors to this work, Léo Andrès [defended his
PhD at the end of 2024]. The topic was about compiling OCaml to Wasm
but also about another [tool named Owi], developed in close
collaboration with the University of Lisboa. Originally developed as a
"Wasm Swissknife", Owi has evolved into a multi-core, multi-solver,
cross-language symbolic engine. Its capabilities include:
• automated, sound, and partially-correct bug-finding (amounting to a
proof);
• solver-aided programming (think of Rosette for Rocket, but for any
language);
• efficient test-case generation.

Looking ahead, we are excited to combine Wasocaml and Owi, aiming to
*perform symbolic execution of OCaml* programs, and even those with
substantial C components! We've already applied these techniques
successfully to Rust, uncovering a subtle bug in the [Rust standard
library]. If you want to know more about it, have a look at our
[journal article].

Some of this work was funded by NGI/NLnet.

[How Prime Video updates its app for more than 8,000 device types]
<https://www.amazon.science/blog/how-prime-video-updates-its-app-for-more-than-8-000-device-types>

[Introducing the Disney+ Application Development Kit (ADK)]
<https://medium.com/disney-streaming/introducing-the-disney-application-development-kit-adk-ad85ca139073>

[WasmGC proposal] <https://github.com/WebAssembly/gc>

[Wasocaml] <https://github.com/OCamlPro/wasocaml>

[defended his PhD at the end of 2024] <https://theses.fr/s340615>

[tool named Owi] <https://github.com/OCamlPro/owi>

[Rust standard library]
<https://github.com/rust-lang/rust/pull/129321>

[journal article] <https://arxiv.org/pdf/2412.06391>

◊ From Niagara to Kopek, a foot in the Cinema industry

2024 was also a new adventure in entrepreneurship for OCamlPro. In
2023, we [won a grant] from the CNC, the French Center for the Cinema
industry, to work with Antoine Devulder and Denis Mérigoux on the
design of a *DSL for movie producers*. Indeed, distributing earnings
is one of the most complex tasks that a producer must do after a movie
is released, mostly because of the complexity of contracts. So we
designed a DSL, initially called Niagara, that is close enough to
contracts to be simple to write, and automatically computes the exact
distribution of earnings during the entire life of the movie.

In 2024, we decided to create the [Kopek company] with Antoine and
Denis, to commercialize this product. The DSL itself is hidden behind
a no-code interface that makes all interactions with the software easy
and intuitive for producers, and the tool can deal with complex
contracts that no other software on the market can deal with. For
French speakers, the tool was recently [presented at a CNC event] .

[won a grant]
<https://www.cnc.fr/professionnels/actualites/resultats-de-lappel-a-projets---transparence-de-la-remontee-de-recettes-dans-le-secteur-cinema-et-audiovisuel_1931182>

[Kopek company] <https://kopek.fr>

[presented at a CNC event]
<https://www.youtube.com/watch?v=6Q3Y7SNTDmg>

◊ SuperBOL, a powerful LSP for COBOL and Visual Studio Code

For a few years now, OCamlPro has been [involved in the COBOL
ecosystem], mostly to help the French tax administration to deal with
the migration of COBOL code from legacy systems (GCOS mainframes from
the 80s) to Cloud-based platforms. Most of our work was to extend the
[free open-source GnuCOBOL compiler] for the needs of the
application. Moreover, we spent some time creating an *OCaml framework
for COBOL* to better understand this programming language. We released
a large part of this work as an open-source extension for Visual
Studio Code called [SuperBOL Studio OSS]. Backed by our powerful LSP
server, this extension empowers its users with all the features that
developers expect from a modern editor for editing and navigating
COBOL code.

In 2024, we improved the parser to support a larger part of the COBOL
language, we added a powerful indentor of code, powerful code
completion features derived directly from the COBOL grammar (using the
recently added features in Menhir), as well as various ways to display
the control-flow graph of programs ; the latter being particularly
useful when your job is to navigate and modify code written many
decades ago. We built an entire CI/CD system for SuperBOL that
automatically releases cross-compiled, statically linked binaries for
Linux, Windows and MacOS.

[involved in the COBOL ecosystem] <https://superbol.eu>

[free open-source GnuCOBOL compiler]
<https://gnucobol.sourceforge.io/>

[SuperBOL Studio OSS]
<https://github.com/OCamlPro/superbol-studio-oss>

◊ Mlang used at the DGFiP

We have also been involved for some time now in the adaptation of the
[Mlang compiler] to replace the deprecated tooling of the DGFiP
(French Public Finances Directorate) to compute the French Income Tax.

2024 was an important milestone for the project, as Mlang was used for
the *first time in production*. It means that we were able to compute
the exact same results, with comparable performance. Moreover, as the
former compiler used to suffer from overflows that require manual
inspections and re-evaluations, the new compiler already provides
benefits for DGFiP. We are now involved in improving Mlang to handle
multi-year computations, something that used to be performed using
hardly maintainable boilerplate in C, and in improving the general
environment around the compiler, with CI/CD and code-navigation tools.

[Mlang compiler] <https://github.com/MLanguage/mlang>

Formal methods
╌╌╌╌╌╌╌╌╌╌╌╌╌╌

◊ The Alt-Ergo SMT Solver

OCamlPro has been developing the [Alt-Ergo SMT solver] since
2011. Alt-Ergo is usually used behind code verification frameworks
such as [Why3] , [Frama-C] , [TIS Analyzer] or [Adacore Spark] , we
maintain a close relationship with its industrial users through the
[Alt-Ergo Users’ Club] who have access to the most recent features
ahead of time. Current members are [Adacore] , [Trust in Soft] ,
[Thales] , [MERCE] and [CEA List] .

In 2024, we released a brand new version, [Alt-Ergo 2.6] . The
highlights are a better support for bit-vectors, model generation for
algebraic data types, optimization of (maximize) and (minimize), FPA
support, and many other features and bug fixes. Part of this work was
also funded by the [Decysif collaborative project] where we try to
improve Alt-Ergo for use with the [Creusot Rust Verifier] .

[Alt-Ergo SMT solver] <https://alt-ergo.ocamlpro.com/>

[Why3] <https://www.why3.org/>

[Frama-C] <https://frama-c.com/>

[TIS Analyzer] <https://www.trust-in-soft.com/trustinsoft-analyzer>

[Adacore Spark] <https://www.adacore.com/about-spark>

[Alt-Ergo Users’ Club] <https://alt-ergo.ocamlpro.com/#club>

[Adacore] <https://www.adacore.com/>

[Trust in Soft] <https://www.trust-in-soft.com/>

[Thales]
<https://www.thalesgroup.com/fr/global/innovation/recherche-technologie>

[MERCE] <https://www.mitsubishielectric-rce.eu/>

[CEA List] <https://list.cea.fr/fr/>

[Alt-Ergo 2.6]
<https://ocamlpro.com/blog/2024_09_01_alt_ergo_2_6_0_released/>

[Decysif collaborative project] <https://decysif.fr/fr/>

[Creusot Rust Verifier] <https://github.com/creusot-rs/creusot>

◊ EAL6+ Certification

In 2024, we have again been involved in a high level software
certification process ([Common Criteria EAL6+] ) where we successfully
proved our capacity to formalize security policies on low level code
for very important customers, using the Coq proof assistant.

[Common Criteria EAL6+] <https://commoncriteriaportal.org/index.cfm>

◊ Taming Test Generators for C with SeaCoral

Writing unit tests is a very good practice, particularly when using a
weakly-typed language like C. Yet, it is also a cumbersome task,
especially when the goal is to reach 100% coverage of the
code. Fortunately, part of this task can be automated by test
generation tools, based on fuzzing, symbolic execution, and other code
analysis techniques. Each of these techniques has its own strengths
and weaknesses (in terms of performance, number of generated tests, or
targeted coverage criteria), so much so that it often becomes
necessary to combine them in order to achieve good results on
realistic source code. Moreover, these tools are often hard to
understand and configure properly for a project.

In 2024, following previous experimentations (see [“An Efficient
Black-Box Support of Advanced Coverage Criteria for Klee”] ), we
started working on Seacoral, a tool that *automates the generation of
unit tests for C*. Seacoral relies on a unified definition of coverage
criteria that is based on the notion of coverage labels, and is able
to leverage the abilities of many existing test generation techniques
by carefully orchestrating the tools to achieve high coverage with as
few tests as possible. Seacoral leverages FramaC/LTest
<https://www.frama-c.com/fc-plugins/ltest.html> to automatically
annotate the code with coverage labels. It currently supports
[libfuzzer] , [Klee], and [CBMC] . Seacoral can also detect
unreachable code using [LUncov], and reports potential runtime errors.

[“An Efficient Black-Box Support of Advanced Coverage Criteria for
Klee”] <https://dl.acm.org/doi/abs/10.1145/3555776.3577713>

[libfuzzer] <https://llvm.org/docs/LibFuzzer.html>

[Klee] <https://klee-se.org/>

[CBMC] <https://www.cprover.org/cbmc/>

[LUncov] <https://git.frama-c.com/pub/ltest/luncov>

A long time ago
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

If you have never heard of OCamlPro, here are a few examples of
projects that we contributed to the OCaml ecosystem, since the
creation of OCamlPro in 2011.

• `opam' (*): probably the most powerful package manager in terms of
constraints optimization, thanks to the work on CUDF by Roberto Di
Cosmo's team. Now the official package manager of OCaml.
• `flambda1' and `flambda2' (*): a backend for the native compiler
with multiple additionnal optimization passes. Flambda1 was merged
into the official OCaml compiler, while Flambda2 is integrated in
the Jane Street OCaml compiler.
• `ocp-indent' (*): a tool to automatically indent OCaml code in
editors, with modes for Emacs, Vi, Vscode, etc. with per-project
configuration. A must-use for collaborative edition instead of
ocamlformat.
• `ocp-index' (*): a tool to lookup types and definitions in an OCaml
project, with modes for Emacs, Vi, etc. based on cmt files.
• `ocp-memprof': the most powerful memory profiler for OCaml to ever
exist. With almost no impact on runtime performance, it was able to
dump compressed memory dumps of the OCaml heap with full type
information.
• `ocp-build' : the first composable build tool for OCaml before dune,
it was able to build any OCaml project with full parallelism. It
supported additional languages to build cross-language projects.
• `ocp-win' : a full OCaml distribution for Windows, coming with a
simple graphical installer. Its compiler could be configured to
target any Windows C toolchain, such as MinGW, MSVC or Cygwin, and
environment, such as Msys, Cygwin and Windows shells, thanks to the
use of an integrated x86/64 and elf/coff assembler in OCaml.

(*) thanks to funding by Jane Street

Your Project, our Expertise
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

If you're looking to leverage the power and flexibility of OCaml for
your projects, we’d love to collaborate with you. At OCamlPro, we
bring years of expertise, innovation, and a deep commitment to
enhancing the OCaml ecosystem. Whether you need support with custom
development, performance optimization, tooling, or anything in
between, we are here to help.

Let's build something great together—reach out to us today to discuss
your project!

Old CWN
═══════

If you happen to miss a CWN, you can [send me a message] and I'll mail
it to you, or go take a look at [the archive] or the [RSS feed of the
archives].

If you also wish to receive it every week by mail, you may subscribe
to the [caml-list].

[Alan Schmitt]

[send me a message] <mailto:alan.schmitt@polytechnique.org>

[the archive] <https://alan.petitepomme.net/cwn/>

[RSS feed of the archives] <https://alan.petitepomme.net/cwn/cwn.rss>

[caml-list] <https://sympa.inria.fr/sympa/info/caml-list>

[Alan Schmitt] <https://alan.petitepomme.net/>

[-- Attachment #2: Type: text/html, Size: 44528 bytes --]