Слияние кода завершено, страница обновится автоматически
CMake — это «метасистема сборки», которая считывает описание проекта, записанное в файлах CMakeLists.txt, и генерирует систему сборки для этого проекта по выбору с помощью одного из «генераторов» CMake. Это позволяет CMake поддерживать множество различных платформ и инструментов сборки. Вы можете запустить cmake --help, чтобы увидеть список поддерживаемых «генераторов» на вашей платформе. Примеры генераторов включают «UNIX Makefiles» и «Visual Studio 12 2013».
Если вы никогда не использовали систему сборки Python, этот шаг можно пропустить.
Существующая система сборки Python создаёт сгенерированные исходные файлы в дереве исходных текстов. Система сборки CMake откажется работать, если обнаружит это, поэтому сначала необходимо очистить дерево исходных текстов.
Для этого выполните следующие действия в корне репозитория:
git clean -nx src
Это отобразит всё, что будет удалено. Если вас устраивает результат, запустите:
git clean -fx src
чтобы удалить сгенерированные исходные файлы.
Выполните следующие действия в верхнем уровне каталога репозитория Z3:
mkdir build
cd build
cmake -G "Unix Makefiles" ../
make -j4 # Замените 4 на подходящее число
Обратите внимание, что на некоторых платформах «Unix Makefiles» является генератором по умолчанию, поэтому на этих платформах вам не нужно передавать параметр командной строки -G "Unix Makefiles" в cmake.
Обратите внимание, что здесь нет ничего особенного в названии каталога build. Вы можете назвать его как угодно.
Обратите внимание, что генератор «Unix Makefile» — это генератор с «единой» конфигурацией, что означает, что вы выбираете тип сборки (например, Debug, Release), когда вызываете CMake. Вы можете установить тип сборки, передав его вызову cmake, например так:
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../
См. раздел о типах сборки для получения информации о различных типах сборок CMake.
Если вы хотите использовать другой компилятор, установите переменные среды CXX и CC, переданные в cmake. Это должно быть сделано при самом первом вызове cmake в каталоге сборки, потому что после настройки компилятор фиксируется. Если вы хотите использовать компилятор, отличный от того, который вы уже настроили, вам нужно либо создать новый каталог сборки, либо удалить содержимое текущего каталога сборки и начать заново.
Например, чтобы использовать clang, строка cmake будет выглядеть так:
CC=clang CXX=clang++ cmake ../
Обратите внимание, что сборка CMake определит целевую архитектуру, для которой настроен компилятор, и созданная система сборки будет собирать для этой архитектуры. Если есть способ указать вашему компилятору сборку для другой архитектуры с помощью флагов компилятора, вы можете установить переменные окружения CFLAGS и CXXFLAGS, чтобы получить цель сборки для этой архитектуры.
Например, если вы работаете на машине x86_64 и хотите выполнить 32-битную сборку и у вас есть многобиблиотечная версия GCC, вы можете запустить cmake следующим образом:
CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../
Обратите внимание, как и в случае с флагами CC и CXX, это должно быть выполнено при самом первом вызове CMake в каталоге сборки.
Ninja — простая система сборки, созданная для скорости. Она может быть значительно быстрее, чем «UNIX Makefile», потому что это не рекурсивная система сборки и она не создаёт новый процесс каждый раз, когда переходит в каталог. Ninja особенно подходит, если вам нужна быстрая инкрементная сборка.
Основное использование выглядит следующим образом:
mkdir build
cd build
cmake -G "Ninja" ../
ninja
Примечание о переменных CC, CXX, CFLAGS и CXXFLAGS для «Unix Makefiles» также применимо здесь.
Также обратите внимание, что, как и генератор «Unix Makefiles», генератор «Ninja» представляет собой генератор с единой конфигурацией, поэтому вы выбираете тип сборки при вызове cmake, передавая CMAKE_BUILD_TYPE=<build_type> в cmake. См. раздел о типах сборки.
Обратите внимание, что Ninja по умолчанию работает параллельно. Используйте флаг -j, чтобы изменить это.
Обратите внимание, что Ninja также работает в Windows. Вам просто нужно запустить: CMake в среде, где можно найти компилятор. Если у вас установлена Visual Studio, то обычно она поставляется с «Командной строкой разработчика для Windows», которую вы можете использовать. В ней уже настроены переменные среды.
NMake — это система сборки, которая поставляется вместе с Visual Studio. Рекомендуется использовать Ninja, который значительно быстрее благодаря поддержке параллельных сборок. Однако CMake поддерживает NMake, если вы хотите его использовать. Обратите внимание, что NMake является генератором с одной конфигурацией, поэтому необходимо установить CMAKE_BUILD_TYPE для определения типа сборки.
Базовое использование:
mkdir build
cd build
cmake -G "NMake Makefiles" ../
nmake
Visual Studio 19 имеет встроенную поддержку CMake. Достаточно открыть папку (z3), в которой находится этот файл и проект Z3 CMakeLists.txt, и Visual Studio сделает всё остальное.
Для устаревших версий Visual Studio процесс выглядит следующим образом: для генераторов Visual Studio необходимо знать, какую версию Visual Studio вы хотите использовать и для какой архитектуры будете строить.
Здесь мы будем использовать cmake-gui, поскольку с ним проще выбрать правильный генератор, но при необходимости это можно сделать и через скрипт.
Вот основные шаги:
Обратите внимание, что в отличие от генераторов «Unix Makefile» и «Ninja», генераторы Visual Studio являются многоконфигурационными, что означает, что вы не устанавливаете тип сборки при вызове CMake. Вместо этого вы устанавливаете тип сборки внутри Visual Studio. Дополнительную информацию см. в разделе «Тип сборки».
Общий рабочий процесс при использовании CMake следующий:
Чтобы выполнить шаги 2 и 3, вы можете выбрать один из трёх инструментов:
cmake — это инструмент командной строки, который следует использовать, если вы пишете скрипт для сборки Z3. Этот инструмент выполняет шаги 1 и 2 одновременно без участия пользователя. Инструменты ccmake и cmake-gui более интерактивны и позволяют изменять различные параметры. В обоих этих инструментах основные шаги следующие:
Дополнительную информацию смотрите на сайте https://cmake.org/runningcmake/.
Обратите внимание, что при вызове CMake вы указываете путь к исходному каталогу. Это верхний уровень в репозитории Z3, содержащий файл CMakeLists.txt. Должен содержать строку «project(Z3 C CXX)».
Если вы укажете путь глубже в репозиторий Z3 (например, каталог «src»), шаг настройки завершится неудачно.
Поддерживается несколько типов сборки:
Для генераторов с одной конфигурацией (например, «Unix Makefile» и «Ninja») вы устанавливаете тип сборки при вызове cmake, передавая -DCMAKE_BUILD_TYPE=<build_type>, где <build_type> — один из указанных выше типов сборки.
Для многоконфигурационных генераторов (например, Visual Studio) вы не устанавливаете тип сборки при вызове CMake, а вместо этого задаёте тип сборки в самой Visual Studio.
Следующие полезные опции можно передать в CMake во время настройки:
Z3_BUILD_DOCUMENTATION — BOOL. Если установлено значение TRUE, документацию для API-связок можно создать, вызвав цель api_docs.
Z3_INSTALL_API_BINDINGS_DOCUMENTATION — BOOL. Если установлено значение TRUE и Z3_BUILD_DOCUMENTATION равно TRUE, документация для API-связок будет установлена при запуске цели install.
Z3_ALWAYS_BUILD_DOCS — BOOL. Если установлено значение TRUE и Z3_BUILD_DOCUMENTATION равно TRUE, документация для API-связок всегда будет создаваться. Отключение этой функции полезно для более быстрой инкрементной сборки. Документацию можно вручную создать, вызвав цель api_docs.
Z3_LINK_TIME_OPTIMIZATION — BOOL. Если установлено значение TRUE, будет включена оптимизация времени компоновки.
Z3_ENABLE_CFI — BOOL. Если установлено значение TRUE, будут включены проверки целостности потока управления (Control Flow Integrity). Эта функция поддерживается только MSVC и Clang и не будет работать на других компиляторах. Для этого также необходимо включить Z3_LINK_TIME_OPTIMIZATION.
Z3_API_LOG_SYNC — BOOL. Если установлено значение TRUE, будет включена экспериментальная функция синхронизации журнала API.
WARNINGS_AS_ERRORS — STRING. Если установлено значение TRUE, предупреждения компилятора будут рассматриваться как ошибки. Если установлено значение False, предупреждения компилятора не будут рассматриваться как ошибки. Если установлено значение SERIOUS_ONLY, подмножество предупреждений компилятора будет рассматриваться как ошибки.
Z3_C_EXAMPLES_FORCE_CXX_LINKER — BOOL. Если установлено значение TRUE, примеры C API запросят использование компоновщика C++ вместо компоновщика C.
Z3_BUILD_EXECUTABLE — BOOL. Если установлено значение TRUE, создайте исполняемый файл z3. По умолчанию используется значение TRUE, если z3 собирается не как подмодуль, в противном случае по умолчанию используется FALSE.
Z3_BUILD_TEST_EXECUTABLES — BOOL. Если установлено значение TRUE, создаются тестовые исполняемые файлы z3. По умолчанию используется значение TRUE, если z3 собирается не как подмодуль, в противном случае по умолчанию используется FALSE.
Z3_SAVE_CLANG_OPTIMIZATION_RECORDS — BOOL. Если установлено значение TRUE, сохраняются записи оптимизации Clang с помощью установки флага компилятора -fsave-optimization-record.
Z3_SINGLE_THREADED — BOOL. Если установлено значение TRUE, Z3 компилируется для однопоточного режима.
Эти параметры можно передать в cmake с помощью параметра -D в командной строке. В ccmake и cmake-gui их можно установить в пользовательском интерфейсе.
Пример:
cmake -DCMAKE_BUILD_TYPE=Release -DZ3_ENABLE_TRACING_FOR_NON_DEBUG=FALSE ../
Z3 предоставляет различные языковые привязки для своего API. Ниже приведены некоторые замечания по созданию и/или установке этих привязок при сборке Z3 с CMake.
Сборка CMake использует модули cmake FindJava и FindJNI для обнаружения установки Java. Если CMake не может найти вашу установку Java, установите переменную среды JAVA_HOME при вызове CMake так, чтобы она указывала на правильное местоположение. Например:
JAVA_HOME=/usr/lib/jvm/default cmake -DZ3_BUILD_JAVA_BINDINGS=ON ../
Обратите внимание, что созданный файл .jar называется com.microsoft.z3-VERSION.jar, где VERSION — это версия Z3. В системах, отличных от Windows, предоставляется символическая ссылка с именем com.microsoft.z3.jar. Эта символическая ссылка не создаётся при сборке в Windows.
Эти примечания предназначены для разработчиков и упаковщиков Z3.
Поддерживаются цели установки и удаления. Используйте CMAKE_INSTALL_PREFIX для установки префикса. Если вам также нужно контролировать, какие каталоги используются для установки, установите задокументированные параметры CMAKE_INSTALL_.
Чтобы установить, запустите:
make install
Чтобы удалить, запустите:
make uninstall
Обратите внимание, что DESTDIR поддерживается для поэтапных установок.
Для установки:
mkdir staged
make install DESTDIR=/full/path/to/staged/
для удаления:
make uninstall DESTDIR=/full/path/to/staged
Приведённое выше также работает для Ninja, но DESTDIR должен быть переменной окружения.
Вы можете оставить комментарий после Вход в систему
Неприемлемый контент может быть отображен здесь и не будет показан на странице. Вы можете проверить и изменить его с помощью соответствующей функции редактирования.
Если вы подтверждаете, что содержание не содержит непристойной лексики/перенаправления на рекламу/насилия/вульгарной порнографии/нарушений/пиратства/ложного/незначительного или незаконного контента, связанного с национальными законами и предписаниями, вы можете нажать «Отправить» для подачи апелляции, и мы обработаем ее как можно скорее.
Опубликовать ( 0 )