  This is an overview of the Isabelle technology behind the Archive of Formal
Proofs (AFP). Interactive development and quasi-interactive build jobs impose
significant demands of scalability on the logic (usually Isabelle/HOL), on
Isabelle/ML for mathematical tool implementation, and on Isabelle/Scala for
physical system integration --- all integrated in Isabelle/PIDE (the Prover
IDE). Continuous growth of AFP has demanded continuous improvements of Isabelle
performance. This is a report on the situation in Isabelle2019 (June 2019),
with notable add-ons like prover session exports and headless PIDE for
automated updates based on semantic information. An example application is
Isabelle/MMT, which is able to turn all of Isabelle + AFP into OMDoc and RDF
triples, but it is straight-forward to reuse the Isabelle technology for other
applications.
