mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

Merge pull request #8682 from Z3Prover/copilot/fix-docs-and-update-script

Browse source 
Add Go API link to documentation index and prevent content overwrite
This commit is contained in:
Nikolaj Bjorner 2026-02-18 11:56:18 -08:00 • committed by GitHub
commit 672d243f0f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.github/workflows/docs.yml vendored
View file

@ -88,7 +88,7 @@ jobs:
working-directory: doc working-directory: doc
run: | run: |
eval $(opam env) eval $(opam env)
python3 mk_api_doc.py --mld --output-dir=api --z3py-package-path=../build-x64/python/z3 --build=../build-x64 python3 mk_api_doc.py --mld --go --output-dir=api --z3py-package-path=../build-x64/python/z3 --build=../build-x64
Z3BUILD=build-x64 python3 mk_params_doc.py Z3BUILD=build-x64 python3 mk_params_doc.py
mkdir api/html/ml mkdir api/html/ml
ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build-x64/api/ml ../build-x64/api/ml/z3enums.mli ../build-x64/api/ml/z3.mli ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build-x64/api/ml ../build-x64/api/ml/z3enums.mli ../build-x64/api/ml/z3.mli
@ -122,7 +122,7 @@ jobs:
working-directory: doc working-directory: doc
run: | run: |
eval $(opam env) eval $(opam env)
python3 mk_api_doc.py --js --output-dir=api --mld --z3py-package-path=../build-x64/python/z3 --build=../build-x64 python3 mk_api_doc.py --js --go --output-dir=api --mld --z3py-package-path=../build-x64/python/z3 --build=../build-x64
- name: Download Go Documentation - name: Download Go Documentation
uses: actions/download-artifact@v4 uses: actions/download-artifact@v4

82
doc/mk_api_doc.py
View file

@ -464,86 +464,10 @@ try:
print("Generated Javascript documentation.") print("Generated Javascript documentation.")
if GO_ENABLED: if GO_ENABLED:
go_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'go') # Go documentation is generated by mk_go_doc.py separately and downloaded as an artifact
mk_dir(go_output_dir) # We just need to register that it exists for the link in the index
go_api_abs_path = os.path.abspath(GO_API_PATH) print("Go documentation link will be included in index.")
# Check if godoc is available
godoc_available = False
try:
subprocess.check_output(['go', 'version'], stderr=subprocess.STDOUT)
godoc_available = True
except (subprocess.CalledProcessError, FileNotFoundError):
print("WARNING: Go is not installed. Skipping godoc generation.")
godoc_available = False
if godoc_available:
# Generate godoc HTML for each Go file
go_files = [
'z3.go', 'solver.go', 'tactic.go', 'bitvec.go',
'fp.go', 'seq.go', 'datatype.go', 'optimize.go'
]
# Create a simple HTML index
index_html = os.path.join(go_output_dir, 'index.html')
with open(index_html, 'w') as f:
f.write('<!DOCTYPE html>\n<html>\n<head>\n')
f.write('<title>Z3 Go API Documentation</title>\n')
f.write('<style>\n')
f.write('body { font-family: Arial, sans-serif; margin: 40px; }\n')
f.write('h1 { color: #333; }\n')
f.write('ul { list-style-type: none; padding: 0; }\n')
f.write('li { margin: 10px 0; }\n')
f.write('a { color: #0066cc; text-decoration: none; font-size: 18px; }\n')
f.write('a:hover { text-decoration: underline; }\n')
f.write('.description { color: #666; margin-left: 20px; }\n')
f.write('</style>\n')
f.write('</head>\n<body>\n')
f.write('<h1>Z3 Go API Documentation</h1>\n')
f.write('<p>Go bindings for the Z3 Theorem Prover.</p>\n')
f.write('<h2>Package: github.com/Z3Prover/z3/src/api/go</h2>\n')
f.write('<ul>\n')
# Add links to the README
readme_path = os.path.join(go_api_abs_path, 'README.md')
if os.path.exists(readme_path):
# Copy README as documentation
readme_md_path = os.path.join(go_output_dir, 'README.md')
try:
shutil.copy(readme_path, readme_md_path)
f.write('<li><a href="README.md">README - Getting Started</a></li>\n')
except Exception as e:
print(f"Warning: Could not copy README.md: {e}")
# Add module descriptions
f.write('<li><a href="#core">z3.go</a> - Core types (Context, Config, Symbol, Sort, Expr, FuncDecl)</li>\n')
f.write('<li><a href="#solver">solver.go</a> - Solver and Model API</li>\n')
f.write('<li><a href="#tactic">tactic.go</a> - Tactics, Goals, Probes, and Parameters</li>\n')
f.write('<li><a href="#bitvec">bitvec.go</a> - Bit-vector operations</li>\n')
f.write('<li><a href="#fp">fp.go</a> - Floating-point operations</li>\n')
f.write('<li><a href="#seq">seq.go</a> - Sequences, strings, and regular expressions</li>\n')
f.write('<li><a href="#datatype">datatype.go</a> - Algebraic datatypes, tuples, enumerations</li>\n')
f.write('<li><a href="#optimize">optimize.go</a> - Optimization with maximize/minimize objectives</li>\n')
f.write('</ul>\n')
f.write('<h2>Usage</h2>\n')
f.write('<pre>\n')
f.write('import "github.com/Z3Prover/z3/src/api/go"\n\n')
f.write('ctx := z3.NewContext()\n')
f.write('solver := ctx.NewSolver()\n')
f.write('x := ctx.MkIntConst("x")\n')
f.write('solver.Assert(ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort())))\n')
f.write('if solver.Check() == z3.Satisfiable {\n')
f.write(' fmt.Println("sat")\n')
f.write('}\n')
f.write('</pre>\n')
f.write('<h2>Installation</h2>\n')
f.write('<p>See <a href="README.md">README</a> for build instructions.</p>\n')
f.write('<p>Go back to <a href="../index.html">main API documentation</a>.</p>\n')
f.write('</body>\n</html>\n')
print("Generated Go documentation.")
print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY)) print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY))
except Exception: except Exception: