Building Z3 dependency failed.

Nov 10, 2013 at 6:04 AM
This is my first time building something from source code in VS.
I'm running into some problems building Formula.

1) What is the minimum requirement for VS to build Formula?

I downloaded an eval of VS 2012 Ultimate but this is clearly overkill...
Can you please indicate the minimum requirement for VS.
Does it matter if we get VS 2012 or VS 2013 or later?

2) What are the "required locations" for the Codeplex dependencies mentioned in the README.txt?

The FORMULA build scripts will try to automatically download these dependencies from Codeplex.
Or you may compile the dependencies manually and place them in the required locations.

3) Automatic download & build of dependencies failed with Z3:
C:\Users\rouquett>cd Source\Repos\formula

C:\Users\rouquett\Source\Repos\formula>cd Bld

C:\Users\rouquett\Source\Repos\formula\Bld>build.bat

C:\Users\rouquett\Source\Repos\formula\Bld>echo off
Bootstrapping the build utility...
Building in release configuration
Gardens Point dependencies have already been built; skipping this build step.
Downloading dependency z3 to C:\Users\rouquett\Source\Repos\formula\Ext\Z3\z3_.zip...
Extracting dependency z3 to C:\Users\rouquett\Source\Repos\formula\Ext\Z3\z3_\...
Building Z3 for x86.
OUT:
OUT: C:\Users\rouquett\Source\Repos\formula\Bld>REM echo off
OUT:
OUT: C:\Users\rouquett\Source\Repos\formula\Bld>call "E:\VSU2012\VC\vcvarsall.bat" x86
OUT:
EXIT: 2
ERROR: Could not build z3 (x86)
ERROR: Build failed
Build failed.
I noticed that in Z3Builder.cs, there's an absolute path for the z3 source dir.
Does that have anything to do with this error?
  • Nicolas
Nov 10, 2013 at 7:37 AM
For (3), I found that I had Python 2.5.1 installed instead of 2.7.5

After uninstalling & installing the correct Python 2.7.5, I had to fix the environment PATH variable (add C:\Python27).

