A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/agda/agda/issues/7675 below:

GitHub ยท Where software is built

Since #6988 (2.6.4.2) the location of an .agdai, which can be local or in a _build directory, depends on where existing files were found:

separatedIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath separatedIFile localIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath localIFile case (separatedIFileExists, localIFileExists) of (False, False) -> fst <$> ifilePreference (False, True) -> pure localIFile (True, False) -> pure separatedIFile

This can lead to scattering of .agdai files belonging to one project, so that some are places locally and some in the _build directory:

E.g., in a fresh directory, do the following:

echo "include: ." > Main.agda-lib
echo "-- empty file" > Foo.agda
echo "import Foo" > Main.agda
touch Foo.agdai
agda-2.7.0.1 Main.agda
find -name "*.agdai"

This gives

./Foo.agdai
./_build/2.7.0.1/agda/Main.agdai

I don't think that .agdai files for a single project should scattered in such a way.
Agda should be more principled in the placement of these interface files and not depend on chance of what interface files exist already.

Probably we need to reevaluate the design behind #6988:

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4