Skip to content

Conversation

@NicolasRouquette
Copy link
Contributor

This PR introduces an optional SourceLinkerFn parameter to htmlOutputResults and htmlOutput, enabling custom source linking logic instead of relying solely on the default URL-based linker.

Motivation

The current doc-gen4 implementation computes source links internally using a fixed algorithm based on sourceUrl?. While this works well for standard GitHub repositories, some use cases require more sophisticated source linking:

  • Multi-repository documentation - Projects that aggregate documentation from multiple repositories need different base URLs for different modules
  • Custom hosting platforms - Source code hosted on platforms with non-standard URL patterns
  • Monorepo support - Projects where different modules map to different subdirectories
  • Integration with other tools - I'm developing a doc-gen4 "plugin" that combines doc-gen4 with additional documentation where I need to customize source URL generation.

New type alias:

abbrev SourceLinkerFn := Option String → Name → Option DeclarationRange → String

Updated signatures:

def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) 
    (sourceUrl? : Option String) (sourceLinker? : Option SourceLinkerFn := none) : IO (Array System.FilePath)

def htmlOutput (buildDir : System.FilePath) (result : AnalyzerResult) (hierarchy : Hierarchy)
    (sourceUrl? : Option String) (sourceLinker? : Option SourceLinkerFn := none) : IO Unit

Backward Compatibility

  • The new sourceLinker? parameter defaults to none, preserving existing behavior
  • When sourceLinker? is none, the existing SourceLinker.sourceLinker is used
  • All existing code calling these functions without the new parameter continues to work unchanged

Example usage:

-- Custom source linker that handles multiple repositories
def mySourceLinker : SourceLinkerFn := fun _sourceUrl? module range =>
  let root := module.getRoot
  let baseUrl := if root == `MyLib then "https://github.com/org/mylib" 
                 else "https://github.com/org/other"
  -- ... compute URL with line range
  s!"{baseUrl}/blob/main/{path}#L{startLine}-L{endLine}"

-- Use custom linker
DocGen4.htmlOutputResults baseConfig result none (some mySourceLinker)

Introduces an optional SourceLinkerFn parameter to allow custom source linking logic instead of only using the default URL-based linker.

This enables more flexible source code linking by accepting a function that maps module names and declaration ranges to URLs.
Updates SourceLinkerFn signature to accept an optional source URL parameter, allowing custom source linkers to utilize the same URL configuration as the default linker. This provides more flexibility for custom implementations.
@hargoniX hargoniX merged commit cc1a619 into leanprover:main Jan 8, 2026
1 check passed
@NicolasRouquette NicolasRouquette deleted the feat/source-linker branch January 16, 2026 15:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants