Skip to content

indexer: open files with FILE_SHARE_DELETE on Windows - #51

Merged
Kristof Roomp (mcroomp) merged 1 commit into
mainfrom
indexer-shared-delete-open
May 27, 2026
Merged

indexer: open files with FILE_SHARE_DELETE on Windows#51
Kristof Roomp (mcroomp) merged 1 commit into
mainfrom
indexer-shared-delete-open

Conversation

@mcroomp

Copy link
Copy Markdown
Contributor

Summary

On Windows, \open()\ acquires an exclusive delete lock on the file, which prevents deletion or renaming while the indexer holds the handle open. This causes friction when a developer deletes or renames a source file that happens to be mid-index.

Change

Adds a _open_shared()\ helper in \indexserver/indexer.py\ that uses \CreateFileW\ with \FILE_SHARE_READ | FILE_SHARE_WRITE | FILE_SHARE_DELETE\ on Windows. On other platforms it falls back to plain \open().

Both file-read callsites now use it:

  • \�uild_document()\ -- source file read for indexing
  • .gitignore\ reader in \walk_source_files()\

Tests

All 1146 existing tests pass.

Use CreateFileW with FILE_SHARE_DELETE so that files being read
during indexing do not block deletion or renaming on Windows.

Adds _open_shared() helper that calls CreateFileW with
FILE_SHARE_READ | FILE_SHARE_WRITE | FILE_SHARE_DELETE on Windows
and falls back to plain open() on other platforms.

Both callsites in build_document (source file reads) and the
.gitignore reader in walk_source_files now use _open_shared().
@mcroomp
Kristof Roomp (mcroomp) merged commit 87c9f46 into main May 27, 2026
7 checks passed
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