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.

5installs
Sourceletta-ai/skills
Added on

NPX Install

npx skill4agent add letta-ai/skills compile-compcert

Tags

Translated version includes tags in frontmatter
compcert-buildcoq-compatibilityocaml-opam-setupmemory-managementbuild-pitfalls

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:
  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
  2. 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
  3. 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