compile-compcert
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
configurescript for version requirements:grep -i "coq" configure - Review
READMEorINSTALLfiles 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
More from letta-ai/skills
extracting-pdf-text
Extract text from PDFs for LLM consumption. Use when processing PDFs for RAG, document analysis, or text extraction. Supports API services (Mistral OCR) and local tools (PyMuPDF, pdfplumber). Handles text-based PDFs, tables, and scanned documents with OCR.
257imessage
Send and read iMessages/SMS from macOS. Use for texting contacts, scheduling services, or automating message-based workflows. Triggers on queries about texting, messaging, SMS, iMessage, or contacting someone via text.
206video-processing
Guide for video analysis and frame-level event detection tasks using OpenCV and similar libraries. This skill should be used when detecting events in videos (jumps, movements, gestures), extracting frames, analyzing motion patterns, or implementing computer vision algorithms on video data. It provides verification strategies and helps avoid common pitfalls in video processing workflows.
189letta-api-client
Build applications with the Letta API — a model-agnostic, stateful API for building persistent agents with memory and long-term learning. Covers SDK patterns for Python and TypeScript. Includes 24 working code examples.
151google-workspace
Connect to Gmail and Google Calendar via OAuth 2.0. Use when users want to search/read emails, create drafts, search calendar events, check availability, or schedule meetings. Triggers on queries about email, inbox, calendar, schedule, or meetings.
127portfolio-optimization
Guidance for implementing high-performance portfolio optimization using Python C extensions. This skill applies when tasks require optimizing financial computations (matrix operations, covariance calculations, portfolio risk metrics) by implementing C extensions for Python. Use when performance speedup requirements exist (e.g., 1.2x or greater) and the task involves numerical computations on large datasets (thousands of assets).
101