diff --git a/src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt b/src/main/kotlin/org/arend/module/AllArendFilesScope.kt
similarity index 53%
rename from src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt
rename to src/main/kotlin/org/arend/module/AllArendFilesScope.kt
index 68a7c14d1..b9d2cd8b0 100644
--- a/src/main/kotlin/org/arend/module/AllArendFilesAndPackagesScope.kt
+++ b/src/main/kotlin/org/arend/module/AllArendFilesScope.kt
@@ -4,7 +4,6 @@ import com.intellij.openapi.components.service
 import com.intellij.openapi.vfs.VfsUtilCore
 import com.intellij.openapi.vfs.VirtualFile
 import com.intellij.openapi.vfs.VirtualFileVisitor
-import com.intellij.psi.PsiFileSystemItem
 import com.intellij.psi.PsiManager
 import org.arend.ext.module.ModulePath
 import org.arend.module.config.LibraryConfig
@@ -14,15 +13,14 @@ import org.arend.prelude.Prelude
 import org.arend.psi.ArendFile
 import org.arend.psi.ext.PsiModuleReferable
 import org.arend.typechecking.TypeCheckingService
-import org.arend.typechecking.execution.TypecheckRunConfigurationProducer.Companion.TEST_PREFIX
 import org.arend.util.FileUtils
 import org.arend.util.getRelativePath
 
