Build:
- 0
2026-06-30 10:49.52: New job: docker build {
"commit": "a6e47a712f7aeb588640f1056e69c62dcaab6491",
"dockerfile": {
"file": "Dockerfile"
},
"docker_context": null,
"squash": false,
"buildx": true,
"build_args": [],
"path": null
}
2026-06-30 10:49.52: Checking out commit a6e47a71. 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 a6e47a71
2026-06-30 10:49.52: Exec: "cp" "-a" "--" "/var/lib/ocurrent/var/git/tarides.com.git-c625fb5f52c964610b54f32d27d46965b6bf2fad211456d66e1ff8a0f4c02fec/.git"
"/tmp/git-checkout3106b3de"
2026-06-30 10:49.54: Exec: "git" "-C" "/tmp/git-checkout3106b3de" "submodule"
"deinit" "--force" "--all"
2026-06-30 10:49.54: Exec: "git" "-C" "/tmp/git-checkout3106b3de" "reset"
"--hard" "-q" "a6e47a712f7aeb588640f1056e69c62dcaab6491"
2026-06-30 10:49.56: Exec: "git" "-c" "protocol.file.allow=always" "-C"
"/tmp/git-checkout3106b3de" "submodule" "update"
"--recursive" "--init" "--no-fetch"
2026-06-30 10:49.56: Exec: "docker" "buildx" "build" "--pull" "-f" "/tmp/git-checkout3106b3de/Dockerfile"
"--iidfile" "/tmp/git-checkout3106b3de/docker-iid"
"--" "/tmp/git-checkout3106b3de"
#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 1.0s
#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 resolve docker.io/library/alpine:3.22@sha256:14358309a308569c32bdc37e2e0e9694be33a9d99e68afb0f5ff33cc1f695dce 0.0s done
#4 sha256:7c8cb692ae09657cbc4a3f3cbd0e8d5a2690ba38386aaaf252dbb060bf5eb2e6 1.02kB / 1.02kB done
#4 sha256:b66e0ce64844f5c6435b0c4bfd965558199ab0f53270846861c979cb1ac29365 611B / 611B done
#4 sha256:14358309a308569c32bdc37e2e0e9694be33a9d99e68afb0f5ff33cc1f695dce 9.22kB / 9.22kB done
#4 DONE 0.1s
#5 [internal] load build context
#5 transferring context: 601.15MB 2.6s done
#5 DONE 2.7s
#6 [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
#6 0.324 fetch https://dl-cdn.alpinelinux.org/alpine/v3.22/main/x86_64/APKINDEX.tar.gz
#6 0.425 fetch https://dl-cdn.alpinelinux.org/alpine/v3.22/community/x86_64/APKINDEX.tar.gz
#6 0.932 OK: 7 MiB in 16 packages
#6 1.583 (1/17) Installing brotli-libs (1.1.0-r2)
#6 1.898 (2/17) Installing c-ares (1.34.6-r0)
#6 1.908 (3/17) Installing libunistring (1.3-r0)
#6 1.927 (4/17) Installing libidn2 (2.3.7-r0)
#6 1.933 (5/17) Installing nghttp2-libs (1.69.0-r0)
#6 1.943 (6/17) Installing libpsl (0.21.5-r3)
#6 1.948 (7/17) Installing zstd-libs (1.5.7-r0)
#6 1.959 (8/17) Installing libcurl (8.14.1-r2)
#6 1.968 (9/17) Installing libexpat (2.8.2-r0)
#6 1.973 (10/17) Installing pcre2 (10.46-r0)
#6 1.984 (11/17) Installing git (2.49.1-r0)
#6 2.413 (12/17) Installing git-init-template (2.49.1-r0)
#6 2.421 (13/17) Installing gmp (6.3.0-r3)
#6 2.436 (14/17) Installing libev (4.33-r1)
#6 2.436 (15/17) Installing oniguruma (6.9.10-r0)
#6 2.446 (16/17) Installing pkgconf (2.4.3-r0)
#6 2.452 (17/17) Installing oniguruma-dev (6.9.10-r0)
#6 2.463 Executing busybox-1.37.0-r20.trigger
#6 2.477 OK: 21 MiB in 33 packages
#6 DONE 3.4s
#7 [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
#7 3.623 fetch https://dl-cdn.alpinelinux.org/alpine/v3.22/main/x86_64/APKINDEX.tar.gz
#7 ...
#8 [run 3/11] RUN chmod -R 755 /var
#8 DONE 0.4s
#7 [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
#7 3.702 fetch https://dl-cdn.alpinelinux.org/alpine/v3.22/community/x86_64/APKINDEX.tar.gz
#7 4.031 OK: 7 MiB in 16 packages
#7 4.398 (1/82) Installing m4 (1.4.19-r4)
#7 4.434 (2/82) Installing libbz2 (1.0.8-r6)
#7 4.439 (3/82) Installing perl (5.40.4-r0)
#7 4.777 (4/82) Installing autoconf (2.72-r1)
#7 4.796 (5/82) Installing ncurses-terminfo-base (6.5_p20250503-r0)
#7 4.802 (6/82) Installing libncursesw (6.5_p20250503-r0)
#7 4.808 (7/82) Installing readline (8.2.13-r1)
#7 4.812 (8/82) Installing bash (5.2.37-r0)
#7 4.841 Executing bash-5.2.37-r0.post-install
#7 4.847 (9/82) Installing brotli-libs (1.1.0-r2)
#7 4.853 (10/82) Installing c-ares (1.34.6-r0)
#7 4.855 (11/82) Installing libunistring (1.3-r0)
#7 4.864 (12/82) Installing libidn2 (2.3.7-r0)
#7 4.866 (13/82) Installing nghttp2-libs (1.69.0-r0)
#7 4.867 (14/82) Installing libpsl (0.21.5-r3)
#7 4.868 (15/82) Installing zstd-libs (1.5.7-r0)
#7 4.873 (16/82) Installing libcurl (8.14.1-r2)
#7 4.878 (17/82) Installing curl (8.14.1-r2)
#7 4.884 (18/82) Installing brotli (1.1.0-r2)
#7 4.887 (19/82) Installing pkgconf (2.4.3-r0)
#7 4.888 (20/82) Installing brotli-dev (1.1.0-r2)
#7 4.893 (21/82) Installing c-ares-dev (1.34.6-r0)
#7 4.909 (22/82) Installing libidn2-dev (2.3.7-r0)
#7 4.912 (23/82) Installing libpsl-utils (0.21.5-r3)
#7 4.916 (24/82) Installing libpsl-dev (0.21.5-r3)
#7 4.920 (25/82) Installing nghttp2-dev (1.69.0-r0)
#7 4.924 (26/82) Installing openssl-dev (3.5.7-r0)
#7 4.949 (27/82) Installing zlib-dev (1.3.2-r0)
#7 4.956 (28/82) Installing libgcc (14.2.0-r6)
#7 4.960 (29/82) Installing libstdc++ (14.2.0-r6)
#7 4.980 (30/82) Installing zstd (1.5.7-r0)
#7 4.986 (31/82) Installing zstd-dev (1.5.7-r0)
#7 4.991 (32/82) Installing curl-dev (8.14.1-r2)
#7 4.997 (33/82) Installing jansson (2.14.1-r0)
#7 5.001 (34/82) Installing binutils (2.44-r3)
#7 5.074 (35/82) Installing libgomp (14.2.0-r6)
#7 5.079 (36/82) Installing libatomic (14.2.0-r6)
#7 5.083 (37/82) Installing gmp (6.3.0-r3)
#7 5.086 (38/82) Installing isl26 (0.26-r1)
#7 5.101 (39/82) Installing mpfr4 (4.2.1_p1-r0)
#7 5.109 (40/82) Installing mpc1 (1.3.1-r1)
#7 5.113 (41/82) Installing gcc (14.2.0-r6)
#7 5.968 (42/82) Installing libexpat (2.8.2-r0)
#7 5.969 (43/82) Installing pcre2 (10.46-r0)
#7 5.974 (44/82) Installing git (2.49.1-r0)
#7 6.030 (45/82) Installing git-init-template (2.49.1-r0)
#7 6.032 (46/82) Installing perl-error (0.17030-r0)
#7 6.036 (47/82) Installing perl-git (2.49.1-r0)
#7 6.041 (48/82) Installing git-perl (2.49.1-r0)
#7 6.045 (49/82) Installing libgmpxx (6.3.0-r3)
#7 6.048 (50/82) Installing gmp-dev (6.3.0-r3)
#7 6.053 (51/82) Installing libxau (1.0.12-r0)
#7 6.056 (52/82) Installing libmd (1.1.0-r0)
#7 6.060 (53/82) Installing libbsd (0.12.2-r0)
#7 6.064 (54/82) Installing libxdmcp (1.1.5-r1)
#7 6.068 (55/82) Installing libxcb (1.17.0-r0)
#7 6.080 (56/82) Installing libx11 (1.8.11-r0)
#7 6.115 (57/82) Installing libxext (1.3.6-r2)
#7 6.118 (58/82) Installing fftw-double-libs (3.3.10-r6)
#7 6.135 (59/82) Installing libpng (1.6.57-r0)
#7 6.147 (60/82) Installing freetype (2.13.3-r0)
#7 6.155 (61/82) Installing fontconfig (2.15.0-r3)
#7 6.180 (62/82) Installing lcms2 (2.19-r0)
#7 6.185 (63/82) Installing libltdl (2.5.4-r1)
#7 6.189 (64/82) Installing xz-libs (5.8.3-r0)
#7 6.193 (65/82) Installing libxml2 (2.13.9-r1)
#7 6.203 (66/82) Installing imagemagick-libs (7.1.2.15-r0)
#7 6.232 (67/82) Installing imagemagick (7.1.2.15-r0)
#7 6.281 (68/82) Installing libjpeg-turbo (3.1.0-r0)
#7 6.288 (69/82) Installing imagemagick-jpeg (7.1.2.15-r0)
#7 6.293 (70/82) Installing libsharpyuv (1.5.0-r0)
#7 6.296 (71/82) Installing libwebp (1.5.0-r0)
#7 6.303 (72/82) Installing libwebpdemux (1.5.0-r0)
#7 6.306 (73/82) Installing libwebpmux (1.5.0-r0)
#7 6.310 (74/82) Installing imagemagick-webp (7.1.2.15-r0)
#7 6.313 (75/82) Installing inotify-tools-libs (4.23.9.0-r0)
#7 6.317 (76/82) Installing inotify-tools (4.23.9.0-r0)
#7 6.323 (77/82) Installing libev (4.33-r1)
#7 6.323 (78/82) Installing libev-dev (4.33-r1)
#7 6.328 (79/82) Installing make (4.4.1-r3)
#7 6.333 (80/82) Installing musl-dev (1.2.5-r12)
#7 6.400 (81/82) Installing oniguruma (6.9.10-r0)
#7 6.404 (82/82) Installing oniguruma-dev (6.9.10-r0)
#7 6.412 Executing busybox-1.37.0-r20.trigger
#7 6.420 OK: 249 MiB in 98 packages
#7 DONE 6.9s
#9 [build 3/13] WORKDIR /root
#9 DONE 0.1s
#10 [build 4/13] RUN curl -fsSL https://get.dune.build/install | sh
#10 0.513
#=#=#
# 2.2%
######## 11.8%
################# 23.8%
############################ 39.4%
####################################### 54.8%
###################################################### 75.9%
#################################################################### 94.6%
######################################################################## 100.0%
#10 1.473 dune x86_64-unknown-linux-musl was installed successfully to ~/.local/bin/dune
#10 1.474
#10 1.712
#=#=#
0.0%
##### 7.1%
########## 14.1%
############### 21.2%
#################### 28.2%
######################### 35.3%
############################## 42.4%
################################### 49.4%
######################################## 56.5%
############################################# 63.5%
################################################## 70.6%
####################################################### 77.6%
############################################################ 84.7%
################################################################## 91.7%
####################################################################### 98.8%
######################################################################## 100.0%
#10 4.577 Revision cache was populated successfully
#10 4.579 To use dune you will need to source the file "$HOME/.local/share/dune/env/env.bash" (or similar as appropriate for your shell)
#10 4.579 export PATH="/root/.local/bin:$PATH"
#10 4.579
#10 4.579 To get started, run:
#10 4.579 dune --help
#10 DONE 4.9s
#11 [build 5/13] COPY --link tarides-com.opam .
#11 DONE 0.1s
#12 [build 6/13] COPY --link dune-project .
#12 DONE 0.1s
#13 [build 7/13] RUN dune --version && dune pkg lock && dune build @pkg-install
#13 0.216 "Nightly build 2026-06-30T05:00:33Z, git revision 5900d9b19612b684a3dcaca0beac5b24fdfd35d9"
#13 36.04 Solution for dune.lock
#13 36.04
#13 36.04 Dependencies common to all supported platforms:
#13 36.04 - alcotest.1.9.1
#13 36.04 - angstrom.0.16.1
#13 36.04 - asn1-combinators.0.3.2
#13 36.04 - astring.0.8.5
#13 36.04 - base-bytes.base
#13 36.04 - base-threads.base
#13 36.04 - base-unix.base
#13 36.04 - base64.3.5.2
#13 36.04 - bigarray-compat.1.1.0
#13 36.04 - bigstringaf.0.10.0
#13 36.04 - bos.0.3.0
#13 36.04 - brr.0.0.8
#13 36.04 - bstr.0.0.4
#13 36.04 - camlp-streams.5.0.1
#13 36.04 - caqti.2.3.2
#13 36.04 - caqti-lwt.2.3.2
#13 36.04 - checkseum.0.5.3
#13 36.04 - cmarkit.dev
#13 36.04 - cmdliner.2.1.1
#13 36.04 - conf-gmp.5
#13 36.04 - conf-gmp-powm-sec.4
#13 36.04 - conf-libev.4-13
#13 36.04 - conf-libssl.4
#13 36.04 - conf-oniguruma.1
#13 36.04 - conf-pkg-config.5
#13 36.04 - cppo.1.8.0
#13 36.04 - csexp.1.5.2
#13 36.04 - cstruct.6.2.0
#13 36.04 - ctypes.0.24.0
#13 36.04 - decompress.1.5.3
#13 36.04 - digestif.1.3.0
#13 36.04 - domain-name.0.5.0
#13 36.04 - dream.1.0.0~alpha8
#13 36.04 - dream-accept.0.1.0
#13 36.04 - dream-encoding.dev
#13 36.04 - dream-html.3.11.2
#13 36.04 - dream-httpaf.1.0.0~alpha4
#13 36.04 - dream-pure.1.0.0~alpha2
#13 36.04 - dune-configurator.3.23.1
#13 36.04 - dune-private-libs.3.23.1
#13 36.04 - dune-site.3.23.1
#13 36.04 - duration.0.3.1
#13 36.04 - dyn.3.23.1
#13 36.04 - eqaf.0.10
#13 36.04 - faraday.0.8.2
#13 36.04 - faraday-lwt.0.8.2
#13 36.04 - faraday-lwt-unix.0.8.2
#13 36.04 - fmt.0.11.0
#13 36.04 - fpath.0.7.3
#13 36.04 - fs-io.3.23.1
#13 36.04 - gen.1.1
#13 36.04 - gluten.0.5.2
#13 36.04 - gluten-lwt.0.5.2
#13 36.04 - gluten-lwt-unix.0.5.2
#13 36.04 - gmap.0.3.0
#13 36.04 - graphql.0.14.0
#13 36.04 - graphql-lwt.0.14.0
#13 36.04 - graphql_parser.0.14.0
#13 36.04 - h2.0.12.0
#13 36.04 - h2-lwt.0.12.0
#13 36.04 - h2-lwt-unix.0.12.0
#13 36.04 - hilite.dev
#13 36.04 - hmap.0.8.1
#13 36.04 - hpack.0.12.0
#13 36.04 - httpun.0.1.0
#13 36.04 - httpun-lwt.0.1.0
#13 36.04 - httpun-lwt-unix.0.1.0
#13 36.04 - httpun-types.0.1.0
#13 36.04 - httpun-ws.0.2.0
#13 36.04 - integers.0.8.0
#13 36.04 - ipaddr.5.6.2
#13 36.04 - js_of_ocaml.6.4.0
#13 36.04 - js_of_ocaml-compiler.6.4.0
#13 36.04 - js_of_ocaml-toplevel.6.4.0
#13 36.04 - kdf.1.0.0
#13 36.04 - ke.0.6
#13 36.04 - lambdasoup.1.1.1
#13 36.04 - logs.0.10.0
#13 36.04 - lru.0.3.1
#13 36.04 - lwt.6.1.2
#13 36.04 - lwt-dllist.1.1.0
#13 36.04 - lwt_ppx.6.1.0
#13 36.04 - lwt_ssl.1.2.0
#13 36.04 - macaddr.5.6.2
#13 36.04 - magic-mime.1.3.1
#13 36.04 - markup.1.0.3
#13 36.04 - menhir.20260209
#13 36.04 - menhirCST.20260209
#13 36.04 - menhirGLR.20260209
#13 36.04 - menhirLib.20260209
#13 36.04 - menhirSdk.20260209
#13 36.04 - mirage-clock.4.2.0
#13 36.04 - mirage-crypto.1.2.0
#13 36.04 - mirage-crypto-ec.1.2.0
#13 36.04 - mirage-crypto-pk.1.2.0
#13 36.04 - mirage-crypto-rng.1.2.0
#13 36.04 - mirage-crypto-rng-lwt.1.2.0
#13 36.04 - mirage-kv.6.1.1
#13 36.04 - mirage-kv-unix.3.0.1
#13 36.04 - mtime.2.1.0
#13 36.04 - multipart_form.0.8.0
#13 36.04 - multipart_form-lwt.0.8.0
#13 36.04 - ocaml.5.2.1
#13 36.04 - ocaml-base-compiler.5.2.1
#13 36.04 - ocaml-compiler-libs.v0.17.0
#13 36.04 - ocaml-syntax-shims.1.0.0
#13 36.04 - ocamlbuild.0.16.1+dune
#13 36.04 - ocamlfind.1.9.8+dune
#13 36.04 - ocplib-endian.1.2
#13 36.04 - ohex.0.2.0
#13 36.04 - oniguruma.0.2.0
#13 36.04 - optint.0.3.0
#13 36.04 - ordering.3.23.1
#13 36.04 - pecu.0.7
#13 36.04 - pp.2.0.0
#13 36.04 - ppx_derivers.1.2.1
#13 36.04 - ppx_deriving.6.1.1
#13 36.04 - ppx_deriving_yaml.0.4.1
#13 36.04 - ppx_import.1.12.0
#13 36.04 - ppxlib.0.38.0
#13 36.04 - prettym.0.0.5
#13 36.04 - psq.0.2.1
#13 36.04 - ptime.1.2.0
#13 36.04 - pure-html.3.11.2
#13 36.04 - re.1.14.0
#13 36.04 - rresult.0.7.0
#13 36.04 - sedlex.3.7
#13 36.04 - seq.base
#13 36.04 - sexplib0.v0.17.0
#13 36.04 - ssl.0.7.0
#13 36.04 - stdlib-shims.0.3.0
#13 36.04 - stdune.3.23.1
#13 36.04 - stringext.1.6.0
#13 36.04 - tailwindcss.dev
#13 36.04 - textmate-language.0.6.0
#13 36.04 - top-closure.3.23.1
#13 36.04 - topkg.1.1.1
#13 36.04 - uchar.0.0.2
#13 36.04 - unstrctrd.0.4
#13 36.04 - uri.4.4.0
#13 36.04 - uucp.17.0.0
#13 36.04 - uunf.17.0.0
#13 36.04 - uutf.1.0.4
#13 36.04 - x509.1.1.1
#13 36.04 - yaml.3.2.0
#13 36.04 - yojson.3.0.0
#13 36.04 - zarith.1.14
#13 DONE 435.8s
#14 [build 8/13] COPY --link ./generate-images.sh .
#14 DONE 0.1s
#15 [build 9/13] COPY --link data/ data/
#15 DONE 1.4s
#16 [build 10/13] COPY --link src/gen src/gen
#16 DONE 0.2s
#17 [build 11/13] RUN ./generate-images.sh
#17 0.211 + dune exec -- src/gen/main.exe file.dune
#17 4.914 + dune build @convert
#17 DONE 382.2s
#18 [build 12/13] COPY --link . .
#18 DONE 1.5s
#19 [build 13/13] RUN dune build && dune build --profile=release
#19 4.961 File "src/data/dune", lines 6-16, characters 0-222:
#19 4.961 6 | (rule
#19 4.961 7 | (target blog_gen.ml)
#19 4.961 8 | (deps
#19 4.961 9 | (source_tree %{workspace_root}/data/blog/)
#19 4.961 10 | (:gen %{workspace_root}/src/gen/main.exe))
#19 4.961 11 | (action
#19 4.961 12 | (chdir
#19 4.961 13 | %{workspace_root}
#19 4.961 14 | (with-stdout-to
#19 4.961 15 | %{target}
#19 4.961 16 | (run %{gen} blog)))))
#19 4.961 gen: internal error, uncaught exception:
#19 4.961 Invalid_argument("expected metadata at the top of the file blog/content/XXXX-XX-XX.ortac-0.8.0.md. Got --- \nauthor: Nicolas Osborne \ntitle: \"Release of Ortac 0.8.0 and Testing with Domains\" \nimage: todo \nimage-alt: todo \ndate: XXXX-XX-XX \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 modes. 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\nThis new release focuses 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 comes for free once we've written the OCaml specification of a library. It is just a matter of instanciating the `STM_domain.Make` functor rather than the `STM_sequential.Make` one. So, why do 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 for that:\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\n functions since version 0.4.0\n\nWe'll start with how we've dealt with the coverage of SUT-returning function 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\nindeed 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\nsame program on the model. You can read more about this [here](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 argument and SUT-returning functions. These functions are not easily tested when we write QCheck-STM tests by hand.\n\nOne example of function with multiple SUTs as 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 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\nAdding support for testing with Domains, we have to be careful about parallel access to the arguments and decide what to do with the 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 about parallel access to the individual SUTs, but we don't want to catch bugs caused by a 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, a stack not being 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 not to add one more layer of\nprobability. Then, once the same SUT has been selected by both domains, it will be pushed back twice.\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\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<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\nNow, regarding the newly created SUTs, do we want to push them on the stack or not?\n\nIn sequential testing, they are indeed pushed on the stack. This it what allows to test them: if a newly created SUT is 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 to put the SUT in a random state and two parallel tails that allows 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 on 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 on how we handle SUTs in the runtime:\n\n1. a call from one of the parallel tails should never pick as argument a SUT\n created in the other parallel tail\n2. a call from one of the parallel tails should be able to pick as argument a\n 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 tail is not allowed to pick as argument a SUT from the stack of SUTs from 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, more complex system means more 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 argument 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 handle the one of states look at this flag to decide whether to push the newly created SUT and corresponding state in 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)\n if it is computable from the Gospel specifications\n3. a reproduction case in the form of a runnable OCaml program\n\nThose 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 run 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. Those are parameterized 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 postconditions 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 does 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 semantic scrutinazable with testing and reviewing.\n\nThe `postcond` function the Ortac/QCheck-STM-generated code uses returns an `option` type rather than a boolean. The `None` case correspond 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 is it 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 of 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, it to try to make it the most clear possible on the syntactic level that the semantic is preserved.\n\nWe've done that by defining 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 modification 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 the easiest possible.\n\n## Funding\nThis work is partly funded by the research grant\n[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 4.961 Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
#19 4.961 Called from Dune__exe__Blog.decode in file "src/gen/blog.ml", line 286, characters 19-58
#19 4.961 Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
#19 4.961 Called from Dune__exe__Utils.map_files in file "src/gen/utils.ml", line 56, characters 23-59
#19 4.961 Called from Dune__exe__Blog.all in file "src/gen/blog.ml", line 302, characters 2-51
#19 4.961 Called from Dune__exe__Blog.template in file "src/gen/blog.ml", line 308, characters 4-12
#19 4.961 Called from Dune__exe__Main.cmds.(fun) in file "src/gen/main.ml", line 19, characters 48-61
#19 4.961 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 22, characters 19-24
#19 4.961 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:
4.961 Invalid_argument("expected metadata at the top of the file blog/content/XXXX-XX-XX.ortac-0.8.0.md. Got --- \nauthor: Nicolas Osborne \ntitle: \"Release of Ortac 0.8.0 and Testing with Domains\" \nimage: todo \nimage-alt: todo \ndate: XXXX-XX-XX \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 modes. 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\nThis new release focuses 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 comes for free once we've written the OCaml specification of a library. It is just a matter of instanciating the `STM_domain.Make` functor rather than the `STM_sequential.Make` one. So, why do 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 for that:\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\n functions since version 0.4.0\n\nWe'll start with how we've dealt with the coverage of SUT-returning function 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\nindeed 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\nsame program on the model. You can read more about this [here](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 argument and SUT-returning functions. These functions are not easily tested when we write QCheck-STM tests by hand.\n\nOne example of function with multiple SUTs as 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 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\nAdding support for testing with Domains, we have to be careful about parallel access to the arguments and decide what to do with the 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 about parallel access to the individual SUTs, but we don't want to catch bugs caused by a 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, a stack not being 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 not to add one more layer of\nprobability. Then, once the same SUT has been selected by both domains, it will be pushed back twice.\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\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<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\nNow, regarding the newly created SUTs, do we want to push them on the stack or not?\n\nIn sequential testing, they are indeed pushed on the stack. This it what allows to test them: if a newly created SUT is 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 to put the SUT in a random state and two parallel tails that allows 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 on 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 on how we handle SUTs in the runtime:\n\n1. a call from one of the parallel tails should never pick as argument a SUT\n created in the other parallel tail\n2. a call from one of the parallel tails should be able to pick as argument a\n 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 tail is not allowed to pick as argument a SUT from the stack of SUTs from 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, more complex system means more 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 argument 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 handle the one of states look at this flag to decide whether to push the newly created SUT and corresponding state in 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)\n if it is computable from the Gospel specifications\n3. a reproduction case in the form of a runnable OCaml program\n\nThose 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 run 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. Those are parameterized 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 postconditions 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 does 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 semantic scrutinazable with testing and reviewing.\n\nThe `postcond` function the Ortac/QCheck-STM-generated code uses returns an `option` type rather than a boolean. The `None` case correspond 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 is it 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 of 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, it to try to make it the most clear possible on the syntactic level that the semantic is preserved.\n\nWe've done that by defining 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 modification 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 the easiest possible.\n\n## Funding\nThis work is partly funded by the research grant\n[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")
4.961 Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
4.961 Called from Dune__exe__Blog.decode in file "src/gen/blog.ml", line 286, characters 19-58
4.961 Called from Stdlib__List.rev_map.rmap_f in file "list.ml", line 105, characters 22-25
4.961 Called from Dune__exe__Utils.map_files in file "src/gen/utils.ml", line 56, characters 23-59
4.961 Called from Dune__exe__Blog.all in file "src/gen/blog.ml", line 302, characters 2-51
4.961 Called from Dune__exe__Blog.template in file "src/gen/blog.ml", line 308, characters 4-12
4.961 Called from Dune__exe__Main.cmds.(fun) in file "src/gen/main.ml", line 19, characters 48-61
4.961 Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 22, characters 19-24
4.961 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 11:03.59: Job failed: Docker build exited with status 1