From 139d8b85f018dc392f85af989af62a920e7c7e48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 11:43:41 -0800 Subject: [PATCH 1/9] core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 88d7d7246..6d3ad3d4b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,7 +456,9 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): - # TBD: check DOTNET + r = exec_cmd([DOTNET, '--help']) + if r != 0: + raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') pass def check_ml(): From 2501a875efcaa5d837601b40eafdcdeb7f351505 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 13:44:40 -0800 Subject: [PATCH 2/9] update script to generate file directly instead of from makefile Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 42 +++++++++++++++++++----------------------- 1 file changed, 19 insertions(+), 23 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 12ccc538c..63938caf9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2399,36 +2399,32 @@ class DotNetExampleComponent(ExampleComponent): out.write(' ') out.write(os.path.join(self.to_ex_dir, csfile)) - def mk_echo(msg, first = False): - echo_ex_qu = '' if IS_WINDOWS else '"' - echo_in_qu = '"' if IS_WINDOWS else '\\"' - echo_esc = '^' if IS_WINDOWS else '' - echo_dir = '>' if first else '>>' - - msg = msg.replace('"', echo_in_qu).replace('<', echo_esc + '<').replace('>', echo_esc + '>') - out.write('\t@echo %s%s%s %s %s\n' % (echo_ex_qu, msg, echo_ex_qu, echo_dir, proj_name)) - - out.write('\n') - mk_echo('', True) - mk_echo(' ') - mk_echo(' Exe') - mk_echo(' netcoreapp2.0') + proj_path = os.path.join(BUILD_DIR, proj_name) if VS_X64: platform = 'x64' elif VS_ARM: platform = 'ARM' else: platform = 'x86' - mk_echo(' %s' % platform) - mk_echo(' ') - mk_echo(' ') - mk_echo(' ' % self.to_ex_dir) - mk_echo(' ') - mk_echo(' Microsoft.Z3.dll') - mk_echo(' ') - mk_echo(' ') - mk_echo('') + dotnet_proj_str = """xemacs + + Exe + netcoreapp2.0 + %s + + + + + Microsoft.Z3.dll + + +""" % (platform, self.to_ex_dir) + + with open(proj_path, 'w') as ous: + ous.write(dotnet_proj_str) + + out.write('\n') dotnetCmdLine = [DOTNET, "build", proj_name] dotnetCmdLine.extend(['-c']) if DEBUG_MODE: From 690bd8502ab66ccae28a3d7538b7933930197e91 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Wed, 14 Nov 2018 13:47:46 -0800 Subject: [PATCH 3/9] Choose runtime for .NET core DLL. --- scripts/mk_util.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index aaeed1dea..c84b1c3a4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1888,6 +1888,15 @@ class DotNetCoreDLLComponent(Component): else: dotnetCmdLine.extend(['Release']) + if IS_WINDOWS: + runtime = "win-" + ("x64" if VS_X64 else "x86") + elif IS_LINUX: + runtime = "linux-x64" if LINUX_X64 else "" + elif IS_OSX: + runtime = "osx-x64" if LINUX_X64 else "" + if runtime != "": + dotnetCmdLine.extend(['-r', runtime]) + path = os.path.abspath(BUILD_DIR) dotnetCmdLine.extend(['-o', path]) From 1cc2cc01431e17e46be7b7bd89127dcbdd05e089 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:07:14 -0800 Subject: [PATCH 4/9] add TBD marker Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 63938caf9..be7132b75 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1839,6 +1839,7 @@ class DotNetCoreDLLComponent(Component): self.key_file = default_key_file def mk_pkg_config_file(self): + # TBD revise """ Create pkgconfig file for the dot net bindings. These are needed by Monodevelop. From c3725000182ef974e1e120c299adaa0377284dc9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:51:58 -0800 Subject: [PATCH 5/9] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 103 ++++++++++++++++++++++++++------------------- 1 file changed, 60 insertions(+), 43 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4037b3996..bd455b95e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -562,6 +562,11 @@ def set_version(major, minor, build, revision): def get_version(): return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) +def get_version_string(n): + if n == 3: + return "{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD) + return "{}.{}.{}.{}".format(VER_MAJOR,VER_MINOR,VER_BUILD,VER_REVISION) + def build_static_lib(): return STATIC_LIB @@ -1639,11 +1644,7 @@ class DotNetDLLComponent(Component): pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) substitutions = { 'PREFIX': PREFIX, 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) + 'VERSION': get_version_string(4) } pkg_config_output = os.path.join(BUILD_DIR, self.build_dir, @@ -1838,30 +1839,14 @@ class DotNetCoreDLLComponent(Component): self.assembly_info_dir = assembly_info_dir self.key_file = default_key_file - def mk_pkg_config_file(self): + def mk_nuget_config_file(self): # TBD revise """ - Create pkgconfig file for the dot net bindings. These + Create nuget file for the dot net bindings. These are needed by Monodevelop. """ - pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name())) - substitutions = { 'PREFIX': PREFIX, - 'GAC_PKG_NAME': self.gac_pkg_name(), - 'VERSION': "{}.{}.{}.{}".format( - VER_MAJOR, - VER_MINOR, - VER_BUILD, - VER_REVISION) - } - pkg_config_output = os.path.join(BUILD_DIR, - self.build_dir, - '{}.pc'.format(self.gac_pkg_name())) - - # FIXME: Why isn't the build directory available? - mk_dir(os.path.dirname(pkg_config_output)) - # Configure file that will be installed by ``make install``. - configure_file(pkg_config_template, pkg_config_output, substitutions) - + return + def mk_makefile(self, out): global DOTNET_KEY_FILE if not is_dotnet_core_enabled(): @@ -1879,26 +1864,55 @@ class DotNetCoreDLLComponent(Component): out.write(cs_file) out.write('\n') - csproj = os.path.join(self.to_src_dir, "core", "core.csproj") + if VS_X64: + platform = 'x64' + elif VS_ARM: + platform = 'ARM' + else: + platform = 'x86' + + version = get_version_string(3) + + core_csproj_str = """ + + + netcoreapp1.0 + %s + $(DefineConstants);DOTNET_CORE + portable + Microsoft.Z3 + Library + Microsoft.Z3 + $(PackageTargetFallback);dnxcore50 + 1.0.4 + %s + true + Microsoft + Microsoft + Z3 is a satisfiability modulo theories solver from Microsoft Research. + © Microsoft Corporation. All rights reserved. + smt constraint solver theorem prover + + + + + + +""" % (platform, version, self.to_src_dir) + + mk_dir(os.path.join(BUILD_DIR, 'dotnet')) + csproj = os.path.join('dotnet', 'z3.csproj') + with open(os.path.join(BUILD_DIR, csproj), 'w') as ous: + ous.write(core_csproj_str) + dotnetCmdLine = [DOTNET, "build", csproj] - # TBD: select build configurations also based on architecture - # Debug|x86, Debug|x64, Debug|arm - # Release|x86, Release|x64, Release|arm dotnetCmdLine.extend(['-c']) if DEBUG_MODE: dotnetCmdLine.extend(['Debug']) else: dotnetCmdLine.extend(['Release']) - if IS_WINDOWS: - runtime = "win-" + ("x64" if VS_X64 else "x86") - elif IS_LINUX: - runtime = "linux-x64" if LINUX_X64 else "" - elif IS_OSX: - runtime = "osx-x64" if LINUX_X64 else "" - if runtime != "": - dotnetCmdLine.extend(['-r', runtime]) path = os.path.abspath(BUILD_DIR) dotnetCmdLine.extend(['-o', path]) @@ -1911,8 +1925,8 @@ class DotNetCoreDLLComponent(Component): out.write('\n') out.write('%s: %s\n\n' % (self.name, dllfile)) - # Create pkg-config file - self.mk_pkg_config_file() + # Create nuget file + self.mk_nuget_config_file() return def main_component(self): @@ -1926,8 +1940,8 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) if DEBUG_MODE: shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) @@ -1937,8 +1951,8 @@ class DotNetCoreDLLComponent(Component): mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR)) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) - shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), - '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) + shutil.copy('%s.deps.json' % os.path.join(build_path, self.dll_name), + '%s.deps.json' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) def mk_install_deps(self, out): if not is_dotnet_core_enabled(): @@ -1949,6 +1963,7 @@ class DotNetCoreDLLComponent(Component): return "{}.Sharp".format(self.dll_name) def _install_or_uninstall_to_gac(self, out, install): + # TBD revise for nuget gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()), '/root', '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR) @@ -1967,6 +1982,7 @@ class DotNetCoreDLLComponent(Component): flags=' '.join(gacUtilFlags))) def mk_install(self, out): + # TBD revise for nuget if not is_dotnet_core_enabled(): return self._install_or_uninstall_to_gac(out, install=True) @@ -1978,6 +1994,7 @@ class DotNetCoreDLLComponent(Component): MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR) def mk_uninstall(self, out): + # TBD revise for nuget if not is_dotnet_core_enabled(): return self._install_or_uninstall_to_gac(out, install=False) From 13d1ccfeaf9463f73740a964a9ab0ee042897ee9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 14:59:53 -0800 Subject: [PATCH 6/9] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index bd455b95e..2662d0933 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1890,7 +1890,7 @@ class DotNetCoreDLLComponent(Component): Microsoft Microsoft Z3 is a satisfiability modulo theories solver from Microsoft Research. - © Microsoft Corporation. All rights reserved. + Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover From 4f4463b2b71e58268a57a127a8fb8b0204b4ab2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 15:06:24 -0800 Subject: [PATCH 7/9] update for nuget/core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 2662d0933..1ac9abd0f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,6 +456,8 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): + if not IS_WINDOWS: + return r = exec_cmd([DOTNET, '--help']) if r != 0: raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities') From c6c4dc456379aa5c9fdede19226686444e579292 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 16:57:47 -0800 Subject: [PATCH 8/9] start script on assembling platform binaries to wrap with nuget install Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_release.py | 62 +++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 scripts/mk_nuget_release.py diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py new file mode 100644 index 000000000..98a7c6362 --- /dev/null +++ b/scripts/mk_nuget_release.py @@ -0,0 +1,62 @@ +# +# Copyright (c) 2018 Microsoft Corporation +# + +# 1. download releases from github +# 2. copy over libz3.dll for the different architectures +# 3. copy over Microsoft.Z3.dll from suitable distribution +# 4. copy nuspec file from packages +# 5. call nuget pack + +import json +import os +import urllib.request +import zipfile +import sys +import os.path + +data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) + +version_str = data['tag_name'] + +def mk_dir(d): + if not os.path.exists(d): + os.makedirs(d) + +def download_installs(): + for asset in data['assets']: + url = asset['browser_download_url'] + name = asset['name'] + print("Downloading ", url) + sys.stdout.flush() + urllib.request.urlretrieve(url, "packages/%s" % name) + +os_names = ["ubuntu-14", "ubuntu-16", "win", "debian", "osx"] + +def unpack(): + for f in os.listdir("packages"): + if f.endswith("zip") and "x64" in f: + print(f) + # determine os from os_names + # instead of this string manipulation. + + name = os.path.splitext(f)[0] + os_name = name[name.find("x64")+4:] + os_name = os_name[:os_name.find("-")] + print(os_name) + + zip_ref = zipfile.ZipFile("packages/%s" % f, 'r') + path = "out/%s" % os_name + zip_ref.extract("%s/bin/libz3.so" % name) + + # unzip files in packages + pass + +def main(): + mk_dir("packages") +# download_installs() +# create_nuget_dir() + unpack() +# create_nuget_package() + +main() From 6a9c8a8999449439ec589ff9f6ee781151ee9d59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Nov 2018 19:40:56 -0800 Subject: [PATCH 9/9] remove spurious string Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1ac9abd0f..9c5b0c9a9 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2436,7 +2436,7 @@ class DotNetExampleComponent(ExampleComponent): else: platform = 'x86' - dotnet_proj_str = """xemacs + dotnet_proj_str = """ Exe netcoreapp2.0