mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-13 06:35:46 +00:00
Code Activity

Fix parallel-make race in OCaml example builds (#10720)

Browse source 
The "Ubuntu with OCaml on z3-static" CI job fails intermittently (e.g.
in the runs for #10718) with:

```
File "../examples/ml/ml_example.ml", line 1:
Error: The file ../examples/ml/ml_example.cmo is not a bytecode object file
```

CI runs `make -j$(nproc) _ex_ml_example_post_install`, which builds
`ml_example_static.byte`, `ml_example_static_custom.byte`, and
`ml_example_static` concurrently. All three rules compile the same
`examples/ml/ml_example.ml`, and ocamlfind writes the intermediate
`.cmi`/`.cmo`/`.cmx` files into that shared source directory, so
concurrent compilations clobber each other (the job's log shows all
three ocamlfind invocations starting within ~5 ms). The same race exists
for the shared-lib variants and for the in-tree
`ml_example.byte`/`ml_example$(EXE_EXT)` pair, which both write
`ml_example.cmi`.

This change chains each of these targets to the previous one with an
order-only prerequisite (`|`), so the compilations run sequentially
under `make -j` while leaving up-to-date semantics unchanged.

Generated Makefile fragment after the change:

```make
ml_example_static.byte: ../examples/ml/ml_example.ml
	ocamlfind ocamlc -o  ml_example_static.byte -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
ml_example_static_custom.byte: ../examples/ml/ml_example.ml | ml_example_static.byte
	ocamlfind ocamlc -custom -o  ml_example_static_custom.byte -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
ml_example_static$(EXE_EXT): ../examples/ml/ml_example.ml | ml_example_static_custom.byte
	ocamlfind ocamlopt -o  ml_example_static$(EXE_EXT) -thread -package z3-static -linkpkg  ../examples/ml/ml_example.ml
```

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
Lev Nachmanson 2026-09-01 16:03:52 -10:00 • committed by GitHub
parent e80eeb1150
commit 7d35c948cd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
scripts/mk_util.py
View file

@ -2390,6 +2390,10 @@ class MLExampleComponent(ExampleComponent):
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
# Order-only prerequisite: both compilations write ml_example.cmi
# into the shared source directory, so keep them from racing
# under make -j.
out.write(' | ml_example.byte')
out.write('\n')
out.write('\tocamlfind %s ' % OCAMLOPT)
if DEBUG_MODE:
@ -2417,15 +2421,23 @@ class MLExampleComponent(ExampleComponent):
(OCAMLOPT, 'ml_example_shared$(EXE_EXT)')
]
# The example compilations below all write intermediate files (.cmi,
# .cmo, .cmx, .o) next to the shared .ml sources, so they clobber each
# other when run concurrently under make -j. Chain each target to the
# previous one with an order-only prerequisite to serialize them.
prev_testname = None
for ocaml_compiler, testname in ml_post_install_tests:
out.write(testname + ':')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
if prev_testname is not None:
out.write(' | %s' % prev_testname)
out.write('\n')
out.write('\tocamlfind %s -o %s %s %s ' % (ocaml_compiler, debug_opt, testname, opam_z3_opts))
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
out.write('\n')
prev_testname = testname
if STATIC_LIB:
out.write('_ex_ml_example_post_install: ml_example_static.byte ml_example_static_custom.byte ml_example_static$(EXE_EXT)\n')