From 68247aa58f2c736eedc9f5eff62a48d25c601d19 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:01:27 +0000 Subject: [PATCH 1/8] Convert README to markdown --- README | 53 ----------------------------------------- README.md | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 53 deletions(-) delete mode 100644 README create mode 100644 README.md diff --git a/README b/README deleted file mode 100644 index 22fc58c7a..000000000 --- a/README +++ /dev/null @@ -1,53 +0,0 @@ -Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under the MIT license. -Z3 can be built using Visual Studio Command Prompt and make/g++. - -1) Building Z3 on Windows using Visual Studio Command Prompt - -32-bit builds, start with: - - python scripts/mk_make.py - -or instead, for a 64-bit build: - - python scripts/mk_make.py -x - -then: - - cd build - nmake - -2) Building Z3 using make/g++ and Python -Execute: - - python scripts/mk_make.py - cd build - make - sudo make install - -By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, -where PREFIX is the installation prefix used for installing Python in your system. -It is usually /usr for most Linux distros, and /usr/local for FreeBSD. -Use the following commands to install in a different prefix (e.g., /home/leo) - - python scripts/mk_make.py --prefix=/home/leo - cd build - make - make install - -In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages, -where X.Y corresponds to the python version in your system. - -To uninstall Z3, use - - sudo make uninstall - -4) Building Z3 using clang and clang++ on Linux/OSX -Remark: clang does not support OpenMP yet. - - CXX=clang++ CC=clang python scripts/mk_make.py - cd build - make - - -To clean Z3 you can delete the build directory and run the mk_make.py script again. diff --git a/README.md b/README.md new file mode 100644 index 000000000..4688e3d01 --- /dev/null +++ b/README.md @@ -0,0 +1,71 @@ +# Z3 + +Z3 is a theorem prover from Microsoft Research. +Z3 is licensed under the MIT license. +Z3 can be built using Visual Studio Command Prompt and make/g++. + +## Building Z3 on Windows using Visual Studio Command Prompt + +32-bit builds, start with: + +```bash + python scripts/mk_make.py +``` + +or instead, for a 64-bit build: + +```bash + python scripts/mk_make.py -x +``` + +then: + +```bash + cd build + nmake +``` + +## Building Z3 using make/g++ and Python + +Execute: + +```bash + python scripts/mk_make.py + cd build + make + sudo make install +``` + +By default, it will install z3 executable at ``PREFIX/bin``, libraries at +``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` +installation prefix used for installing Python in your system. + +It is usually ``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD. +Use the following commands to install in a different prefix (e.g., /home/leo) + +```bash + python scripts/mk_make.py --prefix=/home/leo + cd build + make + make install +``` + +In this example, the Z3 Python bindings will be stored at ``/home/leo/lib/pythonX.Y/dist-packages``, +where X.Y corresponds to the python version in your system. + +To uninstall Z3, use + +```bash + sudo make uninstall +``` + +## Building Z3 using clang and clang++ on Linux/OSX +Remark: clang does not support OpenMP yet. + +```bash + CXX=clang++ CC=clang python scripts/mk_make.py + cd build + make +``` + +To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. From 08610ae243804b0ee22237b7ee0ca53b24ec82d5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:06:10 +0000 Subject: [PATCH 2/8] Correct incorrect information on what ``PREFIX`` is in ``README.md``. It isn't always the root of the Python install. --- README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 4688e3d01..0795c2a40 100644 --- a/README.md +++ b/README.md @@ -38,10 +38,9 @@ Execute: By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` -installation prefix used for installing Python in your system. - -It is usually ``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD. -Use the following commands to install in a different prefix (e.g., /home/leo) +installation prefix if inferred by the ``mk_make.py`` script. It is usually +``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use +the ``--prefix=`` command line option to change the install prefix. For example: ```bash python scripts/mk_make.py --prefix=/home/leo From f09fa3c87b1853f26e4dde2bae4b531a204f431b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:22:56 +0000 Subject: [PATCH 3/8] Recent changes to the build system mean that setting a custom ``--prefix=`` is likely to disable installing the Python bindings so the old instructions aren't helpful. Reword them and mention using ``DESTDIR``. --- README.md | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 0795c2a40..a731a452d 100644 --- a/README.md +++ b/README.md @@ -49,8 +49,30 @@ the ``--prefix=`` command line option to change the install prefix. For example: make install ``` -In this example, the Z3 Python bindings will be stored at ``/home/leo/lib/pythonX.Y/dist-packages``, -where X.Y corresponds to the python version in your system. +Note the above will typically disable the installation of the Python bindings +because the Python ``site-packages`` directory (e.g. +``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and +installing outside of the install prefix is dangerous and misleading. + +To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the +install prefix as the default. The ``DESTDIR`` variable is prepended to the +install locations during ``make install`` and ``make uninstall`` and is intended +to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html). +Therefore it must always contain a trailing slash. + +For example: + +```bash + python scripts/mk_make.py + cd build + make + make install DESTDIR=/home/leo/ +``` + +In this example, the Z3 Python bindings will be stored at +``/home/leo/lib/pythonX.Y/site-packages`` +(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux +distributions) where X.Y corresponds to the python version in your system. To uninstall Z3, use From 2bd9bbafe4eb56f03b67af8918ba371b8453e119 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:31:12 +0000 Subject: [PATCH 4/8] Re-organise the discussion of Clang, it is not a second class citizen and so doesn't deserve to be stuck at the end of the README. It also **does** support OpenMP! --- README.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index a731a452d..f4153b21d 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ then: nmake ``` -## Building Z3 using make/g++ and Python +## Building Z3 using make and GCC/Clang Execute: @@ -36,6 +36,15 @@ Execute: sudo make install ``` +Note by default ``gcc`` is used as the C++ compiler if it is available. If you +would prefer to use Clang change the ``mk_make.py`` line to + +```bash + CXX=clang++ CC=clang python scripts/mk_make.py +``` + +Note that Clang < 3.7 does not support OpenMP. + By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix if inferred by the ``mk_make.py`` script. It is usually @@ -80,13 +89,4 @@ To uninstall Z3, use sudo make uninstall ``` -## Building Z3 using clang and clang++ on Linux/OSX -Remark: clang does not support OpenMP yet. - -```bash - CXX=clang++ CC=clang python scripts/mk_make.py - cd build - make -``` - To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. From 2947893e109f903f2e36ec4e6e9e7f90f86cada4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:04:12 +0000 Subject: [PATCH 5/8] Partially document the Z3 bindings in ``README.md`` --- README.md | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/README.md b/README.md index f4153b21d..c757dee30 100644 --- a/README.md +++ b/README.md @@ -90,3 +90,64 @@ To uninstall Z3, use ``` To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. + +## Z3 bindings + +Z3 has bindings for various programming languages. + +### ``.NET`` + +These bindings are enabled by default on Windows and are enabled on other +platforms if [mono](http://www.mono-project.com/) is detected. On these +platforms the location of the C# compiler and gac utility need to be known. You +can set these as follows if they aren't detected automatically. For example: + +```bash + CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +``` + +To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. + +Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC`` +to ``/usr/bin/dmcs``. + +Note that when ``make install`` is executed on non-windows platforms the GAC +utility is used to install ``Microsoft.Z3.dll`` into the +[GAC](http://www.mono-project.com/docs/advanced/assemblies-and-the-gac/) as the +``Microsoft.Z3.Sharp`` package. During install a +[pkg-config](http://www.freedesktop.org/wiki/Software/pkg-config/) file +(``Microsoft.Z3.Sharp.pc``) is also installed which allows the +[MonoDevelop](http://www.monodevelop.com/) IDE to find the bindings. Running +``make uninstall`` will remove the dll from the GAC and the pkg-config file. + +See [``examples/dotnet``](examples/dotnet) for examples. + +### ``C`` + +These are always enabled. + +See [``examples/c``](examples/c) for examples. + +### ``C++`` + +These are always enabled. + +See [``examples/c++``](examples/c++) for examples. + +### ``Java`` + +Use the ``--java`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/java``](examples/java) for examples. + +### ``OCaml`` + +Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/ml``](examples/ml) for examples. + +### ``Python`` + +These bindings are always enabled. + +See [``examples/python``](examples/python) for examples. From 560810ee6778d85792e2ac3ab6cc925d15a0ce0c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:33:32 +0000 Subject: [PATCH 6/8] Fix command line indent in ``README.md`` --- README.md | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index c757dee30..46a39134b 100644 --- a/README.md +++ b/README.md @@ -9,20 +9,20 @@ Z3 can be built using Visual Studio Command Prompt and make/g++. 32-bit builds, start with: ```bash - python scripts/mk_make.py +python scripts/mk_make.py ``` or instead, for a 64-bit build: ```bash - python scripts/mk_make.py -x +python scripts/mk_make.py -x ``` then: ```bash - cd build - nmake +cd build +nmake ``` ## Building Z3 using make and GCC/Clang @@ -30,17 +30,17 @@ then: Execute: ```bash - python scripts/mk_make.py - cd build - make - sudo make install +python scripts/mk_make.py +cd build +make +sudo make install ``` Note by default ``gcc`` is used as the C++ compiler if it is available. If you would prefer to use Clang change the ``mk_make.py`` line to ```bash - CXX=clang++ CC=clang python scripts/mk_make.py +CXX=clang++ CC=clang python scripts/mk_make.py ``` Note that Clang < 3.7 does not support OpenMP. @@ -52,10 +52,10 @@ installation prefix if inferred by the ``mk_make.py`` script. It is usually the ``--prefix=`` command line option to change the install prefix. For example: ```bash - python scripts/mk_make.py --prefix=/home/leo - cd build - make - make install +python scripts/mk_make.py --prefix=/home/leo +cd build +make +make install ``` Note the above will typically disable the installation of the Python bindings @@ -72,10 +72,10 @@ Therefore it must always contain a trailing slash. For example: ```bash - python scripts/mk_make.py - cd build - make - make install DESTDIR=/home/leo/ +python scripts/mk_make.py +cd build +make +make install DESTDIR=/home/leo/ ``` In this example, the Z3 Python bindings will be stored at @@ -86,7 +86,7 @@ distributions) where X.Y corresponds to the python version in your system. To uninstall Z3, use ```bash - sudo make uninstall +sudo make uninstall ``` To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. @@ -103,7 +103,7 @@ platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example: ```bash - CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py ``` To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. From b4dd5d3d08f309ff2d90a8abbb09bc019af95b7e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:46:02 +0000 Subject: [PATCH 7/8] Rewrite intro text in ``README.md``. --- README.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 46a39134b..9ca373f87 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,14 @@ # Z3 -Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under the MIT license. -Z3 can be built using Visual Studio Command Prompt and make/g++. +Z3 is a theorem prover from Microsoft Research. It is licensed +under the [MIT license](LICENSE.txt). + +Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides +[bindings for several programming languages][3]. + +[1]: #building-z3-on-windows-using-visual-studio-command-prompt +[2]: #building-z3-using-make-and-gccclang +[3]: #z3-bindings ## Building Z3 on Windows using Visual Studio Command Prompt From f9687e780aa6653e1a0c4eb5521c4c6a1b6f7f18 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:50:38 +0000 Subject: [PATCH 8/8] Link to the release notes in ``README.md`` --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 9ca373f87..7d2fc5a24 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,8 @@ under the [MIT license](LICENSE.txt). Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides [bindings for several programming languages][3]. +See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. + [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #z3-bindings