search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.33k stars 1.48k forks source link

Windows x86 build giving an error. #1003

Closed SMTStuck closed 7 years ago

SMTStuck commented 7 years ago

Fix The fix is rather simple - don't have spaces in the path to the Z3 directory. Would be appreciated I'm sure by new Windows users to have a note on the Build page that Z3 should not be part of a path with spaces.

Problem

mem_initializer.cpp cl /Felibz3.dll /nologo /LD api\dll\dll.obj api\dll\gparams_register_modules.obj api\dll\install_tactic.obj api\dll\mem_initializer.obj api\api_algebraic.obj api\api_arith.obj api\api_array.obj api\api_ast.obj api\api_ast_map.obj api\api_ast_vector.obj api\api_bv.obj api\api_commands.obj api\api_config_params.obj api\api_context.obj api\api_datalog.obj api\api_datatype.obj api\api_fpa.obj api\api_goal.obj api\api_interp.obj api\api_log.obj api\api_log_macros.obj api\api_model.obj api\api_numeral.obj api\api_opt.obj api\api_params.obj api\api_parsers.obj api\api_pb.obj api\api_polynomial.obj api\api_quant.obj api\api_rcf.obj api\api_seq.obj api\api_solver.obj api\api_stats.obj api\api_tactic.obj api\z3_replayer.obj opt\opt.lib parsers\smt\smtparser.lib tactic\portfolio\portfolio.lib tactic\fpa\fpa_tactics.lib tactic\smtlogics\smtlogic_tactics.lib sat\sat_solver\sat_solver.lib tactic\ufbv\ufbv_tactic.lib tactic\nlsat_smt\nlsat_smt_tactic.lib muz\fp\fp.lib muz\duality\duality_intf.lib muz\ddnf\ddnf.lib muz\bmc\bmc.lib muz\tab\tab.lib muz\clp\clp.lib muz\pdr\pdr.lib muz\rel\rel.lib muz\transforms\transforms.lib muz\dataflow\dataflow.lib muz\base\muz.lib duality\duality.lib qe\qe.lib tactic\sls\sls_tactic.lib smt\tactic\smt_tactic.lib tactic\bv\bv_tactics.lib smt\smt.lib smt\proto_model\proto_model.lib smt\params\smt_params.lib ast\rewriter\bit_blaster\bit_blaster.lib ast\pattern\pattern.lib ast\macros\macros.lib ast\fpa\fpa.lib ast\simplifier\simplifier.lib ast\proof_checker\proof_checker.lib parsers\smt2\smt2parser.lib cmd_context\extra_cmds\extra_cmds.lib cmd_context\cmd_context.lib interp\interp.lib ackermannization\ackermannization.lib solver\solver.lib tactic\aig\aig_tactic.lib math\subpaving\tactic\subpaving_tactic.lib nlsat\tactic\nlsat_tactic.lib tactic\arith\arith_tactics.lib sat\tactic\sat_tactic.lib tactic\core\core_tactics.lib math\euclid\euclid.lib math\grobner\grobner.lib parsers\util\parser_util.lib ast\substitution\substitution.lib tactic\tactic.lib model\model.lib ast\normal_forms\normal_forms.lib ast\rewriter\rewriter.lib ast\ast.lib math\subpaving\subpaving.lib math\realclosure\realclosure.lib math\interval\interval.lib math\automata\automata.lib math\simplex\simplex.lib math\hilbert\hilbert.lib nlsat\nlsat.lib sat\sat.lib math\polynomial\polynomial.lib util\util.lib /link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO /DEF:..\src\api\dll\api_dll.def Creating library libz3.lib and object libz3.exp copy libz3.dll python 1 file(s) copied. Microsoft (R) Visual C# Compiler version 1.2.0.60317 Copyright (C) Microsoft Corporation. All rights reserved.

error CS2001: Source file 'D:\Development\Z3 Prover\Z3 Code\build\Prover\Z3' could not be found. error CS2001: Source file 'D:\Development\Z3 Prover\Z3 Code\build\Code\src\api\dotnet\Microsoft.Z3.snk' could not be found. NMAKE : fatal error U1077: '"C:\Program Files (x86)\MSBuild\14.0\bin\csc.EXE"' : return code '0x1'

delcypher commented 7 years ago

@SMTStuck Imaginative username ;)

I'm not sure where the Prover or Code came from.

If you want to you can try to workaround this by trying Z3's CMake based build system. The ".NET" bindings should build on Windows.

Here are the steps to the build

  1. Install CMake if you don't already have it.

  2. Install Ninja if you don't have already have it. Although you can use nmake if you really want to (CMake supports it). Ninja is much much better because it runs in parallel giving very fast build times.

  3. In your Z3 git repository run the following

git clean -fxd

This removes unwanted files left behind by the other build system.

Now copy the CMake files into the correct place in the git repository

python contrib/cmake/bootstrap.py create
  1. Now make a new build directory. I'm assuming this is created inside the root directory of the git repository but you can create it any where you like on your system
mkdir build
  1. Now run CMake to generate the build system. Note this should be run from a console where the C++ and C# compiler are available. Typically that requires you to run the vcvarsall.bar x64 command in your console.
cd build
cmake -G Ninja -DCMAKE_BUILD_TYPE=RelWithDebInfo -DBUILD_DOTNET_BINDINGS=ON ..\

Note if you didn't put your build directory in the git repository replace ..\ with the full path to the Z3 git repository on your system. If your're curious about the available configuration options read the README-CMake.md file in the Z3 repository.

  1. Finally start the build. Just run
ninja

in your build directory.

Hope that helps.

SMTStuck commented 7 years ago

Re: username, yeah I'm rather talented like that! :smile:

Thank you very much for the detailed reply. I have tried building to a path with no spaces and it works fine, yet even so the build process finishes with:

Microsoft (R) Visual C# Compiler version 1.2.0.60317 Copyright (C) Microsoft Corporation. All rights reserved.

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

So, even after a successful build, there is still no trace of a mention of a Code or Prover directory in either the output nor the build directory, which I find rather strange.

Shall be having a closer look at Ninja though as the build times are silly long to the point of keeping up to date with the master branch would be next to impossible!

delcypher commented 7 years ago

@SMTStuck

Thank you very much for the detailed reply. I have tried building to a path with no spaces and it works fine, yet even so the build process finishes with:

Ah okay so something in the generated Makefile isn't handling spaces properly.

Shall be having a closer look at Ninja though as the build times are silly long to the point of keeping up to date with the master branch would be next to impossible!

Great. Just to warn you though until #986 is fixed when ever you pull down new code (or do anything that would modify the CMake files in git) you need to re-run the contrib/cmake/bootstrap.py script to make sure all your CMake files are in sync.

wintersteiger commented 7 years ago

Thanks for reporting this issue, this is now fixed and you can have spaces in the keyfile filename. But, I'm sure there's a few other pieces of scripts that don't like spaces, so keep reporting them if you run into something that looks related!