Now, the build failed here:
OUT: CoreCompile:
OUT:   C:\Windows\Microsoft.NET\Framework64\v4.0.30319\Csc.exe /noconfig /nowarn:1701,1702 /nostdlib+ /platform:x86 /errorreport:prompt /define:TRACE /highentropyva+ /reference:C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\Core.dll /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\Microsoft.Build.Framework.dll" /reference:"C:\Program F
iles (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\Microsoft.Build.Utilities.v4.0.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\Microsoft.CSharp.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\mscorlib.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\F
ramework\.NETFramework\v4.5\System.Core.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Data.DataSetExtensions.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Data.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.dll" /refer
ence:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Xml.dll" /reference:"C:\Program Files (x86)\Reference Assemblies\Microsoft\Framework\.NETFramework\v4.5\System.Xml.Linq.dll" /debug:pdbonly /filealign:512 /optimize+ /out:obj\x86\Release\FormulaCodeGeneratorTask.dll /subsystemversion:6.00 /target:library /utf8output GenerateItem.cs Task.cs Properties\As
semblyInfo.cs "C:\Users\rouquett\AppData\Local\Temp\.NETFramework,Version=v4.5.AssemblyAttributes.cs"
OUT: _CopyFilesMarkedCopyLocal:
OUT:   Copying file from "C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\Core.dll" to "bin\x86\Release\Core.dll".
OUT:   Copying file from "C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\Microsoft.Z3.dll" to "bin\x86\Release\Microsoft.Z3.dll".
OUT:   Copying file from "C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\Core.pdb" to "bin\x86\Release\Core.pdb".
OUT:   Copying file from "C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\Microsoft.Z3.pdb" to "bin\x86\Release\Microsoft.Z3.pdb".
OUT:   Copying file from "C:\Users\rouquett\Source\Repos\formula\Src\Core\bin\x86\Release\libz3.dll" to "bin\x86\Release\libz3.dll".
OUT: _CopyOutOfDateSourceItemsToOutputDirectory:
OUT: Skipping target "_CopyOutOfDateSourceItemsToOutputDirectory" because all output files are up-to-date with respect to the input files.
OUT: CopyFilesToOutputDirectory:
OUT:   Copying file from "obj\x86\Release\FormulaCodeGeneratorTask.dll" to "bin\x86\Release\FormulaCodeGeneratorTask.dll".
OUT:   FormulaCodeGeneratorTask -> C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGeneratorTask\bin\x86\Release\FormulaCodeGeneratorTask.dll
OUT:   Copying file from "obj\x86\Release\FormulaCodeGeneratorTask.pdb" to "bin\x86\Release\FormulaCodeGeneratorTask.pdb".
OUT: Done Building Project "C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGeneratorTask\FormulaCodeGeneratorTask.csproj" (default targets).
OUT:
OUT: Build succeeded.
OUT:     0 Warning(s)
OUT:     0 Error(s)
OUT:
OUT: Time Elapsed 00:00:00.38
OUT:
EXIT: 0
ERROR: Build failed
Build failed.

C:\Users\rouquett\Source\Repos\formula\Bld>
I found an executable: FormulaBuild\FormulaBuild\bin\Debug\FormulaBuild.exe

When I ran it, I got this:
OUT: Build started 11/9/2013 11:32:04 PM.
OUT: Project "C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGenerator\FormulaCodeGenerator.csproj" on node 1 (default targets).
OUT: C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGenerator\FormulaCodeGenerator.csproj(246,3): error MSB4019: The imported project "C:\Program Files (x86)\MSBuild\Microsoft\VisualStudio\v11.0\VSSDK\Microsoft.VsSDK.targets" was not found. Confirm that the path in the <Import> declaration is correct, and that the file exists on disk.
OUT: Done Building Project "C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGenerator\FormulaCodeGenerator.csproj" (default targets) -- FAILED.
OUT:
OUT: Build FAILED.
OUT:
OUT: "C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGenerator\FormulaCodeGenerator.csproj" (default target) (1) ->
OUT:   C:\Users\rouquett\Source\Repos\formula\Src\Extensions\FormulaCodeGenerator\FormulaCodeGenerator.csproj(246,3): error MSB4019: The imported project "C:\Program Files (x86)\MSBuild\Microsoft\VisualStudio\v11.0\VSSDK\Microsoft.VsSDK.targets" was not found. Confirm that the path in the <Import> declaration is correct, and that the file exists on disk.
OUT:
OUT:     0 Warning(s)
OUT:     1 Error(s)
OUT:
OUT: Time Elapsed 00:00:00.04
From the output above, I guess that I don't have the VS 2012 SDK installed.
I found it here:

http://www.microsoft.com/en-us/download/details.aspx?id=30668

This should go in the README file.
  • Nicolas.
Nov 10, 2013 at 7:43 AM
After installing VS2012 SDK, the build completed successfully.
  • Nicolas.
Nov 13, 2013 at 6:16 PM
Hi Nicolas,
do you know how I can go on when finishing the build? After that, my Visual 2012 has not any Fomula option installed....

Thank you very much.
Bea
Nov 18, 2013 at 11:50 PM
Hi Bea,

Did you look if you have ...\Source\Repos\formula\Bld\Drops\Formula_Release_x64\Formula.exe

It seems that building Formula 2.0 is sensitive to the version of python -- i.e., check that you really have 2.7.5, not an earlier version -- as well as the VS 2012 SDK installed.
  • Nicolas.
Nov 20, 2013 at 4:04 PM
Edited Nov 20, 2013 at 4:05 PM
Hi Nicolas,
I have checked the phyton version and I have the 2.7.5. My Drops folder is empty, but It seems that I can work with formula executing the Src\CommandLine\bin\x86\Debug\CommandLine.exe file.

I am working with it now...¿have you tried to reload a 4ml file? It seams that the command is unknow....perhaps the reason is that I am executing the wrong .exe...

Thank you,
Bea
Coordinator
Dec 18, 2013 at 12:06 AM
I have updated the Readme file to clarify the python version dependency and the VS 2012 SDK dependency. You are correct that Z3's build scripts do not support Python 3. Formula itself doesn't have a python dependency.