From c59b331c1f4c960e444940c5effc1fdb1a4557cc Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Tue, 13 Nov 2018 12:19:20 -0800 Subject: [PATCH 1/6] Updated nuget package spec and directions --- package/Microsoft.Z3.x64.nuspec | 30 ++++++++++++++-------------- package/PackageCreationDirections.md | 6 ++---- 2 files changed, 17 insertions(+), 19 deletions(-) diff --git a/package/Microsoft.Z3.x64.nuspec b/package/Microsoft.Z3.x64.nuspec index 95d594dfb..506e5f9c7 100644 --- a/package/Microsoft.Z3.x64.nuspec +++ b/package/Microsoft.Z3.x64.nuspec @@ -3,20 +3,20 @@ Microsoft.Z3.x64 $(releaseVersion) - © Microsoft Corporation. All rights reserved. - Microsoft - Microsoft,Z3Prover - $(iconUrlFromReleaseCommit) - https://github.com/Z3Prover/z3 - $(licenseUrlFromReleaseCommit) - - true - Z3 is a constraint/SMT solver and theorem prover from Microsoft Research. - smt constraint solver theorem prover + © Microsoft Corporation. All rights reserved. + Microsoft + https://raw.githubusercontent.com/Z3Prover/z3/$(releaseCommitHash)/package/icon.jpg + https://github.com/Z3Prover/z3 + https://raw.githubusercontent.com/Z3Prover/z3/$(releaseCommitHash)/LICENSE.txt + + true + Z3 is a satisfiability modulo theories solver from Microsoft Research. + smt constraint solver theorem prover + en diff --git a/package/PackageCreationDirections.md b/package/PackageCreationDirections.md index 930ba14f7..6aaee5a1d 100644 --- a/package/PackageCreationDirections.md +++ b/package/PackageCreationDirections.md @@ -15,11 +15,9 @@ | +-- Microsoft.Z3.x64.targets | +-- libz3.dll ``` - 4. Open the nuspec file and fill in the appropriate macro values (note that for all URLs, preserve link integrity by linking to a specific commit): + 4. Open the nuspec file and fill in the appropriate macro values: * $(releaseVersion) - the Z3 version being released in this package - * $(iconUrlFromReleaseCommit) - URL for the Z3 icon file - * $(licenseUrlFromReleaseCommit) - URL for the Z3 repo license - * $(releaseCommitHash) - hash of the release commit + * $(releaseCommitHash) - hash of the release commit (there are several of these) 5. Run `nuget pack Microsoft.Z3.x64\Microsoft.Z3.x64.nuspec` 6. Test the resulting nupkg file (described below) then submit the package for signing before uploading to NuGet.org From 225fb82d9656b17b5c36266b05cc1b0ab051116e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Nov 2018 15:54:37 -0800 Subject: [PATCH 2/6] add TBD for dotnet example 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 08ff771e7..c73e1f1d1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2357,7 +2357,7 @@ class DotNetExampleComponent(ExampleComponent): ExampleComponent.__init__(self, name, path) def is_example(self): - return is_dotnet_enabled() + return is_dotnet_enabled() or is_dotnet_core_enabled() def mk_makefile(self, out): if is_dotnet_enabled(): @@ -2385,6 +2385,8 @@ class DotNetExampleComponent(ExampleComponent): out.write(os.path.join(relative_path, csfile)) out.write('\n') out.write('_ex_%s: %s\n\n' % (self.name, exefile)) + if is_dotnet_core_enabled(): + print("TBD: build script for dotnet_example on core") class JavaExampleComponent(ExampleComponent): def __init__(self, name, path): From bd78558826da01d612847c999866d20f1392742e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Nov 2018 19:51:57 -0800 Subject: [PATCH 3/6] adding dotnetcore handling Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index c73e1f1d1..01c1ea9a2 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -61,6 +61,7 @@ PATTERN_COMPONENT='pattern' UTIL_COMPONENT='util' API_COMPONENT='api' DOTNET_COMPONENT='dotnet' +DOTNET_CORE_COMPONENT='dotnetcore' JAVA_COMPONENT='java' ML_COMPONENT='ml' CPP_COMPONENT='cpp' @@ -3192,6 +3193,8 @@ def mk_z3consts_py(api_files): # Extract enumeration types from z3_api.h, and add .Net definitions def mk_z3consts_dotnet(api_files): dotnet = get_component(DOTNET_COMPONENT) + if not dotnet: + dotnet = get_component(DOTNET_CORE_COMPONENT) full_path_api_files = [] for api_file in api_files: api_file_c = dotnet.find_file(api_file, dotnet.name) From dbd5ef45261dc259d808864d06513b511f92eca4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Nov 2018 19:58:09 -0800 Subject: [PATCH 4/6] more dotnet core Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 01c1ea9a2..c0b2c5fc4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -455,6 +455,10 @@ def check_dotnet(): if r != 0: raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') +def check_dotnet_core(): + # TBD: check DOTNET + pass + def check_ml(): t = TempFile('hello.ml') t.add('print_string "Hello world!\n";;') @@ -3172,9 +3176,12 @@ def mk_bindings(api_files): if is_ml_enabled(): check_ml() mk_z3consts_ml(api_files) - if is_dotnet_enabled(): + if is_dotnet_enabled() check_dotnet() mk_z3consts_dotnet(api_files) + if is_dotnetcore_enabled(): + check_dotnet_core() + mk_z3consts_dotnet(api_files) # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): From 37ec933c664a9ce86be573bb63ad09ffc4a6adf2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Nov 2018 19:58:42 -0800 Subject: [PATCH 5/6] more dotnet 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 c0b2c5fc4..674e75f3c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3176,7 +3176,7 @@ def mk_bindings(api_files): if is_ml_enabled(): check_ml() mk_z3consts_ml(api_files) - if is_dotnet_enabled() + if is_dotnet_enabled(): check_dotnet() mk_z3consts_dotnet(api_files) if is_dotnetcore_enabled(): From ccf6ca310ed26137cbbd2fb133c7016601de6fdb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Nov 2018 19:59:46 -0800 Subject: [PATCH 6/6] more dotnet 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 674e75f3c..88d7d7246 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3179,7 +3179,7 @@ def mk_bindings(api_files): if is_dotnet_enabled(): check_dotnet() mk_z3consts_dotnet(api_files) - if is_dotnetcore_enabled(): + if is_dotnet_core_enabled(): check_dotnet_core() mk_z3consts_dotnet(api_files)