From 9499b1089c1963b86696eb2fecc34123c22f30b8 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 19:30:07 +0000 Subject: [PATCH] Add --go flag to mk_api_doc.py calls and remove go directory overwrite code Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .github/workflows/docs.yml | 4 +- doc/mk_api_doc.py | 84 ++------------------------------------ 2 files changed, 6 insertions(+), 82 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index d9fd44f6c..ea483f6df 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -88,7 +88,7 @@ jobs: working-directory: doc run: | 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 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 @@ -122,7 +122,7 @@ jobs: working-directory: doc run: | 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 uses: actions/download-artifact@v4 diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 50d0656a5..42adaca0a 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -464,86 +464,10 @@ try: print("Generated Javascript documentation.") if GO_ENABLED: - go_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'go') - mk_dir(go_output_dir) - go_api_abs_path = os.path.abspath(GO_API_PATH) - - # 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('\n\n\n') - f.write('Z3 Go API Documentation\n') - f.write('\n') - f.write('\n\n') - f.write('

Z3 Go API Documentation

\n') - f.write('

Go bindings for the Z3 Theorem Prover.

\n') - f.write('

Package: github.com/Z3Prover/z3/src/api/go

\n') - f.write('\n') - - f.write('

Usage

\n') - f.write('
\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('
\n') - - f.write('

Installation

\n') - f.write('

See README for build instructions.

\n') - f.write('

Go back to main API documentation.

\n') - f.write('\n\n') - - print("Generated Go documentation.") + # Go documentation is generated by mk_go_doc.py separately and downloaded as an artifact + # We just need to register that it exists for the link in the index + print("Go documentation link will be included in index.") + print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY)) except Exception: