Not able to install Formula

Nov 14, 2013 at 10:52 AM
I am following the steps stated in the Readme file but I am not able to intall Formula.

I have acquired and installed all Non-Codeplex Dependencies. Later, I execute:

cd myPath\Formula\Bld
built.bat

And I do not get any result. I mean, the command prompt dissapears after about 20 minutes showing the generated output files. I check in the Formula directory and I can see that new files have been generated but I do not know how to continue.

Any idea?

Thank you in advance.
Bea
Nov 15, 2013 at 9:18 AM
The error I get is:

OUT: Generated 'src\parsers\util\parser_params.hpp'
OUT: Generated 'src\sat\sat_asymm_branch_params.hpp'
OUT: Generated 'src\sat\sat_params.hpp'
OUT: Generated 'src\sat\sat_scc_params.hpp'
OUT: Generated 'src\sat\sat_simplifier_params.hpp'
OUT: Generated 'src\smt\params\smt_params_helper.hpp'
OUT: Generated 'src\solver\combined_solver_params.hpp'
OUT: Generated 'src\tactic\sls\sls_params.hpp'
OUT: Generated 'src\ast\pattern\database.h'
OUT: Generated 'src\shell\install_tactic.cpp'
OUT: Generated 'src\test\install_tactic.cpp'
OUT: Generated 'src\api\dll\install_tactic.cpp'
OUT: Generated 'src\shell\mem_initializer.cpp'
OUT: Generated 'src\test\mem_initializer.cpp'
OUT: Generated 'src\api\dll\mem_initializer.cpp'
OUT: Generated 'src\shell\gparams_register_modules.cpp'
OUT: Generated 'src\test\gparams_register_modules.cpp'
OUT: Generated 'src\api\dll\gparams_register_modules.cpp'
OUT: Generated 'src\api\python\z3consts.py'
OUT: Generated 'src\api\dotnet\Enumerations.cs'
OUT: Generated 'src\api\api_log_macros.h'
OUT: Generated 'src\api\api_log_macros.cpp'
OUT: Generated 'src\api\api_commands.cpp'
OUT: Generated 'src\api\python\z3core.py'
OUT: Generated 'src\api\dotnet\Native.cs'
OUT: Listing src\api\python ...
OUT: Compiling src\api\python\z3.py ...
OUT: Compiling src\api\python\z3consts.py ...
OUT: Compiling src\api\python\z3core.py ...
OUT: Compiling src\api\python\z3num.py ...
OUT: Compiling src\api\python\z3poly.py ...
OUT: Compiling src\api\python\z3printer.py ...
OUT: Compiling src\api\python\z3rcf.py ...
OUT: Compiling src\api\python\z3test.py ...
OUT: Compiling src\api\python\z3types.py ...
OUT: Copied 'z3.py'
OUT: Copied 'z3consts.py'
OUT: Copied 'z3core.py'
OUT: Copied 'z3num.py'
OUT: Copied 'z3poly.py'
OUT: Copied 'z3printer.py'
OUT: Copied 'z3rcf.py'
OUT: Copied 'z3test.py'
OUT: Copied 'z3types.py'
OUT: Generated 'z3.pyc'
OUT: Generated 'z3consts.pyc'
OUT: Generated 'z3core.pyc'
OUT: Generated 'z3num.pyc'
OUT: Generated 'z3poly.pyc'
OUT: Generated 'z3printer.pyc'
OUT: Generated 'z3rcf.pyc'
OUT: Generated 'z3test.pyc'
OUT: Generated 'z3types.pyc'
OUT: 64-bit: False
OUT: Writing build\x64\Makefile
OUT: Copied Z3Py example 'example.py' to 'build\x64'
OUT: Makefile was successfully generated.
OUT: compilation mode: Release
OUT: platform: x64
OUT:
OUT: To build Z3, open a [Visual Studio x64 Command Prompt], then
OUT: type 'cd C:\formula\Ext\Z3\z3_\build\x64 && nmake'
OUT:
OUT: Remark: to open a Visual Studio Command Prompt, go to: "Start > All Program
s > Visual Studio > Visual Studio Tools"
OUT:
EXIT: 1
ERROR: Could not build z3 (x64)
ERROR: Build failed
Build failed.


but I have x86.....
Nov 15, 2013 at 9:34 AM
If I build z3 with:

cd C:\formula\Ext\Z3\z3_\build\x86 && nmake

from a Visual Studio Command Prompt (VS2012 x86)

I get:

Compilador de Microsoft (R) Visual C#, versión 4.0.30319.17929
para Microsoft (R) .NET Framework 4.5
(C) Microsoft Corporation. Reservados todos los derechos.

Z3 was successfully built.
"Z3Py scripts can already be executed in the 'build\x86' directory."
"Z3Py scripts stored in arbitrary directories can be also executed if 'build\x86
' directory is added to the PYTHONPATH environment variable."

but I do not know how to continue. I do not get anything in the DROPS folder...

