To run, purely functional programs verified using interactive theorem provers (ITPs) typically need to be extracted: either to a similar language (like Coq to OCaml) or by proving equivalence with a deeply embedded implementation (like a C program). Traditionally, the first approach was unverified but automated, and the second verified but manual. More recently, advances in extraction have achieved automated extraction, with proofs. We introduce the unifying framework of \emph{relational compilation} to capture and extend these recent developments, and develop it through a series of examples, with a novel focus on sound extensibility. This culminates with the presentation of Rupicola, a proof-producing compiler-construction toolkit focused on automatically deriving fast, low-level code from purely functional models. We present novel solutions to loop-invariant inference and genericity in kinds of side effects. Overall, Rupicola is unique in its combination of modularity and extensibility, foundational proofs, and low-level performance. We demonstrate these achievements through a combination of case studies and performance benchmarks that highlight how little effort is required to extend Rupicola and how easy it makes it to generate low-level code with performance on par with that of handwritten C programs.