mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
5f7ae920c6
which allows the location of the temporary directory to be controlled. While I'm here also write `website.dox` into the temporary directory where it belongs instead of in the source tree and simplify the logic that deletes the temporary directory and its contents.
129 lines
4.2 KiB
Python
129 lines
4.2 KiB
Python
# Copyright (c) Microsoft Corporation 2015
|
|
"""
|
|
Z3 API documentation generator script
|
|
"""
|
|
|
|
import argparse
|
|
import os
|
|
import shutil
|
|
import re
|
|
import getopt
|
|
import pydoc
|
|
import sys
|
|
import subprocess
|
|
import shutil
|
|
|
|
ML_ENABLED=False
|
|
BUILD_DIR='../build'
|
|
DOXYGEN_EXE='doxygen'
|
|
TEMP_DIR=os.path.join(os.getcwd(), 'tmp')
|
|
|
|
def parse_options():
|
|
global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR
|
|
parser = argparse.ArgumentParser(description=__doc__)
|
|
parser.add_argument('-b',
|
|
'--build',
|
|
default=BUILD_DIR,
|
|
help='Directory where Z3 is built (default: %(default)s)',
|
|
)
|
|
parser.add_argument('--ml',
|
|
action='store_true',
|
|
default=False,
|
|
help='Include ML/OCaml API documentation'
|
|
)
|
|
parser.add_argument('--doxygen-executable',
|
|
dest='doxygen_executable',
|
|
default=DOXYGEN_EXE,
|
|
help='Doxygen executable to use (default: %(default)s)',
|
|
)
|
|
parser.add_argument('--temp-dir',
|
|
dest='temp_dir',
|
|
default=TEMP_DIR,
|
|
help='Path to directory to use as temporary directory. '
|
|
'(default: %(default)s)',
|
|
)
|
|
pargs = parser.parse_args()
|
|
ML_ENABLED = pargs.ml
|
|
BUILD_DIR = pargs.build
|
|
DOXYGEN_EXE = pargs.doxygen_executable
|
|
TEMP_DIR = pargs.temp_dir
|
|
return
|
|
|
|
def mk_dir(d):
|
|
if not os.path.exists(d):
|
|
os.makedirs(d)
|
|
|
|
# Eliminate def_API, extra_API, and def_Type directives from file 'inf'.
|
|
# The result is stored in 'outf'.
|
|
def cleanup_API(inf, outf):
|
|
pat1 = re.compile(".*def_API.*")
|
|
pat2 = re.compile(".*extra_API.*")
|
|
pat3 = re.compile(r".*def_Type\(.*")
|
|
_inf = open(inf, 'r')
|
|
_outf = open(outf, 'w')
|
|
for line in _inf:
|
|
if not pat1.match(line) and not pat2.match(line) and not pat3.match(line):
|
|
_outf.write(line)
|
|
|
|
try:
|
|
parse_options()
|
|
|
|
print("Creating temporary directory \"{}\"".format(TEMP_DIR))
|
|
mk_dir(TEMP_DIR)
|
|
# Short-hand for path to temporary file
|
|
def temp_path(path):
|
|
return os.path.join(TEMP_DIR, path)
|
|
|
|
fi = open('website.dox', 'r')
|
|
fo = open(temp_path('website.dox'), 'w')
|
|
|
|
for line in fi:
|
|
if (line != '[ML]\n'):
|
|
fo.write(line)
|
|
elif (ML_ENABLED):
|
|
fo.write(' - <a class="el" href="ml/index.html">ML/OCaml API</a>\n')
|
|
fi.close()
|
|
fo.close()
|
|
|
|
|
|
mk_dir('api/html')
|
|
shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py'))
|
|
cleanup_API('../src/api/z3_api.h', temp_path('z3_api.h'))
|
|
cleanup_API('../src/api/z3_ast_containers.h', temp_path('z3_ast_containers.h'))
|
|
cleanup_API('../src/api/z3_algebraic.h', temp_path('z3_algebraic.h'))
|
|
cleanup_API('../src/api/z3_polynomial.h', temp_path('z3_polynomial.h'))
|
|
cleanup_API('../src/api/z3_rcf.h', temp_path('z3_rcf.h'))
|
|
cleanup_API('../src/api/z3_fixedpoint.h', temp_path('z3_fixedpoint.h'))
|
|
cleanup_API('../src/api/z3_optimization.h', temp_path('z3_optimization.h'))
|
|
cleanup_API('../src/api/z3_interp.h', temp_path('z3_interp.h'))
|
|
cleanup_API('../src/api/z3_fpa.h', temp_path('z3_fpa.h'))
|
|
|
|
print("Removed annotations from z3_api.h.")
|
|
try:
|
|
if subprocess.call([DOXYGEN_EXE, 'z3api.dox']) != 0:
|
|
print("ERROR: doxygen returned nonzero return code")
|
|
exit(1)
|
|
except:
|
|
print("ERROR: failed to execute 'doxygen', make sure doxygen (http://www.doxygen.org) is available in your system.")
|
|
exit(1)
|
|
print("Generated C and .NET API documentation.")
|
|
shutil.rmtree(os.path.realpath(TEMP_DIR))
|
|
print("Removed temporary directory \"{}\"".format(TEMP_DIR))
|
|
sys.path.append('../src/api/python/z3')
|
|
pydoc.writedoc('z3')
|
|
shutil.move('z3.html', 'api/html/z3.html')
|
|
print("Generated Python documentation.")
|
|
|
|
if ML_ENABLED:
|
|
mk_dir('api/html/ml')
|
|
if subprocess.call(['ocamldoc', '-html', '-d', 'api\html\ml', '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../src/api/ml/z3.mli']) != 0:
|
|
print("ERROR: ocamldoc failed.")
|
|
exit(1)
|
|
print("Generated ML/OCaml documentation.")
|
|
|
|
print("Documentation was successfully generated at subdirectory './api/html'.")
|
|
except Exception:
|
|
exctype, value = sys.exc_info()[:2]
|
|
print("ERROR: failed to generate documentation: %s" % value)
|
|
exit(1)
|