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

[Alan Schmitt <alan.schmitt@polytechnique.org>]

[-- 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 --]