compile-compcert

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Compile CompCert

编译CompCert

Overview

概述

CompCert is a formally verified C compiler built with Coq proof assistant. Building it from source requires careful attention to dependency versions, particularly Coq compatibility, and resource constraints in containerized environments.

CompCert是一款使用Coq证明助手构建的经过形式验证的C编译器。从源码构建它需要特别注意依赖版本，尤其是Coq的兼容性，以及容器化环境中的资源限制。

Pre-Build Investigation (Critical First Step)

构建前调研（关键第一步）

Before installing any dependencies, download and examine CompCert's requirements:

Download CompCert source first
- Obtain the source tarball or clone the repository
- Check the
```
configure
```
  script for version requirements:
```
grep -i "coq" configure
```
- Review
```
README
```
  or
```
INSTALL
```
  files for dependency specifications
Identify exact Coq version requirements
- CompCert has strict Coq version bounds (e.g., CompCert 3.13.1 requires Coq ≤ 8.16.1)
- Installing an incompatible Coq version wastes significant time and resources
- Check both minimum and maximum supported versions
Assess system environment
- Check architecture:
```
uname -m
```
  (typically x86_64)
- Check available memory:
```
free -h
```
- Determine if running in container (affects swap, permissions)
- Verify privileged operations availability (swap creation usually fails in containers)

在安装任何依赖之前，请下载并查看CompCert的要求：

先下载CompCert源码
- 获取源码压缩包或克隆代码仓库
- 检查
```
configure
```
  脚本中的版本要求：
```
grep -i "coq" configure
```
- 查看
```
README
```
  或
```
INSTALL
```
  文件中的依赖说明
确定准确的Coq版本要求
- CompCert有严格的Coq版本限制（例如，CompCert 3.13.1要求Coq ≤ 8.16.1）
- 安装不兼容的Coq版本会浪费大量时间和资源
- 同时检查最低和最高支持版本
评估系统环境
- 检查架构：
```
uname -m
```
  （通常为x86_64）
- 检查可用内存：
```
free -h
```
- 判断是否在容器中运行（会影响交换分区、权限）
- 验证是否有特权操作权限（容器中通常无法创建交换分区）

Dependency Chain

依赖链

Install dependencies in this order, with version awareness:

按以下顺序安装依赖，注意版本匹配：

1. System Packages

1. 系统包

Install all system dependencies in a single command:

apt-get update && apt-get install -y opam gcc g++ make libgmp-dev pkg-config

使用一条命令安装所有系统依赖：

apt-get update && apt-get install -y opam gcc g++ make libgmp-dev pkg-config

2. OCaml/opam Setup

2. OCaml/opam配置

opam init -y --disable-sandboxing
eval $(opam env)

Memory optimization: Set job limit immediately after init to prevent OOM:

opam config set-global jobs 1

opam init -y --disable-sandboxing
eval $(opam env)

内存优化：初始化后立即设置任务限制以避免内存不足：

opam config set-global jobs 1

3. Coq Installation (Version Critical)

3. Coq安装（版本至关重要）

Do NOT install latest Coq - check CompCert's requirements first
Install the correct version:
```
opam install coq.X.Y.Z menhir
```
Common compatible versions:
- CompCert 3.13.x: Coq 8.16.1 or earlier
- CompCert 3.12.x: Coq 8.15.x or earlier

不要安装最新版Coq - 先检查CompCert的要求
安装正确版本：
```
opam install coq.X.Y.Z menhir
```
常见兼容版本：
- CompCert 3.13.x：Coq 8.16.1或更早版本
- CompCert 3.12.x：Coq 8.15.x或更早版本

4. CompCert Build

4. CompCert构建

./configure <target-arch>   # e.g., x86_64-linux
make
make install PREFIX=<path>

./configure <target-arch>   # 例如：x86_64-linux
make
make install PREFIX=<path>

Memory Management in Constrained Environments

受限环境中的内存管理

Coq and CompCert compilation are memory-intensive:

Limit parallel jobs:

opam config set-global jobs 1

before any

opam install