-class AllArendFilesAndPackagesScope(
-    val libraryConfig: LibraryConfig,
+class AllArendFilesScope(
+    private val libraryConfig: LibraryConfig,
     private val extraPath: ModulePath = ModulePath(),
-    private val withPrelude: Boolean = true,
-    private val withArendExtension: Boolean = true
+    private val isTest: Boolean = false,
+    private val withPrelude: Boolean = true
 ) : Scope {
     override fun getElements(): Collection<Referable> {
         val result = ArrayList<Referable>()
@@ -30,18 +28,22 @@ class AllArendFilesAndPackagesScope(
         val srcDir = libraryConfig.sourcesDirFile
         val testDir = libraryConfig.testsDirFile
 
-        if (extraPath.size() == 0) {
-            srcDir?.let { addArendFiles(it, it, result) }
-            testDir?.let { addArendFiles(it, it.parent, result) }
-        } else if (extraPath.firstName == TEST_PREFIX) {
-            val dir = LibraryConfig.findArendFileOrDirectoryByModulePath(testDir, ModulePath(extraPath.toList().subList(1, extraPath.size())))
-            dir?.let { addArendFiles(it, it, result) }
+        val dir = if (extraPath.size() == 0) {
+            if (isTest) {
+                testDir
+            } else {
+                srcDir
+            }
         } else {
-            val dir = LibraryConfig.findArendFileOrDirectoryByModulePath(srcDir, extraPath)
-            dir?.let { addArendFiles(it, it, result) }
+            if (isTest) {
+                LibraryConfig.findArendFileOrDirectoryByModulePath(testDir, extraPath)
+            } else {
+                LibraryConfig.findArendFileOrDirectoryByModulePath(srcDir, extraPath)
+            }
         }
+        dir?.let { addArendFiles(it, result) }
 
-        if (withPrelude) {
+        if (withPrelude && !isTest) {
             val psiManager = PsiManager.getInstance(libraryConfig.project)
             libraryConfig.project.service<TypeCheckingService>().prelude?.let { psiManager.findFile(it.virtualFile) }?.let {
                 result.add(PsiModuleReferable(listOf(it), Prelude.MODULE_PATH))
@@ -50,17 +52,13 @@ class AllArendFilesAndPackagesScope(
         return result
     }
 
-    private fun addArendFiles(root: VirtualFile, startFile: VirtualFile, result: MutableList<Referable>) {
+    private fun addArendFiles(root: VirtualFile, result: MutableList<Referable>) {
         val psiManager = PsiManager.getInstance(libraryConfig.project)
         val virtualFileVisitor = object : VirtualFileVisitor<Any>() {
             override fun visitFile(file: VirtualFile): Boolean {
                 val psiFile = psiManager.findFile(file)
                 if (psiFile is ArendFile) {
-                    result.add(createPsiModuleReferable(psiFile, root, startFile))
-                }
-                val psiDirectory = psiManager.findDirectory(file)
-                if (psiDirectory != null) {
-                    result.add(createPsiModuleReferable(psiDirectory, root, startFile))
+                    result.add(createPsiModuleReferable(psiFile, root))
                 }
                 return true
             }
@@ -68,16 +66,9 @@ class AllArendFilesAndPackagesScope(
         VfsUtilCore.visitChildrenRecursively(root, virtualFileVisitor)
     }
 
-    private fun createPsiModuleReferable(psiItem: PsiFileSystemItem, root: VirtualFile, startFile: VirtualFile): PsiModuleReferable {
-        val listPath = startFile.getRelativePath(psiItem.virtualFile, if (withArendExtension) FileUtils.EXTENSION else "")
-            ?.apply {
-                if (root != startFile) {
-                    if (size > 1) {
-                        set(0, TEST_PREFIX)
-                    }
-                }
-            }
-        return object : PsiModuleReferable(listOf(psiItem), ModulePath(listPath ?: emptyList())) {
+    private fun createPsiModuleReferable(file: ArendFile, root: VirtualFile): PsiModuleReferable {
+        val listPath = root.getRelativePath(file.virtualFile, FileUtils.EXTENSION)
+        return object : PsiModuleReferable(listOf(file), ModulePath(listPath ?: emptyList())) {
             override fun textRepresentation(): String {
                 val fullName = listPath?.joinToString(".") ?: ""
                 return fullName
@@ -87,5 +78,5 @@ class AllArendFilesAndPackagesScope(
 
     override fun getElements(kind: Referable.RefKind?): Collection<Referable> = if (kind == null || kind == Referable.RefKind.EXPR) elements else emptyList()
 
-    override fun resolveNamespace(name: String, onlyInternal: Boolean) = AllArendFilesAndPackagesScope(libraryConfig, ModulePath(extraPath.toList() + name), false, withArendExtension)
+    override fun resolveNamespace(name: String, onlyInternal: Boolean) = AllArendFilesScope(libraryConfig, ModulePath(extraPath.toList() + name), isTest, false)
 }
diff --git a/src/main/kotlin/org/arend/module/AllModulesScope.kt b/src/main/kotlin/org/arend/module/AllModulesScope.kt
index 8f40f1bdf..bc62672c6 100644
--- a/src/main/kotlin/org/arend/module/AllModulesScope.kt
+++ b/src/main/kotlin/org/arend/module/AllModulesScope.kt
@@ -4,10 +4,8 @@ import com.intellij.openapi.project.Project
 import com.intellij.openapi.roots.ModuleRootManager
 import com.intellij.psi.PsiManager
 import org.arend.ext.module.ModulePath
-import org.arend.naming.reference.ModuleReferable
 import org.arend.naming.reference.Referable
 import org.arend.naming.scope.Scope
-import org.arend.prelude.Prelude.MODULE_PATH
 import org.arend.psi.ext.PsiModuleReferable
 import org.arend.util.allModules
 
@@ -20,7 +18,6 @@ class AllModulesScope(private val project: Project) : Scope {
             val psiModuleFile = psiManager.findDirectory(moduleFile) ?: return@forEach
             result.add(PsiModuleReferable(listOf(psiModuleFile), ModulePath(listOf(it.name))))
         }
-        result.add(ModuleReferable(MODULE_PATH))
         return result
     }
 
diff --git a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt
index 8cf606bf7..60c08b55a 100644
--- a/src/main/kotlin/org/arend/module/config/LibraryConfig.kt
+++ b/src/main/kotlin/org/arend/module/config/LibraryConfig.kt
@@ -157,37 +157,6 @@ abstract class LibraryConfig(val project: Project) {
                 findArendFile(modulePath, false) ?: if (withTests) findArendFile(modulePath, true) else null
         }
 
-    fun getArendDirectoryOrFile(modulePath: ModulePath, isTest: Boolean): PsiFileSystemItem? {
-        val psiManager = PsiManager.getInstance(project)
-        return if (modulePath.size() == 0) {
-            if (isTest) {
-                psiManager.findDirectory(testsDirFile!!)
-            } else {
-                psiManager.findDirectory(sourcesDirFile!!)
-            }
-        } else {
-            getArendSubdirectoryOrFile(modulePath, isTest)
-        }
-    }
-
-    fun getArendSubdirectoryOrFile(modulePath: ModulePath, isTest: Boolean): PsiFileSystemItem? {
-        val psiManager = PsiManager.getInstance(project)
-        if (modulePath == MODULE_PATH) {
-            return project.service<TypeCheckingService>().prelude
-        }
-        return if (isTest) {
-            (findArendFileOrDirectoryByModulePath(testsDirFile, modulePath) ?:
-                findArendFileOrDirectoryByModulePath(sourcesDirFile, modulePath))?.let {
-                    psiManager.findDirectory(it) ?: psiManager.findFile(it)
-            } ?: findArendFile(modulePath, withAdditional = false, withTests = true)
-        } else {
-            (findArendFileOrDirectoryByModulePath(sourcesDirFile, modulePath) ?:
-                findArendFileOrDirectoryByModulePath(testsDirFile, modulePath))?.let {
-                psiManager.findDirectory(it) ?: psiManager.findFile(it)
-            } ?: findArendFile(modulePath, withAdditional = false, withTests = true)
-        }
-    }
-
     fun findArendFileOrDirectory(modulePath: ModulePath, withAdditional: Boolean, withTests: Boolean): PsiFileSystemItem? {
         if (modulePath.size() == 0) {
             return findArendDirectory(modulePath)
@@ -275,13 +244,10 @@ abstract class LibraryConfig(val project: Project) {
             val path = modulePath.toList()
             var curElement = root
             for (index in path.indices) {
-                if (index == path.indices.last - 1 && path[index + 1] == EXTENSION.drop(1)) {
-                    curElement = curElement?.findChild(path[index] + EXTENSION)
-                    break
-                } else if (index == path.indices.last) {
-                    curElement = curElement?.findChild(path[index]) ?: curElement?.findChild(path[index] + EXTENSION)
+                curElement = if (index == path.indices.last) {
+                    curElement?.findChild(path[index]) ?: curElement?.findChild(path[index] + EXTENSION)
                 } else {
-                    curElement = curElement?.findChild(path[index])
+                    curElement?.findChild(path[index])
                 }
             }
             return curElement
diff --git a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt
index 8e9592609..75eb2d206 100644
--- a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt
+++ b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt
@@ -23,7 +23,7 @@ import com.intellij.util.Alarm
 import org.arend.ArendFileTypeInstance
 import org.arend.codeInsight.ArendCodeInsightUtils
 import org.arend.ext.module.ModulePath
-import org.arend.module.AllArendFilesAndPackagesScope
+import org.arend.module.AllArendFilesScope
 import org.arend.module.config.ArendModuleConfigService
 import org.arend.naming.reference.Referable
 import org.arend.naming.scope.EmptyScope
@@ -75,7 +75,7 @@ class ArendMoveMembersDialog(project: Project,
         }
 
         val containingFile = container.containingFile as? ArendFile
-        val globalScope = containingFile?.libraryConfig?.let { AllArendFilesAndPackagesScope(it) } ?: EmptyScope.INSTANCE
+        val globalScope = containingFile?.libraryConfig?.let { AllArendFilesScope(it) } ?: EmptyScope.INSTANCE
 
         targetFileField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.modulePath?.toString() ?: "", null, customScopeGetter = { globalScope })), project, ArendFileTypeInstance)
         targetModuleField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.longName?.toString() ?: "", null, customScopeGetter = {
diff --git a/src/main/kotlin/org/arend/resolving/ArendReference.kt b/src/main/kotlin/org/arend/resolving/ArendReference.kt
index 68c2a0274..415050310 100644
--- a/src/main/kotlin/org/arend/resolving/ArendReference.kt
+++ b/src/main/kotlin/org/arend/resolving/ArendReference.kt
@@ -10,8 +10,6 @@ import org.arend.codeInsight.completion.ReplaceInsertHandler
 import org.arend.core.definition.Definition
 import org.arend.error.DummyErrorReporter
 import org.arend.ext.module.ModulePath
-import org.arend.module.AREND_LIB
-import org.arend.module.AllArendFilesAndPackagesScope
 import org.arend.naming.reference.*
 import org.arend.naming.reference.Referable.RefKind
 import org.arend.naming.reference.converter.ReferableConverter
@@ -26,7 +24,6 @@ import org.arend.psi.ext.*
 import org.arend.psi.ext.ArendDefMeta
 import org.arend.psi.ext.ReferableBase
 import org.arend.refactoring.ArendNamesValidator
-import org.arend.refactoring.move.ArendLongNameCodeFragment
 import org.arend.term.abs.Abstract
 import org.arend.term.abs.ConcreteBuilder
 import org.arend.term.concrete.Concrete
@@ -136,25 +133,6 @@ abstract class ArendReferenceBase<T : ArendReferenceElement>(element: T, range:
                     when (module) {
                         null -> LookupElementBuilder.create(ref, ref.path.toString()).withIcon(ArendIcons.DIRECTORY)
                         is ArendFile -> LookupElementBuilder.create(module, ref.path.toString()).withIcon(ArendIcons.AREND_FILE)
-                        is PsiDirectory -> {
-                            val libraryConfig = ((containingFile as? ArendLongNameCodeFragment?)?.scope as? AllArendFilesAndPackagesScope?)?.libraryConfig
-                            if (ref is PsiModuleReferable) {
-                                if (ref.modulePath.size() == 0 || (ref.modulePath.size() == 1 && ref.modulePath.firstName == libraryConfig?.testsDirFile?.name)) {
-                                    if (libraryConfig?.sourcesDirFile == module.virtualFile ||
-                                            (libraryConfig?.testsDirFile == module.virtualFile && ref.modulePath.size() != 0)) {
-                                        LookupElementBuilder.create(module, module.name).withIcon(module.getIcon(0))
-                                    } else {
-                                        null
-                                    }
-                                } else if (ref.toString() == AREND_LIB) {
-                                    LookupElementBuilder.create(module, ref.modulePath.toString()).withIcon(ArendIcons.AREND)
-                                } else {
-                                    LookupElementBuilder.create(module, ref.modulePath.toString()).withIcon(ArendIcons.DIRECTORY)
-                                }
-                            } else {
-                                LookupElementBuilder.create(ref, ref.path.toString()).withIcon(ArendIcons.DIRECTORY)
-                            }
-                        }
                         else -> LookupElementBuilder.createWithIcon(module)
                     }
                 }
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckCommand.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckCommand.kt
index e714ad061..7503df126 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckCommand.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckCommand.kt
@@ -2,6 +2,7 @@ package org.arend.typechecking.execution
 
 data class TypeCheckCommand(
     val library: String = "",
+    val isTest: Boolean = false,
     val modulePath: String = "",
     val definitionFullName: String = ""
 )
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
index e0d617d27..412a3f77e 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
@@ -39,10 +39,8 @@ import org.arend.term.concrete.Concrete
 import org.arend.typechecking.*
 import org.arend.typechecking.error.ParserError
 import org.arend.typechecking.error.TypecheckingErrorReporter
-import org.arend.typechecking.execution.TypecheckRunConfigurationProducer.Companion.TEST_PREFIX
 import org.arend.typechecking.order.Ordering
 import org.arend.typechecking.order.listener.CollectingOrderingListener
-import org.arend.util.FileUtils.EXTENSION
 import org.arend.util.afterTypechecking
 import org.jetbrains.ide.PooledThreadExecutor
 import java.io.OutputStream
@@ -122,36 +120,22 @@ class TypeCheckProcessHandler(
                         }
 
                         val modulePaths = if (modulePath == null) library.loadedModules else listOf(modulePath)
-                        val modules = modulePaths.flatMap {
-                            var newModulePath = it
-                            val isTest = (newModulePath.firstName == TEST_PREFIX && newModulePath.toList().getOrNull(1) != EXTENSION.drop(1)) ||
-                                    (newModulePath.size() == 1 && newModulePath.firstName == library.config.testsDirFile?.name)
-                            val isSource = newModulePath.firstName == library.config.sourcesDirFile?.name
-                            if (isTest || isSource) {
-                                newModulePath = ModulePath(newModulePath.toList().subList(1, newModulePath.size()))
-                            }
-                            val items = when (val fileItem = library.config.getArendDirectoryOrFile(newModulePath, isTest)) {
-                                is ArendFile -> listOf(fileItem)
-                                is PsiDirectory -> getAllFilesInDirectory(fileItem)
-                                else -> {
-                                    typecheckingErrorReporter.report(LibraryError.moduleNotFound(newModulePath, library.name))
-                                    emptyList()
-                                }
-                            }
-                             for (module in items) {
-                                if (command.definitionFullName == "") {
-                                    val sourcesModuleScopeProvider = typeCheckerService.libraryManager.getAvailableModuleScopeProvider(library)
-                                    val moduleScopeProvider = if (module.moduleLocation?.locationKind == ModuleLocation.LocationKind.TEST) {
-                                        val testsModuleScopeProvider = library.testsModuleScopeProvider
-                                        ModuleScopeProvider { modulePath ->
-                                            sourcesModuleScopeProvider.forModule(modulePath)
-                                                ?: testsModuleScopeProvider.forModule(modulePath)
-                                        }
-                                    } else sourcesModuleScopeProvider
-                                    DefinitionResolveNameVisitor(concreteProvider, ArendReferableConverter, typecheckingErrorReporter).resolveGroup(module, ScopeFactory.forGroup(module, moduleScopeProvider))
-                                }
+                        val modules = modulePaths.mapNotNull {
+                            val module = library.config.findArendFile(it, withAdditional = false, withTests = command.isTest)
+                            if (module == null) {
+                                typecheckingErrorReporter.report(LibraryError.moduleNotFound(it, library.name))
+                            } else if (command.definitionFullName == "") {
+                                val sourcesModuleScopeProvider = typeCheckerService.libraryManager.getAvailableModuleScopeProvider(library)
+                                val moduleScopeProvider = if (module.moduleLocation?.locationKind == ModuleLocation.LocationKind.TEST) {
+                                    val testsModuleScopeProvider = library.testsModuleScopeProvider
+                                    ModuleScopeProvider { modulePath ->
+                                        sourcesModuleScopeProvider.forModule(modulePath)
+                                            ?: testsModuleScopeProvider.forModule(modulePath)
+                                    }
+                                } else sourcesModuleScopeProvider
+                                DefinitionResolveNameVisitor(concreteProvider, ArendReferableConverter, typecheckingErrorReporter).resolveGroup(module, ScopeFactory.forGroup(module, moduleScopeProvider))
                             }
-                            items
+                            module
                         }
 
                         if (command.definitionFullName == "") {
@@ -220,15 +204,6 @@ class TypeCheckProcessHandler(
         }
     }
 
-    private fun getAllFilesInDirectory(directory: PsiDirectory): List<ArendFile> {
-        val arendFiles = mutableListOf<ArendFile>()
-        for (subDir in directory.subdirectories) {
-            arendFiles.addAll(getAllFilesInDirectory(subDir))
-        }
-        arendFiles.addAll(directory.files.filterIsInstance<ArendFile>())
-        return arendFiles
-    }
-
     private fun resetGroup(group: ArendGroup) {
         if (indicator.isCanceled) {
             return
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt
index 47868ae0b..f2616c079 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt
@@ -6,11 +6,12 @@ import com.intellij.openapi.options.SettingsEditor
 import com.intellij.openapi.project.Project
 import com.intellij.psi.PsiDocumentManager
 import com.intellij.ui.EditorTextField
+import com.intellij.ui.components.JBCheckBox
 import com.intellij.ui.dsl.builder.panel
 import org.arend.ArendFileTypeInstance
 import org.arend.definition.ArendFileDefinitionScope
 import org.arend.ext.module.ModulePath
-import org.arend.module.AllArendFilesAndPackagesScope
+import org.arend.module.AllArendFilesScope
 import org.arend.module.AllModulesScope
 import org.arend.module.ArendPreludeLibrary.Companion.PRELUDE
 import org.arend.module.ArendPreludeScope
@@ -21,18 +22,21 @@ import org.arend.psi.ext.PsiModuleReferable
 import org.arend.refactoring.move.ArendLongNameCodeFragment
 import org.arend.typechecking.TypeCheckingService
 import org.arend.typechecking.execution.configurations.TypeCheckConfiguration
-import org.arend.util.FileUtils
 import org.arend.util.aligned
 import javax.swing.JComponent
 
 class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEditor<TypeCheckConfiguration>() {
     private val libraryComponent: EditorTextField
+    private val isTestComponent: JBCheckBox
     private val modulePathComponent: EditorTextField
     private val definitionNameComponent: EditorTextField
 
+
     init {
         libraryComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(
-            ArendLongNameCodeFragment(project, LIBRARY_TEXT, null, customScopeGetter = { AllModulesScope(project) })), project, ArendFileTypeInstance)
+            ArendLongNameCodeFragment(project, LIBRARY_TEXT, null, customScopeGetter = { AllModulesScope(project) })), project, ArendFileTypeInstance
+        )
+        isTestComponent = JBCheckBox()
         val moduleDocument = ArendLongNameCodeFragment(project, MODULE_TEXT, null, customScopeGetter = {
             val library = libraryComponent.text
             if (library == PRELUDE) {
@@ -40,7 +44,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
             }
             val module = ModuleManager.getInstance(project).findModuleByName(library)
             val arendModuleConfigService = ArendModuleConfigService.getInstance(module)
-            arendModuleConfigService?.let { AllArendFilesAndPackagesScope(it, ModulePath(), withPrelude = true, withArendExtension = false) } ?: EmptyScope.INSTANCE
+            arendModuleConfigService?.let { AllArendFilesScope(it, ModulePath(), isTest = isTestComponent.isSelected) } ?: EmptyScope.INSTANCE
         })
         modulePathComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(moduleDocument), project, ArendFileTypeInstance)
         definitionNameComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, DEFINITION_TEXT, null, customScopeGetter = {
@@ -60,6 +64,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
     override fun resetEditorFrom(configuration: TypeCheckConfiguration) {
         with(configuration.arendTypeCheckCommand) {
             libraryComponent.text = library
+            isTestComponent.isSelected = isTest
             modulePathComponent.text = modulePath
             definitionNameComponent.text = definitionFullName
         }
@@ -68,6 +73,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
     override fun applyEditorTo(configuration: TypeCheckConfiguration) {
         configuration.arendTypeCheckCommand = TypeCheckCommand(
             libraryComponent.text,
+            isTestComponent.isSelected,
             modulePathComponent.text,
             definitionNameComponent.text
         )
@@ -75,12 +81,17 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
 
     override fun createEditor(): JComponent = panel {
         aligned("$LIBRARY_TEXT:", libraryComponent)
+        aligned("$IS_TEST_TEXT:", isTestComponent)
         aligned("$MODULE_TEXT:", modulePathComponent)
         aligned("$DEFINITION_TEXT:", definitionNameComponent)
+        row {
+            text("If the definitions from the $MODULE_TEXT (Arend file) are not loaded, then either they are not there, or they have not loaded completely. Try opening the $MODULE_TEXT (Arend file) in the editor and re-view the list of definitions in the Run configuration window")
+        }
     }
 
     companion object {
         private const val LIBRARY_TEXT = "Arend library"
+        private const val IS_TEST_TEXT = "Search in the test directory"
         private const val MODULE_TEXT = "Arend module"
         private const val DEFINITION_TEXT = "Definition"
     }
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt b/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt
index a8602dbb3..53a1e5f16 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/TypecheckRunConfigurationProducer.kt
@@ -3,7 +3,6 @@ package org.arend.typechecking.execution
 import com.intellij.execution.actions.ConfigurationContext
 import com.intellij.execution.actions.LazyRunConfigurationProducer
 import com.intellij.openapi.util.Ref
-import com.intellij.psi.PsiDirectory
 import com.intellij.psi.PsiElement
 import org.arend.module.config.ArendModuleConfigService
 import org.arend.psi.ArendFile
@@ -13,7 +12,6 @@ import org.arend.psi.parentOfType
 import org.arend.typechecking.execution.configurations.ArendRunConfigurationFactory
 import org.arend.typechecking.execution.configurations.TypeCheckConfiguration
 import org.arend.typechecking.execution.configurations.TypecheckRunConfigurationType
-import org.arend.util.FileUtils.EXTENSION
 import org.arend.util.getRelativePath
 
 class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer<TypeCheckConfiguration>() {
@@ -38,7 +36,7 @@ class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer<TypeCheckC
 
     private fun configurationFromContext(context: ConfigurationContext, sourceElement: Ref<PsiElement>?): MyConfiguration? {
         val element = context.location?.psiElement
-        when (val definition = element?.parentOfType<TCDefinition>(false) ?: element?.parentOfType<ArendFile>(false) ?: if (element is PsiDirectory) element else null) {
+        when (val definition = element?.parentOfType<TCDefinition>(false) ?: element?.parentOfType<ArendFile>(false)) {
             is TCDefinition -> {
                 val file = definition.containingFile as? ArendFile ?: return null
                 val modulePath = file.moduleLocation ?: return null
@@ -46,51 +44,24 @@ class TypecheckRunConfigurationProducer: LazyRunConfigurationProducer<TypeCheckC
                 val fullName = definition.fullName
 
                 val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile
-                val fullNameTest = test?.getRelativePath(file.virtualFile)?.joinToString(".")
+                val isTest = test?.getRelativePath(file.virtualFile)?.joinToString(".")
 
-                return if (fullNameTest != null) {
-                    MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", "$TEST_PREFIX.$modulePath$EXTENSION", fullName))
-                } else {
-                    MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", "$modulePath$EXTENSION", fullName))
-                }
+                return MyConfiguration("Typecheck $fullName", TypeCheckCommand(file.libraryName ?: "", isTest != null, modulePath.toString(), fullName))
             }
             is ArendFile -> {
                 sourceElement?.set(definition)
                 val fullName = definition.moduleLocation?.toString() ?: return null
+
                 val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile
-                val fullNameTest = test?.getRelativePath(definition.virtualFile)?.joinToString(".")
-                return if (fullNameTest != null) {
-                    MyConfiguration("Typecheck $TEST_PREFIX.$fullName$EXTENSION", TypeCheckCommand(definition.libraryName ?: "", "$TEST_PREFIX.$fullName$EXTENSION"))
-                } else {
-                    MyConfiguration("Typecheck $fullName$EXTENSION", TypeCheckCommand(definition.libraryName ?: "", "$fullName$EXTENSION"))
-                }
-            }
-            is PsiDirectory -> {
-                sourceElement?.set(definition)
-                val source = ArendModuleConfigService.getInstance(context.module)?.sourcesDirFile
-                val test = ArendModuleConfigService.getInstance(context.module)?.testsDirFile
-                val fullNameSrc = source?.getRelativePath(definition.virtualFile)?.joinToString(".")
-                val fullNameTest = test?.getRelativePath(definition.virtualFile)?.joinToString(".")
-                val libraryName = ArendModuleConfigService.getInstance(context.module)?.library?.name?: ""
-                return if (fullNameSrc != null) {
-                    getMyConfiguration(fullNameSrc, source.name, libraryName)
-                } else if (fullNameTest != null) {
-                    getMyConfiguration(if (fullNameTest.isEmpty()) "" else "$TEST_PREFIX.$fullNameTest", test.name, libraryName)
-                } else {
-                    null
-                }
+                val isTest = test?.getRelativePath(definition.virtualFile)?.joinToString(".")
+
+                return MyConfiguration("Typecheck $fullName", TypeCheckCommand(definition.libraryName ?: "", isTest != null, fullName))
             }
             else -> return null
         }
     }
 
-    private fun getMyConfiguration(fullName: String, virtualFileName: String, libraryName: String): MyConfiguration {
-        return MyConfiguration("Typecheck ${fullName.ifEmpty { virtualFileName }}",
-            TypeCheckCommand(libraryName, fullName.ifEmpty { virtualFileName }))
-    }
-
     companion object {
         private val TYPECHECK_CONFIGURATION_FACTORY = ArendRunConfigurationFactory(TypecheckRunConfigurationType())
-        const val TEST_PREFIX = "Test"
     }
 }
diff --git a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckConfiguration.kt b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckConfiguration.kt
index 190bbd0d0..9058c113b 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckConfiguration.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckConfiguration.kt
@@ -34,9 +34,10 @@ class TypeCheckConfiguration(
     @get: com.intellij.util.xmlb.annotations.Transient
     @set: com.intellij.util.xmlb.annotations.Transient
     var arendTypeCheckCommand: TypeCheckCommand
-        get() = TypeCheckCommand(_arendArgs.library, _arendArgs.modulePath, _arendArgs.definitionFullName)
+        get() = TypeCheckCommand(_arendArgs.library, _arendArgs.isTest, _arendArgs.modulePath, _arendArgs.definitionFullName)
         set(value) = with(value) {
             _arendArgs.library = library
+            _arendArgs.isTest = isTest
             _arendArgs.modulePath = modulePath
             _arendArgs.definitionFullName = definitionFullName
         }
@@ -94,6 +95,7 @@ class TypeCheckConfiguration(
 @Tag(value = "parameters")
 data class SerializableTypeCheckCommand(
     var library: String = "",
+    var isTest: Boolean = false,
     var modulePath: String = "",
     var definitionFullName: String = ""
 )
diff --git a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt
index 2ec17bbfe..fa78cac16 100644
--- a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt
+++ b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt
@@ -18,6 +18,7 @@ import com.intellij.execution.testframework.sm.runner.ui.SMTRunnerConsoleView
 import com.intellij.execution.testframework.sm.runner.ui.SMTRunnerUIActionsHandler
 import com.intellij.execution.testframework.sm.runner.ui.SMTestRunnerResultsForm
 import com.intellij.execution.ui.ConsoleView
+import com.intellij.openapi.application.ApplicationManager
 import com.intellij.openapi.components.service
 import com.intellij.psi.PsiManager
 import org.arend.ext.module.ModulePath
@@ -74,7 +75,13 @@ class TypeCheckRunState(private val environment: ExecutionEnvironment, private v
                         NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath))
                         return null
                     }
-                    library.resetGroup(group)
+                    ApplicationManager.getApplication().run {
+                        executeOnPooledThread {
+                            runReadAction {
+                                library.resetGroup(group)
+                            }
+                        }
+                    }
                 } else {
                     val scope = library?.moduleScopeProvider?.forModule(modulePath) ?: library?.testsModuleScopeProvider?.forModule(modulePath)
                     if (library == null || scope == null) {