From 81ba729aab8d2181244de354f0bdb1ea8415691a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 15:25:45 +0100 Subject: [PATCH 01/20] [Doxygen] Fix script `--help` functionality. --- doc/mk_api_doc.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index edabcbd1b..bb5a19e5f 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -13,11 +13,13 @@ ML_ENABLED=False BUILD_DIR='../build' def display_help(exit_code): + assert isinstance(exit_code, int) print("mk_api_doc.py: Z3 documentation generator\n") print("\nOptions:") print(" -h, --help display this message.") print(" -b , --build= subdirectory where Z3 is built (default: ../build).") print(" --ml include ML/OCaml API documentation.") + sys.exit(exit_code) def parse_options(): global ML_ENABLED, BUILD_DIR @@ -34,8 +36,7 @@ def parse_options(): if opt in ('-b', '--build'): BUILD_DIR = mk_util.norm_path(arg) elif opt in ('h', '--help'): - display_help() - exit(1) + display_help(0) elif opt in ('--ml'): ML_ENABLED=True else: @@ -128,7 +129,7 @@ try: print("Generated ML/OCaml documentation.") print("Documentation was successfully generated at subdirectory './api/html'.") -except: +except Exception: exctype, value = sys.exc_info()[:2] print("ERROR: failed to generate documentation: %s" % value) exit(1) From ca678c3675a7aa1bd5b396b15660b7ab1163c193 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 15:45:57 +0100 Subject: [PATCH 02/20] [Doxygen] Fix bug where `def_Type` directives in `z3.h` would appear in generated doxygen documentation. --- doc/mk_api_doc.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index bb5a19e5f..e86205a7a 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -50,15 +50,16 @@ def mk_dir(d): if not os.path.exists(d): os.makedirs(d) -# Eliminate def_API and extra_API directives from file 'inf'. +# 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): + if not pat1.match(line) and not pat2.match(line) and not pat3.match(line): _outf.write(line) try: From 2cdb45605dcc3f17d0101f9669fb6ad8a4923e83 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 16:24:15 +0100 Subject: [PATCH 03/20] [Doxygen] Switch to using `argparse` to parse command line arguments in `mk_api_doc.py`. Given that we need to add a bunch of new command line options it makes sense to use a less clumsy and concise API. --- doc/mk_api_doc.py | 50 ++++++++++++++++++----------------------------- 1 file changed, 19 insertions(+), 31 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index e86205a7a..d27351015 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -1,5 +1,9 @@ # Copyright (c) Microsoft Corporation 2015 +""" +Z3 API documentation generator script +""" +import argparse import os import shutil import re @@ -12,39 +16,23 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' -def display_help(exit_code): - assert isinstance(exit_code, int) - print("mk_api_doc.py: Z3 documentation generator\n") - print("\nOptions:") - print(" -h, --help display this message.") - print(" -b , --build= subdirectory where Z3 is built (default: ../build).") - print(" --ml include ML/OCaml API documentation.") - sys.exit(exit_code) - 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 = mk_util.norm_path(arg) - elif opt in ('h', '--help'): - display_help(0) - elif opt in ('--ml'): - ML_ENABLED=True - else: - print("ERROR: Invalid command line option: %s" % opt) - display_help(1) - - - + 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' + ) + pargs = parser.parse_args() + ML_ENABLED = pargs.ml + BUILD_DIR = pargs.build + return def mk_dir(d): if not os.path.exists(d): From 8a1df3df6293b5f8ac9be6d42d8ba6f23d708864 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 21:52:59 +0100 Subject: [PATCH 04/20] [Doxygen] Add `--doxygen-executable` command line option to `mk_api_doc.py`. This allows a custom path to Doxygen to be specified. --- doc/mk_api_doc.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index d27351015..62130d73c 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -15,9 +15,10 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' +DOXYGEN_EXE='doxygen' def parse_options(): - global ML_ENABLED, BUILD_DIR + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -29,9 +30,15 @@ def parse_options(): 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)', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml BUILD_DIR = pargs.build + DOXYGEN_EXE = pargs.doxygen_executable return def mk_dir(d): @@ -81,7 +88,7 @@ try: print("Removed annotations from z3_api.h.") try: - if subprocess.call(['doxygen', 'z3api.dox']) != 0: + if subprocess.call([DOXYGEN_EXE, 'z3api.dox']) != 0: print("ERROR: doxygen returned nonzero return code") exit(1) except: From 5f7ae920c6758f1b359fc1827b8492b750243e4b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 22:25:51 +0100 Subject: [PATCH 05/20] [Doxygen] Teach `mk_api_doc.py` a new command line option (`--temp-dir`) 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. --- doc/mk_api_doc.py | 61 ++++++++++++++++++++++------------------------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 62130d73c..a8ee1e220 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -16,9 +16,10 @@ 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 + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -35,10 +36,17 @@ def parse_options(): 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): @@ -60,8 +68,14 @@ def cleanup_API(inf, outf): 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('website-adj.dox', 'w') + fo = open(temp_path('website.dox'), 'w') for line in fi: if (line != '[ML]\n'): @@ -71,20 +85,18 @@ try: fi.close() fo.close() + mk_dir('api/html') - mk_dir('tmp') - shutil.copyfile('website-adj.dox', 'tmp/website.dox') - os.remove('website-adj.dox') - shutil.copyfile('../src/api/python/z3/z3.py', 'tmp/z3py.py') - cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h') - cleanup_API('../src/api/z3_ast_containers.h', 'tmp/z3_ast_containers.h') - cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h') - cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h') - cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') - cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h') - cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h') - cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') - cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h') + 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: @@ -95,23 +107,8 @@ try: 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.") - os.remove('tmp/z3_api.h') - os.remove('tmp/z3_ast_containers.h') - os.remove('tmp/z3_algebraic.h') - os.remove('tmp/z3_polynomial.h') - os.remove('tmp/z3_rcf.h') - os.remove('tmp/z3_fixedpoint.h') - os.remove('tmp/z3_optimization.h') - os.remove('tmp/z3_interp.h') - os.remove('tmp/z3_fpa.h') - print("Removed temporary file header files.") - - os.remove('tmp/website.dox') - print("Removed temporary file website.dox") - os.remove('tmp/z3py.py') - print("Removed temporary file z3py.py") - os.removedirs('tmp') - print("Removed temporary directory tmp.") + 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') From b4f8b001cecb9a341ddacb4e590b1dcaa01889fd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 22:55:41 +0100 Subject: [PATCH 06/20] [Doxygen] Teach `mk_api_doc.py` a new command line option (`--output-dir`) to control where output files are emitted. This is implemented by making `z3api.dox` a template file (renamed `z3api.cfg.in`) and populating the template at build time with the required settings. --- doc/mk_api_doc.py | 64 +++++++++++++++++++++++++++++---- doc/{z3api.dox => z3api.cfg.in} | 2 +- 2 files changed, 58 insertions(+), 8 deletions(-) rename doc/{z3api.dox => z3api.cfg.in} (99%) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index a8ee1e220..b4a58f392 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -17,9 +17,10 @@ ML_ENABLED=False BUILD_DIR='../build' DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') +OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -42,11 +43,17 @@ def parse_options(): help='Path to directory to use as temporary directory. ' '(default: %(default)s)', ) + parser.add_argument('--output-dir', + dest='output_dir', + default=OUTPUT_DIRECTORY, + help='Path to output 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 + OUTPUT_DIRECTORY = pargs.output_dir return def mk_dir(d): @@ -65,6 +72,41 @@ def cleanup_API(inf, outf): if not pat1.match(line) and not pat2.match(line) and not pat3.match(line): _outf.write(line) +def configure_file(template_file_path, output_file_path, substitutions): + """ + Read a template file ``template_file_path``, perform substitutions + found in the ``substitutions`` dictionary and write the result to + the output file ``output_file_path``. + + The template file should contain zero or more template strings of the + form ``@NAME@``. + + The substitutions dictionary maps old strings (without the ``@`` + symbols) to their replacements. + """ + assert isinstance(template_file_path, str) + assert isinstance(output_file_path, str) + assert isinstance(substitutions, dict) + assert len(template_file_path) > 0 + assert len(output_file_path) > 0 + print("Generating {} from {}".format(output_file_path, template_file_path)) + + if not os.path.exists(template_file_path): + raise Exception('Could not find template file "{}"'.format(template_file_path)) + + # Read whole template file into string + template_string = None + with open(template_file_path, 'r') as f: + template_string = f.read() + + # Do replacements + for (old_string, replacement) in substitutions.items(): + template_string = template_string.replace('@{}@'.format(old_string), replacement) + + # Write the string to the file + with open(output_file_path, 'w') as f: + f.write(template_string) + try: parse_options() @@ -74,6 +116,13 @@ try: def temp_path(path): return os.path.join(TEMP_DIR, path) + # Create configuration file from template + doxygen_config_substitutions = { + 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, + } + doxygen_config_file = temp_path('z3api.cfg') + configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) + fi = open('website.dox', 'r') fo = open(temp_path('website.dox'), 'w') @@ -86,7 +135,7 @@ try: fo.close() - mk_dir('api/html') + mk_dir(os.path.join(OUTPUT_DIRECTORY, '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')) @@ -100,7 +149,7 @@ try: print("Removed annotations from z3_api.h.") try: - if subprocess.call([DOXYGEN_EXE, 'z3api.dox']) != 0: + if subprocess.call([DOXYGEN_EXE, doxygen_config_file]) != 0: print("ERROR: doxygen returned nonzero return code") exit(1) except: @@ -111,17 +160,18 @@ try: 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') + shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, '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: + ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') + mk_dir(ml_output_dir) + if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-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 '{}'.".format(OUTPUT_DIRECTORY)) except Exception: exctype, value = sys.exc_info()[:2] print("ERROR: failed to generate documentation: %s" % value) diff --git a/doc/z3api.dox b/doc/z3api.cfg.in similarity index 99% rename from doc/z3api.dox rename to doc/z3api.cfg.in index c96a7be73..7e6c81e4f 100644 --- a/doc/z3api.dox +++ b/doc/z3api.cfg.in @@ -52,7 +52,7 @@ PROJECT_LOGO = # If a relative path is entered, it will be relative to the location # where doxygen was started. If left blank the current directory will be used. -OUTPUT_DIRECTORY = api +OUTPUT_DIRECTORY = @OUTPUT_DIRECTORY@ # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create # 4096 sub-directories (in 2 levels) under the output directory of each output From 5a66f053848c05947a48e2aec953610291b39e28 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:38:40 +0100 Subject: [PATCH 07/20] [Doxygen] Teach `mk_api_doc.py` to use `@` style substitutions to control whether OCaml documentation link is emitted. --- doc/mk_api_doc.py | 17 ++++++----------- doc/{website.dox => website.dox.in} | 3 +-- 2 files changed, 7 insertions(+), 13 deletions(-) rename doc/{website.dox => website.dox.in} (92%) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index b4a58f392..0a7efacfa 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -123,17 +123,12 @@ try: doxygen_config_file = temp_path('z3api.cfg') configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) - 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(' - ML/OCaml API\n') - fi.close() - fo.close() - + website_dox_substitutions = {} + if ML_ENABLED: + website_dox_substitutions['OCAML_API'] = '\n - ML/OCaml API\n' + else: + website_dox_substitutions['OCAML_API'] = '' + configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) diff --git a/doc/website.dox b/doc/website.dox.in similarity index 92% rename from doc/website.dox rename to doc/website.dox.in index 799949752..b00874c97 100644 --- a/doc/website.dox +++ b/doc/website.dox.in @@ -14,7 +14,6 @@ - \ref cppapi - .NET API - Java API - - Python API (also available in pydoc format) -[ML] + - Python API (also available in pydoc format)@OCAML_API@ - Try Z3 online at RiSE4Fun. */ From c78bf66df34ad6ea9aa104ec13f37b01de30769e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:49:44 +0100 Subject: [PATCH 08/20] [Doxygen] Fix bug in `mk_api_doc.py` where the generated doxygen configuration would not point at the correct path to the temporary directory. --- doc/mk_api_doc.py | 1 + doc/z3api.cfg.in | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 0a7efacfa..cc59ffa69 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -119,6 +119,7 @@ try: # Create configuration file from template doxygen_config_substitutions = { 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, + 'TEMP_DIR': TEMP_DIR } doxygen_config_file = temp_path('z3api.cfg') configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 7e6c81e4f..bcc7113cc 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -684,7 +684,7 @@ WARN_LOGFILE = INPUT = ../src/api/dotnet \ ../src/api/java \ ../src/api/c++ \ - ./tmp + @TEMP_DIR@ # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is From 33af478ce24b33393b23952833064638fead3e8a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:55:51 +0100 Subject: [PATCH 09/20] [Doxygen] Fix some indentation in doxygen configuration file template. --- doc/z3api.cfg.in | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index bcc7113cc..cb07045b3 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -703,15 +703,15 @@ INPUT_ENCODING = UTF-8 # *.f90 *.f *.for *.vhd *.vhdl FILE_PATTERNS = website.dox \ - z3_api.h \ - z3_algebraic.h \ - z3_polynomial.h \ - z3_rcf.h \ - z3_interp.h \ - z3_fpa.h \ + z3_api.h \ + z3_algebraic.h \ + z3_polynomial.h \ + z3_rcf.h \ + z3_interp.h \ + z3_fpa.h \ z3++.h \ z3py.py \ - *.cs \ + *.cs \ *.java # The RECURSIVE tag can be used to turn specify whether or not subdirectories From eb1c985a944b59a1cbbb55912a6fcfb030c5670e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:24:46 +0100 Subject: [PATCH 10/20] [Doxygen] Fixed malformed code blocks in `z3_api.h`. These malformed `\code` blocks caused broken documentation to be generated. --- src/api/z3_api.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 272c94dda..557667b03 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3091,8 +3091,8 @@ extern "C" { \brief Create a numeral of a given sort. \param c logical context. - \param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}. - If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}. + \param numeral A string representing the numeral value in decimal notation. The string may be of the form `[num]*[.[num]*][E[+|-][num]+]`. + If the given sort is a real, then the numeral can be a rational, that is, a string of the form `[num]* / [num]*` . \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size. \sa Z3_mk_int From 7242a77a3f377308dbfdd4b62a4dca7d80cb05d2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:31:05 +0100 Subject: [PATCH 11/20] [Doxygen] Fix typo found with Doxygen warning ``` warning: Found unknown command `\s' ``` --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 557667b03..04f84fa2a 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3306,7 +3306,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst); /** - \brief Retrieve from \s the unit sequence positioned at position \c index. + \brief Retrieve from \c s the unit sequence positioned at position \c index. def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ From fe702d7782db990cb90ff2bea390b100fdd65872 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:36:53 +0100 Subject: [PATCH 12/20] [Doxygen] Fix warning about non-existent functions. `Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop` respectively. --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 04f84fa2a..45065f856 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1500,7 +1500,7 @@ extern "C" { All main interaction with Z3 happens in the context of a \c Z3_context. In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects - are determined by the scope level of #Z3_push and #Z3_pop. + are determined by the scope level of #Z3_solver_push and #Z3_solver_pop. In other words, a Z3_ast object remains valid until there is a call to Z3_pop that takes the current scope below the level where the object was created. From e309174ec968d378f36415611dee1a09be52ccdd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 11:32:26 +0100 Subject: [PATCH 13/20] [Doxygen] Add `--z3py-package-path` command line option to `mk_api_doc.py` so that the location of the z3py package can be specified. This is needed by the CMake build system because the complete Z3py package is not emitted in the source tree. Also fix a bug in the path added to the module/package search path. The directory containing the `z3` package needs to be added not the `z3` package directory itself. --- doc/mk_api_doc.py | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index cc59ffa69..3a1f8b3f8 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -18,9 +18,10 @@ BUILD_DIR='../build' DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') +Z3PY_PACKAGE_PATH='../src/api/python/z3' def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY, Z3PY_PACKAGE_PATH parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -48,12 +49,22 @@ def parse_options(): default=OUTPUT_DIRECTORY, help='Path to output directory (default: %(default)s)', ) + parser.add_argument('--z3py-package-path', + dest='z3py_package_path', + default=Z3PY_PACKAGE_PATH, + help='Path to directory containing Z3py package (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 OUTPUT_DIRECTORY = pargs.output_dir + Z3PY_PACKAGE_PATH = pargs.z3py_package_path + if not os.path.exists(Z3PY_PACKAGE_PATH): + raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH)) + if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3': + raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH)) return def mk_dir(d): @@ -154,7 +165,7 @@ try: 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') + sys.path.append(os.path.dirname(Z3PY_PACKAGE_PATH)) pydoc.writedoc('z3') shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) print("Generated Python documentation.") From cb6baa8bcb5f987cf6577307e1f7f0809386d981 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 11:47:50 +0100 Subject: [PATCH 14/20] [Doxygen] Put the path to the directory containing the Z3py package at the beginning of the search path so it is picked up first. This is to try to avoid picking an installed copy of Z3py. --- doc/mk_api_doc.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 3a1f8b3f8..10b2fcf55 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -165,7 +165,9 @@ try: print("Generated C and .NET API documentation.") shutil.rmtree(os.path.realpath(TEMP_DIR)) print("Removed temporary directory \"{}\"".format(TEMP_DIR)) - sys.path.append(os.path.dirname(Z3PY_PACKAGE_PATH)) + # Put z3py at the beginning of the search path to try to avoid picking up + # an installed copy of Z3py. + sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) pydoc.writedoc('z3') shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) print("Generated Python documentation.") From fa8f6f20a5fa59f3e4e180cbfbb0c575d7b4e1ed Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:07:30 +0100 Subject: [PATCH 15/20] [Doxygen] Teach `mk_api_doc.py` to prevent ".NET", "Z3py" and "Java" bindings from appearing in the generated documentation. This can be enabled with `--no-dotnet`, `--no-z3py`, and `--no-java` respectively. This fine-grained control is being added for the CMake build system which will need this control. --- doc/mk_api_doc.py | 102 ++++++++++++++++++++++++++++++++++++++++----- doc/website.dox.in | 7 +--- doc/z3api.cfg.in | 9 ++-- 3 files changed, 97 insertions(+), 21 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 10b2fcf55..b61036d44 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -19,9 +19,13 @@ DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') Z3PY_PACKAGE_PATH='../src/api/python/z3' +Z3PY_ENABLED=True +DOTNET_ENABLED=True +JAVA_ENABLED=True def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY, Z3PY_PACKAGE_PATH + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY + global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -54,6 +58,28 @@ def parse_options(): default=Z3PY_PACKAGE_PATH, help='Path to directory containing Z3py package (default: %(default)s)', ) + # FIXME: I would prefer not to have negative options (i.e. `--z3py` + # instead of `--no-z3py`) but historically these bindings have been on by + # default so we have options to disable generating documentation for these + # bindings rather than enable them. + parser.add_argument('--no-z3py', + dest='no_z3py', + action='store_true', + default=False, + help='Do not generate documentation for Python bindings', + ) + parser.add_argument('--no-dotnet', + dest='no_dotnet', + action='store_true', + default=False, + help='Do not generate documentation for .NET bindings', + ) + parser.add_argument('--no-java', + dest='no_java', + action='store_true', + default=False, + help='Do not generate documentation for Java bindings', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml BUILD_DIR = pargs.build @@ -65,6 +91,9 @@ def parse_options(): raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH)) if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3': raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH)) + Z3PY_ENABLED = not pargs.no_z3py + DOTNET_ENABLED = not pargs.no_dotnet + JAVA_ENABLED = not pargs.no_java return def mk_dir(d): @@ -132,18 +161,70 @@ try: 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, 'TEMP_DIR': TEMP_DIR } + + if Z3PY_ENABLED: + print("Z3Py documentation enabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py' + else: + print("Z3Py documentation disabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = '' + if DOTNET_ENABLED: + print(".NET documentation enabled") + doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs' + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '../src/api/dotnet' + else: + print(".NET documentation disabled") + doxygen_config_substitutions['DOTNET_API_FILES'] = '' + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '' + if JAVA_ENABLED: + print("Java documentation enabled") + doxygen_config_substitutions['JAVA_API_FILES'] = '*.java' + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '../src/api/java' + else: + print("Java documentation disabled") + doxygen_config_substitutions['JAVA_API_FILES'] = '' + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '' + doxygen_config_file = temp_path('z3api.cfg') configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) website_dox_substitutions = {} + bullet_point_prefix='\n - ' + if Z3PY_ENABLED: + website_dox_substitutions['PYTHON_API'] = ( + '{prefix}Python API ' + '(also available in pydoc format)' + ).format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['PYTHON_API'] = '' + if DOTNET_ENABLED: + website_dox_substitutions['DOTNET_API'] = ( + '{prefix}' + '' + '.NET API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['DOTNET_API'] = '' + if JAVA_ENABLED: + website_dox_substitutions['JAVA_API'] = ( + '{prefix}' + 'Java API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['JAVA_API'] = '' if ML_ENABLED: - website_dox_substitutions['OCAML_API'] = '\n - ML/OCaml API\n' + website_dox_substitutions['OCAML_API'] = ( + 'ML/OCaml API' + ).format( + prefix=bullet_point_prefix) else: website_dox_substitutions['OCAML_API'] = '' configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) - shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) + if Z3PY_ENABLED: + 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')) @@ -162,15 +243,16 @@ try: 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.") + print("Generated Doxygen based documentation") shutil.rmtree(os.path.realpath(TEMP_DIR)) print("Removed temporary directory \"{}\"".format(TEMP_DIR)) - # Put z3py at the beginning of the search path to try to avoid picking up - # an installed copy of Z3py. - sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) - pydoc.writedoc('z3') - shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) - print("Generated Python documentation.") + if Z3PY_ENABLED: + # Put z3py at the beginning of the search path to try to avoid picking up + # an installed copy of Z3py. + sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) + pydoc.writedoc('z3') + shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) + print("Generated pydoc Z3Py documentation.") if ML_ENABLED: ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') diff --git a/doc/website.dox.in b/doc/website.dox.in index b00874c97..17a8552d1 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -10,10 +10,7 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref capi - - \ref cppapi - - .NET API - - Java API - - Python API (also available in pydoc format)@OCAML_API@ + - \ref capi + - \ref cppapi @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ - Try Z3 online at RiSE4Fun. */ diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index cb07045b3..408e981d2 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -681,10 +681,9 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = ../src/api/dotnet \ - ../src/api/java \ +INPUT = @TEMP_DIR@ \ ../src/api/c++ \ - @TEMP_DIR@ + @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is @@ -710,9 +709,7 @@ FILE_PATTERNS = website.dox \ z3_interp.h \ z3_fpa.h \ z3++.h \ - z3py.py \ - *.cs \ - *.java + @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@ # The RECURSIVE tag can be used to turn specify whether or not subdirectories # should be searched for input files as well. Possible values are YES and NO. From 09d7ebf1adcc3a4dfea3125f126f7a27a059797e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:17:21 +0100 Subject: [PATCH 16/20] [Doxygen] Fix bug where temporary directory and output directory paths were not handled properly if paths contained spaces. --- doc/z3api.cfg.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 408e981d2..7ccad3fbb 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -52,7 +52,7 @@ PROJECT_LOGO = # If a relative path is entered, it will be relative to the location # where doxygen was started. If left blank the current directory will be used. -OUTPUT_DIRECTORY = @OUTPUT_DIRECTORY@ +OUTPUT_DIRECTORY = "@OUTPUT_DIRECTORY@" # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create # 4096 sub-directories (in 2 levels) under the output directory of each output @@ -681,7 +681,7 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = @TEMP_DIR@ \ +INPUT = "@TEMP_DIR@" \ ../src/api/c++ \ @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ From e4bec1572aa404298abbacf7693e3f37e7453d04 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:36:48 +0100 Subject: [PATCH 17/20] [Doxygen] Teach `mk_api_doc.py` to allow multiple search paths for the ".NET" and "Java" bindings. The CMake build system needs this because the generated files exist in a different directory to the source files. Multiple paths can be specified using the `--dot-search-paths` and `--java-search-paths` options. --- doc/mk_api_doc.py | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index b61036d44..e331c60b9 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -22,10 +22,13 @@ Z3PY_PACKAGE_PATH='../src/api/python/z3' Z3PY_ENABLED=True DOTNET_ENABLED=True JAVA_ENABLED=True +DOTNET_API_SEARCH_PATHS=['../src/api/dotnet'] +JAVA_API_SEARCH_PATHS=['../src/api/java'] def parse_options(): global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED + global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -80,6 +83,18 @@ def parse_options(): default=False, help='Do not generate documentation for Java bindings', ) + parser.add_argument('--dotnet-search-paths', + dest='dotnet_search_paths', + nargs='+', + default=DOTNET_API_SEARCH_PATHS, + help='Specify one or more path to look for .NET files (default: %(default)s).', + ) + parser.add_argument('--java-search-paths', + dest='java_search_paths', + nargs='+', + default=JAVA_API_SEARCH_PATHS, + help='Specify one or more paths to look for Java files (default: %(default)s).', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml BUILD_DIR = pargs.build @@ -94,6 +109,8 @@ def parse_options(): Z3PY_ENABLED = not pargs.no_z3py DOTNET_ENABLED = not pargs.no_dotnet JAVA_ENABLED = not pargs.no_java + DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths + JAVA_API_SEARCH_PATHS = pargs.java_search_paths return def mk_dir(d): @@ -171,7 +188,11 @@ try: if DOTNET_ENABLED: print(".NET documentation enabled") doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs' - doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '../src/api/dotnet' + dotnet_api_search_path_str = "" + for p in DOTNET_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + dotnet_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = dotnet_api_search_path_str else: print(".NET documentation disabled") doxygen_config_substitutions['DOTNET_API_FILES'] = '' @@ -179,7 +200,11 @@ try: if JAVA_ENABLED: print("Java documentation enabled") doxygen_config_substitutions['JAVA_API_FILES'] = '*.java' - doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '../src/api/java' + java_api_search_path_str = "" + for p in JAVA_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + java_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = java_api_search_path_str else: print("Java documentation disabled") doxygen_config_substitutions['JAVA_API_FILES'] = '' From 121fd06cc2f3dec7fd2412815b9340e8dbfb90c0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 14:36:02 +0100 Subject: [PATCH 18/20] [Doxygen] Fix `mk_api_doc.py` so it is not required that the current working directory be the `doc` directory in the source tree. --- doc/mk_api_doc.py | 39 +++++++++++++++++++++++++-------------- doc/z3api.cfg.in | 2 +- 2 files changed, 26 insertions(+), 15 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index e331c60b9..6007b77c4 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -24,6 +24,7 @@ DOTNET_ENABLED=True JAVA_ENABLED=True DOTNET_API_SEARCH_PATHS=['../src/api/dotnet'] JAVA_API_SEARCH_PATHS=['../src/api/java'] +SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__)) def parse_options(): global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY @@ -172,11 +173,15 @@ try: # Short-hand for path to temporary file def temp_path(path): return os.path.join(TEMP_DIR, path) + # Short-hand for path to file in `doc` directory + def doc_path(path): + return os.path.join(SCRIPT_DIR, path) # Create configuration file from template doxygen_config_substitutions = { 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, - 'TEMP_DIR': TEMP_DIR + 'TEMP_DIR': TEMP_DIR, + 'CXX_API_SEARCH_PATHS': doc_path('../src/api/c++'), } if Z3PY_ENABLED: @@ -211,7 +216,10 @@ try: doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '' doxygen_config_file = temp_path('z3api.cfg') - configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) + configure_file( + doc_path('z3api.cfg.in'), + doxygen_config_file, + doxygen_config_substitutions) website_dox_substitutions = {} bullet_point_prefix='\n - ' @@ -245,20 +253,23 @@ try: prefix=bullet_point_prefix) else: website_dox_substitutions['OCAML_API'] = '' - configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) + configure_file( + doc_path('website.dox.in'), + temp_path('website.dox'), + website_dox_substitutions) mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) if Z3PY_ENABLED: - 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')) + shutil.copyfile(doc_path('../src/api/python/z3/z3.py'), temp_path('z3py.py')) + cleanup_API(doc_path('../src/api/z3_api.h'), temp_path('z3_api.h')) + cleanup_API(doc_path('../src/api/z3_ast_containers.h'), temp_path('z3_ast_containers.h')) + cleanup_API(doc_path('../src/api/z3_algebraic.h'), temp_path('z3_algebraic.h')) + cleanup_API(doc_path('../src/api/z3_polynomial.h'), temp_path('z3_polynomial.h')) + cleanup_API(doc_path('../src/api/z3_rcf.h'), temp_path('z3_rcf.h')) + cleanup_API(doc_path('../src/api/z3_fixedpoint.h'), temp_path('z3_fixedpoint.h')) + cleanup_API(doc_path('../src/api/z3_optimization.h'), temp_path('z3_optimization.h')) + cleanup_API(doc_path('../src/api/z3_interp.h'), temp_path('z3_interp.h')) + cleanup_API(doc_path('../src/api/z3_fpa.h'), temp_path('z3_fpa.h')) print("Removed annotations from z3_api.h.") try: @@ -282,7 +293,7 @@ try: if ML_ENABLED: ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') mk_dir(ml_output_dir) - if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../src/api/ml/z3.mli']) != 0: + if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0: print("ERROR: ocamldoc failed.") exit(1) print("Generated ML/OCaml documentation.") diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 7ccad3fbb..9e946aa7f 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -682,7 +682,7 @@ WARN_LOGFILE = # with spaces. INPUT = "@TEMP_DIR@" \ - ../src/api/c++ \ + "@CXX_API_SEARCH_PATHS@" \ @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ # This tag can be used to specify the character encoding of the source files From a6a6a9c29f96c63eec7d5efef6860553d366be21 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 15:43:03 +0100 Subject: [PATCH 19/20] [Doxygen] Fix link to ".NET" documentation it should point to the "Microsoft.Z3" namespace, not the "Microsoft.Z3.Context" class. This mirrors the link provided for the Java API. --- doc/mk_api_doc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 6007b77c4..014a152b4 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -234,7 +234,7 @@ try: if DOTNET_ENABLED: website_dox_substitutions['DOTNET_API'] = ( '{prefix}' - '' + '' '.NET API').format( prefix=bullet_point_prefix) else: From d4b7b489d072daaf268ee15f3f1517c4388cf8b3 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 14:16:14 +0100 Subject: [PATCH 20/20] [CMake] Teach CMake to build the documentation for the API bindings and install them. The target for building the documentation is `api_docs`. This is off by default but can be enabled with the `BUILD_DOCUMENTATION` option. The C and C++ API documentation is always built but the Python, ".NET", and Java documentation are only built if they are enabled in the build system. The rationale for this is that it would be confusing to install documentation for API bindings that are not installed. By default `ALWAYS_BUILD_DOCS` is on which will slow down builds significantly but will ensure that when the `install` target is invoked the documentation is up-to-date. Unfortunately I couldn't find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled to get faster builds and still have the `api_docs` target available. --- CMakeLists.txt | 16 +++++- README-CMake.md | 7 +++ contrib/cmake/doc/CMakeLists.txt | 93 ++++++++++++++++++++++++++++++++ 3 files changed, 115 insertions(+), 1 deletion(-) create mode 100644 contrib/cmake/doc/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index cf46e7012..47a081e75 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -43,10 +43,13 @@ message(STATUS "Z3 version ${Z3_VERSION}") # Set various useful variables depending on CMake version ################################################################################ if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2")) - # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument + # In CMake >= 3.2 add_custom_command() and add_custom_target() + # supports a ``USES_TERMINAL`` argument set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL") + set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "USES_TERMINAL") else() set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "") + set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "") endif() ################################################################################ @@ -528,3 +531,14 @@ option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON) if (ENABLE_EXAMPLE_TARGETS) add_subdirectory(examples) endif() + +################################################################################ +# Documentation +################################################################################ +option(BUILD_DOCUMENTATION "Build API documentation" OFF) +if (BUILD_DOCUMENTATION) + message(STATUS "Building documentation enabled") + add_subdirectory(doc) +else() + message(STATUS "Building documentation disabled") +endif() diff --git a/README-CMake.md b/README-CMake.md index 6a78b5d4c..4bbbd36a8 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -268,6 +268,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files. * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. * ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``). +* ``CMAKE_INSTALL_API_BINDINGS_DOC`` - STRING. The path to install documentation for API bindings. * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. @@ -286,6 +287,11 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. * ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. +* ``BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. +* ``INSTALL_API_BINDINGS_DOCUMENTATION`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION` is ``TRUE`` then documentation for API bindings will be installed + when running the ``install`` target. +* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built. + Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. @@ -417,6 +423,7 @@ There are a few special targets: * ``clean`` all the built targets in the current directory and below * ``edit_cache`` will invoke one of the CMake tools (depending on which is available) to let you change configuration options. * ``rebuild_cache`` will reinvoke ``cmake`` for the project. +* ``api_docs`` will build the documentation for the API bindings. ### Setting build type specific flags diff --git a/contrib/cmake/doc/CMakeLists.txt b/contrib/cmake/doc/CMakeLists.txt new file mode 100644 index 000000000..86e208ab1 --- /dev/null +++ b/contrib/cmake/doc/CMakeLists.txt @@ -0,0 +1,93 @@ +find_package(Doxygen REQUIRED) +message(STATUS "DOXYGEN_EXECUTABLE: \"${DOXYGEN_EXECUTABLE}\"") +message(STATUS "DOXYGEN_VERSION: \"${DOXYGEN_VERSION}\"") + +set(DOC_DEST_DIR "${CMAKE_CURRENT_BINARY_DIR}/api") +set(DOC_TEMP_DIR "${CMAKE_CURRENT_BINARY_DIR}/temp") +set(MK_API_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_api_doc.py") + +set(PYTHON_API_OPTIONS "") +set(DOTNET_API_OPTIONS "") +set(JAVA_API_OPTIONS "") +SET(DOC_EXTRA_DEPENDS "") + +if (BUILD_PYTHON_BINDINGS) + # FIXME: Don't hard code this path + list(APPEND PYTHON_API_OPTIONS "--z3py-package-path" "${CMAKE_BINARY_DIR}/python/z3") + list(APPEND DOC_EXTRA_DEPENDS "build_z3_python_bindings") +else() + list(APPEND PYTHON_API_OPTIONS "--no-z3py") +endif() + +if (BUILD_DOTNET_BINDINGS) + # FIXME: Don't hard code these paths + list(APPEND DOTNET_API_OPTIONS "--dotnet-search-paths" + "${CMAKE_SOURCE_DIR}/src/api/dotnet" + "${CMAKE_BINARY_DIR}/src/api/dotnet" + ) + list(APPEND DOC_EXTRA_DEPENDS "build_z3_dotnet_bindings") +else() + list(APPEND DOTNET_API_OPTIONS "--no-dotnet") +endif() + +if (BUILD_JAVA_BINDINGS) + # FIXME: Don't hard code these paths + list(APPEND JAVA_API_OPTIONS "--java-search-paths" + "${CMAKE_SOURCE_DIR}/src/api/java" + "${CMAKE_BINARY_DIR}/src/api/java" + ) + list(APPEND DOC_EXTRA_DEPENDS "build_z3_java_bindings") +else() + list(APPEND JAVA_API_OPTIONS "--no-java") +endif() + +option(ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON) +if (ALWAYS_BUILD_DOCS) + set(ALWAYS_BUILD_DOCS_ARG "ALL") +else() + set(ALWAYS_BUILD_DOCS_ARG "") + # FIXME: This sucks but there doesn't seem to be a way to make the top level + # install target depend on the `api_docs` target. + message(WARNING "Building documentation for API bindings is not part of the" + " all target. This may result in stale files being installed when running" + " the install target. You should run the api_docs target before running" + " the install target. Alternatively Set ALWAYS_BUILD_DOCS to ON to" + " automatically build documentation when running the install target." + ) +endif() + +add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG} + COMMAND + "${PYTHON_EXECUTABLE}" "${MK_API_DOC_SCRIPT}" + --doxygen-executable "${DOXYGEN_EXECUTABLE}" + --output-dir "${DOC_DEST_DIR}" + --temp-dir "${DOC_TEMP_DIR}" + ${PYTHON_API_OPTIONS} + ${DOTNET_API_OPTIONS} + ${JAVA_API_OPTIONS} + DEPENDS + ${DOC_EXTRA_DEPENDS} + BYPRODUCTS "${DOC_DEST_DIR}" + COMMENT "Generating documentation" + ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG} +) + +# Remove generated documentation when running `clean` target. +set_property(DIRECTORY APPEND PROPERTY + ADDITIONAL_MAKE_CLEAN_FILES + "${DOC_DEST_DIR}" +) + +option(INSTALL_API_BINDINGS_DOCUMENTATION "Install documentation for API bindings" ON) +set(CMAKE_INSTALL_API_BINDINGS_DOC + "${CMAKE_INSTALL_DOCDIR}" + CACHE + PATH + "Path to install documentation for API bindings" +) +if (INSTALL_API_BINDINGS_DOCUMENTATION) + install( + DIRECTORY "${DOC_DEST_DIR}" + DESTINATION "${CMAKE_INSTALL_API_BINDINGS_DOC}" + ) +endif()