mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 19:45:41 +00:00
cfee267068
The "Ubuntu with OCaml on z3-static" CI job intermittently fails with `Fatal error: exception End_of_file` from the OCaml bytecode linker when compiling `ml_example_static.byte`. ## Root cause `ocamlfind install z3-static build/api/ml/* build/libz3-static.a` auto-recognizes `dllz3ml-static.so` (starts with `dll`) as a C stub and copies it to `stublibs`, but without an explicit `-dll` flag it **does not update `ld.conf`**—confirmed by the CI warning: ``` ocamlfind: [WARNING] You have installed DLLs but the directory .../stublibs is not mentioned in ld.conf ``` `ocamlc` searches `ld.conf` for stub DLLs at bytecode link time; the missing entry causes `End_of_file`. The non-static job is unaffected because it passes `-dll build/libz3.*` explicitly, which triggers the `ld.conf` update as a side-effect. ## Fix After `ocamlfind install`, append the `stublibs` path to `ld.conf` if absent: ```bash STUBLIBS="$(dirname "$(ocamlfind printconf destdir)")/stublibs" LDCONF="$(ocamlfind printconf ldconf)" if [ -d "$STUBLIBS" ] && ! grep -qF "$STUBLIBS" "$LDCONF" 2>/dev/null; then echo "$STUBLIBS" >> "$LDCONF" fi ``` Idempotent; uses `ocamlfind printconf` to avoid hardcoded paths. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| shared | ||
| a3-python.lock.yml | ||
| a3-python.md | ||
| academic-citation-tracker.lock.yml | ||
| academic-citation-tracker.md | ||
| agentics-maintenance.yml | ||
| android-build.yml | ||
| api-coherence-checker.lock.yml | ||
| api-coherence-checker.md | ||
| build-warning-fixer.lock.yml | ||
| build-warning-fixer.md | ||
| build-z3-cache.yml | ||
| ci.yml | ||
| code-conventions-analyzer.lock.yml | ||
| code-conventions-analyzer.md | ||
| code-simplifier.lock.yml | ||
| code-simplifier.md | ||
| compare-stats-anomaly-reporter.lock.yml | ||
| compare-stats-anomaly-reporter.md | ||
| copilot-setup-steps.yml | ||
| coverage.yml | ||
| cross-build.yml | ||
| csa-analysis.lock.yml | ||
| csa-analysis.md | ||
| docs.yml | ||
| fstar-master-build.yml | ||
| issue-backlog-processor.lock.yml | ||
| issue-backlog-processor.md | ||
| mark-prs-ready-for-review.yml | ||
| memory-safety-report.lock.yml | ||
| memory-safety-report.md | ||
| memory-safety.yml | ||
| msvc-static-build-clang-cl.yml | ||
| msvc-static-build.yml | ||
| nightly-validation.yml | ||
| nightly.yml | ||
| nuget-build.yml | ||
| ocaml.yaml | ||
| ostrich-benchmark.lock.yml | ||
| ostrich-benchmark.md | ||
| pyodide-pypi.yml | ||
| qf-s-benchmark.lock.yml | ||
| qf-s-benchmark.md | ||
| release-notes-updater.lock.yml | ||
| release-notes-updater.md | ||
| release.yml | ||
| smtlib-benchmark-finder.lock.yml | ||
| smtlib-benchmark-finder.md | ||
| specbot-crash-analyzer.lock.yml | ||
| specbot-crash-analyzer.md | ||
| tactic-to-simplifier.lock.yml | ||
| tactic-to-simplifier.md | ||
| tptp-benchmark.lock.yml | ||
| tptp-benchmark.md | ||
| wasm-release.yml | ||
| wasm.yml | ||
| Windows.yml | ||
| wip.yml | ||
| workflow-suggestion-agent.lock.yml | ||
| workflow-suggestion-agent.md | ||
| zipt-code-reviewer.lock.yml | ||
| zipt-code-reviewer.md | ||