bianhaifeng789-hue/compile-compcert

Building CompCert (Verified C Compiler)

Overview

CompCert is a formally verified optimizing C compiler. Building it requires careful coordination of Coq (proof assistant), OCaml, and Menhir (parser generator) versions. The primary challenge is ensuring version compatibility across all dependencies before beginning compilation.

Critical Pre-Build Analysis

Before installing any dependencies, perform these steps in order:

1. Obtain Source First

Download and extract the CompCert source before installing dependencies:

• Download the specific version tarball from GitHub releases or official mirrors
• Extract and locate the configure script
• Read the configure script to identify supported Coq versions

2. Check Version Requirements

Examine CompCert's configure script to find exact dependency requirements:

• Supported Coq version range (often specific minor versions only)
• Required OCaml version
• Required Menhir version
• The configure script typically contains explicit version checks

3. Verify System Compatibility

Check system requirements before proceeding:

• Architecture (x86_64 is most commonly supported for full backend)
• Operating system (Linux is primary target)
• Available memory (builds can be memory-intensive)
• Disk space for build artifacts

Dependency Installation Approach

Environment Setup with opam

CompCert requires opam (OCaml Package Manager) for managing OCaml and Coq:

1. Initialize opam if not already done
2. Create a switch with appropriate OCaml version
3. Set up the environment: eval $(opam env)
4. Install dependencies in correct order: OCaml → Menhir → Coq

Version Selection Strategy

To avoid wasted effort from incompatible versions:

1. Check CompCert's configure script BEFORE installing Coq
2. Install the highest compatible Coq version within the supported range
3. Ensure Menhir version matches requirements
4. Verify all versions after installation

Build Process

Configuration

Run configure with appropriate target:

• Common targets: x86_64-linux, x86_32-linux, arm-linux
• Check available targets with ./configure --help
• Note the installation prefix and binary locations

Compilation

Build considerations:

• Full build includes proof checking and can be memory-intensive
• If encountering OOM (Out of Memory) errors:
  • Reduce parallel jobs (make -j1 instead of parallel)
  • Consider adding swap space if in a container that allows it
  • Monitor memory usage during proof checking phases

Installation and Verification

After successful build:

• Note where ccomp binary is installed
• Create symlinks if binary needs to be at a specific location
• Test with a simple C program compilation
• Verify the reported version matches expected version

Common Pitfalls

Dependency Order Mistakes

• Installing Coq before checking CompCert's requirements wastes time
• Multiple failed installation attempts consume significant resources
• Always read project requirements before installing dependencies

Memory Issues

• Coq proof checking is memory-intensive
• Container environments may have memory limits
• Swap creation may be restricted in some environments
• Sequential builds (-j1) use less memory than parallel builds

Environment Persistence

• opam environment must be sourced in each shell session
• eval $(opam env) needed before running opam-installed tools
• Consider setting up persistent environment configuration

Version Verification

• CompCert version reported at runtime may differ from release tag
• Version 3.13.1 source may report as "3.13" at runtime
• Verify functionality rather than relying solely on version strings

Verification Checklist

Before considering the task complete:

1. [ ] Binary exists at required location
2. [ ] ccomp --version executes without error
3. [ ] Simple C program compiles successfully
4. [ ] Generated executable runs correctly
5. [ ] Any linker warnings are understood (some are benign)

Resource Management

Cleanup Considerations

After successful build:

• Source tarballs can be removed
• Extracted source directories may be kept for reference or removed
• Build artifacts in source tree consume significant space

Security Notes

• Verify source downloads against official checksums when available
• Building from official release tarballs preferred over arbitrary commits
• Note and investigate any unexpected warnings during compilation