How I can continue?

Thank you very much
Bea
Dec 11, 2013 at 8:21 AM
Finally, after trying lots of times in a x86 computer, I have been able to install it (obtaining the corresponding folders and files in the DROPS folder), in a virtual machine with W7 and x64.

I am not sure if the installation works in a x86 computer...
Coordinator
Dec 17, 2013 at 11:09 PM
You are right, currently the script requires successful builds of both the x86 and x64 versions. I will add this as an issue.
Feb 7, 2014 at 2:43 AM
Edited Feb 10, 2014 at 12:35 AM
Hello Ethan and Bea, I have followed all the instructions but the build.bat could not really compile the GPLEX dependency :

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
OUT: "C:\PW\Temp\FORMULA_bld\Ext\GPLEX\gplex_\GPLEXv1.csproj" (default target) (1) ->
OUT: (_CheckForInvalidConfigurationAndPlatform target) ->
OUT: C:\Windows\Microsoft.NET\Framework64\v4.0.30319\Microsoft.Common.targets(609,5):
error : The OutputPath property is not set for project 'GPLEXv1.csproj'.
Please check to make sure that you have specified a valid combination of Configuration and Platform for this project. Configuration='Release' Platform='MCD'
. You may be seeing this message because you are trying to build a project without a solution file, and have specified a non-default Configuration or Platform that doesn't exist for this project. [C:\PW\Temp\FORMULA_bld\Ext\GPLEX\gplex_\GPLEXv1.csproj]
OUT:
OUT: 0 Warning(s)
OUT: 1 Error(s)
OUT:
OUT: Time Elapsed 00:00:01.79
OUT:
EXIT: 1
ERROR: Could not compile the gplex dependency
ERROR: Build failed
Build failed.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Could you let me know how I can fix these please?

Thanks,
Pakorn
Feb 7, 2014 at 7:38 AM
Hello Pakorn,
it seems that you are having a problem with the GPLEX dependency. Are you downloading the dependencies "automatically" (that is, executing the built.bat without any particular option) or "manually" (executing the built.bat with the "-l" option)?
If you have used one of these options, you can try with the other.
Bea
Feb 10, 2014 at 12:33 AM
Edited Feb 10, 2014 at 12:37 AM
Hi Bea,

Many thanks for your reply. I did it automatically using build.bat. It seems that the GPLEX has been successfully downloaded and extracted, as I can see a newly created folder "C:\PW\Temp\FORMULA_bld\Ext\GPLEX\gplex_" with GPLEX code in it. But the compilation has errors as shown in the above post.

I also tried build.bat -l as you suggested, the message I've got is:

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
C:\PW\Temp\FORMULA_bld\Bld>build.bat -l

C:\PW\Temp\FORMULA_bld\Bld>echo off
Bootstrapping the build utility...
Source code: http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=z3&changeSetId=33f941aaec11bf7ef754d5779e581ba4a26b3018

Source code: http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=gppg&changeSetId=84257
Source code: http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=gplex&changeSetId=84980
Gardens Point dependency: ..........\Ext\GPLEX\gplex45.exe
Gardens Point dependency: ..........\Ext\GPPG\gppg45.exe
Z3 dependency: ..........\Ext\Z3\x86\libz3.dll
Z3 dependency: ..........\Ext\Z3\x86\libz3.exp
Z3 dependency: ..........\Ext\Z3\x86\libz3.lib
Z3 dependency: ..........\Ext\Z3\x86\libz3.pdb
Z3 dependency: ..........\Ext\Z3\x86\vc110.pdb
Z3 dependency: ..........\Ext\Z3\x86\Microsoft.Z3.dll
Z3 dependency: ..........\Ext\Z3\x86\Microsoft.Z3.pdb
Z3 dependency: ..........\Ext\Z3\x86\z3.exe
Z3 dependency: ..........\Ext\Z3\x86\z3.exp
Z3 dependency: ..........\Ext\Z3\x86\z3.lib
Z3 dependency: ..........\Ext\Z3\x86\z3.pdb
Z3 dependency: ..........\Ext\Z3\x64\libz3.dll
Z3 dependency: ..........\Ext\Z3\x64\libz3.exp
Z3 dependency: ..........\Ext\Z3\x64\libz3.lib
Z3 dependency: ..........\Ext\Z3\x64\vc110.pdb
Z3 dependency: ..........\Ext\Z3\x64\Microsoft.Z3.dll
Z3 dependency: ..........\Ext\Z3\x64\Microsoft.Z3.pdb
Z3 dependency: ..........\Ext\Z3\x64\z3.exe
Z3 dependency: ..........\Ext\Z3\x64\z3.exp
Z3 dependency: ..........\Ext\Z3\x64\z3.lib

C:\PW\Temp\FORMULA_bld\Bld>
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

So, I tried to download the code manually following the link "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx?ProjectName=gplex&changeSetId=84980" but I got exactly the same code as the one automatically downloaded.