compile-compcert（编译 comcert）

Compile 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.

Pre-Build Investigation (Critical First Step)

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

1. 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

1. 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

1. 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)

Dependency Chain

Install dependencies in this order, with version awareness:

1. System Packages

Install all system dependencies in a single command:

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

2. OCaml/opam Setup

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

3. Coq Installation (Version Critical)

• 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

4. CompCert Build

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

Memory Management in Constrained Environments

Coq and CompCert compilation are memory-intensive:

1. Limit parallel jobs: opam config set-global jobs 1 before any opam install
2. Do NOT attempt swap creation in containers - swapon fails with "Operation not permitted"
3. Monitor memory usage during compilation: watch free -h
4. If OOM occurs: Kill stuck processes and retry with lower parallelism

Verification Strategy

After build completion, verify:

1. Binary exists and is executable test -x /path/to/ccomp && echo "exists"
2. Compiler functions correctly echo 'int main() {return 0;}' > /tmp/test.c ccomp -o /tmp/test /tmp/test.c /tmp/test && echo "success"
3. 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

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

OOM During Coq Installation

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

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.)

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

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

Efficient Build Workflow Summary

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