diff --git a/ide-lsp/src/main/java/org/aya/lsp/actions/LensMaker.java b/ide-lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
index 6509205c34..3926d2f62c 100644
--- a/ide-lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
+++ b/ide-lsp/src/main/java/org/aya/lsp/actions/LensMaker.java
@@ -1,9 +1,10 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.actions;
 
 import com.google.gson.Gson;
 import com.google.gson.JsonElement;
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import org.aya.cli.library.source.LibraryOwner;
@@ -22,10 +23,10 @@
 import java.util.List;
 
 public record LensMaker(
-  @NotNull SeqView<LibraryOwner> libraries,
+  @NotNull CollectionView<LibraryOwner> libraries,
   @NotNull MutableList<CodeLens> codeLens
 ) implements SyntaxDeclAction {
-  public static @NotNull List<CodeLens> invoke(@NotNull LibrarySource source, @NotNull SeqView<LibraryOwner> libraries) {
+  public static @NotNull List<CodeLens> invoke(@NotNull LibrarySource source, @NotNull CollectionView<LibraryOwner> libraries) {
     var maker = new LensMaker(libraries, MutableList.create());
     var program = source.program().get();
     if (program != null) program.forEach(maker);
diff --git a/ide-lsp/src/main/java/org/aya/lsp/actions/SymbolMaker.java b/ide-lsp/src/main/java/org/aya/lsp/actions/SymbolMaker.java
index 13325ae147..758100902d 100644
--- a/ide-lsp/src/main/java/org/aya/lsp/actions/SymbolMaker.java
+++ b/ide-lsp/src/main/java/org/aya/lsp/actions/SymbolMaker.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.actions;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.cli.library.source.LibraryOwner;
@@ -23,7 +24,7 @@ public interface SymbolMaker {
     return ProjectSymbol.invoke(options, source).map(SymbolMaker::documentSymbol);
   }
 
-  static @NotNull ImmutableSeq<WorkspaceSymbol> workspaceSymbols(@NotNull PrettierOptions options, @NotNull SeqView<LibraryOwner> libraries) {
+  static @NotNull ImmutableSeq<WorkspaceSymbol> workspaceSymbols(@NotNull PrettierOptions options, @NotNull CollectionView<LibraryOwner> libraries) {
     return ProjectSymbol.invoke(options, libraries).mapNotNull(SymbolMaker::workspaceSymbol);
   }
 
diff --git a/ide-lsp/src/main/java/org/aya/lsp/models/ProjectOrFile.java b/ide-lsp/src/main/java/org/aya/lsp/models/ProjectPath.java
similarity index 57%
rename from ide-lsp/src/main/java/org/aya/lsp/models/ProjectOrFile.java
rename to ide-lsp/src/main/java/org/aya/lsp/models/ProjectPath.java
index 618797f7ac..c4d1c467ae 100644
--- a/ide-lsp/src/main/java/org/aya/lsp/models/ProjectOrFile.java
+++ b/ide-lsp/src/main/java/org/aya/lsp/models/ProjectPath.java
@@ -3,18 +3,26 @@
 package org.aya.lsp.models;
 
 import org.aya.generic.Constants;
+import org.aya.util.FileUtil;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 import java.nio.file.Files;
 import java.nio.file.Path;
 
-public sealed interface ProjectOrFile {
-  /// @return null if {@param path} is neither represents an aya project nor an aya file
-  static @Nullable ProjectOrFile resolve(@NotNull Path path) {
+public sealed interface ProjectPath {
+  /// Resolve {@param path} to:
+  /// * {@link Project}, which represents an aya project ("aya.json" exists)
+  /// * {@link Directory}, which represents a normal directory (lack of "aya.json")
+  /// * {@link File}, which represents an aya file (with ".aya" pr ".aya.md" extension)
+  /// * null, which represents a normal file (unknown file type)
+  static @Nullable ProjectPath resolve(@NotNull Path path) {
+    path = FileUtil.canonicalize(path);
     if (Files.isDirectory(path)) {
       if (Files.exists(path.resolve(Constants.AYA_JSON))) {
         return new Project(path);
+      } else {
+        return new Directory(path);
       }
     } else {
       var fileName = path.getFileName().toString();
@@ -23,17 +31,21 @@ public sealed interface ProjectOrFile {
         // ^ never null, a file must belong to some directory
       } else if (fileName.endsWith(Constants.AYA_POSTFIX) || fileName.endsWith(Constants.AYA_LITERATE_POSTFIX)) {
         return new File(path);
+      } else {
+        return null;
       }
     }
-
-    return null;
   }
 
+  /// @return canonicalized path
   @NotNull Path path();
 
-  record Project(@Override @NotNull Path path) implements ProjectOrFile {
+  record Project(@Override @NotNull Path path) implements ProjectPath {
     public @NotNull Path ayaJsonPath() { return path.resolve(Constants.AYA_JSON); }
   }
 
-  record File(@Override @NotNull Path path) implements ProjectOrFile { }
+  record Directory(@Override @NotNull Path path) implements ProjectPath {
+  }
+
+  record File(@Override @NotNull Path path) implements ProjectPath { }
 }
diff --git a/ide-lsp/src/main/java/org/aya/lsp/server/AyaLanguageServer.java b/ide-lsp/src/main/java/org/aya/lsp/server/AyaLanguageServer.java
index fa0aa187b3..98a87fe6ca 100644
--- a/ide-lsp/src/main/java/org/aya/lsp/server/AyaLanguageServer.java
+++ b/ide-lsp/src/main/java/org/aya/lsp/server/AyaLanguageServer.java
@@ -3,10 +3,10 @@
 package org.aya.lsp.server;
 
 import com.google.gson.Gson;
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableMap;
 import kala.collection.immutable.ImmutableSeq;
-import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableMap;
 import kala.collection.mutable.MutableSet;
 import kala.control.Option;
@@ -59,7 +59,7 @@ public class AyaLanguageServer implements LanguageServer {
   private static final @NotNull CompilerFlags FLAGS = new CompilerFlags(CompilerFlags.Message.EMOJI, false, false, null, SeqView.empty(), null);
 
   private final BufferReporter reporter = new BufferReporter();
-  private final @NotNull MutableList<LibraryOwner> libraries = MutableList.create();
+  private final @NotNull MutableMap<Path, LibraryOwner> libraries = MutableMap.create();
   /**
    * When working with LSP, we need to track all previously created Primitives.
    * This is shared per library.
@@ -83,36 +83,50 @@ public AyaLanguageServer(@NotNull CompilerAdvisor advisor, @NotNull AyaLanguageC
     Log.init(this.client);
   }
 
-  public @NotNull SeqView<LibraryOwner> libraries() {
-    return libraries.view();
+  public @NotNull CollectionView<LibraryOwner> libraries() {
+    return libraries.valuesView();
   }
 
-  /// TODO: handle duplicate registering
-  ///
   /// @return the libraries that are actually loaded
-  public SeqView<LibraryOwner> registerLibrary(@NotNull Path path) {
+  public @NotNull SeqView<LibraryOwner> registerLibrary(@NotNull Path path) {
     Log.i("Adding library path %s", path);
-    var tryLoad = tryAyaLibrary(path);
-    if (tryLoad != null) return tryLoad;
-    return SeqView.narrow(mockLibraries(path).view());
+    var resolved = ProjectPath.resolve(path);
+    if (resolved == null) return SeqView.empty();
+
+    if (resolved instanceof ProjectPath.Project project) {
+      return tryAyaLibrary(project);
+    }
+
+    // resolved is Directory or File
+    return SeqView.narrow(mockLibraries(resolved.path()));
+  }
+
+  /// Check whether the project/the aya file {@param projectOrFile} represents is registered in this {@link AyaLanguageServer}.
+  public @Nullable LibraryOwner getRegisteredLibrary(@NotNull ProjectPath projectOrFile) {
+    return libraries.getOrNull(projectOrFile.path());
   }
 
-  private @Nullable SeqView<LibraryOwner> tryAyaLibrary(@NotNull Path path) {
-    var projectOrFile = ProjectOrFile.resolve(path);
-    if (!(projectOrFile instanceof ProjectOrFile.Project project)) return null;
-    return importAyaLibrary(project);
+  /// @apiNote requires the lock to {@link #libraries}
+  private @NotNull SeqView<LibraryOwner> tryAyaLibrary(@NotNull ProjectPath.Project path) {
+    var registered = getRegisteredLibrary(path);
+    if (registered != null) {
+      Log.i("Duplicated: %s", path.path());
+      return SeqView.of(registered);
+    }
+
+    return importAyaLibrary(path);
   }
 
   /// @param project a path to the directory that contains "aya.json"
-  /// @return null if the path needs to be "mocked", empty if the library fails to load (due to IO exceptions
+  /// @return empty if the library fails to load (due to IO exceptions
   /// or possibly malformed config files), and nonempty if successfully loaded.
-  private @Nullable SeqView<LibraryOwner> importAyaLibrary(@NotNull ProjectOrFile.Project project) {
-    var ayaJson = project.ayaJsonPath();
-    if (!Files.exists(ayaJson)) return null;
+  /// @apiNote requires the lock to {@link #libraries}
+  private @NotNull SeqView<LibraryOwner> importAyaLibrary(@NotNull ProjectPath.Project project) {
+    var projectPath = project.path();
     try {
-      var config = LibraryConfigData.fromLibraryRoot(project.path());
+      var config = LibraryConfigData.fromLibraryRoot(projectPath);
       var owner = DiskLibraryOwner.from(config);
-      libraries.append(owner);
+      libraries.put(projectPath, owner);
       return SeqView.of(owner);
     } catch (IOException e) {
       Log.e("Cannot load library. Stack trace:");
@@ -124,10 +138,13 @@ public SeqView<LibraryOwner> registerLibrary(@NotNull Path path) {
     return SeqView.empty();
   }
 
-  private ImmutableSeq<WsLibrary> mockLibraries(@NotNull Path path) {
-    var mocked = AyaFiles.collectAyaSourceFiles(path, 1).map(WsLibrary::mock);
-    libraries.appendAll(mocked);
-    return mocked;
+  /// @apiNote requires the lock to {@link #libraries}
+  private SeqView<WsLibrary> mockLibraries(@NotNull Path path) {
+    var mocked = AyaFiles.collectAyaSourceFiles(path, 1)
+      .map(f -> Tuple.of(f, WsLibrary.mock(f)));
+
+    mocked.forEach(libraries::put);
+    return mocked.view().map(Tuple2::component2);
   }
 
   @Override public void initialized() {
@@ -185,7 +202,7 @@ private void initializeOptions(@Nullable ServerOptions options) {
     var ayaJson = path.resolve(Constants.AYA_JSON);
     if (!Files.exists(ayaJson)) return findOwner(path.getParent());
     var book = MutableSet.<LibraryConfig>create();
-    for (var lib : libraries) {
+    for (var lib : libraries()) {
       var found = findOwner(book, lib, path);
       if (found != null) return found;
     }
@@ -214,7 +231,8 @@ private void initializeOptions(@Nullable ServerOptions options) {
   }
 
   public @Nullable LibrarySource find(@NotNull Path moduleFile) {
-    for (var lib : libraries) {
+    // TODO: check librarySrcRoot before find?
+    for (var lib : libraries()) {
       var found = find(lib, moduleFile);
       if (found != null) return found;
     }
@@ -274,7 +292,7 @@ private void clearProblems(@NotNull ImmutableSeq<ImmutableSeq<LibrarySource>> af
             case null -> {
               var mock = WsLibrary.mock(newSrc);
               Log.d("Created new file: %s, mocked a library %s for it", newSrc, mock.mockConfig().name());
-              libraries.append(mock);
+              libraries.put(newSrc, mock);
             }
             default -> { }
           }
@@ -285,7 +303,14 @@ private void clearProblems(@NotNull ImmutableSeq<ImmutableSeq<LibrarySource>> af
           Log.d("Deleted file: %s, removed from owner: %s", src.underlyingFile(), src.owner().underlyingLibrary().name());
           switch (src.owner()) {
             case MutableLibraryOwner owner -> owner.removeLibrarySource(src);
-            case WsLibrary owner -> libraries.removeIf(o -> o == owner);
+            case WsLibrary owner -> {
+              // TODO: how about `AyaLanguageServer#find` returns a tuple?
+              var key = libraries.keysView()
+                .find(t -> libraries.get(t) == owner)
+                .get();
+
+              libraries.remove(key);
+            }
             default -> { }
           }
         }
@@ -304,7 +329,7 @@ private void clearProblems(@NotNull ImmutableSeq<ImmutableSeq<LibrarySource>> af
   @Override public Optional<List<? extends GenericLocation>> gotoDefinition(TextDocumentPositionParams params) {
     var source = find(params.textDocument.uri);
     if (source == null) return Optional.empty();
-    return Optional.of(GotoDefinition.findDefs(source, libraries.view(), LspRange.pos(params.position)).mapNotNull(pos -> {
+    return Optional.of(GotoDefinition.findDefs(source, libraries(), LspRange.pos(params.position)).mapNotNull(pos -> {
       var from = pos.sourcePos();
       var to = pos.data();
       var res = LspRange.toLoc(from, to);
@@ -331,7 +356,7 @@ public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params)
     var source = find(params.textDocument.uri);
     if (source == null) return Optional.empty();
     return Optional.of(FindReferences
-      .findRefs(source, libraries.view(), LspRange.pos(params.position))
+      .findRefs(source, libraries(), LspRange.pos(params.position))
       .map(LspRange::toLoc)
       .collect(Collectors.toList()));
   }
@@ -339,7 +364,7 @@ public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params)
   @Override public WorkspaceEdit rename(RenameParams params) {
     var source = find(params.textDocument.uri);
     if (source == null) return null;
-    var renames = Rename.rename(source, params.newName, libraries.view(), LspRange.pos(params.position))
+    var renames = Rename.rename(source, params.newName, libraries(), LspRange.pos(params.position))
       .view()
       .flatMap(t -> t.sourcePos().file().underlying().map(f -> Tuple.of(f.toUri(), t)))
       .collect(Collectors.groupingBy(
@@ -377,7 +402,7 @@ public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params)
   @Override public List<CodeLens> codeLens(CodeLensParams params) {
     var source = find(params.textDocument.uri);
     if (source == null) return Collections.emptyList();
-    return LensMaker.invoke(source, libraries.view());
+    return LensMaker.invoke(source, libraries());
   }
 
   @Override public CodeLens resolveCodeLens(CodeLens codeLens) {
@@ -391,7 +416,7 @@ public Optional<SignatureHelp> signatureHelp(TextDocumentPositionParams params)
   }
 
   @Override public List<? extends GenericWorkspaceSymbol> workspaceSymbols(WorkspaceSymbolParams params) {
-    return SymbolMaker.workspaceSymbols(options, libraries.view()).asJava();
+    return SymbolMaker.workspaceSymbols(options, libraries()).asJava();
   }
 
   @Override
diff --git a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
index 0c8e9f5578..d08f32c2c7 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp;
 
@@ -6,8 +6,10 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.cli.render.RenderOptions;
 import org.aya.generic.Constants;
+import org.aya.lsp.models.ProjectPath;
 import org.aya.lsp.models.ServerOptions;
 import org.aya.lsp.models.ServerRenderOptions;
+import org.aya.lsp.server.AyaLanguageServer;
 import org.aya.lsp.tester.LspTestClient;
 import org.aya.lsp.tester.LspTestCompilerAdvisor;
 import org.aya.syntax.concrete.Pattern;
@@ -15,6 +17,7 @@
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
 import org.aya.syntax.core.term.MetaPatTerm;
 import org.aya.syntax.core.term.call.DataCall;
+import org.aya.util.FileUtil;
 import org.javacs.lsp.InitializeParams;
 import org.javacs.lsp.Position;
 import org.javacs.lsp.TextDocumentIdentifier;
@@ -24,19 +27,25 @@
 
 import java.nio.file.Path;
 
-import static org.aya.lsp.tester.TestCommand.compile;
-import static org.aya.lsp.tester.TestCommand.mutate;
+import static org.aya.lsp.tester.TestCommand.*;
 import static org.junit.jupiter.api.Assertions.*;
 
 public class LspTest {
-  public static final @NotNull Path TEST_LIB = Path.of("src", "test", "resources", "lsp-test-lib");
+  public static final @NotNull Path RES_DIR = FileUtil.canonicalize(Path.of("src", "test", "resources"));
+  public static final @NotNull Path TEST_LIB = RES_DIR.resolve("lsp-test-lib");
+  public static final @NotNull Path TEST_LIB0 = RES_DIR.resolve("lsp-test-lib0");
+  public static final @NotNull Path TEST_FILE = TEST_LIB0.resolve("unwatched.aya");
 
   public @NotNull LspTestClient launch(@NotNull Path libraryRoot) {
-    var client = new LspTestClient();
+    var client = launch();
     client.registerLibrary(libraryRoot);
     return client;
   }
 
+  public @NotNull LspTestClient launch() {
+    return new LspTestClient();
+  }
+
   @Test public void testJustLoad() {
     launch(TEST_LIB).execute(compile((_, _) -> {}));
   }
@@ -81,6 +90,26 @@ public class LspTest {
     );
   }
 
+  private void duplicateRegisterTester(int count, @NotNull ProjectPath check, @NotNull AyaLanguageServer lsp) {
+    assertEquals(count, lsp.libraries().size());
+    assertNotNull(lsp.getRegisteredLibrary(check));
+  }
+
+  @Test public void testDuplicateRegister() {
+
+    launch().execute(
+      register(TEST_LIB, (_, lsp) ->
+        duplicateRegisterTester(1, new ProjectPath.Project(TEST_LIB), lsp)),
+      register(TEST_LIB0.resolve(Constants.AYA_JSON), (_, lsp) ->
+        duplicateRegisterTester(2, new ProjectPath.Project(TEST_LIB0), lsp)),
+      // test dup here
+      register(TEST_LIB0, (_, lsp) ->
+        duplicateRegisterTester(2, new ProjectPath.Project(TEST_LIB0), lsp)),
+      register(TEST_FILE, (_, lsp) ->
+        duplicateRegisterTester(3, new ProjectPath.File(TEST_FILE), lsp))
+    );
+  }
+
   @Test public void colorful() {
     var initParams = new InitializeParams();
     initParams.initializationOptions = new Gson().toJsonTree(new ServerOptions(new ServerRenderOptions(null, null, RenderOptions.OutputTarget.HTML)));
diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestClient.java b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestClient.java
index a287761c67..99ca61c4d9 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestClient.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestClient.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.tester;
 
@@ -64,6 +64,10 @@ private void executeOne(@NotNull TestCommand cmd) {
         var elapsed = loadLibraries();
         c.checker().check(advisor, elapsed);
       }
+      case TestCommand.Register(var path, var checker) -> {
+        registerLibrary(path);
+        checker.check(advisor, service);
+      }
     }
   }
 
diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/TestCommand.java b/ide-lsp/src/test/java/org/aya/lsp/tester/TestCommand.java
index bb2e7cb0ca..137c548274 100644
--- a/ide-lsp/src/test/java/org/aya/lsp/tester/TestCommand.java
+++ b/ide-lsp/src/test/java/org/aya/lsp/tester/TestCommand.java
@@ -1,10 +1,13 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.lsp.tester;
 
 import kala.tuple.Unit;
+import org.aya.lsp.server.AyaLanguageServer;
 import org.jetbrains.annotations.NotNull;
 
+import java.nio.file.Path;
+
 public sealed interface TestCommand {
   @FunctionalInterface
   interface Checker<T> {
@@ -17,6 +20,8 @@ record Mutate(@NotNull String moduleName, @NotNull Checker<Unit> checker) implem
 
   record Compile(@NotNull Checker<Long> checker) implements TestCommand {}
 
+  record Register(@NotNull Path path, @NotNull Checker<AyaLanguageServer> checker) implements TestCommand { }
+
   static @NotNull Mutate mutate(@NotNull String moduleName, @NotNull Checker<Unit> checker) {
     return new Mutate(moduleName, checker);
   }
@@ -28,4 +33,8 @@ record Compile(@NotNull Checker<Long> checker) implements TestCommand {}
   static @NotNull Compile compile(@NotNull Checker<Long> checker) {
     return new Compile(checker);
   }
+
+  static @NotNull Register register(@NotNull Path path, Checker<AyaLanguageServer> checker) {
+    return new Register(path, checker);
+  }
 }
diff --git a/ide-lsp/src/test/resources/lsp-test-lib0/aya.json b/ide-lsp/src/test/resources/lsp-test-lib0/aya.json
new file mode 100644
index 0000000000..e84faa595b
--- /dev/null
+++ b/ide-lsp/src/test/resources/lsp-test-lib0/aya.json
@@ -0,0 +1,6 @@
+{
+  "ayaVersion" : "0.31",
+  "name" : "lsp-test-lib0",
+  "group" : "org.aya-prover",
+  "version" : "0.1.0"
+}
diff --git a/ide-lsp/src/test/resources/lsp-test-lib0/unwatched.aya b/ide-lsp/src/test/resources/lsp-test-lib0/unwatched.aya
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/ide/src/main/java/org/aya/ide/Resolver.java b/ide/src/main/java/org/aya/ide/Resolver.java
index d9aa9e77df..ac45cd1f13 100644
--- a/ide/src/main/java/org/aya/ide/Resolver.java
+++ b/ide/src/main/java/org/aya/ide/Resolver.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.ide;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import kala.control.Option;
@@ -88,7 +89,7 @@ public interface Resolver {
   }
 
   /** resolve a top-level module by its qualified name */
-  static @NotNull Option<LibrarySource> resolveModule(@NotNull SeqView<LibraryOwner> owners, @NotNull ModulePath module) {
+  static @NotNull Option<LibrarySource> resolveModule(@NotNull CollectionView<LibraryOwner> owners, @NotNull ModulePath module) {
     for (var owner : owners) {
       var found = resolveModule(owner, module);
       if (found.isDefined()) return found;
diff --git a/ide/src/main/java/org/aya/ide/action/FindReferences.java b/ide/src/main/java/org/aya/ide/action/FindReferences.java
index 4181e71ce8..2960d7b487 100644
--- a/ide/src/main/java/org/aya/ide/action/FindReferences.java
+++ b/ide/src/main/java/org/aya/ide/action/FindReferences.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.ide.action;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.mutable.MutableList;
 import org.aya.cli.library.source.LibraryOwner;
@@ -17,7 +18,7 @@
 public interface FindReferences {
   static @NotNull SeqView<SourcePos> findRefs(
     @NotNull LibrarySource source,
-    @NotNull SeqView<LibraryOwner> libraries, XY xy
+    @NotNull CollectionView<LibraryOwner> libraries, XY xy
   ) {
     var vars = Resolver.resolveVar(source, xy);
     return findRefs(vars.map(WithPos::data), libraries);
@@ -25,7 +26,7 @@ public interface FindReferences {
 
   static @NotNull SeqView<SourcePos> findRefs(
     @NotNull SeqView<AnyVar> vars,
-    @NotNull SeqView<LibraryOwner> libraries
+    @NotNull CollectionView<LibraryOwner> libraries
   ) {
     return vars.flatMap(var -> {
       var resolver = new Resolver.UsageResolver(var, MutableList.create());
@@ -43,7 +44,7 @@ public interface FindReferences {
 
   static @NotNull SeqView<SourcePos> findRefsOutsideDefs(
     @NotNull SeqView<AnyVar> vars,
-    @NotNull SeqView<LibraryOwner> libraries
+    @NotNull CollectionView<LibraryOwner> libraries
   ) {
     var defPos = vars.filterIsInstance(DefVar.class).map(def -> def.concrete.entireSourcePos());
     return findRefs(vars, libraries).filter(ref -> defPos.noneMatch(pos -> pos.containsIndex(ref)));
@@ -51,7 +52,7 @@ public interface FindReferences {
 
   static @NotNull SeqView<SourcePos> findOccurrences(
     @NotNull LibrarySource source,
-    @NotNull SeqView<LibraryOwner> libraries, XY xy
+    @NotNull CollectionView<LibraryOwner> libraries, XY xy
   ) {
     var defs = GotoDefinition.findDefs(source, libraries, xy).map(WithPos::data);
     var refs = FindReferences.findRefs(source, libraries, xy);
diff --git a/ide/src/main/java/org/aya/ide/action/GotoDefinition.java b/ide/src/main/java/org/aya/ide/action/GotoDefinition.java
index df3c02eecd..28bc0a0e8e 100644
--- a/ide/src/main/java/org/aya/ide/action/GotoDefinition.java
+++ b/ide/src/main/java/org/aya/ide/action/GotoDefinition.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.ide.action;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import org.aya.cli.library.source.LibraryOwner;
 import org.aya.cli.library.source.LibrarySource;
@@ -23,7 +24,7 @@
 public interface GotoDefinition {
   static @NotNull SeqView<WithPos<SourcePos>> findDefs(
     @NotNull LibrarySource source,
-    @NotNull SeqView<LibraryOwner> libraries, XY xy
+    @NotNull CollectionView<LibraryOwner> libraries, XY xy
   ) {
     return Resolver.resolveVar(source, xy).mapNotNull(pos -> {
       var from = pos.sourcePos();
@@ -39,7 +40,7 @@ public interface GotoDefinition {
     });
   }
 
-  private static @Nullable SourcePos mockSourcePos(@NotNull SeqView<LibraryOwner> libraries, @NotNull ModuleVar moduleVar) {
+  private static @Nullable SourcePos mockSourcePos(@NotNull CollectionView<LibraryOwner> libraries, @NotNull ModuleVar moduleVar) {
     return Resolver.resolveModule(libraries, new ModulePath(moduleVar.path().ids()))
       .map(src -> src.originalFile(""))
       .map(src -> new SourcePos(src, 0, 0, 1, 0, 1, 0))
diff --git a/ide/src/main/java/org/aya/ide/action/ProjectSymbol.java b/ide/src/main/java/org/aya/ide/action/ProjectSymbol.java
index d49ea0dc68..90e67f661e 100644
--- a/ide/src/main/java/org/aya/ide/action/ProjectSymbol.java
+++ b/ide/src/main/java/org/aya/ide/action/ProjectSymbol.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.ide.action;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
@@ -30,7 +31,7 @@ public record ProjectSymbol(
     return symbol.symbols.toImmutableSeq();
   }
 
-  public static @NotNull ImmutableSeq<Symbol> invoke(@NotNull PrettierOptions options, @NotNull SeqView<LibraryOwner> libraries) {
+  public static @NotNull ImmutableSeq<Symbol> invoke(@NotNull PrettierOptions options, @NotNull CollectionView<LibraryOwner> libraries) {
     var symbol = new ProjectSymbol(options, MutableList.create());
     libraries.forEach(symbol::collectLib);
     return symbol.symbols.toImmutableSeq();
diff --git a/ide/src/main/java/org/aya/ide/action/Rename.java b/ide/src/main/java/org/aya/ide/action/Rename.java
index aea4b12f8c..85dec64eee 100644
--- a/ide/src/main/java/org/aya/ide/action/Rename.java
+++ b/ide/src/main/java/org/aya/ide/action/Rename.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.ide.action;
 
+import kala.collection.CollectionView;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Option;
@@ -23,7 +24,7 @@ public interface Rename {
   static @NotNull ImmutableSeq<RenameEdit> rename(
     @NotNull LibrarySource source,
     @NotNull String newName,
-    @NotNull SeqView<LibraryOwner> libraries, XY xy
+    @NotNull CollectionView<LibraryOwner> libraries, XY xy
   ) {
     return FindReferences.findOccurrences(source, libraries, xy)
       .map(to -> new RenameEdit(to, newName))