Broken library resolution unit tests

Author: nvarner

test/Test.hs

@@ -15,6 +15,7 @@ import qualified Test.Indexer.Invariants as IndexerInvariants
 import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol
 import qualified Test.Uri as URI
 import qualified Test.Indexer as Indexer
+import qualified Test.AgdaLibResolution as AgdaLibResolution
 
 -- Define the custom option
 newtype AlsPathOption = AlsPathOption FilePath
@@ -43,6 +44,7 @@ tests = do
         URI.tests,
         Model.tests,
         ModelMonad.tests,
+        AgdaLibResolution.tests,
         indexerTests
 #if defined(wasm32_HOST_ARCH)
       , WASM.tests alsPath

test/Test/AgdaLibResolution.hs

@@ -0,0 +1,47 @@
+module Test.AgdaLibResolution (tests) where
+
+import Agda.Syntax.Common.Pretty (prettyShow)
+import Control.Monad.IO.Class (liftIO)
+import Indexer (indexFile, usingSrcAsCurrent)
+import qualified Language.LSP.Protocol.Types as LSP
+import qualified Language.LSP.Server as LSP
+import Monad (runServerT)
+import Server.Model.Monad (MonadAgdaLib (askAgdaLib), runWithAgdaLib)
+import System.Directory (makeAbsolute)
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (assertFailure, testCase)
+import qualified TestData
+
+natPath, constPath :: FilePath
+natPath = "test/data/libs/no-deps/src/Data/Nat.agda"
+constPath = "test/data/libs/no-deps/src/Constants.agda"
+
+tests :: TestTree
+tests =
+  testGroup
+    "Agda lib resolution"
+    [ testCase "Module without imports in lib without dependencies" $ do
+        model <- TestData.getModel
+
+        LSP.runLspT undefined $ do
+          env <- TestData.getServerEnv model
+          runServerT env $ do
+            runWithAgdaLib (LSP.filePathToUri natPath) $ do
+              natSrc <- TestData.parseSourceFromPath natPath
+              _ <- indexFile natSrc
+              return (),
+      testCase "Module with imports in lib without lib dependencies" $ do
+        model <- TestData.getModel
+
+        absConstPath <- makeAbsolute constPath
+
+        LSP.runLspT undefined $ do
+          env <- TestData.getServerEnv model
+          runServerT env $ do
+            runWithAgdaLib (LSP.filePathToUri absConstPath) $ do
+              lib <- askAgdaLib
+              _ <- liftIO $ assertFailure $ prettyShow lib
+              constSrc <- TestData.parseSourceFromPath constPath
+              _ <- indexFile constSrc
+              return ()
+    ]

test/data/libs/no-deps/no-deps.agda-lib

@@ -0,0 +1,2 @@
+name: no-deps
+include: src

test/data/libs/no-deps/src/Constants.agda

@@ -0,0 +1,9 @@
+module Constants where
+
+open import Data.Nat
+
+one : Nat
+one = suc zero
+
+two : Nat
+two = suc one

test/data/libs/no-deps/src/Data/Nat.agda

@@ -0,0 +1,5 @@
+module Data.Nat where
+
+data Nat : Set where
+  zero : Nat
+  suc : Nat -> Nat