ToolsTools Automatic Proof Search (Auto) UsageLimitationsUser feedback Command-line options Command-line optionsCommand-line and pragma optionsWarningsCommand-line examplesChecking options for consistency Compilers BackendsOptimizations Emacs Mode MenusConfigurationKeybindingsUnicode inputBackground highlighting Literate Programming Literate TeXLiterate reStructuredTextLiterate Markdown and TypstLiterate Org Generating HTML Options Generating LaTeX Known pitfalls and issuesOptionsQuicker generation without typecheckingFeaturesExamples Interface files StorageCompilation Library Management Example: Using the standard libraryLibrary filesThe .agda-lib files associated to a given Agda fileInstalling librariesUsing a libraryDefault librariesVersion numbersUpgrading Performance debugging Measuring typechecking performanceMeasuring run-time performance Search Definitions in Scope Usage