Do NOT attempt swap creation in containers -
```
swapon
```
fails with "Operation not permitted"
Monitor memory usage during compilation:
```
watch free -h
```
If OOM occurs: Kill stuck processes and retry with lower parallelism

Coq和CompCert编译非常消耗内存：

限制并行任务数：在任何
```
opam install
```
之前设置
```
opam config set-global jobs 1
```
不要在容器中尝试创建交换分区 -
```
swapon
```
会报错："Operation not permitted"
编译期间监控内存使用：
```
watch free -h
```
如果出现内存不足：终止卡住的进程，然后以更低的并行度重试

Verification Strategy

验证策略

After build completion, verify:

Binary exists and is executable
```
test -x /path/to/ccomp && echo "exists"
```

Compiler functions correctly

echo 'int main() { return 0; }' > /tmp/test.c
ccomp -o /tmp/test /tmp/test.c
/tmp/test && echo "success"

Expected behavior for unsupported features
- CompCert should reject certain C features (e.g., some GNU extensions)
- Test with known unsupported constructs to verify proper rejection

构建完成后，进行验证：

检查二进制文件是否存在且可执行
```
test -x /path/to/ccomp && echo "exists"
```

验证编译器功能正常

echo 'int main() { return 0; }' > /tmp/test.c
ccomp -o /tmp/test /tmp/test.c
/tmp/test && echo "success"

验证不支持特性的预期行为
- CompCert会拒绝某些C特性（例如，部分GNU扩展）
- 使用已知不支持的代码结构进行测试，验证编译器是否正确拒绝

Common Pitfalls

常见陷阱

Version Mismatch (Most Common)

版本不匹配（最常见）

Symptom: Build fails with Coq compatibility errors
Cause: Installed Coq version outside CompCert's supported range
Prevention: Always check
```
configure
```
script before installing Coq

症状：构建时出现Coq兼容性错误
原因：安装的Coq版本超出CompCert支持范围
预防措施：安装Coq前务必检查
```
configure
```
脚本

OOM During Coq Installation

Coq安装时内存不足

Symptom: Process killed, system becomes unresponsive
Cause: Parallel compilation exceeds available memory
Prevention: Set
```
jobs 1
```
immediately after
```
opam init
```

症状：进程被终止，系统无响应
原因：并行编译超出可用内存
预防措施：
```
opam init
```
后立即设置
```
jobs 1
```

Missing System Dependencies

缺少系统依赖

Symptom: Configure or build fails with missing library errors
Cause: Incremental dependency installation
Prevention: Install all system packages upfront (libgmp-dev, pkg-config, etc.)

症状：配置或构建时出现缺少库的错误
原因：增量安装依赖
预防措施：一次性安装所有系统包（libgmp-dev、pkg-config等）

Binary Path Confusion

二进制文件路径混淆

Symptom:
```
make install
```
places binary in unexpected location
Cause: Default PREFIX vs expected installation path differ
Prevention: Specify exact paths during configure, or create symlinks post-install

症状：
```
make install
```
将二进制文件放在意外位置
原因：默认PREFIX与预期安装路径不一致
预防措施：配置时指定准确路径，或安装后创建符号链接

Swap Creation Failure in Containers

容器中交换分区创建失败

Symptom:
```
swapon failed: Operation not permitted
```
Cause: Container lacks privileges for swap operations
Prevention: Do not attempt swap creation; rely on job limiting instead

症状：
```
swapon failed: Operation not permitted
```
原因：容器没有交换分区操作的权限
预防措施：不要尝试创建交换分区；改用限制任务数的方式

Efficient Build Workflow Summary

高效构建工作流总结

Download CompCert source
Check version requirements in
```
configure
```
script
Assess system resources and environment
Install ALL system packages in one command
Initialize opam with job limit set to 1
Install correct Coq version (not latest)
Configure and build CompCert
Verify binary location and create symlinks if needed
Run verification tests

下载CompCert源码
查看
```
configure
```
脚本中的版本要求
评估系统资源和环境
一次性安装所有系统包
初始化opam并将任务限制设置为1
安装正确版本的Coq（不要最新版）
配置并构建CompCert
验证二进制文件位置，必要时创建符号链接
运行验证测试