215 Name Skill F54f3252

---
name: compile-compcert
description: 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.
---

# 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