Skip to content

Replace single-file tracking with whole-project type-checking#241

Open
Russoul wants to merge 1 commit into
idris-community:mainfrom
Russoul:chip-in
Open

Replace single-file tracking with whole-project type-checking#241
Russoul wants to merge 1 commit into
idris-community:mainfrom
Russoul:chip-in

Conversation

@Russoul

@Russoul Russoul commented Mar 6, 2025

Copy link
Copy Markdown
Member

Summary

  • Whole-project type-checking: loadURI now invokes check pkg (full project build via the .ipkg file) instead of buildDeps on a single file. On success, the main module's TTM is reloaded into a clean context.
  • ipkgPath config option: Clients can supply the path to the .ipkg file via the ipkgPath workspace setting. If unset, findIpkgFile is used as a fallback.
  • Metadata loading decoupled from type-checking: withURI no longer triggers a re-type-check per request — it loads metadata from the pre-built TTM file directly, making hover/definition/highlight responses much faster.
  • Project-wide diagnostics: sendDiagnostics now groups errors by source file and publishes per-file diagnostic notifications across the whole project. Previously issued diagnostics are cleared before each new build.
  • Remove openFile / loadIfNeeded: The single-file tracking field and the "only re-check if the file changed" guard are removed; the server always operates on the full project.
  • Remove URI guards: The "request URI must match the currently open file" checks in Definition, DocumentHighlight, and DocumentSymbol handlers are dropped — they are no longer meaningful in a project-wide model.

@Russoul
Russoul force-pushed the chip-in branch 3 times, most recently from 7884970 to 85247cd Compare May 22, 2026 16:02
@Russoul
Russoul marked this pull request as ready for review May 22, 2026 16:02
@Russoul Russoul changed the title Chip in Replace single-file tracking with whole-project type-checking May 22, 2026
- Remove the `openFile` field and `loadIfNeeded` logic; add `ipkgPath`
  config option so the server knows which .ipkg to use
- `loadURI` now builds the full project via `check pkg` instead of
  `buildDeps`, then reloads the main module's TTM on success
- `withURI` loads metadata from TTM directly without re-type-checking
- `sendDiagnostics` now groups errors by source file and sends per-file
  diagnostics across the whole project; clears stale diagnostics first
- Drop the "must match currently open file" guard from Definition,
  DocumentHighlight, and DocumentSymbol handlers
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.

1 participant