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