3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Commit graph

590 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
06deb07a49 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-17 12:47:34 +00:00
Christoph M. Wintersteiger
0fe1e3248f .NET build fix 2015-12-17 12:47:24 +00:00
Christoph M. Wintersteiger
1cc2385fd2 typo 2015-12-17 12:33:45 +00:00
Christoph M. Wintersteiger
90b1b07af4 build fixes 2015-12-15 15:03:53 +00:00
Christoph M. Wintersteiger
22a77721ef Updated build options for .NET API 2015-12-15 14:20:31 +00:00
Christoph M. Wintersteiger
f4e3989766 .NET API build fixes 2015-12-15 13:09:02 +00:00
Christoph M. Wintersteiger
942b6ba5ec Updated .NET build. 2015-12-15 12:24:59 +00:00
Christoph M. Wintersteiger
fc5b9156cf Merge pull request #363 from delcypher/dotnet_configure_assembly_info
Refactor ``mk_all_assembly_infos()`` to use the ``configure_file()`` and misc fixes for dotnet bindings
2015-12-15 11:35:14 +00:00
Dan Liew
439d8d8afe Fix issue on non-windows systems when emitting the build rule
for the ".NET" bindings example.

Previously there was a hack that would to path separator replacement
( '/' -> '\' ) which breaks paths under non-windows platforms. The hack
has been made slightly better by doing ( '/' -> os.path.sep). This
preserves the existing behaviour under Windows and unbreaks the build
on non-windows platforms.

I'm not entirely sure why the path replacement needs to be done in
the first place. I thought Windows was supposed to support using
'/' as a path separator (as well as '/'). Maybe ``csc.exe`` doesn't
support these kind of paths?
2015-12-15 08:56:47 +00:00
Dan Liew
44393b37de Emit dependency of phony target `examples on _ex_dotnet_example`
when building of the ".NET" bindings is enabled.
2015-12-15 08:46:47 +00:00
Christoph M. Wintersteiger
edb1f4d896 ML API build fix 2015-12-14 14:55:38 +00:00
Christoph M. Wintersteiger
134b93b43e ML API build fixes for Windows. 2015-12-14 14:41:19 +00:00
Dan Liew
d3d10490ea Fix bug in `Makefile` generation when emitting the command to build
the ".NET" bindings when in debug mode.

``;`` is a shell command separator so it needs to be quoted when
emitting ``/define:DEBUG;TRACE``.
2015-12-14 09:56:03 +00:00
Dan Liew
81c98cf3ee Refactor `mk_all_assembly_infos() to use the configure_file()`
function. The old implementation was buggy under Python 3.5 and
unsafe (not using with statements on calls to ``open()``).
2015-12-14 09:51:45 +00:00
Christoph M. Wintersteiger
5a357097c0 ML API Windows build fixes 2015-12-12 20:01:52 +00:00
Christoph M. Wintersteiger
d456400f93 Merge branch 'new_ocaml_install' of https://github.com/wintersteiger/z3 into new_ocaml_install 2015-12-12 19:34:02 +00:00
Christoph M. Wintersteiger
d5f79c1f17 build fix for ML API 2015-12-12 19:30:25 +00:00
Dan Liew
140b3de3aa Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 19:30:24 +00:00
Christoph M. Wintersteiger
325d516825 ocaml build fix 2015-12-12 19:30:22 +00:00
Christoph M. Wintersteiger
02f7ae4a4d updated ocaml build and installation 2015-12-12 19:30:22 +00:00
Dan Liew
948df47027 Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 09:34:50 +00:00
Christoph M. Wintersteiger
f164f17190 ocaml build fix 2015-12-11 20:01:55 +00:00
Christoph M. Wintersteiger
50f17e403c updated ocaml build and installation 2015-12-11 19:56:23 +00:00
Nikolaj Bjorner
8949790c16 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 07:37:51 -08:00
Nikolaj Bjorner
820fb10ef8 create .so impages for OpenBSD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 07:37:40 -08:00
Nikolaj Bjorner
d11022cf2d Merge pull request #362 from NikolajBjorner/master
Combined updates to seq, add openbsd cases to build script.
2015-12-09 07:30:51 -08:00
Christoph M. Wintersteiger
84291825e6 Resolved conflicts 2015-12-09 13:07:25 +00:00
Christoph M. Wintersteiger
a0f9f461f8 Build fix 2015-12-09 13:01:42 +00:00
Nikolaj Bjorner
aebdc8950a Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 00:40:36 -08:00
Dan Liew
0a1c645b5e Don't emit install commands and dependencies if ML bindings are
disabled!
2015-12-08 23:20:39 +00:00
Dan Liew
edf5ed27df Attempt to allow (but warn about) installation of Python bindings
under OSX when the Python ``site-packages`` directory doesn't live
under the install prefix. Also disallow installing under Windows
as it doesn't really make sense.
2015-12-08 23:10:48 +00:00
Dan Liew
d98d392aac Try unbreak OSX build when Python installation doesn't live under
PREFIX. In this case it is not safe to call ``strip_path_prefix()``
due to the assertion error it will raise.
2015-12-08 23:10:48 +00:00
Dan Liew
0a8cd3ae19 Refactor the install and uninstall commands for the python bindings
out of ``DLLComponent`` and into ``PythonInstallComponent`` where they
belong.
2015-12-08 23:10:48 +00:00
Dan Liew
38b45919b5 Unbreak running `make install. The python site-package` directory
was not created before trying to create files in it.

The ``install_deps()`` method was also dead. It looks like that
should have been named ``mk_install_deps()`` but even if we give it
the right name it does the wrong thing. That method is supposed
emit target names (i.e. dependencies) not commands.
2015-12-08 23:10:48 +00:00
Dan Liew
e2546d2b95 Refactor references to `pythonPkgDirWithoutPrefix` to a object
attribute.
2015-12-08 23:08:23 +00:00
Christoph M. Wintersteiger
83db19654f refactored ocamlfind_install target 2015-12-08 18:57:17 +00:00
Nikolaj Bjorner
895d032996 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 10:33:09 -08:00
Christoph M. Wintersteiger
ea79d0eacd Bugfix for Python installation on linuxes 2015-12-08 13:45:55 +00:00
Christoph M. Wintersteiger
f6a10b0b82 tabs 2015-12-07 19:28:04 +00:00
Nikolaj Bjorner
34a0d7dfed remove python_install target from all
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-07 09:59:46 -08:00
Nikolaj Bjorner
70b10d53cf fix build break - remove tabs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 22:17:36 -08:00
Nikolaj Bjorner
e1ab2370e1 fix python w.o. proper intallation, #338, #340
Signed-off-by: Nikolaj Bjorner <nbjorner@z3-mac.local>
2015-12-07 03:32:58 +00:00
Nikolaj Bjorner
92a4ac9eb7 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 19:28:39 -08:00
Nikolaj Bjorner
febd83912e make dotnet optional and recover from python installation mismatch. Pull requests #338, #340
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 19:25:18 -08:00
Nikolaj Bjorner
a940230301 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 19:14:53 -08:00
Nikolaj Bjorner
6c73c176b3 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 19:10:11 -08:00
Nikolaj Bjorner
b5fcbd7099 Merge branch 'mono_dotnet_bindings' of https://github.com/delcypher/z3-1 2015-12-06 13:51:43 -08:00
Nikolaj Bjorner
4ec6bc0825 Merge branch 'better_packaging' of https://github.com/delcypher/z3-1 2015-12-06 12:31:55 -08:00
Dan Liew
c8a2b6645a Teach the build system to generate and install a pkg-config file for the
".NET" bindings. This file is required for Monodevelop to find the
bindings because Monodevelop uses pkg-config to find packages
(it doesn't use the GAC).

For lack of a better name the GAC (and pkg-config) package name is now
``Microsoft.Z3.Sharp``. I don't want to call it ``Microsoft.Z3`` because
someone may want to create a ``Microsoft.Z3.pc`` file in the future for
the native Z3 library (i.e. C++ or C bindings).

In addition there is a new utility function ``configure_file()``
which reads a template file, applies some substitutions and writes
the result to another file. This very similar to what CMake does.

There is a new environment variable ``Z3_INSTALL_PKGCONFIG_DIR``
which allows pkgconfig directory to be controlled for the install.
2015-12-05 07:52:31 +00:00
Dan Liew
61d1cd524e Teach the build system to build and install the ".NET bindings"
under non Windows systems (i.e. Using mono).

Building these bindings is unfortunately on by default because
I didn't want to change the command line interface (i.e. ``--nodotnet``)
which people might be relying on. This should really be changed to
match the other binding flags (e.g. ``--java``) but I will leave
this for now.

To perform the build a C# compiler and the GAC utility are required.
The script will try to automatically detect them but the user can
override this by setting the ``CSC`` and ``GACUTIL`` environment
variables.

In order for the ".NET bindings" to be installed the assembly
(``Microsoft.Z3.dll``) needs to have a strong name which means
we need a Strong name key file which is what the
``Microsoft.Z3.mono.snk`` is for. This is the public and private
key so this key **must never** be used for checking integrity. Instead its
only purpose is to avoid any name clashes in the GAC.

It is also worth noting that slightly different flags needs to
be passed to the C# compiler on non Windows platforms. I don't
understand why some of the flags are being used on Windows but I left
a comment there that hopefully someone can fix...
2015-12-05 07:52:31 +00:00