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 diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 08ff771e7..88d7d7246 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' @@ -454,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";;') @@ -2357,7 +2362,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 +2390,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): @@ -3172,6 +3179,9 @@ def mk_bindings(api_files): if is_dotnet_enabled(): check_dotnet() mk_z3consts_dotnet(api_files) + if is_dotnet_core_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): @@ -3190,6 +3200,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)