[WIP] Suggestion: build .NET package for both x86 and x64 and rename #5021

dsyme · 2021-02-11T15:19:30Z

The Z3 .NET package is 64-bit only, however I don't see any real reason why

This proposes to rename the package in the obvious way and include the x86 bits in the build:

Microsoft.Z3.x64 --> Microsoft.Z3

Advice welcome - in particular are you open to renaming the nuget package?

Apart from the rename the only change is removing this line: https://github.com/Z3Prover/z3/pull/5021/files#diff-56aeb133db14143ea8b4d74e24d17aafd198b6233d27676ed0ee951acf53062cL30. The comment in that line doesn't make any sense to me - the Microsoft.Z3.dll is already an AnyCPU DLL as far as I can see. However I don't yet understand whether the necessary x86 bits will be available when assembling the release package.

NikolajBjorner · 2021-02-11T17:29:28Z

The comments are likely stale
The naming Microsoft.Z3.X64 is because someone hijacked the Microsoft.Z3 nuget name and it wasn't available when I started publishing packages. This is maybe fixed now.
Nightly builds create packages. They are put in the "Nightly" github releases.
We can test this version by triggering nightly builds and check the created package

dsyme · 2021-02-11T19:01:15Z

Yay I contributed to Z3!! I'm so happy!!!!

NikolajBjorner · 2021-02-11T19:11:31Z

Hmm, if you are not careful I will start pestering you about how to organize the Azure pipelines and packaging issues. The stream of things to do is perpetual. Maybe more to the point, the .NET API could probably use some input. Having to cast arguments to the right types seems more like a nuisance than an advantage (a recent effort overhauled the Java API to leverage generics).

NikolajBjorner · 2021-02-11T19:13:13Z

Note also, that the Nightly build remains broken at this point so I have yet to produce the new Nuget to test.
There was an ubuntu update to the pipelines earlier this week and it roughed some feathers

NikolajBjorner · 2021-02-11T23:34:39Z

It finally completed. There were some recent regressions due to change in naming conventions.
Everything seems to be libgc now. Linux skew branding is gone. I am out of touch with what is going on in this area.

Could you try the following:

https://github.com/Z3Prover/z3/releases/download/Nightly/Microsoft.Z3.4.8.11.nupkg

dsyme · 2021-02-12T11:44:48Z

Hmmm THe Microsoft.Z3.dll is being labelled as a 64-bit PE file format. I'm not sure why, I didn't spot that in the build

E:\GitHub\dsyme\DiffSharp>corflags C:\Users\Administrator\.nuget\packages\microsoft.z3\4.8.11\lib\netstandard1.4\Microsoft.Z3.dll
Microsoft (R) .NET Framework CorFlags Conversion Tool.  Version  4.8.3928.0
Copyright (c) Microsoft Corporation.  All rights reserved.

Version   : v4.0.30319
CLR Header: 2.5
PE        : PE32+
CorFlags  : 0x9
ILONLY    : 1
32BITREQ  : 0
32BITPREF : 0
Signed    : 1

Here PE32+ means 64-bit https://stackoverflow.com/questions/4284351/whats-the-difference-between-pe32-and-pe32#:~:text=The%20PE32%20format%20stands%20for,Portable%20Executable%2064%2Dbit%20format.

This results in the expected warning:

Severity	Code	Description	Project	File	Line	Suppression State
Warning	MSB3270	There was a mismatch between the processor architecture of the project being built "x86" and the processor architecture of the reference "C:\Users\Administrator\.nuget\packages\microsoft.z3\4.8.11\lib\netstandard1.4\Microsoft.Z3.dll", "AMD64". This mismatch may cause runtime failures. Please consider changing the targeted processor architecture of your project through the Configuration Manager so as to align the processor architectures between your project and references, or take a dependency on references with a processor architecture that matches the targeted processor architecture of your project.	DiffSharp.Tools.ShapeAnalyzer	E:\Program Files (x86)\Microsoft Visual Studio\2019\Preview\MSBuild\Current\Bin\Microsoft.Common.CurrentVersion.targets	2181

dsyme · 2021-02-12T11:56:25Z

I can't work out where that 64-bitness is coming from in that package.

> corflags "C:\Users\Administrator\Downloads\Microsoft.Z3.4.8.11\lib\netstandard1.4\Microsoft.Z3.dll"
...
PE        : PE32+
...

Did that DLL get rebuilt in the nightly build package you linked above? Or is there something in the signing process?

When I do a local build it comes up as PE32

> python scripts/mk_make.py -x  --dotnet    
...
>dotnet build E:\GitHub\dsyme\z3\build\dotnet\z3.csproj
...
  z3 -> E:\GitHub\dsyme\z3\build\dotnet\bin\Debug\netstandard1.4\Microsoft.Z3.dll
