Function mine_errors 

pub fn mine_errors(
    file: &LeanFile,
    source: &str,
    diagnostics: &[Diagnostic],
    project: &str,
    root: &Utf8Path,
) -> Vec<MineTask>

Mine error tasks from one file’s source plus its tracer diagnostics.

Each error diagnostic maps to the enclosing declaration (or the error line when no declaration is found). Diagnostics that share a span are de-duplicated so one broken declaration yields one task.