compile-compcert

Original：🇺🇸 English

Translated

Guide for building CompCert, the formally verified C compiler, from source. This skill should be used when compiling, building, or installing CompCert, or when working with Coq-based software that has strict dependency version requirements. Covers OCaml/opam setup, Coq version compatibility, memory management, and common build pitfalls.

1installs

Sourceletta-ai/skills

Added on2026-02-07

NPX Install

npx skill4agent add letta-ai/skills compile-compcert

SKILL.md Content

View Translation Comparison →

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:

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)

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:

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

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

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

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