基础工具链安装：GCC、G++、Make、CMake、Git

各位同学，咱们今天来搞定形式化验证环境的第一块基石——基础工具链。说白了，就是先把C/C++编译器、构建工具和版本控制工具装好。这些工具你可能觉得稀松平常，但在我多年的工程生涯里，因为工具链版本不匹配、路径配错导致项目翻车的案例，见过太多了。

嗯，咱们一个一个来。

GCC与G++：编译器的选择

GCC和G++是Linux下最常用的编译器。GCC管C，G++管C++。形式化验证工具很多是用C++写的，所以这两个都得装。

安装命令（Ubuntu/Debian系）：

sudo apt update
sudo apt install build-essential

这个build-essential是个元包，会把GCC、G++、make等核心工具一并拉下来。我个人习惯装完后先看一眼版本：

gcc --version
g++ --version

安装命令（CentOS/RHEL系）：

sudo yum groupinstall "Development Tools"

或者用dnf：

sudo dnf groupinstall "Development Tools"

我曾经在CentOS 7上踩过一个坑——默认的GCC 4.8.5太老了，编译某个模型检查工具时疯狂报错。后来老老实实装了devtoolset-9才搞定。

Make：自动化构建的基石

Make是Linux世界最经典的构建工具。虽然现在有CMake、Ninja这些新秀，但Make依然是底层依赖。

安装很简单：

sudo apt install make

验证：

make --version

你想想看，Makefile写得好不好，直接决定了你的项目能不能一键编译。我在一个大型形式化验证项目中，就因为Makefile里漏了一个头文件依赖，导致每次改完代码都要手动make clean，浪费了整整两天时间。

CMake：跨平台构建利器

CMake是Make的上层工具。它不直接编译代码，而是生成Makefile（或者Ninja的构建文件）。形式化验证工具里，像Z3、CVC4这些，都是用CMake构建的。

安装：

sudo apt install cmake

验证：

cmake --version

我个人习惯用CMake 3.16以上版本。为什么？因为3.16开始对CUDA和Fortran的支持更完善了。虽然形式化验证很少用到CUDA，但保不齐哪天你要跑GPU加速的SMT求解呢？

一个典型的CMakeLists.txt示例：

cmake_minimum_required(VERSION 3.10)
project(FormalVerificationDemo)

set(CMAKE_CXX_STANDARD 17)
set(CMAKE_CXX_STANDARD_REQUIRED ON)

add_executable(demo main.cpp)

构建流程：

mkdir build && cd build
cmake ..
make

Git：版本控制的灵魂

Git的重要性不用我多说。形式化验证项目往往涉及大量代码、脚本和文档的迭代，没有Git，你根本没法追溯谁改了什么、为什么改。

安装：

sudo apt install git

验证：

git --version

基础配置（每个人必须做）：

git config --global user.name "Your Name"
git config --global user.email "your.email@example.com"
git config --global core.editor "vim"

我曾经见过一个同事，Git没配用户名就直接提交，结果提交记录里全是"unknown"。后来项目回溯问题时，根本不知道是谁改的代码。嗯，这种坑咱们别踩。

推荐配置：

git config --global init.defaultBranch main
git config --global pull.rebase true
git config --global fetch.prune true

为什么把默认分支改成main？因为master这个词在开源社区已经逐渐被替换了。我个人从2020年开始就用main了。

知识体系总览

下面这张图，是我梳理的基础工具链关系。你看一眼就能明白这些工具是怎么协作的：

验证安装是否成功

装完别急着走。我建议你写个简单的测试程序，验证整个工具链是否打通：

// test.cpp
#include <iostream>
int main() {
    std::cout << "Toolchain works!" << std::endl;
    return 0;
}

然后：

g++ test.cpp -o test
./test

如果输出"Toolchain works!"，恭喜你，环境搭好了。

再用Git试试：

git init test-repo
cd test-repo
echo "hello" > readme.md
git add .
git commit -m "first commit"
git log

能看到提交记录，说明Git也正常。

可可精品资料库