...
>corflags  E:\GitHub\dsyme\z3\build\dotnet\bin\Debug\netstandard1.4\Microsoft.Z3.dll
...
PE        : PE32
...

dsyme · 2021-02-12T12:24:23Z

I see there's also a cmake build system, that might be setting 64-bitness, though I can't spot where.

Do you have end-to-end logs for the package construction?

NikolajBjorner · 2021-02-12T18:08:48Z

Microsoft.z3.dll is built by https://github.com/Z3Prover/z3/blob/master/scripts/mk_win_dist.py,
This uses an older script

z3/scripts/mk_util.py

Line 1623 in d0c96ab

class DotNetDLLComponent(Component):

to package the DLL
Furthermore "dotnet.exe" is invoked from a 64 bit VS environment and I copy only the managed dll from the 64bit build.
We can change this behavior by modifying packaging code here:

z3/scripts/mk_nuget_task.py

Line 67 in d0c96ab

if "x64-win" in f:

NikolajBjorner · 2021-02-12T18:12:25Z

The CMAKE build system is not used for the releases (it would be nicer if we could port everything to CMAKE, but I don't have the bandwidth nor skillsets to accomplish this so we are stuck with the python build which remains stable in spite of these dark corners).

NikolajBjorner · 2021-02-12T18:19:54Z

Did that DLL get rebuilt in the nightly build package you linked above?

Correct

NikolajBjorner · 2021-02-12T18:39:29Z

Looks like the VS build environment produces the setting

C:\z3n\build>dotnet build dotnet\z3.csproj
Microsoft (R) Build Engine version 16.8.3+39993bd9d for .NET
Copyright (C) Microsoft Corporation. All rights reserved.

  Determining projects to restore...
  Restored C:\z3n\build\dotnet\z3.csproj (in 751 ms).
  z3 -> C:\z3n\build\dotnet\bin\x64\Debug\netstandard1.4\Microsoft.Z3.dll
  Successfully created package 'C:\z3n\build\dotnet\bin\x64\Debug\Microsoft.Z3.4.8.11.nupkg'.

Build succeeded.
    0 Warning(s)
    0 Error(s)

Time Elapsed 00:00:03.83

C:\z3n\build>corflags dotnet\bin\x64\Debug\netstandard1.4\Microsoft.Z3.dll
Microsoft (R) .NET Framework CorFlags Conversion Tool.  Version  4.6.1055.0
Copyright (c) Microsoft Corporation.  All rights reserved.

Version   : v4.0.30319
CLR Header: 2.5
PE        : PE32+
CorFlags  : 0x9
ILONLY    : 1
32BITREQ  : 0
32BITPREF : 0
Signed    : 1

vs vsvarsall32.bat:

C:\z3n\build>dotnet build dotnet\z3.csproj
Microsoft (R) Build Engine version 16.8.3+39993bd9d for .NET
Copyright (C) Microsoft Corporation. All rights reserved.

  Determining projects to restore...
  Restored C:\z3n\build\dotnet\z3.csproj (in 763 ms).
  z3 -> C:\z3n\build\dotnet\bin\x86\Debug\netstandard1.4\Microsoft.Z3.dll
  Successfully created package 'C:\z3n\build\dotnet\bin\x86\Debug\Microsoft.Z3.4.8.11.nupkg'.

Build succeeded.
    0 Warning(s)
    0 Error(s)

Time Elapsed 00:00:03.77

C:\z3n\build>corflags dotnet\bin\x64\Debug\netstandard1.4\Microsoft.Z3.dll
Microsoft (R) .NET Framework CorFlags Conversion Tool.  Version  4.6.1055.0
Copyright (c) Microsoft Corporation.  All rights reserved.

corflags : error CF002 : Could not open file for reading

C:\z3n\build>corflags dotnet\bin\x86\Debug\netstandard1.4\Microsoft.Z3.dll
Microsoft (R) .NET Framework CorFlags Conversion Tool.  Version  4.6.1055.0
Copyright (c) Microsoft Corporation.  All rights reserved.

Version   : v4.0.30319
CLR Header: 2.5
PE        : PE32
CorFlags  : 0xb
ILONLY    : 1
32BITREQ  : 1
32BITPREF : 0
Signed    : 1

dsyme · 2021-02-12T20:27:43Z

Weird. I wonder why your build is producing "x86/x64-qualified" paths and mine isn't?

Yours:
z3 -> C:\z3n\build\dotnet\bin\x64\Debug\netstandard1.4\Microsoft.Z3.dll
z3 -> C:\z3n\build\dotnet\bin\x86\Debug\netstandard1.4\Microsoft.Z3.dll

Mine (no x64/x86)

z3 -> E:\GitHub\dsyme\z3\build\dotnet\bin\Debug\netstandard1.4\Microsoft.Z3.dll

Could you list the dotnet\z3.csproj file? And how that was generated? I used python scripts/mk_make.py -x --dotnet afresh

NikolajBjorner · 2021-02-12T20:29:47Z

Yes, I used python scripts/mk_make.py -x --dotnet afresh from a VS2017 prompt. Will now try VS2019

dsyme · 2021-02-12T20:29:48Z

BTW I am building from environment produced by VsDevCmd.bat

C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\Common7\Tools\VsDevCmd.bat"

Will check vsvarsall32.bat

It could maybe be an environment variable difference in these environments (i.e. something we don't want set at all)

NikolajBjorner · 2021-02-12T20:38:47Z

It makes a difference: vsdevcmd produces PE without the +.

NikolajBjorner · 2021-02-12T20:40:27Z

It could imply that we need to change this pre-historic beauty:

def mk_z3(x64):
    cmds = []
    if x64:
        cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
        cmds.append('cd %s' % BUILD_X64_DIR)
    else:
        cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86')
        cmds.append('cd %s' % BUILD_X86_DIR)
    cmds.append('nmake')
    if exec_cmds(cmds) != 0:
        raise MKException("Failed to make z3, x64: %s" % x64)

to some other obscure invocation

dsyme · 2021-02-12T21:19:54Z

Those environments set

__DOTNET_ADD_64BIT=1
__DOTNET_PREFERRED_BITNESS=64

and

__DOTNET_ADD_32BIT=1
__DOTNET_PREFERRED_BITNESS=64

I think nuke both of these after the scripts are run (or perhaps clean them in the project file)

Or else use VsDevCmd.bat to set up the environment to build managed code.

NikolajBjorner · 2021-02-12T21:23:17Z

VsDevCmd.bat seems the way to go, but it would need to be set up with some parameter to select x84 vs x64.
As a first stab I am targeting nightly to windows-latest (VS2019). The environment variable for the path to VsDevCmd uses the version number of VS. I hope Azure set up the paths already so the script bit-rots less.

dsyme · 2021-02-12T21:40:53Z

I suspect (not sure) you'll still need vcvarsall.bat for native code. I don't see any documented arguments to vsdevcmd.bat https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/compiler-options/how-to-set-environment-variables-for-the-visual-studio-command-line

NikolajBjorner · 2021-02-12T22:50:07Z

Latest nightly is ready.
Unpacked it says:

C:\Users\nbjorner\Downloads\m\lib\netstandard1.4>corflags Microsoft.Z3.dll
Microsoft (R) .NET Framework CorFlags Conversion Tool.  Version  4.6.1055.0
Copyright (c) Microsoft Corporation.  All rights reserved.

Version   : v4.0.30319
CLR Header: 2.5
PE        : PE32
CorFlags  : 0x9
ILONLY    : 1
32BITREQ  : 0
32BITPREF : 0
Signed    : 1

So far so good, but I don't have a handy environment for end-to-end testing.

Don Syme added 3 commits February 11, 2021 15:14

build package for x86

954caa0

build package for x86

9feae5e

build package for x86

12b0164

NikolajBjorner merged commit 504b655 into Z3Prover:master Feb 11, 2021

iscottb122 mentioned this pull request May 21, 2021

Remove x64 suffix from NuGet package names. #5292

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Suggestion: build .NET package for both x86 and x64 and rename #5021

[WIP] Suggestion: build .NET package for both x86 and x64 and rename #5021

dsyme commented Feb 11, 2021 •

edited

Loading

NikolajBjorner commented Feb 11, 2021

dsyme commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

dsyme commented Feb 12, 2021 •

edited

Loading

dsyme commented Feb 12, 2021 •

edited

Loading

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021 •

edited

Loading

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

[WIP] Suggestion: build .NET package for both x86 and x64 and rename #5021

[WIP] Suggestion: build .NET package for both x86 and x64 and rename #5021

Conversation

dsyme commented Feb 11, 2021 • edited Loading

NikolajBjorner commented Feb 11, 2021

dsyme commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

NikolajBjorner commented Feb 11, 2021

dsyme commented Feb 12, 2021 • edited Loading

dsyme commented Feb 12, 2021 • edited Loading

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021 • edited Loading

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 12, 2021

NikolajBjorner commented Feb 12, 2021

dsyme commented Feb 11, 2021 •

edited

Loading

dsyme commented Feb 12, 2021 •

edited

Loading

dsyme commented Feb 12, 2021 •

edited

Loading

NikolajBjorner commented Feb 12, 2021 •

edited

Loading