Build:
- 0
2026-06-30 18:06.27: New job: docker build {
"commit": "3a83af79c14bb0b43f22508d4aa72cbb21ed8144",
"dockerfile": {
"file": "Dockerfile"
},
"docker_context": null,
"squash": false,
"buildx": true,
"build_args": [],
"path": null
}
2026-06-30 18:06.27: Checking out commit 3a83af79. To reproduce:
git clone --recursive "https://github.com/tarides/tarides.com.git" && cd "tarides.com" && git fetch origin "refs/pull/1110/head" && git reset --hard 3a83af79
2026-06-30 18:06.27: Exec: "cp" "-a" "--" "/var/lib/ocurrent/var/git/tarides.com.git-c625fb5f52c964610b54f32d27d46965b6bf2fad211456d66e1ff8a0f4c02fec/.git"
"/tmp/git-checkout5ae025"
2026-06-30 18:06.31: Exec: "git" "-C" "/tmp/git-checkout5ae025" "submodule"
"deinit" "--force" "--all"
2026-06-30 18:06.31: Exec: "git" "-C" "/tmp/git-checkout5ae025" "reset"
"--hard" "-q" "3a83af79c14bb0b43f22508d4aa72cbb21ed8144"
2026-06-30 18:06.33: Exec: "git" "-c" "protocol.file.allow=always" "-C"
"/tmp/git-checkout5ae025" "submodule" "update"
"--recursive" "--init" "--no-fetch"
2026-06-30 18:06.33: Exec: "docker" "buildx" "build" "--pull" "-f" "/tmp/git-checkout5ae025/Dockerfile"
"--iidfile" "/tmp/git-checkout5ae025/docker-iid"
"--" "/tmp/git-checkout5ae025"
#0 building with "default" instance using docker driver
#1 [internal] load build definition from Dockerfile
#1 transferring dockerfile: 1.98kB done
#1 DONE 0.0s
#2 [internal] load metadata for docker.io/library/alpine:3.22
#2 DONE 0.5s
#3 [internal] load .dockerignore
#3 transferring context: 77B done
#3 DONE 0.0s
#4 [build 1/13] FROM docker.io/library/alpine:3.22@sha256:14358309a308569c32bdc37e2e0e9694be33a9d99e68afb0f5ff33cc1f695dce
#4 DONE 0.0s
#5 [run 2/11] RUN --mount=type=cache,target=/var/cache/apk,sharing=locked ln -s /var/cache/apk /etc/apk/cache && apk -U upgrade && apk add git gmp libev oniguruma-dev
#5 CACHED
#6 [run 3/11] RUN chmod -R 755 /var
#6 CACHED
#7 [internal] load build context
#7 transferring context: 601.15MB 2.0s done
#7 DONE 2.0s
#8 [build 2/13] RUN --mount=type=cache,target=/var/cache/apk,sharing=locked ln -s /var/cache/apk /etc/apk/cache && apk -U upgrade && apk add autoconf curl-dev gmp-dev imagemagick imagemagick-jpeg imagemagick-webp inotify-tools libev-dev oniguruma-dev openssl-dev curl bash gcc musl-dev make m4 git autoconf
#8 CACHED
#9 [build 3/13] WORKDIR /root
#9 CACHED
#10 [build 4/13] RUN curl -fsSL https://get.dune.build/install | sh
#10 CACHED
#11 [build 5/13] COPY --link tarides-com.opam .
#11 CACHED
#12 [build 6/13] COPY --link dune-project .
#12 CACHED
#13 [build 7/13] RUN dune --version && dune pkg lock && dune build @pkg-install
#13 CACHED
#14 [build 8/13] COPY --link ./generate-images.sh .
#14 CACHED
#15 [build 9/13] COPY --link data/ data/
#15 DONE 2.5s
#16 [build 10/13] COPY --link src/gen src/gen
#16 DONE 0.1s
#17 [build 11/13] RUN ./generate-images.sh
#17 0.248 + dune exec -- src/gen/main.exe file.dune
#17 5.383 + dune build @convert
#17 DONE 381.8s
#18 [build 12/13] COPY --link . .
#18 DONE 1.6s
#19 [build 13/13] RUN dune build && dune build --profile=release
#19 6.610 File "src/data/dune", lines 6-16, characters 0-222:
#19 6.610 6 | (rule
#19 6.610 7 | (target blog_gen.ml)
#19 6.610 8 | (deps
#19 6.610 9 | (source_tree %{workspace_root}/data/blog/)
#19 6.610 10 | (:gen %{workspace_root}/src/gen/main.exe))
#19 6.610 11 | (action
#19 6.610 12 | (chdir
#19 6.610 13 | %{workspace_root}
#19 6.610 14 | (with-stdout-to
#19 6.610 15 | %{target}
#19 6.610 16 | (run %{gen} blog)))))
#19 6.610 gen: internal error, uncaught exception:
#19 6.610 Invalid_argument("expected metadata at the top of the file blog/content/2026-07-22.ortac-0.8.0.md. Got --- \nauthor: Nicolas Osborne \ntitle: \"Formal Verification: Release of Ortac 0.8.0 and Testing with Domains\" \nimage: todo \nimage-alt: todo \ndate: 2026-07-22 \ntags: ocaml, devtools, \nsynopsis: todo \ndescription: todo \n--- \nWe have recently released a new version, number [0.8.0](https://github.com/ocaml-gospel/ortac/releases/tag/0.8.0), of the Ortac tool as part of the [Gospel](https://github.com/ocaml-gospel) ecosystem for dynamic formal verification. \n\nGospel is a contract-based formal specification language for OCaml. It allows the user to give logical models to abstract data-types and describe the expected behaviour of functions with pre- and post-conditions. Specifications are type-checked with `gospel check file.mli`. In order to obtain some guarantees about your OCaml implementation with respect to the Gospel annotations, you need to use Ortac. The core idea behind `ortac` is to translate a subset of the Gospel specification language into OCaml code and use these translations to generate runtime checking.\n\nFor more context, you can explore our [previous post discussing our involvement in the Gospel Project](https://tarides.com/blog/2024-09-03-getting-specific-announcing-the-gospel-and-ortac-projects/) or check out our [tutorial on how to use Ortac/QCheck-STM](https://tarides.com/blog/2025-09-10-dynamic-formal-verification-in-ocaml-an-ortac-qcheck-stm-tutorial/). \n\n## How Ortac Works: Modes\nOrtac has a plugin architecture proposing mainly two modes: one to generate QCheck-STM tests and one to wrap original functions with runtime assertion checking. Those are respectively called the QCheck-STM mode (or Ortac/QCheck-STM) and the wrapper mode (or Ortac/Wrapper). We also propose a `dune` mode to help generate the necessary Dune boilerplate.\n\nOne other important piece of the architecture is the Ortac runtime. The code generated by the two first modes (QCheck-STM and Wrapper), depends on runtime functionalities. Among those is the OCaml trusted implementation of the Gospel logical library (used to write the specifications). Then, there are some pieces that are specific to each mode. Adding new functionalities can involve modifying or extending the runtime. This needs to be done carefully as it involves reasoning about the interaction between the generated code and the runtime.\n\nThe new release focusses on making Ortac/QCheck-STM take advantage of more features from the [QCheck-STM test framework](https://ocaml-multicore.github.io/multicoretests/dev/qcheck-stm/):\nnamely testing in a parallel context and flexibility of the command generation. In this post, I will focus on testing with multiple domains using the latest version of Ortac. \n\n## Parallel Safety Testing and Ortac 0.8.0\nNow, regarding testing in a parallel context, in the original QCheck-STM test framework, this feature is included 'for free' when we write an OCaml specification for a library. It is just a matter of instanciating the `STM_domain.Make` functor rather than the `STM_sequential.Make` one. So, why did we need a new release for Ortac to be able to generate a test suite for parallel safety with QCheck-STM? \n\nThere are two reasons:\n1. The introduction of the bug report feature in version 0.2.0\n2. The coverage of the function with multiple SUT arguments and SUT-returning functions since version 0.4.0\n\nWe'll start with how we've dealt with the coverage of SUT-returning functions and then move to the bug report feature.\n\n### Multiple SUTs and SUT-Returning Functions\nAs a reminder, SUT stands for System Under Test. It is the type of the OCaml value that is being tested against its model (called the `state`) in the QCheck-STM tests.\n\nFor example, if we have a library exposing a type `'a t` and want to write some QCheck-STM tests for this library, we will declare a `type sut = char t`. We indeed have to instantiate the `'a` type parameter in order to run tests.\n\nQCheck-STM tests generate a program based on calls to function from the library we want to test, run them and compare the traces of this run with a run of the same program on the model. You can read more about this [in our blog post on property based tests for OCaml 5](https://tarides.com/blog/2024-04-24-under-the-hood-developing-multicore-property-based-tests-for-ocaml-5/).\n\n<!-- TODO: add more references? -->\n\nNow, since version 0.4.0, and thanks to [Nikolaus Huber's internship](https://tarides.com/blog/2024-09-24-summer-of-internships-projects-from-the-ocaml-compiler-team/),\nOrtac/QCheck-STM supports testing functions with multiple SUTs as arguments and SUT-returning functions. These functions are not easily tested when we write QCheck-STM tests by hand.\n\nOne example of a function with multiple SUTs as its argument is the comparison function. If you have only one SUT at hand, you can't really test the comparison function.\n\nOne example of a SUT-returning function is the copy function. The SUT being an abstract data-type, you can't really check postconditions about it. You'll need to wait until it appears as an argument to a later call, for example to a `length` or a `get` function.\n\nIn order to include these functions in the test coverage, the generated tests call a runtime that maintains a stack of SUTs. When the tests run a command, the SUTs arguments are popped from the stack. After the call the returned SUT value is pushed on the stack *after* the arguments have also been pushed back on the stack in an order-preserving way. You can read more on this topic [here](https://hal.science/hal-05073121).\n\n<!-- TODO: schema? -->\n\nWhen adding support for testing with Domains, we had to be careful about parallel access to the arguments and decide what to do with newly created SUTs.\n\nRegarding the SUT arguments, we have to make parallel access safe, but not too much: we still want to be able to catch bugs from parallel access to individual SUTs, but we don't want to catch bugs caused by race conditions on the stack of SUTs implemented in `ortac-qcheck-stm-runtime`. In other words, we need to make access to the stack safe, but we don't want to add safety to the element of the stack beyond the one provided by the library we are testing.\n\nIn the original implementation, the SUT arguments were popped from the stack. In a parallel setting when a stack is not made parallel-safe, anything can happen. First of all, we would be relying on the scheduler to make a race condition on the stack of SUTs in order to test parallel access to the same SUT. Parallel-safety is hard enough to test without adding one more layer of probability. Then, once the same SUT has been selected by both domains, it will be pushed back twice.\n\n```\n<p align=\"center\">\n <img alt=\"Parallel access to the top of the SUT stack\" src=\"../images/parallel-access.jpg\" width=\"30%\">\n \n <img alt=\"Parallel run of two calls with the same SUT\" src=\"../images/parallel-run.jpg\" width=\"30%\">\n \n <img alt=\"Deduplication of the SUT when pushing back on the stack\" src=\"../images/push-back-arguments.jpg\" width=\"30%\">\n</p>\n```\n\nWe can't make the stack of SUTs completely parallel safe neither. Indeed, in this case we will end up never testing parallel access to the same SUT, completely defeating the point of targeting QCheck-STM+Domains tests.\n\n<!-- TODO: schema? -->\n\nThe solution we've chosen is to modify the SUTs in place in the stack.\n\n```\n<p align=\"center\">\n<img alt=\"Call0 access top of the stack without poping\" src=\"../images/call0-access.jpg\" width=\"30%\">\n \n<img alt=\"Call1 access top of the stack without poping\" src=\"../images/call1-access.jpg\" width=\"30%\">\n \n<img alt=\"Parallel run modifying the SUT in place on the stack\" src=\"../images/safe-parallel-run.jpg\" width=\"30%\">\n</p>\n```\n\nNow, regarding the newly created SUTs, do we want to push them to the stack or not?\n\nIn sequential testing, they are indeed pushed onto the stack. This it what allows us to test them: if a newly created SUT does not conform to its model (there is a bug in the function), then the behaviour of the rest of the program will most probably differ from the behaviour of the model.\n\nWhen testing in a parallel context, the generated program is a triplet: a sequential prefix that allows us to put the SUT in a random state and two parallel tails that allows us to test the behaviour of the library in a parallel context. It is quite clear that we can still push the SUTs created in the sequential prefix on the stack: the behaviour is no different than when testing in a sequential context. But the stack of SUTs being shared, we can't push the ones created in the parallel tails onto it: this would allow a function from the other domain to access it, which is not the desired semantic.\n\nMore precisely, we need to enforce two new properties of how we handle SUTs in the runtime:\n\n1. A call from one of the parallel tails should never pick as argument a SUT created in the other parallel tail\n2. A call from one of the parallel tails should be able to pick as argument a shared SUT (created at initialisation or during the sequential prefix)\n\n(1) is a behaviour that doesn't happen in a real run and (2) is precisely the behaviour we want to test.\n\nOne possibility would be to add two other stacks to the runtime: one for each of the parallel tails. Enforcing the first property is then relatively easy: a call fom one of the parallel tails is not allowed to pick as an argument a SUT from the stack of SUTs on the other parallel tail. Enforcing the second property would in contrast necessitate a bit more work. Indeed, we want to be able to pick SUTs from the stack attached to the parallel tail **and** from the one attached to the sequential prefix. This means replacing the current mechanism that just takes the arguments at the top of the stack by one that randomly chooses arguments from the two stacks (the sequential one and the correct parallel one).\n\nThe main concern here is not really the technical challenge (though, a more complex system means a greater possibility of bugs and we don't want bugs in our test frameworks). The main concern is that this implementation would reduce the probability that one SUT appears as argument of two parallel calls.\n\nThe solution we've chosen is to simply not push on the stack SUTs created in the parallel tails. This enforces the two properties above: SUTs from a parallel call are never taken as arguments of any call and every SUT argument is a shared SUT.\n\nIn order to differentiate between the different contexts at runtime, we simply add a flag to the generated commands to indicate whether they are meant to be run in a sequential context or in a parallel one. Then, the function that handles the stack of SUTs and the one that handles the stack of states look at this flag to decide whether to push the newly created SUT and corresponding state to the relevant stacks.\n\nThis way, SUT-returning functions are still fully tested thanks to the sequential prefix, and how the parallel tails are handled is not made more complex than necessary. In particular, no modification of the runtime was needed (which made reasoning about the modifications a lot easier).\n\n## The Bug Report Feature\n\nSince version 0.2.0, tests generated by Ortac/QCheck-STM generate a bug report in case of test failure. This is a very nice feature that provides the user with:\n\n1. The piece(s) of Gopsel specification that has been violated\n2. The expected returned value (to be compared with the actual returned value) if it is computable from the Gospel specifications\n3. A reproduction case in the form of a runnable OCaml program\n\nThese pieces of information need to be collected while checking the equivalence between the observed behaviour and the behaviour of the model.\n\nIn the original QCheck-STM test framework, a program is generated, then it runs and the observable behaviour is stored (for example the returned value of a `length` function). Finally, the observed behaviour is compared to the behaviour of running the equivalent program on a model, checking user-defined postconditions.\n\nThis comparison is done in `STM.Internal.Make.check_disagree` for the sequential run and in `STM.Internal.Make.check_obs` for the parallel one. Both are parameterised by the `postcond` predicate. In hand-written QCheck-STM tests, this `postcond` predicate is obviously hand-writeen and in Ortac-generated QCheck-STM tests, it is generated based on Gospel postcondition clauses and invariants.\n\nNow, in order to build the bug report in case of test failure, we need the `postcond` function to not be a simple predicate anymore. We need it to return an optional report with the Gospel terms that were violated, the string representation of the call and, if possible, the expected result of the call.\n\nThe consequence of this change is that we have to reimplement the `check_disagree` and the `check_obs` functions. The former was reimplemented as part of the 0.2.0 release, the latter in the present one. But, as these are the pieces of code that actually do the testing, one has to be extra-careful when modifying them. We've adopted a step-by-step approach to make the preservation of the semantics scrutinasable with testing and reviewing.\n\nThe `postcond` function that the Ortac/QCheck-STM-generated code uses returns an `option` type rather than a boolean. The `None` case corresponds to `true` and the `Some report` one to `false`. The idea is to return an explanation in case of test failure.\n\nThe first step is to adapt the original function to deal with this `postcond` functional argument. On a technical level it is trivial, the main benefit is that the `check_obs` function is now in the `ortac` code base.\n\nThis function now looks like this:\n\n```ocaml\nlet check_obs postcond =\n (* ignore the report for now *)\n let postcond c s r = Option.is_none @@ postcond c s r in\n let rec aux pref cs1 cs2 s =\n match pref with\n | (c, res) :: pref' ->\n let b = postcond c s res in\n b && aux pref' cs1 cs2 (Spec.next_state c s)\n | [] -> (\n match (cs1, cs2) with\n | [], [] -> true\n | [], (c2, res2) :: cs2' ->\n let b = postcond c2 s res2 in\n b && aux pref cs1 cs2' (Spec.next_state c2 s)\n | (c1, res1) :: cs1', [] ->\n let b = postcond c1 s res1 in\n b && aux pref cs1' cs2 (Spec.next_state c1 s)\n | (c1, res1) :: cs1', (c2, res2) :: cs2' ->\n (let b1 = postcond c1 s res1 in\n b1 && aux pref cs1' cs2 (Spec.next_state c1 s))\n ||\n let b2 = postcond c2 s res2 in\n b2 && aux pref cs1 cs2' (Spec.next_state c2 s))\n in\n aux\n```\n\nThe general idea behind this `check_obs` function is to find a sequential explanation for the behaviour observed in the run involving parallelism. The sequential prefix is first checked against the `state` and using the `postcond` function provided as argument. Then, we explore all the possible sequential interleavings of the two parallel tails, using boolean operators short-circuits to stop when we found one interleaving that expains the observed behaviour.\n\nThe next step is to actually deal with the optional report `postcond` is returning. This means modifying the body of `check_obs` to make it return the report.\n\nMoving from boolean to option type implies adding a lot of `match`es that could render the code harder to read. Adding to that, the translation is somewhat counter-intuitive: `None` is actually the max and `Some` the min of the boolean algebra. This makes the translation error-prone.\n\nThe path we've chosen to gain trust in our modifications, is to try to make it as clear as possible on the syntactic level that the semantics are preserved.\n\nWe've done that by defining an infix operator corresponding to the equivalent of the conjunction and to the equivalent of the disjunction, using the `lazy` type to translate the boolean short-circuits.\n\nBy using these new infix operators in place of the boolean ones, we can clearly see in the diff between the two implementations that the semantic is preserved:\n\n```diff\n+ let ( &&& ) o1 o2 = match o1 with None -> Lazy.force o2 | _ -> o1\n+ let ( ||| ) o1 o2 = match o1 with None -> None | Some _ -> Lazy.force o2\n+\n let check_obs postcond =\n- (* ignore the report for now *)\n- let postcond c s r = Option.is_none @@ postcond c s r in\n let rec aux pref cs1 cs2 s =\n match pref with\n | (c, res) :: pref' ->\n- let b = postcond c s res in\n- b && aux pref' cs1 cs2 (Spec.next_state c s)\n+ postcond c s res &&& lazy (aux pref' cs1 cs2 (Spec.next_state c s))\n | [] -> (\n match (cs1, cs2) with\n- | [], [] -> true\n+ | [], [] -> None\n | [], (c2, res2) :: cs2' ->\n- let b = postcond c2 s res2 in\n- b && aux pref cs1 cs2' (Spec.next_state c2 s)\n+ postcond c2 s res2\n+ &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))\n | (c1, res1) :: cs1', [] ->\n- let b = postcond c1 s res1 in\n- b && aux pref cs1' cs2 (Spec.next_state c1 s)\n+ postcond c1 s res1\n+ &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))\n | (c1, res1) :: cs1', (c2, res2) :: cs2' ->\n- (let b1 = postcond c1 s res1 in\n- b1 && aux pref cs1' cs2 (Spec.next_state c1 s))\n- ||\n- let b2 = postcond c2 s res2 in\n- b2 && aux pref cs1 cs2' (Spec.next_state c2 s))\n+ postcond c1 s res1\n+ &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))\n+ ||| lazy\n+ (postcond c2 s res2\n+ &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))))\n in\n aux\n```\n\nObviously, this commit needs special attention in the review process, but it is made quite easy to review. In order to be able to display a runnable program leading to the reported postcondition violation, we need to collect the traces of calls. Adding this collection on top of the previous modifications doesn't change the structure and the logic of the function.\n\nIn conclusion, in order to get a bug report for Ortac/QCheck-STM+Domains, we had to reimplement the heart of the test framework, the `check_obs` function. As it should be, we heavily rely on code review to make sure we implement the expected logic, and we tried to make the code review as easy as possible.\n\n## Funding\nThis work is partly funded by the research grant [ANR-22-CE48-0013](https://anr.fr/Projet-ANR-22-CE48-0013).\n\n## Until Next Time\nYou can connect with us on [Bluesky](https://bsky.app/profile/tarides.com),\n[Mastodon](https://mastodon.social/@tarides),\n[Threads](https://www.threads.net/@taridesltd), and\n[LinkedIn](https://www.linkedin.com/company/tarides) or sign up for our mailing\nlist to stay updated on our latest projects. We look forward to hearing from\nyou!\n")
#19 6.610 Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
#19 6.610 Called from Dune__exe__Blog.decode in file "src/gen/blog.ml", line 286, characters 19-58
#19 6.610 Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
#19 6.610 Called from Dune__exe__Utils.map_files in file "src/gen/utils.ml", line 56, characters 23-59
#19 6.610 Called from Dune__exe__Blog.all in file "src/gen/blog.ml", line 302, characters 2-51
#19 6.610 Called from Dune__exe__Blog.template in file "src/gen/blog.ml", line 308, characters 4-12
#19 6.610 Called from Dune__exe__Main.cmds.(fun) in file "src/gen/main.ml", line 19, characters 48-61
#19 6.610 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 22, characters 19-24
#19 6.610 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 41, characters 7-16
#19 ERROR: process "/bin/sh -c dune build && dune build --profile=release" did not complete successfully: exit code: 1
------
> [build 13/13] RUN dune build && dune build --profile=release:
6.610 Invalid_argument("expected metadata at the top of the file blog/content/2026-07-22.ortac-0.8.0.md. Got --- \nauthor: Nicolas Osborne \ntitle: \"Formal Verification: Release of Ortac 0.8.0 and Testing with Domains\" \nimage: todo \nimage-alt: todo \ndate: 2026-07-22 \ntags: ocaml, devtools, \nsynopsis: todo \ndescription: todo \n--- \nWe have recently released a new version, number [0.8.0](https://github.com/ocaml-gospel/ortac/releases/tag/0.8.0), of the Ortac tool as part of the [Gospel](https://github.com/ocaml-gospel) ecosystem for dynamic formal verification. \n\nGospel is a contract-based formal specification language for OCaml. It allows the user to give logical models to abstract data-types and describe the expected behaviour of functions with pre- and post-conditions. Specifications are type-checked with `gospel check file.mli`. In order to obtain some guarantees about your OCaml implementation with respect to the Gospel annotations, you need to use Ortac. The core idea behind `ortac` is to translate a subset of the Gospel specification language into OCaml code and use these translations to generate runtime checking.\n\nFor more context, you can explore our [previous post discussing our involvement in the Gospel Project](https://tarides.com/blog/2024-09-03-getting-specific-announcing-the-gospel-and-ortac-projects/) or check out our [tutorial on how to use Ortac/QCheck-STM](https://tarides.com/blog/2025-09-10-dynamic-formal-verification-in-ocaml-an-ortac-qcheck-stm-tutorial/). \n\n## How Ortac Works: Modes\nOrtac has a plugin architecture proposing mainly two modes: one to generate QCheck-STM tests and one to wrap original functions with runtime assertion checking. Those are respectively called the QCheck-STM mode (or Ortac/QCheck-STM) and the wrapper mode (or Ortac/Wrapper). We also propose a `dune` mode to help generate the necessary Dune boilerplate.\n\nOne other important piece of the architecture is the Ortac runtime. The code generated by the two first modes (QCheck-STM and Wrapper), depends on runtime functionalities. Among those is the OCaml trusted implementation of the Gospel logical library (used to write the specifications). Then, there are some pieces that are specific to each mode. Adding new functionalities can involve modifying or extending the runtime. This needs to be done carefully as it involves reasoning about the interaction between the generated code and the runtime.\n\nThe new release focusses on making Ortac/QCheck-STM take advantage of more features from the [QCheck-STM test framework](https://ocaml-multicore.github.io/multicoretests/dev/qcheck-stm/):\nnamely testing in a parallel context and flexibility of the command generation. In this post, I will focus on testing with multiple domains using the latest version of Ortac. \n\n## Parallel Safety Testing and Ortac 0.8.0\nNow, regarding testing in a parallel context, in the original QCheck-STM test framework, this feature is included 'for free' when we write an OCaml specification for a library. It is just a matter of instanciating the `STM_domain.Make` functor rather than the `STM_sequential.Make` one. So, why did we need a new release for Ortac to be able to generate a test suite for parallel safety with QCheck-STM? \n\nThere are two reasons:\n1. The introduction of the bug report feature in version 0.2.0\n2. The coverage of the function with multiple SUT arguments and SUT-returning functions since version 0.4.0\n\nWe'll start with how we've dealt with the coverage of SUT-returning functions and then move to the bug report feature.\n\n### Multiple SUTs and SUT-Returning Functions\nAs a reminder, SUT stands for System Under Test. It is the type of the OCaml value that is being tested against its model (called the `state`) in the QCheck-STM tests.\n\nFor example, if we have a library exposing a type `'a t` and want to write some QCheck-STM tests for this library, we will declare a `type sut = char t`. We indeed have to instantiate the `'a` type parameter in order to run tests.\n\nQCheck-STM tests generate a program based on calls to function from the library we want to test, run them and compare the traces of this run with a run of the same program on the model. You can read more about this [in our blog post on property based tests for OCaml 5](https://tarides.com/blog/2024-04-24-under-the-hood-developing-multicore-property-based-tests-for-ocaml-5/).\n\n<!-- TODO: add more references? -->\n\nNow, since version 0.4.0, and thanks to [Nikolaus Huber's internship](https://tarides.com/blog/2024-09-24-summer-of-internships-projects-from-the-ocaml-compiler-team/),\nOrtac/QCheck-STM supports testing functions with multiple SUTs as arguments and SUT-returning functions. These functions are not easily tested when we write QCheck-STM tests by hand.\n\nOne example of a function with multiple SUTs as its argument is the comparison function. If you have only one SUT at hand, you can't really test the comparison function.\n\nOne example of a SUT-returning function is the copy function. The SUT being an abstract data-type, you can't really check postconditions about it. You'll need to wait until it appears as an argument to a later call, for example to a `length` or a `get` function.\n\nIn order to include these functions in the test coverage, the generated tests call a runtime that maintains a stack of SUTs. When the tests run a command, the SUTs arguments are popped from the stack. After the call the returned SUT value is pushed on the stack *after* the arguments have also been pushed back on the stack in an order-preserving way. You can read more on this topic [here](https://hal.science/hal-05073121).\n\n<!-- TODO: schema? -->\n\nWhen adding support for testing with Domains, we had to be careful about parallel access to the arguments and decide what to do with newly created SUTs.\n\nRegarding the SUT arguments, we have to make parallel access safe, but not too much: we still want to be able to catch bugs from parallel access to individual SUTs, but we don't want to catch bugs caused by race conditions on the stack of SUTs implemented in `ortac-qcheck-stm-runtime`. In other words, we need to make access to the stack safe, but we don't want to add safety to the element of the stack beyond the one provided by the library we are testing.\n\nIn the original implementation, the SUT arguments were popped from the stack. In a parallel setting when a stack is not made parallel-safe, anything can happen. First of all, we would be relying on the scheduler to make a race condition on the stack of SUTs in order to test parallel access to the same SUT. Parallel-safety is hard enough to test without adding one more layer of probability. Then, once the same SUT has been selected by both domains, it will be pushed back twice.\n\n```\n<p align=\"center\">\n <img alt=\"Parallel access to the top of the SUT stack\" src=\"../images/parallel-access.jpg\" width=\"30%\">\n \n <img alt=\"Parallel run of two calls with the same SUT\" src=\"../images/parallel-run.jpg\" width=\"30%\">\n \n <img alt=\"Deduplication of the SUT when pushing back on the stack\" src=\"../images/push-back-arguments.jpg\" width=\"30%\">\n</p>\n```\n\nWe can't make the stack of SUTs completely parallel safe neither. Indeed, in this case we will end up never testing parallel access to the same SUT, completely defeating the point of targeting QCheck-STM+Domains tests.\n\n<!-- TODO: schema? -->\n\nThe solution we've chosen is to modify the SUTs in place in the stack.\n\n```\n<p align=\"center\">\n<img alt=\"Call0 access top of the stack without poping\" src=\"../images/call0-access.jpg\" width=\"30%\">\n \n<img alt=\"Call1 access top of the stack without poping\" src=\"../images/call1-access.jpg\" width=\"30%\">\n \n<img alt=\"Parallel run modifying the SUT in place on the stack\" src=\"../images/safe-parallel-run.jpg\" width=\"30%\">\n</p>\n```\n\nNow, regarding the newly created SUTs, do we want to push them to the stack or not?\n\nIn sequential testing, they are indeed pushed onto the stack. This it what allows us to test them: if a newly created SUT does not conform to its model (there is a bug in the function), then the behaviour of the rest of the program will most probably differ from the behaviour of the model.\n\nWhen testing in a parallel context, the generated program is a triplet: a sequential prefix that allows us to put the SUT in a random state and two parallel tails that allows us to test the behaviour of the library in a parallel context. It is quite clear that we can still push the SUTs created in the sequential prefix on the stack: the behaviour is no different than when testing in a sequential context. But the stack of SUTs being shared, we can't push the ones created in the parallel tails onto it: this would allow a function from the other domain to access it, which is not the desired semantic.\n\nMore precisely, we need to enforce two new properties of how we handle SUTs in the runtime:\n\n1. A call from one of the parallel tails should never pick as argument a SUT created in the other parallel tail\n2. A call from one of the parallel tails should be able to pick as argument a shared SUT (created at initialisation or during the sequential prefix)\n\n(1) is a behaviour that doesn't happen in a real run and (2) is precisely the behaviour we want to test.\n\nOne possibility would be to add two other stacks to the runtime: one for each of the parallel tails. Enforcing the first property is then relatively easy: a call fom one of the parallel tails is not allowed to pick as an argument a SUT from the stack of SUTs on the other parallel tail. Enforcing the second property would in contrast necessitate a bit more work. Indeed, we want to be able to pick SUTs from the stack attached to the parallel tail **and** from the one attached to the sequential prefix. This means replacing the current mechanism that just takes the arguments at the top of the stack by one that randomly chooses arguments from the two stacks (the sequential one and the correct parallel one).\n\nThe main concern here is not really the technical challenge (though, a more complex system means a greater possibility of bugs and we don't want bugs in our test frameworks). The main concern is that this implementation would reduce the probability that one SUT appears as argument of two parallel calls.\n\nThe solution we've chosen is to simply not push on the stack SUTs created in the parallel tails. This enforces the two properties above: SUTs from a parallel call are never taken as arguments of any call and every SUT argument is a shared SUT.\n\nIn order to differentiate between the different contexts at runtime, we simply add a flag to the generated commands to indicate whether they are meant to be run in a sequential context or in a parallel one. Then, the function that handles the stack of SUTs and the one that handles the stack of states look at this flag to decide whether to push the newly created SUT and corresponding state to the relevant stacks.\n\nThis way, SUT-returning functions are still fully tested thanks to the sequential prefix, and how the parallel tails are handled is not made more complex than necessary. In particular, no modification of the runtime was needed (which made reasoning about the modifications a lot easier).\n\n## The Bug Report Feature\n\nSince version 0.2.0, tests generated by Ortac/QCheck-STM generate a bug report in case of test failure. This is a very nice feature that provides the user with:\n\n1. The piece(s) of Gopsel specification that has been violated\n2. The expected returned value (to be compared with the actual returned value) if it is computable from the Gospel specifications\n3. A reproduction case in the form of a runnable OCaml program\n\nThese pieces of information need to be collected while checking the equivalence between the observed behaviour and the behaviour of the model.\n\nIn the original QCheck-STM test framework, a program is generated, then it runs and the observable behaviour is stored (for example the returned value of a `length` function). Finally, the observed behaviour is compared to the behaviour of running the equivalent program on a model, checking user-defined postconditions.\n\nThis comparison is done in `STM.Internal.Make.check_disagree` for the sequential run and in `STM.Internal.Make.check_obs` for the parallel one. Both are parameterised by the `postcond` predicate. In hand-written QCheck-STM tests, this `postcond` predicate is obviously hand-writeen and in Ortac-generated QCheck-STM tests, it is generated based on Gospel postcondition clauses and invariants.\n\nNow, in order to build the bug report in case of test failure, we need the `postcond` function to not be a simple predicate anymore. We need it to return an optional report with the Gospel terms that were violated, the string representation of the call and, if possible, the expected result of the call.\n\nThe consequence of this change is that we have to reimplement the `check_disagree` and the `check_obs` functions. The former was reimplemented as part of the 0.2.0 release, the latter in the present one. But, as these are the pieces of code that actually do the testing, one has to be extra-careful when modifying them. We've adopted a step-by-step approach to make the preservation of the semantics scrutinasable with testing and reviewing.\n\nThe `postcond` function that the Ortac/QCheck-STM-generated code uses returns an `option` type rather than a boolean. The `None` case corresponds to `true` and the `Some report` one to `false`. The idea is to return an explanation in case of test failure.\n\nThe first step is to adapt the original function to deal with this `postcond` functional argument. On a technical level it is trivial, the main benefit is that the `check_obs` function is now in the `ortac` code base.\n\nThis function now looks like this:\n\n```ocaml\nlet check_obs postcond =\n (* ignore the report for now *)\n let postcond c s r = Option.is_none @@ postcond c s r in\n let rec aux pref cs1 cs2 s =\n match pref with\n | (c, res) :: pref' ->\n let b = postcond c s res in\n b && aux pref' cs1 cs2 (Spec.next_state c s)\n | [] -> (\n match (cs1, cs2) with\n | [], [] -> true\n | [], (c2, res2) :: cs2' ->\n let b = postcond c2 s res2 in\n b && aux pref cs1 cs2' (Spec.next_state c2 s)\n | (c1, res1) :: cs1', [] ->\n let b = postcond c1 s res1 in\n b && aux pref cs1' cs2 (Spec.next_state c1 s)\n | (c1, res1) :: cs1', (c2, res2) :: cs2' ->\n (let b1 = postcond c1 s res1 in\n b1 && aux pref cs1' cs2 (Spec.next_state c1 s))\n ||\n let b2 = postcond c2 s res2 in\n b2 && aux pref cs1 cs2' (Spec.next_state c2 s))\n in\n aux\n```\n\nThe general idea behind this `check_obs` function is to find a sequential explanation for the behaviour observed in the run involving parallelism. The sequential prefix is first checked against the `state` and using the `postcond` function provided as argument. Then, we explore all the possible sequential interleavings of the two parallel tails, using boolean operators short-circuits to stop when we found one interleaving that expains the observed behaviour.\n\nThe next step is to actually deal with the optional report `postcond` is returning. This means modifying the body of `check_obs` to make it return the report.\n\nMoving from boolean to option type implies adding a lot of `match`es that could render the code harder to read. Adding to that, the translation is somewhat counter-intuitive: `None` is actually the max and `Some` the min of the boolean algebra. This makes the translation error-prone.\n\nThe path we've chosen to gain trust in our modifications, is to try to make it as clear as possible on the syntactic level that the semantics are preserved.\n\nWe've done that by defining an infix operator corresponding to the equivalent of the conjunction and to the equivalent of the disjunction, using the `lazy` type to translate the boolean short-circuits.\n\nBy using these new infix operators in place of the boolean ones, we can clearly see in the diff between the two implementations that the semantic is preserved:\n\n```diff\n+ let ( &&& ) o1 o2 = match o1 with None -> Lazy.force o2 | _ -> o1\n+ let ( ||| ) o1 o2 = match o1 with None -> None | Some _ -> Lazy.force o2\n+\n let check_obs postcond =\n- (* ignore the report for now *)\n- let postcond c s r = Option.is_none @@ postcond c s r in\n let rec aux pref cs1 cs2 s =\n match pref with\n | (c, res) :: pref' ->\n- let b = postcond c s res in\n- b && aux pref' cs1 cs2 (Spec.next_state c s)\n+ postcond c s res &&& lazy (aux pref' cs1 cs2 (Spec.next_state c s))\n | [] -> (\n match (cs1, cs2) with\n- | [], [] -> true\n+ | [], [] -> None\n | [], (c2, res2) :: cs2' ->\n- let b = postcond c2 s res2 in\n- b && aux pref cs1 cs2' (Spec.next_state c2 s)\n+ postcond c2 s res2\n+ &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))\n | (c1, res1) :: cs1', [] ->\n- let b = postcond c1 s res1 in\n- b && aux pref cs1' cs2 (Spec.next_state c1 s)\n+ postcond c1 s res1\n+ &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))\n | (c1, res1) :: cs1', (c2, res2) :: cs2' ->\n- (let b1 = postcond c1 s res1 in\n- b1 && aux pref cs1' cs2 (Spec.next_state c1 s))\n- ||\n- let b2 = postcond c2 s res2 in\n- b2 && aux pref cs1 cs2' (Spec.next_state c2 s))\n+ postcond c1 s res1\n+ &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))\n+ ||| lazy\n+ (postcond c2 s res2\n+ &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))))\n in\n aux\n```\n\nObviously, this commit needs special attention in the review process, but it is made quite easy to review. In order to be able to display a runnable program leading to the reported postcondition violation, we need to collect the traces of calls. Adding this collection on top of the previous modifications doesn't change the structure and the logic of the function.\n\nIn conclusion, in order to get a bug report for Ortac/QCheck-STM+Domains, we had to reimplement the heart of the test framework, the `check_obs` function. As it should be, we heavily rely on code review to make sure we implement the expected logic, and we tried to make the code review as easy as possible.\n\n## Funding\nThis work is partly funded by the research grant [ANR-22-CE48-0013](https://anr.fr/Projet-ANR-22-CE48-0013).\n\n## Until Next Time\nYou can connect with us on [Bluesky](https://bsky.app/profile/tarides.com),\n[Mastodon](https://mastodon.social/@tarides),\n[Threads](https://www.threads.net/@taridesltd), and\n[LinkedIn](https://www.linkedin.com/company/tarides) or sign up for our mailing\nlist to stay updated on our latest projects. We look forward to hearing from\nyou!\n")
6.610 Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
6.610 Called from Dune__exe__Blog.decode in file "src/gen/blog.ml", line 286, characters 19-58
6.610 Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
6.610 Called from Dune__exe__Utils.map_files in file "src/gen/utils.ml", line 56, characters 23-59
6.610 Called from Dune__exe__Blog.all in file "src/gen/blog.ml", line 302, characters 2-51
6.610 Called from Dune__exe__Blog.template in file "src/gen/blog.ml", line 308, characters 4-12
6.610 Called from Dune__exe__Main.cmds.(fun) in file "src/gen/main.ml", line 19, characters 48-61
6.610 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 22, characters 19-24
6.610 Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 41, characters 7-16
------
Dockerfile:48
--------------------
46 | RUN ./generate-images.sh
47 | COPY --link . .
48 | >>> RUN dune build && dune build --profile=release
49 |
50 | FROM alpine:3.22 AS run
--------------------
ERROR: failed to solve: process "/bin/sh -c dune build && dune build --profile=release" did not complete successfully: exit code: 1
2026-06-30 18:13.10: Job failed: Docker build exited with status 1