Repository navigation
Conversation
Vendor menhir sources into a dune workspace as an alternative to the opam-based macrobenchmark build. Avoids opam solver overhead, satellite switch creation, and OxCaml ecosystem incompatibilities.
Switch from manual vendor scripts to opam-monorepo for dependency management. All transitive deps are locked in macro-benches.opam.locked (31 packages) and pulled into duniverse/ at build time. Working tools: - menhir 20250912 (all 3 runtimes: 5.4.1, trunk, OxCaml) - cpdf 2.8.1 (5.4.1 + trunk; OxCaml has locality type errors) - alt-ergo 2.6.2 (5.4.1; trunk/OxCaml need dep compat fixes) - coqc/Rocq 9.2 (needs build isolation fix for multi-runtime) Key additions: - dune-project with opam-monorepo package declarations - .opam.template files with x-opam-monorepo-opam-repositories pointing at dune-universe overlays for non-dune packages - dune-overlays/ for camlpdf, cpdf-source, zarith (hand-written dune files for upstream packages that use Makefile/configure) - benchmarks/ with build scripts and input files for running-ng - Lock file (macro-benches.opam.locked) for reproducible builds
Clear OPAM_SWITCH_PREFIX, OCAMLTOP_INCLUDE_PATH, CAML_LD_LIBRARY_PATH, and OCAMLPATH in all build scripts before calling dune build. Without this, findlib resolves library paths from the user's active opam switch, causing "not a compiled interface for this version" errors when building with a different runtime. Also pre-generate rocq config fallback files (coq_config.ml etc.) so rocq's configure step doesn't need ocamlfind+zarith in each runtime. The dunestrap files are also pre-generated and reused across runtimes. Fixes coq builds for 5.4.1 and trunk (OxCaml still fails due to source-level incompatibilities like Gc.ramp_up).
ppxlib from opam-monorepo lock (0.38.0) doesn't support OCaml 5.6. Document the post-pull patch: replace duniverse/ppxlib/ with the main branch which adds Ast_506. Fixes alt-ergo on trunk.
Vendor devkit and its deps via opam-monorepo (50 packages total). C-binding deps (libevent, ocurl) are manually vendored with dune overlays since they use Makefile/autoconf upstream. Patches applied to vendored sources: - libevent: add ~persist and ~signal labels to match .mli (OCaml 5.x) - devkit/lwt_engines.ml: add engine_id type extension for lwt 6.x System deps: libevent-dev, libcurl4-openssl-dev
lwt 6.1.0 (from opam-monorepo lock) has C stubs incompatible with OCaml 5.6's renamed socketaddr.h macros. Replace with lwt 6.1.1 from git which fixes this. Fixes devkit benchmarks on OCaml trunk (5.6.0). All 30 stock OCaml benchmarks now pass (15 on 5.4.1 + 15 on trunk).
Add an idempotent setup script that handles the full monorepo setup: opam-monorepo pull, vendoring (cpdf, zarith, devkit deps), all 7 source patches, rocq config/dunestrap generation, and a test build. Update README to reflect the setup-script-first workflow and document all system deps including libpcre3-dev for devkit. Keep duniverse/ and vendor/ gitignored to avoid bloating the repo.
- Skip vendor scripts entirely when target dirs already exist (avoids re-downloading rocq and ocurl just to delete them) - Fix ppxlib check path: astlib/ast_506.ml not ast/versions/ast_506.ml - Fix lwt check: use opam version string instead of missing header path
- Fix sed regex for devkit lwt_engines.ml patch (escape issue) - Replace fragile sed for alt-ergo dune with full file rewrite - Add Makefile with clean/clean-all/setup targets
js_of_ocaml 6.2.0 added to opam-monorepo lock (53 packages total). Binary builds on OCaml 5.4.1 but NOT on trunk (5.6) — jsoo requires ocaml < 5.5. Runtime execution also needs findlib to locate stdlib (not yet wired up in build script). Setup script fixes: - Skip manual zarith vendor when dune-universe provides it in duniverse - Drop ppxlib/lwt git replacements (breaks extunix and other packages) - Trunk (5.6) support deferred until ppxlib releases official 5.6 support - Add jsoo public_name removal patch (step 8) Current trunk status: only menhir, cpdf, coq work on trunk (they don't use ppxlib). All other benchmarks (alt-ergo, devkit, jsoo) work on 5.4.1.
irmin_mem_rw: in-memory key-value store read/write benchmark using Irmin.mem. Adapted from sandmark for irmin 3.x API. Exercises GC via Lwt + persistent data structure allocation. ocamlformat: format a 3322-line OCaml file (Rocq tactics.ml). Exercises parsing, AST manipulation, and pretty-printing. Also: - Lock file updated to 79 packages (irmin + ocamlformat + deps) - Setup script: skip zarith vendor when duniverse has it; add ocamlformat public_name patch (step 9)
decompress: zlib compress/decompress benchmark from sandmark, adapted for decompress 1.x API (Lz77.make_window, positional i/o args). Exercises buffer allocation and GC via repeated compress+decompress. Also fixes: - ocamlformat setup patch: targeted sed to avoid breaking install stanza - Lock file: 81 packages total
eio_fiber_stream: 4 producers × 4 consumers passing 20M items through an Eio.Stream. Exercises OCaml 5 effect-based scheduler, fiber switching, and GC pressure from concurrent allocation. Requires OCaml >= 5.2 (uses effects). ~2s runtime on 5.4.1. Lock file: 88 packages total.
sedlex_tokenize: Unicode-aware lexer processing 12MB of generated pseudo-code. Exercises lexer table lookup, string allocation, and GC pressure. ~1.5s for 200k lines. Dream dropped: alpha releases have broken opam dependency chains (dream-pure/dream-httpaf version conflicts). Can revisit when dream reaches stable release. Lock file: 88 packages total.
yojson ydump: JSON parse + compact serialize (~0.6s) zarith_pi: compute 10000 digits of pi with GMP bignum (~3s) owl_gc: matrix/graph computation with OpenBLAS (~2.5s) Lock file: 92 packages total. System dep: libopenblas-dev (for owl).
DaCapo targets 10-60s per benchmark. Several of ours were under 2s, too noisy for regression detection. Updated: - irmin: 3k keys / 20k ops (was 10k/100k) → 12s - sedlex: 700k lines (was 200k) → 5.5s - eio: 15M items (was 5M) → 5.8s - zarith: 15000 digits (was 10000) → 7s - yojson: new ydump_repeat binary, 1000 parse+serialize iterations → 5.5s - ocamlformat: 5x larger workload file (16k lines) → 5.3s Still fast (need bigger inputs, deferred): - alt-ergo: 0.02s (tiny .why files) - coqc: 0.002s (tiny .v files — no real proof computation) - menhir_ocamly: 0.4s (but menhir_sysver is already 20s)
ppxlib main branch now works with all vendored packages including extunix (the pexp_function API issue was fixed upstream). This means ALL ppxlib-dependent benchmarks now build on both 5.4.1 AND trunk. Re-enabled in setup-monorepo.sh: - Patch 4: replace ppxlib with git main (has Ast_506) - Patch 5: replace lwt with git main (socketaddr.h fix for 5.6) - Patch 6: devkit lwt_engines.ml (engine_id for lwt 6.1.1+) Expected result: all benchmarks work on 5.4.1 and trunk. Only jsoo (< 5.5 constraint) and OxCaml (source compat) remain blocked.
unsat.smt2 is a 54KB SMT-LIB 2 file from alt-ergo's own test suite that exercises the solver for ~8s with --timelimit 15. This replaces the tiny fill.why/yyll.why inputs (0.02s) as the main alt-ergo macro benchmark. The old fill.why and yyll.why are kept as quick smoke tests. Note: coqc benchmarks remain instant (0.002s) because coqc needs the compiled Rocq stdlib (.vo files) to do any real work. Building the stdlib is itself a major task — deferred.
owl_stats_dist_exponpow.c calls std_gaussian_rvs(a/sqrt(2.0)) and std_gaussian_rvs(B), but the function takes no arguments. This works on some compilers (K&R empty parens = unspecified args) but fails on stricter ones (C23, -Werror=incompatible-function-pointer-types). Fix: replace with gaussian_rvs(0, scale) which correctly passes the scale factor as the sigma parameter. Added as patch 10 in setup-monorepo.sh.
…ies) Comprehensive rewrite reflecting: - All 14 benchmark tools with timings and categories - Runtime compatibility table (5.4.1, trunk, OxCaml) - Complete patch table (10 patches) - Known limitations (coqc, jsoo, OxCaml) - Updated directory layout - Adding a new benchmark workflow
coqc can now type-check .v files by installing rocq-runtime + rocq-core into a local _rocq_prefix/ during setup. The benchmark exercises: - fib 25 (exponential kernel reduction) - sum_to 2000 (linear recursion, large nat) - ack 3 10 (Ackermann, super-exponential GC stress) - tree_size(make_tree 15) (65535-node tree construction) Setup changes: - setup-monorepo.sh now builds and installs rocq-runtime + rocq-core into _rocq_prefix/ (requires a symlink at ~/install/default/lib/ for dune's .vo compilation deps) - coq.build.sh creates a wrapper script that sets OCAMLPATH and -coqlib for the local install - _rocq_prefix/ added to .gitignore Replaces the old BasicSyntax.v/AbstractInterpretation.v benchmarks (which were instant because they needed external Frap library).
- setup-monorepo.sh: compute symlink path dynamically from monorepo location (works regardless of where the repo is cloned) - Makefile: clean-all removes _rocq_prefix/ and the install symlink - .gitignore: add _rocq_prefix/ - README: update coqc entry (44s stress test), add rocq symlink to known limitations, update directory layout and how-it-works steps
Vendor pplacer + mcl (Markov Cluster Algorithm) manually since pplacer is not in opam. The benchmark runs pplacer's 224-test suite which exercises likelihood calculations, tree operations, and phylogenetic placement algorithms (~10s at 8 iterations). New files: - scripts/vendor-pplacer.sh: clones pplacer+mcl, builds mcl C libraries - benchmarks/pplacer/pplacer.build.sh: builds test suite, creates wrapper - macro-bench-pplacer.opam.template: declares OCaml deps (batteries, gsl, sqlite3, camlzip, csv, xmlm, ounit2) New patches in setup-monorepo.sh: - [11] batteries batGc.mli: add live_stacks_words for OCaml 5.6 trunk - [12] mcl caml_mcl.c: add #include <stdint.h> for trunk headers System deps: libgsl-dev, libsqlite3-dev (in addition to existing)
Benchmarks building dune itself from source via `ocaml boot/bootstrap.ml`. This exercises the OCaml compiler on ~100K LOC of real-world code (~8s). Works on all 3 runtimes (5.4.1, trunk, OxCaml) since the bootstrap only uses the OCaml compiler directly (no external OCaml libraries).
Benchmarks the liquidsoap language compiler: repeatedly parses and typechecks a liquidsoap script exercising functions, pattern matching, lists, closures, and recursive definitions (50000 iterations, ~9s). liquidsoap-lang is pure OCaml with no C deps. Its deps (ppx_hash, ppx_string from Jane Street v0.17) require OCaml >= 5.3.0. Also adds liq_bench.exe to the setup-monorepo.sh test build list.
Add pplacer, dune-bootstrap, liquidsoap-lang to the benchmark table. Update package counts (110 vendored), patch list (12 patches), system deps (libgsl-dev, libsqlite3-dev), runtime compatibility table, directory layout, and known limitations (parked: melange, Frama-C).
devkit_stre, devkit_gzip, devkit_network, and owl_gc run too fast (<1s) to produce meaningful GC stress signal. Wrap the build output with a shell loop that accepts an iteration count as argv[1]. The running-ng config passes iteration counts via args to bring runtimes into the 5-20s DaCapo sweet spot: - devkit_stre: 80 iterations - devkit_gzip: 15 iterations - devkit_network: 10 iterations - owl_gc: 7 iterations
coqc produces .vo / .vos / .vok / .glob / .<name>.aux files next to the .v sources when it compiles them. These are regenerated every time the coq benchmarks run, so they should not be tracked.
- Fix program counts (16 active tools, 26 programs, 14 categories) - Add fp_flambda_macrobenchmarks.yml to the Run benchmarks section (FP × flambda 2×2 sweep, 3 invocations) - Update runtime compatibility table with OxCaml-working benchmarks (menhir, dune-bootstrap, test_decompress, zarith_pi) and the new FP/flambda runtime variants
Upstream batteries gates the live_stacks_words field on ##V>=5.6##, but the field landed in OCaml 5.5 (5.5.0-beta1 == ocaml/ocaml d8bb46c3). With the 5.6 gate, batteries compiles against 5.4 (field absent on both sides) and trunk 5.6 (field present on both sides), but fails against 5.5 where the compiler has the field and batteries doesn't. Patch 11 now handles both "upstream gated at 5.6" and "field entirely missing", producing ##V>=5.5## in either case. Idempotent. Unblocks pplacer builds against 5.5.x runtimes.
…hes (#28) * scripts: make the monorepo setup portable to BSD userland `make setup` cannot run on FreeBSD or macOS: the vendoring and patching scripts use GNU coreutils and GNU sed throughout, and the failures range from silent to fatal. 22 sed -i BSD sed REQUIRES an argument to -i, GNU forbids one 7 of those GNU-only constructs that fail even with that fixed: four `0,/re/{...}` line-0 ranges (meaning "first match only"), two `/re/a text` one-line appends, and one `{N;N;N; a text}` block 6 md5sum BSD has md5, with different output; these verify downloads 1 nproc BSD has sysctl hw.ncpu Adds scripts/lib-portable.sh, sourced from lib-sources.sh so every vendor script and setup-monorepo.sh get it through the one line they already share. Portable, not FreeBSD-specific, and Linux behaviour must not change. `sed_i` avoids -i altogether rather than branching on platform, so there is one code path; it writes through a temp file and copies back, preserving the file's mode, and leaves the file untouched if sed fails. `insert_after`, `insert_after_offset`, `insert_at_line` and `delete_first_match` replace the GNU-only sed constructs with awk, taking inserted text as arguments so leading whitespace and backslashes need no escaping, which is what made the sed spellings fragile. This also covers macOS, whose sed and md5 are the BSD ones. vendor-apron.sh already had a hand-rolled nproc/sysctl fallback; it now calls ncpu, so there is one place to fix if a platform needs a third. One dialect trap: awk understands only EREs, so a literal parenthesis is `[(]`, not `\(`. The sed spelling reaches awk as a capture group, which matches the same text in some cases and silently not in others. The four affected call sites use bracket form and the module header says why. Verified three ways. scripts/tests/test-lib-portable.sh runs each helper against the GNU command it replaces and requires byte-identical output: 13 checks, passing on Linux, with the GNU comparisons skipped on a BSD host. Every rewritten regex matches the real vendored files exactly as the old one did. And for the two patches not yet applied to this tree, old and new were run on the real files: the jsoo dune goes 55 lines to 53 under both, leaving the same second occurrence, byte-identical, and the batteries N;N;N patch likewise on a reverted copy. What this does NOT prove: that a cold `make setup` applies all 40 patches correctly end to end. This tree is already vendored and the patches are guarded, and setup also rebuilds vendor/rocq. A clean run is the remaining check, which FreeBSD will exercise anyway. * scripts: two GNU-only constructs the portability pass missed Both found by running `make setup` cold on FreeBSD. vendor-pplacer.sh passed `make --quiet`, which bmake rejects outright ("usage: make [-BeikNnqrSstWwX] ..."), aborting the mcl build. GNU vs BSD *make* is a class that was not on the list alongside sed -i / md5sum / nproc, and the line already used the ncpu helper, so the portability pass touched it and left the GNU flag behind. `-s` is the POSIX spelling and means the same thing to both (GNU treats it as --silent); verified identical on GNU Make 4.4.1, so Linux behaviour does not change. setup-monorepo.sh's patch 12 called sed_i with a GNU-only script BODY: `1a text` is GNU one-line append syntax, and BSD sed wants `1a\` plus a newline. sed_i fixes `-i` portability but passes the script through verbatim, so it could not help here. insert_at_line exists for exactly this and its own docstring says so; the call site simply was not converted. Verified the replacement is byte-identical to `sed -i '1a text'` on the real caml_mcl.c shape, and that the grep -q idempotence guard still skips a second run. All 19 sed_i / sed -i call sites were checked for GNU-only bodies and this was the only one. A grep for GNU-only long options across every script found no other hit: the tar --strip-components uses are fine, bsdtar supports them. * tests: assert the insert helpers on BSD, not only against GNU sed insert_at_line and insert_after_offset were exercised only inside `if gnu`, so on a BSD host they ran and nothing checked their output: the suite reported "8 passed" with two of six helpers functionally unverified on the very platform they exist for. That is the blind spot patch 12 fell into, where the helper was fine and the call site was not. Both now carry unconditional assertions against expected files, as the insert_after and delete_first_match tests already did: insert_at_line at line 1 (the patch 12 call site exactly), multi-line, mid-file, and past the end of file; insert_after_offset at offset N, at offset 0, and across two matches. On a simulated BSD host the suite goes from 8 to 14 assertions, 6 of them covering these two helpers where there were none. The multi-match case is worth stating: insert_after_offset fires on EVERY match, like GNU `a` does. Its `!target` guard only stops a second match from moving a target that is still pending. delete_first_match is the deliberately first-only one; the two do not agree and a comment now says so. Also corrects the usage line from `sh` to `bash`: lib-portable.sh uses bash arrays and so does every script that sources it, so `sh` never worked. * README: FreeBSD prerequisites Mapped from the existing apt list, which the README already calls the one CI actually exercises, plus the goblint/pplacer autotools. The FreeBSD list is deliberately SHORTER than the apt one, and the section says why rather than just listing packages: - zlib and the C toolchain are in the FreeBSD base system, so there is nothing to install for either. - libcurl, libev, libevent and pcre/pcre2 are all devkit's, and devkit cannot build on FreeBSD at all, so on FreeBSD they buy nothing. Checked against the conf-* depexts across the vendored tree rather than assumed: conf-libevent and conf-libpcre2-8 are named only by macro-bench-devkit; conf-libpcre and conf-libcurl add only pcre-ocaml and ocurl, which nothing but duniverse/devkit depends on; and conf-libev is a DEPOPT of lwt, whose discover step passes --use-libev %{conf-libev:installed}%, so lwt builds without it. - perl5 and the autotools are goblint's apron build (setup patch 15 needs aclocal/autoreconf), pplacer's mcl build, and cpu's conf-autoconf. Also records that devkit is not a dependency problem at all. It calls U.gettid, which is Linux-only with no FreeBSD equivalent, so duniverse/devkit fails to compile whatever is installed. Worth saying in the prerequisites section so nobody goes looking for a package that would fix it. The apt list is untouched: devkit does build on Linux, so its five entries stay there. Package NAMES are mapped from the Debian ones and still need confirming against `pkg search` on a FreeBSD host before anyone runs the command as root. * setup: patch extunix so devkit builds on FreeBSD, and drop the unused PCRE2 dep Two findings that turned out to be related, both reached by asking why the devkit benchmark needs both pcre and pcre2. extunix (patch 25). devkit's log.ml and files.ml call `U.gettid ()`, where prelude.ml has `module U = ExtUnix.Specific`, and ExtUnix.Specific exposes only what the platform actually has. On FreeBSD that binding is absent, so duniverse/devkit fails to COMPILE with "Unbound value U.gettid", taking benchmarks/ahrefs-devkit with it. This is neither a missing system library nor a devkit bug. extunix already implements gettid four ways in src/unistd.c: Win32 GetCurrentThreadId, macOS pthread_threadid_np, older macOS SYS_thread_selfid, and Linux SYS_gettid. Its discover.ml probes them as an ordered ANY[...], and FreeBSD matches none of them purely on spelling: FreeBSD calls it pthread_getthreadid_np(), declared in <pthread_np.h>, where macOS calls it pthread_threadid_np(). So the patch adds a fifth alternative shaped exactly like the macOS one, plus the matching #elif branch. `I` and `DEFINE` are both documented in discover.ml as "promoted to config", so the include and the define land in the generated config.h that unistd.c already includes. Linux is unaffected, and checked rather than assumed: pthread_np.h does not exist there, so the new alternative fails and the probe still falls through to SYS_gettid, which still compiles. The patch verifies both files are in the expected shape before touching them, and is idempotent. PCRE2. conf-libpcre2-8 sat in macro-bench-devkit.opam.template, but nothing in the tree has ever used PCRE2: devkit depends on the `pcre` OCaml library, which is PCRE 1 via conf-libpcre; there is no `Pcre2.` anywhere under duniverse/; and it is not a dependency of any package in the solution, only an entry in the hand-maintained x-opam-monorepo-opam-provided list. It is a latent Linux bug too, not just FreeBSD noise. The README's apt list installs libpcre3-dev and has never installed libpcre2-dev, so the requirement was satisfied only because libgio-2.0-dev and libselinux1-dev happen to drag libpcre2-dev in. Dropped from the template, the generated opam file and the lock's opam-provided list, which is the union of the templates'. README updated for both. The earlier claim there, that devkit could not be enabled by installing packages, was right that it is not a dependency problem and wrong that the suite is unreachable: with patch 25 it is a source patch setup applies, so devkit's own deps (curl, libev, libevent, pcre) belong on the FreeBSD list after all. Neither half is verified on FreeBSD hardware yet. * setup: put LOCALBASE on the C toolchain's search path on FreeBSD A cold FreeBSD `make setup` failed at [9/9] with fatal error: 'gsl/gsl_vector.h' file not found even with gsl and libevent installed, because pkg puts headers in /usr/local/include and libraries in /usr/local/lib, and FreeBSD's base clang searches NEITHER: its default list is /usr/lib/clang/<v>/include and /usr/include, nothing else. On Linux every -dev package lands in /usr/include, so this cannot appear there, which is why it took a cold run on the platform to surface. It is a CLASS, not two libraries: any vendored C stub including a pkg-installed header hits it. gsl and libevent are just the two that happened to be reached first. Exported from lib-portable.sh rather than setup-monorepo.sh so a vendor-*.sh script run directly gets it too; they all source that file. Three properties, each with a test: - appended, not prepended, so a caller who set these deliberately keeps priority over us; - idempotent, because setup exports them and then every vendor script is a subprocess that inherits them AND re-sources this file, which would otherwise add a duplicate entry per nesting level; - inert anywhere that is not FreeBSD. The tests drive it through a fake `uname`/`sysctl` on PATH, so the FreeBSD branch is exercised on Linux rather than only on the platform it exists for. That is exactly the blind spot that let a GNU-only sed body survive in patch 12: a helper whose only coverage is on the platform where it does nothing. LOCALBASE is honoured, falling back to `sysctl -n user.localbase` and then to /usr/local, so a non-default prefix works. FreeBSD only: NetBSD and OpenBSD use different prefixes and neither has been tested. README documents the automatic behaviour and the manual export for building a benchmark by hand outside make setup. * setup: fix the four suites that still fail to build on FreeBSD A cold FreeBSD run with the system libraries installed got 67 of 95 programs running. Of the six suites that did not build, one (frama-c) already builds and one (devkit) already builds and runs; these are the remaining four, each a different cause. goblint: apron's chain builds camlidl with make, and camlidl's Makefile uses GNU conditionals that bmake rejects outright ("Invalid line \"ifneq ...\""). Unlike the mcl `--quiet` case this is SYNTAX, so no flag helps; it needs GNU make, which FreeBSD ships as gmake. New `gnu_make` helper in lib-portable.sh picks gmake when present and plain make otherwise, so Linux is unchanged. mlgmpidl's and apron's Makefiles are GNU-flavoured too, so all four stages use it. And vendor-apron.sh no longer hides why. Every make in it went to /dev/null 2>&1, so the camlidl failure produced a nine-line log ending at "[2/4] camlidl" with no error at all, and goblint's absence surfaced much later as something unrelated. That is the third instance of the pattern the patch 15 comment already warns about (after patch 15 itself and the [2/9] duniverse guard). Output is now captured rather than discarded: silent on success, and on failure the stage name plus the last 25 lines, then exit 1. owl (patch 26): stubs compile, link fails with undefined __kmpc_fork_call. Those symbols come from -fopenmp, so something adds it at compile time while nothing adds the runtime at link time. Two holes closed: get_openmp_config falls through to `_ -> [], []` on FreeBSD, where clang wants -fopenmp/-lomp (the macOS pair without -Xpreprocessor); and, since that arm only fires when OWL_ENABLE_OPENMP=1 which is not the default, -lomp is also added whenever the assembled cflags ask for OpenMP and the libs carry no runtime. The second is the one that most likely bit, because openblas_conf comes from pkg-config and FreeBSD's openblas is built with OpenMP. INFERRED from the link error and the flag assembly, not observed: if owl still fails, dump the assembled flags rather than guessing again. pplacer (patch 27): gsl-ocaml's discover hardcodes `let default_gsl_include = [ "/usr/include" ]`, and on FreeBSD gsl is under LOCALBASE. The default is reached even though pkg-config is installed and gsl.pc exists, because discover only uses pkg-config's answer if it can find a -I in --cflags, and pkgconf STRIPS -I/usr/local/include as a system include path. This is the one member of the /usr/local class a compiler search path cannot fix: the literal is read by OCaml and used to open a file, never passed to a compiler. Now probes candidates for gsl/gsl_cdf.h, with /usr/include still ahead of /usr/local/include so Linux resolves exactly as before, and LOCALBASE first when set. infer: needs `zip`, which was in NEITHER prerequisite list. Added to both, with a note that it is a plain command-line tool rather than a library, so a minimal Linux image can hit this too. Both new patches verified: they apply, are idempotent, refuse to touch a file that is not in the expected shape, and the OCaml they produce parses. The gsl candidate search was run both ways, picking /usr/include on this Linux box (identical to the hardcoded value) and a LOCALBASE prefix when gsl is there. Neither is verified on FreeBSD hardware. * Build scripts source lib-portable.sh; pin goblint's domainslib select Two blockers from the round 2 FreeBSD run, plus a correction. Build scripts (unblocks devkit, 7 programs). dc24520's commit message claimed the LOCALBASE exports reach "every entry point". That was wrong. It holds for the SETUP path, setup-monorepo.sh -> lib-sources.sh -> lib-portable.sh, which is why make setup completes. But running-ng invokes benchmarks/<suite>/<suite>.build.sh DIRECTLY at run time, in a fresh process that inherits none of it, and none of the 24 build scripts sourced the library. So devkit built during setup [9/9] and then failed when running-ng built it: event_stubs.c:13:10: fatal error: 'event.h' file not found with libevent installed, at /usr/local/include/event.h. devkit is the only casualty today because owl and pplacer each got a patch that solves their need internally, while devkit depends on the include path alone. Any future benchmark needing a pkg-installed header hits the same wall, so all 24 now source it rather than devkit getting a special case. The line makes the same ../.. assumption every one of them already makes for MONOREPO_DIR, and it goes after the script's OWN `set -euo pipefail`, never the one inside a heredoc that emits a wrapper (12 of the 24 have two; liq-video-frames and pplacer have three). scripts/tests/test-build-scripts-portable.sh enforces it, and verifies the relative path resolves and each script is still valid bash. Confirmed it fails when a script loses the line. The export is gated off on Linux, so a missing line is invisible here without the check. goblint (patch 28). domain-local-await is a HARD dep of goblint so opam-monorepo vendors it, while domainslib is a DEPOPT so it is not, and src/util/parallel/dune chooses an implementation with `(select gobMutex.ml from (domainslib -> ...) ( -> ...))`. Where the switch carries domainslib, that select resolves to the domainslib branch, which pulls the SWITCH's domain-local-await in beside the vendored one, and dune refuses. Whether the switch carries domainslib is not a property of this repo: running-ng's install_deps_*.sh install it for the MICRO suite's multicore benchmarks. Rosemary ran micro first, which is why it appeared there and not here. So this is a measurement bug, not only a build failure: goblint silently switches threadpool implementation depending on what else has been run on the box. Pinning the select to the no-domainslib branch makes it deterministic everywhere AND matches established behaviour, since no switch used for goblint numbers so far has carried domainslib. Reproduced on Linux before fixing, with a minimal dune project against a switch that does have domainslib: same "Conflict between the following libraries" error, same shape. After dropping the alternative, clean build, and the no-domainslib variant is the one selected. Correction. The reason recorded for patch 27, that pkgconf strips -I/usr/local/include as a system include path, is FALSE. Measured on FreeBSD, `pkg-config --cflags gsl` prints `-I/usr/local/include`. Why discover.ml falls through to its hardcoded default is therefore unknown; the comment now says so and lists the remaining candidates as guesses. The probe-based fix stands because it never consults pkg-config, but the reasoning under it is not a guide. Patch 26's reasoning, by contrast, is now confirmed rather than inferred: OWL_ENABLE_OPENMP is unset, and `pkg-config --cflags openblas` returns `-I/usr/local/include -fopenmp` while `--libs` returns no OpenMP runtime. The second hole was the one that bit, as suspected. * setup: patch 29 for CIL's gcc search, gmake for javalib/sawja, apron idempotence Three items from FreeBSD round 3. Patch 29, CIL's real-GCC search. goblint dies at configure time with Failure("couldn't find real gcc") because duniverse/cil/bin/realGccConfigure.ml tries only "gcc" and the hyphenated "gcc-7".."gcc-16". FreeBSD's pkg installs versioned GCC WITHOUT the hyphen (gcc14, not gcc-14), so every candidate misses on a machine that has a perfectly good compiler. It does have to be real GCC: CIL's own is_bad_gcc_version rejects clang, which is correct, and FreeBSD's cc IS clang. The unhyphenated names go after plain "gcc", so where that exists the chosen compiler does not change, and the extra candidates simply are not present on Linux. Verified on rosemary that this alone took goblint from 0/4 to 2/4. javalib/sawja. Same class as camlidl: camlzip's Makefile is GNU-flavoured and bmake cannot parse it ("Cannot open /Makefile.config"), while gmake builds it cleanly. One correction to the report this came from: vendor-javalib-sawja.sh DOES already reach lib-portable.sh, transitively through lib-sources.sh, so gnu_make was in scope; only the seven call sites needed changing. Resolves to plain make on Linux. Checked the rest of the tree for others in the same position: the only remaining bare `make` calls are two inside echo strings and mcl's, whose Makefile is portable and was verified building under bmake with -s in round 1. Apron chain idempotence. goblint.build.sh invokes vendor-apron.sh unconditionally and running-ng invokes goblint.build.sh once per BENCHMARK, so four goblint programs rebuilt mpfr, camlidl, mlgmpidl and apron four times over, git-cleaning the shared source trees on each pass. A stamp recording the compiler now short-circuits the whole script when the prefix is already built, written only AFTER the hermetic self-test has linked apron out of that prefix, so a half-built prefix can never be mistaken for a good one. Verified in four states: absent stamp, matching stamp, stamp from another compiler, and stamp with lib/apron missing. On the bigarray-compat failure that prompted that last change: it does NOT reproduce on Linux. Four sequential wipe-and-rebuild cycles of exactly the failing stage all succeeded, and running-ng builds sequentially (no thread or process pool), so the suggested concurrent-invocation race cannot be the mechanism either. The idempotence guard is committed because it is right on its own merits and because it stops any transient failure in the chain repeating once per remaining program, NOT because it is a proven fix. The underlying FreeBSD error is still unexplained. * Untrack menhir's generated parser; make the apron cache hit legible menhir. benchmarks/menhir/sysver.{ml,mli,automaton,conflicts} were tracked, but they are the benchmark's OUTPUT, not its input. menhir_sysver runs menhir -v --table benchmarks/menhir/sysver.mly and menhir writes the generated parser next to the grammar, with -v adding the automaton and conflicts reports, so every run rewrote all four and left the tree dirty. 113MB of them, sysver.ml alone at 57MB, which meant `git checkout --` before a pull became routine and a real local change could hide in the noise. Nothing reads them: outside results/, the only reference to `sysver` anywhere is the benchmark's own args, which pass the .mly. The grammar stays tracked; the four outputs are now gitignored, with the reason recorded there. apron stamp. The guard works, but its output did not say so. On a cache hit it printed "PREFIX READY", which is also how the BUILD path ends, so a skip read as a rebuild in the logs and the guard looked like it was only half firing. A hit now says "apron prefix: CACHED, no rebuild (stamp matches <version>)" and a real build says "apron prefix: BUILT from source", so the two cannot be confused. Nothing parses either string; both are for humans, which is exactly why the ambiguity mattered. To count real builds in a log, grep for "BUILT from source" or for the "[1/4] bigarray-compat" line, which only the build path emits. * ci: run the same build-and-run-once gate on FreeBSD, via Cirrus GitHub has no FreeBSD runners, and its only free route is a QEMU VM inside a Linux runner, several times slower than native. The Linux gate takes about 35 minutes, so emulated it would be flirting with the 6 hour job cap for no reason. Cirrus runs FreeBSD natively. Runs the whole suite rather than a portability smoke test, because the port turned up two distinct classes of breakage and only one is cheap to catch. GNU-only shell constructs (make --quiet, sed '1a text', /bin/true, build scripts not sourcing lib-portable.sh) are caught by the two test scripts in under a second. The other class only appears when something actually compiles: extunix's gettid probe, owl's OpenMP link flags, gsl-ocaml's hardcoded include path, goblint's domainslib select, CIL's real-GCC search. That was the larger half, and nothing short of a real build finds it. Kept step for step alongside .github/workflows/ci.yml so the two do not drift. Three differences, all forced by the platform: - pkg replaces apt, with the shorter FreeBSD list the README explains (zlib and the C toolchain are in the base system, nothing uses PCRE2). gmake is required, not optional: camlidl's and camlzip's Makefiles use GNU conditionals bmake rejects as syntax errors. - ocaml/setup-ocaml does not exist here, so the switch is created by hand, with --disable-sandboxing because opam's sandbox is bwrap-based. - Cirrus folder caches replace actions/cache, keyed the same way on the lock file, sources.yml and the scripts. Both legs, matching the Linux matrix. The trunk leg is allow_failures for the same reason its twin is continue-on-error: it tracks a moving compiler and pinned ppxlib git main. As of today trunk added a Pexp_hole constructor that the pinned ppxlib does not know, which fails 41 of 95 programs on Linux too. The portability tests run first, before anything is compiled, so a GNU-ism fails in seconds rather than deep into a build. They earn their place twice over: on Linux they exercise the FreeBSD paths through a fake uname and report 24 checks, here they run for real and report 14. Nothing else confirms the simulation is honest. Two things to confirm on the first run, both noted at the top of the file: Cirrus's current free-tier limits for public repositories, and the newest FreeBSD image family it publishes. The port was validated on 15.1 while this asks for 14.2. * Revert the Cirrus FreeBSD CI: the service is shut down Cirrus CI shut down on 2026-06-01. Adding a .cirrus.yml was a mistake on my part, made from stale knowledge of it being the standard FreeBSD OSS CI; it has been dead for three months and installing the app only redirects to a shutdown notice. The file could never have run, which is why the PR showed two Linux checks and nothing else. Removing it rather than leaving it dormant: a config for a service that does not exist is worse than no config at all, because it reads as coverage that is not there. The replacement is a GitHub Actions job driving a FreeBSD VM, which is what the projects migrating off Cirrus are using. vmactions/freebsd-vm publishes a FreeBSD 15.1 image, matching the host this port was validated on. It runs under nested virtualisation rather than natively, so whether the full build-and-run gate fits inside the 6 hour job cap is an empirical question: the Linux gate takes about 35 minutes, and the slowdown factor depends on whether the runner grants /dev/kvm, which is not documented either way. Worth measuring before committing a workflow that claims to be a gate, so it is left out of this PR rather than guessed at twice. ---------
…gate (#30) * ci: a FreeBSD build-and-run-once job, to measure whether it can be a gate The port was validated by hand (95/95 on FreeBSD 15.1) and nothing checks it since. This runs the same three phases as the Linux gate, in a FreeBSD VM on a Linux runner: setup-monorepo, ci-build-all, ci-run-all. A VM because there is no alternative. GitHub has no FreeBSD runners, and Cirrus CI, which had native ones, shut down on 2026-06-01. Nested virtualisation is what the projects migrating off Cirrus are using. vmactions/freebsd-vm publishes a 15.1 image, the exact release the port was validated on. IT IS A MEASUREMENT, NOT YET A GATE, and is continue-on-error with no cache. The question the design turns on is unanswered: the Linux gate takes ~35 minutes natively, and the slowdown here depends on whether the runner grants /dev/kvm, which neither GitHub nor the action documents. So the first step reports it, the run block timestamps every phase, and the timeout is 350 minutes, just under GitHub's 6 hour cap, so a merely slow job reports a duration instead of being killed with nothing to show. Then: near 35-60 min -> drop continue-on-error, add caching, make it a gate 1-4 hours -> keep it non-gating, or move it to the weekly cron hits the cap -> fall back to the portability suites alone, which still catch the GNU-ism class that was most of what broke No caching yet, on purpose. The VM is ephemeral and only the workspace is copied back, so a cache would require the opam root to live inside the workspace, which is gigabytes of churn on every run. Choosing that trade before knowing the job is viable would be guessing. For the same reason OPAMROOT is set to /opamroot, outside the workspace: the repo tree still comes back, which is what lets ci-logs/ upload as an artifact, but the from-source compiler does not. The two portability suites run first, before any compilation. They take under a second, so a GNU-only construct fails immediately rather than deep into a build, and they check something nothing else does: on Linux they drive the FreeBSD paths through a fake uname and report 24 checks, here they run for real and report 14. Both legs, matching the Linux matrix. They are separate matrix jobs, so each gets its own 6 hour budget rather than sharing one. Details forced by the platform: pkg replaces apt with the shorter list README explains (zlib and the toolchain are in the base system, nothing uses PCRE2), gmake is required because camlidl's and camlzip's Makefiles use GNU conditionals bmake rejects, ocaml/setup-ocaml does not run inside the VM so the switch is created by hand with --disable-sandboxing, and the action executes prepare/run under sh, so every script of ours is invoked through bash explicitly. Both blocks are POSIX-sh clean; the action is pinned to a commit. * ci: the FreeBSD opam package is called ocaml-opam The first run died in under four minutes with pkg: No packages available to install matching 'opam' have been found in the repositories FreeBSD ships opam as devel/ocaml-opam, so `pkg install opam` matches nothing. Everything else in the list resolved; pkg named only this one. Also dropped rsync, which the action installs into the VM itself. The run did answer the question this workflow was written to ask. /dev/kvm IS present on ubuntu-latest, and the action chmods it, so the guest is hardware-accelerated rather than software-emulated and should run near native speed. VM boot is about 3.5 minutes. That makes a full build-and-run plausible here, which was not a safe assumption beforehand. The comment block is updated to record that, and the reporting step is kept as a regression check rather than an open question: if GitHub ever stops granting /dev/kvm, the job should not silently become ten times slower with no explanation in the log. Still unmeasured, and still why this stays continue-on-error with no cache: how long the build itself takes. The per-phase timestamps are there to report it. * ci: run the portability suites on Linux too, and close the FreeBSD job's drift Two things, both found by comparing the two workflows side by side rather than reading either on its own. The portability suites ran nowhere on Linux. They were added with the FreeBSD port and wired only into the FreeBSD job, which is backwards: the GNU half of test-lib-portable.sh can ONLY run on GNU userland. Each helper is asserted to produce byte-identical output to the GNU command it replaces, and those comparisons are skipped on FreeBSD, where the suite reports 14 checks against 24 here. So the FreeBSD job cannot cover for this one, and until now nothing ran the comparisons at all. test-build-scripts-portable.sh is in the Linux job for the opposite reason. The LOCALBASE export it guards is gated off on Linux, so a build script that stops sourcing lib-portable.sh is invisible here at runtime and only breaks on FreeBSD. The check is static, so it catches it regardless of platform. Then the FreeBSD job had drift from ci.yml that was not deliberate: - cancel-in-progress was unconditional. ci.yml limits it to pull requests because cancelling a master run leaves that merge unverified. Harmless while there is no push trigger, wrong the moment one is added, so it is written conditionally now. - no compiler identity step. ci.yml resolves the trunk tip to fold it into cache keys AND to record what was tested. Only the second reason applies here, but for a moving compiler it is the one that matters: a trunk run that does not say which trunk is a result nobody can act on. - no disk usage report. Worth more here than on Linux, since the host carries a VM image on top of the vendored tree and running out of disk looks like an unrelated build failure. The remaining differences are deliberate and now say so in the file: no push-to-master trigger and no weekly cron, for as long as this is a non-gating measurement. The push trigger would burn a VM on every merge to tell nobody anything, and the cron exists on Linux to bypass the cache, whereas every run here is already cold because there is no cache. Both go in together with the change that makes this a gate. * ci: give the FreeBSD job the same shape as the Linux one It collapsed eight logical phases into a single opaque "FreeBSD build and run" step, so the two workflows could not be read side by side and any drift between them was invisible. The VM persists across steps, and the action documents a `shell: freebsd {0}` for running in it, so the phases can be separate named steps. They now mirror ci.yml name for name and in order: Install system dependencies / Set up the OCaml switch / Portability helpers and build-script wiring / Validate the manifest against the tree / Install dune / Set up the monorepo / Build every benchmark / Run every benchmark once / Disk and cache usage / Upload logs Everything that is the same now LOOKS the same, and what is left differing is only what the platform forces, each with a reason in place: - three extra steps at the front (report virtualisation support, free host disk, boot the VM), which have no Linux counterpart; - ocaml/setup-ocaml@v3 becomes "Set up the OCaml switch", because that action is a GitHub Action and does not run inside the VM; - "Cache vendored sources" is absent while this is a measurement. The job key is build-and-run in both, so the step lists line up directly. This also required switching sync from the default rsync to nfs. With rsync the action copies the whole workspace into the VM and back around EACH step, which for a tree carrying duniverse/, vendor/ and _build-ci/ would cost more than the build it is measuring. nfs makes it a live mount, so there is nothing to copy. Splitting the phases is what makes the measurement legible, too: GitHub reports a duration per step, so "where does the time go" is answered by the run page rather than by grepping timestamps out of one long log, which is what the hand-rolled phase() markers were doing. Disk and cache usage is continue-on-error because it runs under always() in the VM shell, which does not exist if the boot step failed; that is not a reason to add a second failure to a job that already has one. * CLAUDE.md: document the FreeBSD workflow and the portability step The repo's rule is that documentation stays consistent with every commit, and the CI section described only ci.yml. Adds the FreeBSD workflow to "Where things live" and a section under CI covering: why a VM (no FreeBSD runners, Cirrus shut down 2026-06-01), that /dev/kvm is present so the guest is accelerated, that the steps deliberately mirror ci.yml so drift is visible, the four platform-forced differences, and why it is a measurement rather than a gate for now. Also records the two portability suites now running on BOTH platforms, and the reason they cannot substitute for each other: the GNU comparisons in test-lib-portable.sh need GNU userland and are skipped on FreeBSD (14 checks there against 24 here), while test-build-scripts-portable.sh is static and catches a build script that stops sourcing lib-portable.sh, which is invisible on Linux at runtime because the export it carries is gated off here. * ci: install PyYAML explicitly, on both platforms The FreeBSD job got as far as the manifest check and died with error: PyYAML not found — install it with `python3 -m pip install pyyaml` `pkg install python3` is a bare interpreter; scripts/ci-manifest.py imports yaml. FreeBSD names Python packages pyXY-<name>, so the version is derived from the python3 that was just installed rather than hardcoded, and the import is verified in the same step: otherwise a missing module surfaces two steps later as something else. The same gap exists on Linux and was only hidden. The apt list carries libyaml-dev, which is the C library frama-c needs, NOT the Python module; the Linux job has been relying on ubuntu-latest happening to ship PyYAML preinstalled. That is the same accident as the missing `zip`: fine on a stock runner, broken on a minimal container. python3-yaml is now in the apt list and in README's prerequisites for both platforms, with a note that it is a different thing from libyaml-dev. Numbers from the run that failed, which is what this workflow exists to produce. VM boot 0.8-1.3 min, system dependencies 0.2-0.4 min, and the OCaml switch built FROM SOURCE in 2.7 minutes, trunk included. That is close to native and confirms /dev/kvm is doing real work, so the full build should land near the Linux 35 minutes rather than the multi-hour figure that would have made this unusable. The portability suites ran on real FreeBSD in CI for the first time and passed. * ci: PyYAML on FreeBSD is py3XX-pyyaml, and verify rather than assert py312-yaml does not exist. The version I derived was right; the base name was not. devel/py-yaml was renamed devel/py-pyyaml in 2024, so FreeBSD 15 ships py312-pyyaml. This is the second FreeBSD package name I have guessed wrong in this workflow (opam is ocaml-opam), so the fix is to stop asserting names and start verifying the thing that is actually needed. Both spellings are tried, neither is fatal on its own, and `python3 -c 'import yaml'` decides. If that fails the message says what is missing, what needs it, and where to check the current name, rather than leaving a pkg error that says nothing about the build. Two things make the name genuinely hard to state up front: FreeBSD builds Python packages only for the default Python, so the pyXY prefix has to come from the interpreter that was installed rather than being hardcoded, and the base name differs by release because of the rename. README says both, and points at the import as the check that matters. * ci: tell git the NFS-mounted workspace is safe to use The monorepo setup died two minutes into [2/9] with fatal: detected dubious ownership in repository at '/home/runner/work/macro-benches/macro-benches/duniverse/merlin' The workspace is NFS-mounted from the host, where it belongs to the `runner` user, while everything inside the VM runs as root. git refuses to operate on a repository owned by somebody else, so the first pinned clone the vendoring tries to inspect stops it dead. actions/checkout does exactly this on the host for the same reason; the VM is a second user of the same tree and needs it too. Worth being clear that this is NOT a portability problem. It is an artefact of running as a different uid across a mount, and would happen identically on Linux in a container with the workspace bind-mounted. Nothing about the FreeBSD build is implicated. Progress this run, with the per-step timings that are the point of the workflow: VM boot 0.9 min, system dependencies 0.3 min, OCaml switch from source 4.2-4.8 min, portability suites and manifest check instant, dune 0.9-1.1 min. Roughly eight minutes to a working toolchain before the vendoring starts. * scripts: do not restore archive ownership when extracting vendored sources The FreeBSD CI reached [2.3/9] and died in tar: test/example_cp.ml: Can't set user=0/group=0 ...: Operation not permitted tar: Error exit delayed from previous errors As root, both GNU tar and bsdtar try to restore the archive's uid/gid. The workspace there is an NFS export with root squashed, so the chown fails with EPERM and tar exits non-zero even though every file extracted fine. On the Linux runner the workspace is local disk, so it never showed up. Ownership of a vendored source tree is never wanted, and a non-root extraction already behaves this way, so --no-same-owner does not change the result: it only makes it independent of who runs the extraction. Applied to all eight extraction sites rather than the two that happen to land on the mount today, since any of them would fail the same way if a destination moved. Two things about the flag placement, both of which bit while writing this: - it cannot go before the no-dash bundle (`tar --no-same-owner xzf ...`), because GNU tar only accepts that bundle as the FIRST argument and otherwise reads it as a file operand; - it cannot go between `-xzf` and its argument, because `-f` takes the next argument as the archive name and would swallow the flag. So it is `tar --no-same-owner -xzf <archive>`, verified on GNU tar 1.35 to produce byte-identical output to the unflagged extraction, including with --strip-components. Long form deliberately: `-o` means different things to GNU tar and bsdtar. * ci: make opam download with curl, not FreeBSD's fetch The monorepo pull died fetching a vendored tarball: opam-monorepo: [ERROR] Failed to pull .../duniverse/camlzip: "/usr/bin/fetch -o ... --user-agent opam/2.3.0 -- <github release url>" exited with code 1 "fetch: ...: Authentication error" opam on FreeBSD defaults to the base system's fetch(1), which fails on the GitHub release URL. OPAMFETCH=curl switches it; opam understands "curl" as a value and supplies the invocation itself, so this is not a hand-rolled command that can drift from what opam expects. curl is already installed with the other dependencies, and setup-ocaml gives the Linux job the equivalent. What is NOT established is why fetch fails. The candidates are the redirect to the signed asset URL and rate limiting from GitHub Actions addresses, and the error text does not distinguish them. Worth saying plainly because rosemary runs the same setup with the same opam and gets through it, so this may be about where the request comes from rather than about FreeBSD. curl is the robust choice under either explanation, which is why it is worth doing without settling the question. Timings from this run: VM boot 0.9 min, dependencies 0.3 min, OCaml switch 3 min, dune 0.8 min. The monorepo step now gets 1.6 min in before failing, which is the pull doing real network work rather than stalling. * ci: build on VM-local disk, not on the mounted workspace Third mount artefact in a row: mv: chflags: .../vendor/camlpdf/pdfcodec.ml: Operation not supported FreeBSD's mv preserves BSD file flags when moving across filesystems and NFS does not support chflags, so the vendoring dies. Before it: tar could not restore ownership (EPERM under root squash), and before that git refused the tree entirely ("detected dubious ownership"). Each was fixed on its own and each time the next appeared one stage later. They are all the same thing: the workspace is an NFS export owned by the host's `runner` while the VM runs as root, so every operation that touches ownership or filesystem metadata fails. None of it is a portability bug, and Linux in a container with a bind-mounted workspace behaves identically. Patching the fourth symptom was not going to be the last one. So the tree is copied once to /work on the VM's local disk and everything builds there. That removes the class rather than the instance, and it keeps dune's build directory off NFS as well, where its locking and many-small-files behaviour would have been a risk of its own once the build actually started. The copy runs after the package install, because git comes from pkg and the step checks out what it copied. Only ci-logs/ needs to travel back, since the artifact upload runs on the host and can only see the workspace; that step is continue-on-error so a missing log directory does not add a second failure to a job that already has one. Also reverts the one real thing this was hiding: --no-same-owner on the tar extractions stays, because it is correct regardless of where the tree lives. * ci: check FreeBSD package names from Linux, before spending a FreeBSD run Two of the failed CI runs were a wrong package name, and each cost a full round trip to find: `opam` does not exist on FreeBSD (it is `ocaml-opam`), and `py312-yaml` does not either (the port was renamed devel/py-yaml -> devel/py-pyyaml in 2024, so it is `py312-pyyaml`). Neither is guessable from the Linux name, and both are discoverable only by running the FreeBSD job, one name per attempt. FreeBSD publishes its package index over HTTP, so this is checkable from anywhere. scripts/tests/check-freebsd-packages.py downloads the index for the ABI the workflow targets, extracts the names from the workflow itself rather than keeping a second list that would drift, and reports any that do not resolve. 38131 packages in FreeBSD:15:amd64 today; all 23 the workflow asks for are present. Verified it fails on `opam` and passes once corrected. It runs in the LINUX job, which is the point: the class of bug is FreeBSD-only but the check does not need FreeBSD, so it gates before a VM is ever booted. Scoped to the main multi-line `pkg install` list. The PyYAML step installs a dynamically-named package with a fallback, which is not checkable statically and does not need to be, since it verifies itself by importing the module. Scraping it would yield shell tokens rather than package names, which the first version of this did. Skips rather than fails when the index cannot be fetched: it is advisory about the network, not a reason to fail a build. * setup: patch 30, goblint's preprocessor search, and install a real GCC The FreeBSD CI built all 95 programs on both 5.5.0 and trunk and ran 19 of the 20 it runs. The one failure is goblint, at RUN time: Fatal error: exception Failure("No good preprocessor (cpp) found") This is the first genuine portability bug CI has found, as opposed to an artefact of the sandbox, and it is the twin of patch 29 one layer up. src/util/preprocessor.ml tries plain `cpp` and rejects it when its --version mentions clang/apple/darwin. On FreeBSD /usr/bin/cpp IS clang, so that rejection is correct: goblint wants gcc preprocessor semantics. It then falls back to `compgen -c cpp-`, which only matches HYPHENATED names such as Debian's cpp-14. FreeBSD installs cpp14, so the fallback finds nothing and the analysis aborts. Exactly the gcc-14 versus gcc14 spelling that patch 29 fixed for CIL's compiler search, in a second place nobody had reached yet because it only bites at run time. Patch 30 searches the unhyphenated prefix too. "cpp-" stays first, so Linux selects precisely what it selected before, and the unhyphenated list is only consulted when the hyphenated one yields nothing good. Every candidate still passes through the same is_good check, so a binary that merely starts with "cpp" cannot be chosen unless it really is a working non-clang preprocessor. The patch is necessary but not sufficient: the FreeBSD package list installed no compiler at all, while the Linux list gets one from build-essential. Base clang covers everything else, which is why it was not noticed, and goblint is the one consumer that specifically needs GCC. `gcc` is added to the workflow and to README's prerequisites, with the failure mode written down: it aborts at run time, long after everything has built cleanly, which is a confusing place to start looking. Verified: the patch applies, is idempotent, refuses a file that is not in the expected shape, and the OCaml it produces parses. The package name was checked against FreeBSD's index with scripts/tests/check-freebsd-packages.py rather than guessed. * ci: promote the FreeBSD job to a gate, and record why it has no cache The first green run: 26.9 min on stable, 31.2 on trunk, against ~35 for the Linux gate, with no cache. 95 of 95 programs build and 19 of the 20 CI runs pass, on both 5.5.0 and trunk. The one that did not was goblint, and it found a real portability bug (patch 30) rather than a problem with the job. So it gates, on the same terms as ci.yml: stable required, trunk continue-on-error because it tracks a moving compiler and pinned ppxlib git main. Triggers match too. The push run matters for the reason it does there, that required checks are not `strict`, so two PRs can each be green against an older master and break it together. The cron is staggered an hour after ci.yml's so the two are not fetching every pinned source at once; its purpose differs slightly, since every run here is already cold, so what it adds is a weekly check that the pins remain fetchable in a week with no pull requests. NO CACHE, and that is a decision, not unfinished work. The header carries the arithmetic: 4.5 min is cacheable, 17% of the job, and collecting it means moving ~2.7 GB across the NFS mount twice per run, because the build happens in the VM while actions/cache runs on the host. The checkout copy is far smaller and already costs 0.3-1.1 min across that mount. Paying that twice to save 4.5 minutes is at best a wash, and it adds a failure mode to a job that has had enough of them. The honest place to revisit is the build phase, which at 16.2 min is what actually dominates and is not cacheable in ci.yml either. Making the stable leg a REQUIRED check still needs branch protection; adding the leg here does not do it. * docs: move the FreeBSD forensics out of the README, and fill the patch table The README had accumulated the reasoning behind every FreeBSD finding: why base clang searches neither /usr/local path, the extunix gettid spelling story, the PCRE2 archaeology, why zip and PyYAML and lapacke are each on the list. That is the record of how we got here, and it belongs in CLAUDE.md. The README should say what to install and how to build and run, which it now does in 252 lines instead of 317. Corrections found while moving it: - it said the goblint FreeBSD fix was "patch 28". It is 29 and 30; 28 is the platform-independent domainslib `select` pin, which is a measurement bug rather than a FreeBSD one. - it claimed the apt line is "the same list CI installs". It is not: ci.yml omits zip, because a hosted runner ships it. The list is right and the claim was wrong, so the claim goes. - the pkg line was missing bash, git and python3. None are in the FreeBSD base system and all three are needed, so anyone following it on a clean host stopped at the first build script. - RUNNING_OCAML_SWITCH_PREFIX was in the contract table as though running-ng passes it. running-ng sets four variables; this one is honoured if an orchestrator sets it and otherwise derived. The patch table was missing eight rows: 21 and 22 (sedlex) and 25 through 30 (the FreeBSD five plus the domainslib pin), so a third of the patches setup-monorepo.sh applies were undocumented. Every row now carries what the symptom looks like, including that 27's root cause is NOT established and 26's second half is inferred rather than observed. No em dashes, per the docs convention. * setup: patch 31, zarith's version rule dies of SIGPIPE under pipefail The FreeBSD gate failed in the rocq bootstrap, step [8/9], with (cd _build/default/duniverse/Zarith && bash -e -u -o pipefail -c 'grep "version" META | head -1') > .../zarith_version.ml Command exited with code 141 141 is 128+13, SIGPIPE. dune runs every (bash ...) action with pipefail, and zarith's META has two lines matching "version": the package's own 1.14 and zarith_top's 1.13. `head -1` exits after the first, grep still has the second to write, grep dies of SIGPIPE, and pipefail promotes that 141 to the pipeline's status. The rule fails and takes the bootstrap with it. This is NOT a FreeBSD bug and not new. It is a buffering race that has been latent in the vendored source all along: GNU grep block-buffers when stdout is a pipe, so both lines usually land in a single write() that completes before head exits, and the race is quietly won. FreeBSD's grep is line-buffered, so the second write happens after head is gone and the race is lost far more often. That is also why it is intermittent there: the run an hour earlier, on the same sources, never built this rule at all. `grep -m1` stops at the first match, so there is no second write and no pipe to break. The output is byte-identical (the first matching line), `-m` is in both GNU and BSD grep, and Linux behaviour is unchanged. Verified by building duniverse/Zarith/zarith_version.ml before and after: both give let version = "1.14" The patch is idempotent like the others, checks the rule is in the shape it expects before touching it, and skips cleanly when Zarith is not vendored.
* Trimming comments in the source code * Refactoring and simplifying README
* docs(README): rewrite the RUNNING_TAG table from a fresh audit of the benchmarks The feature tags in running-ng's macro_base.yml were re-derived by reading every enabled benchmark again and checking each claim against a perf profile and an strace of the small rungs on 5.5.0. The table listed only the four ladder tags, so this adds the feature tags, and the ladder rows gain their program counts. What the audit changed, for the reader of this table: - ephemerons is no longer a coverage gap. Compute parses to CbvVm, so every coq rung runs the bytecode VM, which looks up each global through CEphemeron, an Ephemeron.K1 table with a data field. - weak_refs is not just alt-ergo: frama-c hash-conses EVA's state maps through Weak.Make. - domains is infer, not lavyek: infer analyze --multicore is the only multi-domain workload while lavyek is disabled, so also the only parallel GC coverage. - io_uring is a gap: eio does create a ring, but eio_conc_small issues two io_uring_enter calls for a whole run. - custom_blocks (was custom_block_finalisation) states that the finalize op is included, since for a Bigarray that is caml_ba_finalize, and ocaml#14571 showed the order it frees in is measurable on owl. Tags only earn a row if they name runtime code someone edits and select a set no other tag gives you, which is why there is no row for polymorphic atomics, mutexes, affinity, digests, lexer engines, signals, subprocess spawning or foreign threads. * docs(CLAUDE): re-audit the runtime-feature coverage matrix Checked every row against the benchmark it names, with a perf profile and an strace of each small rung on 5.5.0 behind the claims. Several rows were wrong, not just stale. Corrected: - goblint does not hash-cons through Weak.Make. It has no Weak.Make anywhere in analyzer/src, its GWeak is a lattice of its own, and vendored CIL contains no Weak at all. Removed from both the ephemeron-machinery and Weak.Make rows. - The ephemeron data-field gap is closed by coq. Compute parses to CbvVm, so every rung runs the bytecode VM, and vmsymtable looks up each global through CEphemeron, which is Ephemeron.K1.Make with a value attached. Partial: it runs at VM-compile time, not in the reduction loop. - pplacer never opens a SQLite database; libsqlite3 only loads. Its hot kernel is its own linear_c.c over Bigarrays (61.6% of cycles), not BLAS and not GSL BLAS. Removed sqlite3 from its rows, added infer, which does use it. - Gc.finalise is a near-gap, not pplacer coverage: only pplacer_testsuite registers any, through Gsl.Eigen.symmv, and the like_* ladder registers none. - Marshal is four shapes, not one: ocamlc writes, jsoo input_values whole bytecode sections, coqc does both for .vo, infer round-trips summaries with Closures through SQLite blobs. - io_uring is measured now: eio does create a ring, then issues two io_uring_enter for a whole run. - CPU pinning is no longer a gap (patched into infer's DomainPool), and infer's scheduler is source-audited: a hand-rolled pool, not Domainslib. - goblint's apron octagon domain fires only for the legacy goblint program; autotune does not enable it for the gen_* ladder. - Atomics have no measurable coverage: uncontended and inlined, no caml_atomic_* symbol in any profile. Recorded as a new gap, since the live runtime work there (fences, arm64 LSE, make_contended) only shows under contention. Added rows for polymorphic compare/hash and for C-side allocation into the OCaml heap, both of which are now running-ng tags, and a note on how that tag set relates to this matrix: it is a coarser selection layer, and a tag exists only if it names runtime code someone edits and selects a set no other tag gives you. * docs(CLAUDE): split the runnable tags from the documented gaps The README table lists the twelve tags you can actually run. This file also carries io_uring and ocaml_finalisers, which select nothing and abort when named, so say that explicitly rather than quoting a count of fourteen that the README appears to contradict. Also drops a stale reference: re-enabling lavyek no longer moves an `atomics` tag from cold to exercised, because there is no such tag — the mechanism has no measurable coverage, which the matrix records as a gap.
* owl: run OpenBLAS single-threaded, re-size the ladder, drop huge OpenBLAS started one thread per core, so under running-ng's single-core pin owl_gc_huge ran 4x the instructions and hit its timeout. With one thread the old large rung was 99% BLAS, so the ladder is now dim 250/400/800. * ocaml_intrinsics_kernel: rename clz/ctz stubs clashing with trunk runtime OCaml trunk (ocaml/ocaml#15018) added caml_int_clz/caml_int_ctz, which ocaml_intrinsics_kernel also defines. Temporary until upstream resolves it. * ci: let a failing trunk leg fail the run continue-on-error marked the run green while trunk was red. Branch protection already requires only the stable check, so trunk still doesn't block merges. --------- Co-authored-by: Eduardo Souza <eduardo@tarides.com>
* Replace ppx preprocessing with its expanded source Setup builds every benchmark once on a dedicated pinned switch (macro-benches-ppx) and expands every ppx output in place, so benchmark builds on any compiler never build a ppx. The expansion is checked against scripts/ppx-expand/manifest. * Run all of setup on its own pinned switch setup creates macro-benches-tools (scripts/lib-switch.sh) instead of requiring an existing switch, and the ppx expansion runs on it too. CI no longer passes its runtime switch. * Start the ppx expansion's build from an empty build dir Outputs left from an earlier build were being expanded too. * Allow per-OS entries in the ppx expansion manifest extunix's ppx_have expands by the features found on the machine, so its two files differ between Linux and FreeBSD. * Create the tools switch from opam's default repository only Another registered repository can resolve ocaml-base-compiler.5.4.1 to a relocatable compiler. Also check the compiler itself, and never change an existing switch's compiler. * Add the FreeBSD expansion of extunix to the ppx manifest From a FreeBSD 15.1 run, whose expansion otherwise matched. * Show the manifest diff when the ppx expansion check fails Both sides are this OS's view, so per-OS tags and other OSes' lines do not appear as differences. * Keep CLAUDE.md's reference to patch 32 after renumbering * Document the ppx expansion and the tools switch * Read opam's switch and package lists without colour CI forces colour, and the escape codes hid ocaml-base-compiler from the tools switch check. * CI: install ocamlfind in the runtime switch goblint's apron and infer's javalib/sawja build with it, and setup no longer installs its tools there.
* Patch vendored sources so they also compile with OxCaml OxCaml's stdlib takes local arguments, which breaks curried re-exports of stdlib functions; eta-expanding them is equivalent on stock OCaml. 45/95 programs now build on OxCaml, and 95/95 still build on 5.4.1 and 5.5.0. scripts/tests/oxcaml-repros.sh reproduces each class of incompatibility. * Also patch ocaml_intrinsics_kernel and ctypes for OxCaml Drop [@@Builtin] from the eight intrinsics this OxCaml lacks (stock ignores the attribute; both call the C stub), and eta-expand ctypes' bigarray_kind. OxCaml now builds 50/95; stock 5.4.1 and 5.5.0 still build 95/95. Also fixes setup-oxcaml.sh reporting a replacement as applied when <new> is a prefix of <old>. * Renumber the OxCaml patches after master's patch 32 and ppx-expand's 33-34 * Expand ppx for OxCaml too, and add five more portable OxCaml patches Files with oxcaml or flambda_backend conditionals get an expansion for OxCaml's 5.4.0+ox. Patches 50-54: jsoo, devkit, goblint, base's mapper.mll and apron. * Record the expansion with the OxCaml variants and patches 50-54 * Patch read_cma and base's shadow-stdlib generator for OxCaml (55-57) Both use compiler-libs, whose API differs on OxCaml, so they get an OxCaml source chosen by %{ocaml_version}, as OxCaml's own vendored copies do. jsoo now builds on OxCaml (78/94). * Patch base, core, liquidsoap, frama-c and infer for OxCaml (58-62) * Record the expansion with patches 58-62; OxCaml now builds 94/94 * ci: an oxcaml leg building oxcaml/oxcaml main * README: OxCaml patches * ci: select the oxcaml switch through OPAMSWITCH * setup-oxcaml: skip files the ppx expansion already rewrote * ci: add swap on the oxcaml leg (#36)
Anonymous API requests share a per-IP rate limit on hosted runners and intermittently 403 (trunk leg of run 37096710444).
oxcaml main broke the released dune 3.22.2+ox (oxcaml#5462), so the leg now builds the commit in .github/oxcaml-pin.env (the last green one). oxcaml-bump.yml points the pin at main on the oxcaml-bump branch weekly, runs CI there and fails unless the oxcaml leg passes.
A GitHub 5xx on one tarball failed the whole setup. A failed attempt's partial duniverse/ is removed, since setup skips the pull when it exists.
* alt-ergo: run unsat_smt2 to a step bound instead of a time limit --timelimit 15 made its wall time 15 s on every runtime, and its timeout handler raises from a signal handler, which OxCaml makes fatal (exit 2 instead of 142). --steps-bound 12000 is ~15 s of fixed work and exits 0. * docs: alt_ergo_unsat_smt2 runs to a step bound
* setup: patches 63-65 for OCaml trunk 5.7 (O_NOFOLLOW, jsoo hint rename) * ppx-expand: manifest with jsoo's 5.7 bucket * setup: patch 65 switches at 5.6, where #15135 was backported * ppx-expand: manifest for patch 65 at 5.6
…ain (#42) * setup: restate option's any parameter for oxcaml#5462 Patch 66: base and ppx_yojson_conv_lib get an OxCaml variant declaring type ('a : any) t = 'a option = None | Some of 'a; odoc-parser's compat drops the constructors. variant now handles .mli too. * setup: restate option's any parameter in core's Base.Option re-export Applied after the ppx expansion, which rewrites core's option.mli. * ci: build the oxcaml leg's dune from a pinned ocaml/dune main commit Dune's CI bootstraps dune main with OxCaml main, while the +ox dunes in oxcaml/opam-repository target OxCaml releases. The bump job moves DUNE_SHA with the oxcaml pin. Pin oxcaml to 792234e, where 3.22.2+ox broke (oxcaml#5462).
oxcaml/oxcaml@792234e...a5da9e9 ocaml/dune@99a7166...99a7166 Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
* Build scripts safe to run in parallel across runtimes Every dune call holds its build dir's lock and a shared tree lock; infer holds the tree lock exclusively while it hides duniverse packages. Shared inputs are generated under a lock, jsoo compiles its workload in a private dir, and apron/javalib build from per-runtime source copies. .parallel-builds tells running-ng it may build this tree in parallel. * ocamlc-compile-uucp: stage inputs only when stale, swapped in whole Another runtime's build of the same rung reads the staged dir outside the lock, and the unconditional rm -rf + regenerate broke it mid-read (found on FreeBSD; reproduces on Linux). ocamldep errors now reach the build log. * CLAUDE.md: shared inputs are regenerated only when stale
* setup: start over when setup's inputs change Every step skips when its output exists, so a tree set up from an older pin survived a bump and failed the ppx manifest check. scripts/setup-stamp.sh hashes the inputs; on a mismatch setup removes the trees and the benchmark build products before re-vendoring. CI keys its cache on the same hash. * README: make setup re-vendors when a setup input changed
* setup: patch 67, let the pinned jsoo run on OCaml 5.7 Trunk is 5.7, and jsoo built by it exits with "OCaml version unsupported. Upgrade js_of_ocaml." Upstream's 5.6 support was only this bound; on trunk cfa217c jsoo_default builds, runs and emits the same JavaScript as on 5.4.1. * CI: trunk legs build ocaml/ocaml trunk (5.7), not the 5.6 branch ocaml-variants.5.6.0+trunk now tracks the 5.6 branch, while the workflows resolved the trunk tip for their cache keys and summaries.
A transient 404 for guava's jar from Maven Central failed the cache-less FreeBSD job. curl now retries (--retry-all-errors covers HTTP errors), and a corpus jar failing its checksum is deleted so the next setup refetches it.
* CI: a macOS leg; Homebrew paths and ld64-friendly libevent flags lib-portable.sh adds Homebrew's include/lib dirs (and keg-only openblas's pkg-config dir) on macOS, as it does LOCALBASE on FreeBSD. libevent and devkit pick their link flags by OS (ld64 has no --no-as-needed; .dylib). ci-run-all.sh falls back to gtimeout and expands empty arrays safely under bash 3.2. The macOS leg's setup step has a TEMP(macos-discovery) fallback that records the Darwin ppx manifest lines; to be removed before merge. * CI: key the vendored-sources cache by OS actions/cache shares a key between Linux and macOS, so the macOS leg restored the stable leg's Linux-configured trees. * setup: patch 68, link libomp for owl on macOS Homebrew's openblas pkg-config asks for OpenMP without its runtime, like FreeBSD's (patch 26), so owl's link fails with ___kmpc_* undefined. * macOS: Darwin ppx manifest lines; drop the discovery fallback; docs * README: macOS prerequisites * CI: macOS installs README's brew line, pyyaml included * macOS: PyYAML by pip (Homebrew has no formula for it)
…eptions (#57) * oxcaml-repros: cases for patches 54, 55-59, 62 and signal-handler exceptions Eight new cases: base's 'a ref constraint (58), %array_length on an abstract type (59), constructor disambiguation across |> with a labelled partial application (62), the compiler-libs changes (55, 56, 57), a C stub defining its own bool (54), and an exception raised from a signal handler, which OxCaml makes fatal (alt-ergo, #39). The harness now takes an optional m.mli, extra compiler flags (`flags`), an OxCaml-only fix (fixed.oxcaml.ml, as setup-oxcaml.sh's variant files), and a test.sh for cases that link, run or compile C. Checked on oxcaml main @ dbaa270 (macOS arm64) against stock 5.4.1: stock accepts every case, OxCaml fails every original. stdbool-stub's fixed one fails there too, as OxCaml's C compiler is -std=gnu23 on macOS. * oxcaml-repros: record-field and stdlib-type-annotation cases; later-use-mode in iter's shape record-field is devkit's string ops record (patch 43), stdlib-type-annotation is base's Obj.magic ascriptions (58). later-use-mode now has iter's concat_str shape, a call that is not in tail position: OxCaml then reports the error against iter's .mli rather than at the partial application. CLAUDE.md: why OxCaml's C compiler is -std=gnu23 on macOS.
5.6 dev snapshots from before ocaml/ocaml#15135 still have Hint_physical_comparison but report the same version, so the version check picked the wrong constructor. A wildcard covers both.
* setup: SDKROOT for Homebrew gcc on macOS; init an unused opam root Homebrew's gcc cannot find stdio.h when the Command Line Tools lag the macOS SDK (goblint's CIL). lib-portable.sh exports xcrun's SDK on Darwin when SDKROOT is unset. ensure_tools_switch runs opam init --bare on a root with no config. * README: brew upgrades installed formulae; setup handles a lagging SDK
* setup: build PCRE 1 from pinned source; no system package * README: PCRE comes from setup
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Moves the oxcaml leg to oxcaml main
5e9594dand dune to94c25b0.