mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 22:23:22 +00:00
Documentation generator bugfixes and updates.
This commit is contained in:
parent
dd0d0a9075
commit
f993d3df15
2 changed files with 66 additions and 2 deletions
|
@ -1,11 +1,52 @@
|
||||||
import os
|
import os
|
||||||
import shutil
|
import shutil
|
||||||
import re
|
import re
|
||||||
|
import getopt
|
||||||
import pydoc
|
import pydoc
|
||||||
import sys
|
import sys
|
||||||
import subprocess
|
import subprocess
|
||||||
import shutil
|
import shutil
|
||||||
|
|
||||||
|
ML_ENABLED=False
|
||||||
|
BUILD_DIR='../build'
|
||||||
|
|
||||||
|
def norm_path(p):
|
||||||
|
# We use '/' on mk_project for convenience
|
||||||
|
return os.path.join(*(p.split('/')))
|
||||||
|
|
||||||
|
def display_help(exit_code):
|
||||||
|
print("mk_api_doc.py: Z3 documentation generator\n")
|
||||||
|
print("\nOptions:")
|
||||||
|
print(" -h, --help display this message.")
|
||||||
|
print(" -b <subdir>, --build=<subdir> subdirectory where Z3 is built (default: ../build).")
|
||||||
|
print(" --ml include ML/OCaml API documentation.")
|
||||||
|
|
||||||
|
def parse_options():
|
||||||
|
global ML_ENABLED, BUILD_DIR
|
||||||
|
|
||||||
|
try:
|
||||||
|
options, remainder = getopt.gnu_getopt(sys.argv[1:],
|
||||||
|
'b:h',
|
||||||
|
['build=', 'help', 'ml'])
|
||||||
|
except:
|
||||||
|
print("ERROR: Invalid command line option")
|
||||||
|
display_help(1)
|
||||||
|
|
||||||
|
for opt, arg in options:
|
||||||
|
if opt in ('-b', '--build'):
|
||||||
|
BUILD_DIR = norm_path(arg)
|
||||||
|
elif opt in ('h', '--help'):
|
||||||
|
display_help()
|
||||||
|
exit(1)
|
||||||
|
elif opt in ('--ml'):
|
||||||
|
ML_ENABLED=True
|
||||||
|
else:
|
||||||
|
print("ERROR: Invalid command line option: %s" % opt)
|
||||||
|
display_help(1)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
def mk_dir(d):
|
def mk_dir(d):
|
||||||
if not os.path.exists(d):
|
if not os.path.exists(d):
|
||||||
os.makedirs(d)
|
os.makedirs(d)
|
||||||
|
@ -22,9 +63,23 @@ def cleanup_API(inf, outf):
|
||||||
_outf.write(line)
|
_outf.write(line)
|
||||||
|
|
||||||
try:
|
try:
|
||||||
|
parse_options()
|
||||||
|
|
||||||
|
fi = open('website.dox', 'r')
|
||||||
|
fo = open('website-adj.dox', 'w')
|
||||||
|
|
||||||
|
for line in fi:
|
||||||
|
if (line != '[ML]\n'):
|
||||||
|
fo.write(line)
|
||||||
|
elif (ML_ENABLED):
|
||||||
|
fo.write(' - <a class="el" href="api/html/ml/index.html">ML/OCaml API</a>\n')
|
||||||
|
fi.close()
|
||||||
|
fo.close()
|
||||||
|
|
||||||
mk_dir('api/html')
|
mk_dir('api/html')
|
||||||
mk_dir('tmp')
|
mk_dir('tmp')
|
||||||
shutil.copyfile('website.dox', 'tmp/website.dox')
|
shutil.copyfile('website-adj.dox', 'tmp/website.dox')
|
||||||
|
os.remove('website-adj.dox')
|
||||||
shutil.copyfile('../src/api/python/z3.py', 'tmp/z3py.py')
|
shutil.copyfile('../src/api/python/z3.py', 'tmp/z3py.py')
|
||||||
cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h')
|
cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h')
|
||||||
cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h')
|
cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h')
|
||||||
|
@ -59,6 +114,14 @@ try:
|
||||||
pydoc.writedoc('z3')
|
pydoc.writedoc('z3')
|
||||||
shutil.move('z3.html', 'api/html/z3.html')
|
shutil.move('z3.html', 'api/html/z3.html')
|
||||||
print "Generated Python documentation."
|
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'."
|
print "Documentation was successfully generated at subdirectory './api/html'."
|
||||||
except:
|
except:
|
||||||
print "ERROR: failed to generate documentation"
|
print "ERROR: failed to generate documentation"
|
||||||
|
|
|
@ -14,6 +14,7 @@
|
||||||
- \ref cppapi
|
- \ref cppapi
|
||||||
- <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
|
- <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
|
||||||
- <a class="el" href="namespacecom_1_1microsoft_1_1z3.html">Java API</a>
|
- <a class="el" href="namespacecom_1_1microsoft_1_1z3.html">Java API</a>
|
||||||
- <a class="el" href="namespacez3py.html">Python API</a> (also available in <a class="el" href="z3.html">pydoc format</a>).
|
- <a class="el" href="namespacez3py.html">Python API</a> (also available in <a class="el" href="z3.html">pydoc format</a>)
|
||||||
|
[ML]
|
||||||
- Try Z3 online at <a href="http://rise4fun.com/z3">RiSE4Fun</a>.
|
- Try Z3 online at <a href="http://rise4fun.com/z3">RiSE4Fun</a>.
|
||||||
*/
|
*/
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue