I reported issue #8875 and locally I can reproduce it as follows.

❯ cd tmp/cover
❯ agda --build-library
Checking Context (/Users/abela/agda-issue-8336/tmp/cover/src/Context.agda).
 Checking Context.Base (/Users/abela/agda-issue-8336/tmp/cover/src/Context/Base.agda).
 Checking Context.Properties (/Users/abela/agda-issue-8336/tmp/cover/src/Context/Properties.agda).
/Users/abela/agda-issue-8336/tmp/cover/src/Context/Properties.agda:4.1-5.55: error: [AmbiguousTopLevelModuleName]
Ambiguous module name. The module name Data.Product could refer to
any of the following files:
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/src/Data/Product.agda
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/src/Data/Product.agda
  /Users/abela/agda/std-lib/src/Data/Product.agda
when scope checking the declaration
  open import Data.Product using (Σ; ∃; ∃₂; _×_; _,_; -,_; proj₁;
                                  proj₂)

Somehow two different versions of standard-library end up in the dependency tree.
The user should be alerted of this fact when the include paths are constructed, not just getting these ambiguous modules as in the current error.
I would like to get some warning that the library standard-library is depended on in different versions, and I would like to see the provenance of this duplication.
Something like:

warning: -W[no]LibraryVersionConflict ...
Different versions of the library 'standard-library' depended on:
- '2.0', via ...
- '2.4', via ...

The via should list a dependency path.

Please:

1. Analyse where the conflict comes from in the present example.
2. Make a minimal reproducer for our testsuite.
3. Make a plan how to implement this warning.

My hunch is that the conflict can be detected when we build the libraryIncludePaths:

./TypeChecking/Monad/Options.hs:205:    paths     <- libToTCM $ libraryIncludePaths (optOverrideLibrariesFile o) installed libs

Answer 1

I've done all three: the analysis, a test-suite reproducer, and an implementation plan. No compiler code is changed yet.

1. Where the conflict comes from in tmp/cover

cover.agda-lib depends on standard-library-2.4, frames and agda-categories. Each of these resolves to a different standard-library:

• frames (/Users/abel/bib/authors/Nachi/frames/frames.agda-lib) pins standard-library-2.0.
• agda-categories resolves to /Users/abela/agda/ecosystem/agda-categories. It is patched by ecosystem/patches/agda-categories-use-vendored-std-lib.patch to depend on the unversioned standard-library. findLib resolves an unversioned name to the highest installed version. Here that is standard-library-3.0 from the line /Users/abel/agda-erasure/std-lib/standard-library.agda-lib in ~/.agda/libraries. /Users/abel/agda-erasure is a symlink to /Users/abela/agda, which is why the error shows a third path.

So it's a three-way conflict, and the unversioned case matters: the requested name and the resolved name differ, so the warning should show both.

The reason it goes unnoticed: find in libraryIncludePaths (src/full/Agda/Interaction/Library.hs:530) only skips names it has already seen. It never compares the base names of the libraries it resolves, and it doesn't record which library asked for which.

2. Minimal reproducer (added to the worktree)

test/Fail/Issue8875.agda          -- module Issue8875 where; import M
test/Fail/Issue8875.flags         -- --library-file=test/Fail/Issue8875/libraries
                                  -- --library=lib-2.0
                                  -- --library=mid
test/Fail/Issue8875/libraries     -- lists the three .agda-lib files below
test/Fail/Issue8875/lib-1.agda-lib   name: lib-1.0, include: lib-1   (lib-1/M.agda)
test/Fail/Issue8875/lib-2.agda-lib   name: lib-2.0, include: lib-2   (lib-2/M.agda)
test/Fail/Issue8875/mid.agda-lib     name: mid, depend: lib-1.0, include: mid

Running it with the Fail runner's arguments reproduces the error:

test/Fail/Issue8875.agda:10.1-9: error: [AmbiguousTopLevelModuleName]
Ambiguous module name. The module name M could refer to any of the following files:
  …/Issue8875/lib-2/M.agda
  …/Issue8875/lib-1/M.agda

I haven't created Issue8875.err yet. It should be generated with --accept once the warning exists, so that it contains the warning too.

3. Implementation plan

a. The warning type (Library/Base.hs, Options/Warnings.hs)

• Add a new LibWarning' constructor:
  LibraryVersionConflict Text (List2 (AgdaLibFile, List1 LibName)). The Text is the base name. Each entry is a resolved .agda-lib file plus the dependency path that reached it, ending with the name exactly as it was requested.
• Add LibraryVersionConflict_ to WarningName, on by default, with a description for --help=warning, and a case in libraryWarningName.
• Pretty-printing:

  Different versions of the library 'standard-library' depended on:
  - 'standard-library-2.4' (…/agda-stdlib-2.4/standard-library.agda-lib), directly
  - 'standard-library-2.0' (…/agda-stdlib-2.0/…), via frames
  - 'standard-library-3.0' (/Users/abela/agda/std-lib/…), via agda-categories (as 'standard-library')
  

b. Detection in libraryIncludePaths.find (Library.hs:543)

• Change the work list from [LibName] to [(LibName, [LibName])], carrying the reversed path of parents. When a library resolves, push its _libDepends with x : path.
• Return [(AgdaLibFile, path)]. incs keeps using only the files.
• After find, deduplicate by _libFile. Requests like standard-library and standard-library-2.4 that land on the same file are not a conflict. Then group by libNameBase . _libName. Any group with two or more distinct files emits the warning through warnings'. libToTCM already turns it into a LibraryWarning, as for LibUnknownField.
• The traversal is depth-first, so each file keeps the first path that reached it. That's enough for "via" (any path is a valid witness).

c. Root of the path (design choice)
optLibraries comes from three places: the project's depend: (via getDefaultLibraries), -l flags, or the defaults file. The project's own name (cover) is lost before libraryIncludePaths runs.

• Option 1 (recommended): print "directly" for roots.
• Option 2: thread the project's LibName from getDefaultLibraries through CommandLineOptions so paths read cover → frames. This touches more code.

d. Suppressibility
I checked that -WnoLibUnknownField on the command line is honored for library warnings at this stage, so -WnoLibraryVersionConflict should work the same way without extra plumbing.

e. Tests and docs

• test/Fail/Issue8875: the reproducer above, with the warning plus the ambiguity error.
• A test/Succeed variant that has the conflict but imports no clashing module, with a .warn file. This is also what test/test-suite-covers-warnings.sh needs.
• A case where an unversioned request resolves to the highest version while another dependency pins an older one (the agda-categories situation).
• A no-false-positive case: lib and lib-2.0 resolving to the same file give no warning.
• Document the warning in doc/user-manual/tools/command-line-options.rst next to LibUnknownField, and add a CHANGELOG entry.

Your earlier request to review PR #8870 got cut off by the login, and I haven't started it. Should I do that next, or implement this first?

Prompt 2

I like a dependency tree formatting in the warning, pruned to the conflicts, with file references coming later in markdown-style:

Different versions of the library 'standard-library' depended on:
[root]
  ├─ [agda-categories]
  │   └─ standard-library-3.0 as [standard-library]
  ├─ [frames]
  │   └─ [standard-library-2.0]
  └─ [standard-library-2.4]

Library files:
[root]: ./root.agda-lib
[agda-categories]: .../agda-categories.agda-lib
[frames]: ...
[standard-library]: /Users/abela/agda/std-lib/standard-library.agda-lib
[standard-library-2.0]: …/agda-stdlib-2.0/…
...

This allows the user to comprehend the conflict visually and serves her/him the involved library file paths explicitly.

The "root" should be the current project name, and if it has no name, it could be <root>.
You say the name is lost lost before libraryIncludePaths runs, so maybe we need to remember it in the respective data structures concerning the library management.

Please refine the plan accordingly.

Answer 2

The plan now uses your tree format, and I've added a reproducer whose root is a named project.

Reproducers

Root with a project name (new): test/BuildFail/Issue8875/

Issue8875.agda-lib    name: issue8875, depend: lib-2.0, mid, include: src
src/Issue8875.agda    module Issue8875 where; import M
libraries             libs/lib-1.agda-lib, libs/lib-2.agda-lib, libs/mid.agda-lib
libs/{lib-1,lib-2,mid}.agda-lib (+ M.agda / Mid.agda)
test/BuildFail/Issue8875.flags   --library-file=libraries

Running agda --build-library in that directory gives the AmbiguousTopLevelModuleName error for M. The .flags file won't take effect yet because of a test-runner bug: test/BuildFail/Tests.hs looks for ".." </> testName <.> "flags", resolved from the repo root, so it never finds the file. The fix is dir <.> "flags" (same for .vars).

Root without a name: test/Fail/Issue8875, from before, uses -l flags.

Neither .err file exists yet; they get generated with --accept after the change.

Refined plan

1. Keeping the root project's name

The name is dropped in only one place: getDefaultLibraries keeps the project's _libDepends but throws away the AgdaLibFile they came from. Its caller and libraryIncludePaths both run inside setLibraryPaths (TypeChecking/Monad/Options.hs:196). So passing the file along as an argument is enough; nothing needs to go into CommandLineOptions or the TC state.

• getDefaultLibraries :: … -> LibM (Maybe AgdaLibFile, [LibName], [FilePath]). The first component is the project's .agda-lib (listToMaybe of what getAgdaLibFile returns).
• addDefaultLibraries returns (Maybe AgdaLibFile, CommandLineOptions). It returns Nothing when -l is given or the defaults file is used, because then the project's depend: is ignored anyway.
• setLibraryIncludes and libraryIncludePaths get a Maybe AgdaLibFile argument for the root.
• Root label: the project's name:. If the project has no name, or has no .agda-lib at all, the label is <root>. The root's file goes in the file list only when the project has an .agda-lib.

2. Resolution keeps a map of requested to resolved names (find, Library.hs:543)

• Change visited :: [LibName] to Map LibName AgdaLibFile, mapping each name as requested to the file it resolved to. This also removes the quadratic elem check.
• No extra edge bookkeeping is needed: the edges of the graph are the _libDepends of each resolved file.

3. Finding conflicts

• Group the distinct resolved files (by _libFile), including the root, by libNameBase . _libName. Every group with two or more files gives one warning.
• No false positive: standard-library and standard-library-3.0 landing on the same file is not a conflict.

4. Pruning the tree

• A node is kept if it resolves to one of the conflicting files, or if one of its dependencies is kept. This is computed with a visited set, since dependency cycles are possible.
• Start at the root and keep only the kept children, in depend: order. Your sketch was alphabetical; depend: order matches what the user wrote in the file.
• A node reachable by several paths (a diamond) is expanded the first time it appears. Later occurrences print [x] (see above), so the output stays bounded.
• Payload: Data.Tree LibNode, with data LibNode = LibNode { requested, resolved :: LibName, seenAbove :: Bool }, plus the list of files [(label, FilePath)].

5. The warning (Library/Base.hs, Options/Warnings.hs)

• LibWarning' gets LibraryVersionConflict Text (Tree LibNode) [(Text, FilePath)].
• Add LibraryVersionConflict_ to WarningName, on by default. I checked that -WnoLibUnknownField on the command line is honored for library warnings at this stage, so suppressing this one will work the same way.
• Node label: [requested]. When the resolved name differs from the requested one, it reads resolved as [requested]. The keys in the file list are the bracketed labels.
• Tree glyphs ├─ └─ │: add them to Agda.Syntax.Concrete.Glyph's SpecialCharacters with ASCII fallbacks (|-, `-, |). That way --no-unicode is respected, and the Pretty instance can stay pure.

Expected output for tmp/cover:

warning: -W[no]LibraryVersionConflict
Different versions of the library 'standard-library' depended on:
[cover]
  ├─ [standard-library-2.4]
  ├─ [frames]
  │   └─ [standard-library-2.0]
  └─ [agda-categories]
      └─ standard-library-3.0 as [standard-library]

Library files:
[cover]: /Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib
[standard-library-2.4]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/standard-library.agda-lib
[frames]: /Users/abel/bib/authors/Nachi/frames/frames.agda-lib
[standard-library-2.0]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/standard-library.agda-lib
[agda-categories]: /Users/abela/agda/ecosystem/agda-categories/agda-categories.agda-lib
[standard-library]: /Users/abel/agda-erasure/std-lib/standard-library.agda-lib

6. Tests and docs

• BuildFail/Issue8875: named root, warning plus the ambiguity error. Needs the runner fix above.
• Fail/Issue8875: <root> via -l.
• Succeed tests with .flags and .warn:
  • a conflict with no clashing import (warning only);
  • the unversioned request resolving to a newer version (… as [lib]);
  • a diamond (see above);
  • a root that is itself one of the conflicting versions;
  • no warning when two requested names resolve to the same file.
• Document the warning in doc/user-manual/tools/command-line-options.rst and add a CHANGELOG entry.

Shall I start implementing?

Prompt 3

Yes please implement the plan.
If you can make the filenames clickable when the warning is displayed in emacs, please do this change in the warning printout.
(This might involve putting some colons around the filename, if I remember correctly, but you can find this out from the emacs mode implementation, I suppose.)

Answer 3

The LibraryVersionConflict warning is implemented on a new branch issue8875. Nothing is committed yet. On your tmp/cover example, both agda <file> and agda --build-library now print this before the ambiguity error:

warning: -W[no]LibraryVersionConflict
Different versions of the library 'standard-library' depended on:
[cover]
  ├─ [standard-library-2.4]
  ├─ [frames]
  │   └─ [standard-library-2.0]
  └─ [agda-categories]
      └─ standard-library-3.0 as [standard-library]

Library files:
[cover]: /Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib
[standard-library-2.4]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/standard-library.agda-lib
…

I haven't run the real test runner (agda-tests) because building it would mean another full rebuild. I made the golden files by hand: I ran agda-quicker with each runner's arguments and applied its path cleanup with sed. I also spot-checked the existing library tests (installed-libs, Fail/Issue7678, BuildFail/LibTooFarDown), and they behave as before.

What changed

• Detection (Interaction/Library.hs): while resolving dependencies, Agda now records which name resolved to which .agda-lib. Files are compared by canonical path, so two names resolving to the same file are not a conflict. One warning is raised per library base name. The tree only shows the paths that lead to the conflicting versions. A library reached a second way is printed as [mid] (see above) instead of being expanded again.
• Root name: getDefaultLibraries now also returns the project's .agda-lib, and setLibraryPaths passes it on to libraryIncludePaths. Nothing is added to the persistent state. When the project has no name, or the libraries come from -l or the defaults file, the root is shown as [<root>].
• Warning type (Library/Base.hs, Options/Warnings.hs, serialisation): new warning LibraryVersionConflict, on by default. I bumped the interface version.
• Tree glyphs (Syntax/Concrete/Glyph.hs): with --no-unicode the tree is drawn with |-, `- and |.
• Emacs: the paths are now absolute, and I added a second regex to the Agda info buffer for lines of the form [label]: /path, which links to the file. The existing regex requires the path at the start of a line followed by :line.col. I adapted the new regex to the markdown-style list rather than changing the format. I checked the regex and that agda2-mode.el still loads in emacs --batch. I haven't clicked a link in a live Emacs session yet.
• Warnings lost in --build-library: a module error only carried that module's warnings, so library warnings disappeared whenever a module failed. BuildLibrary.hs now prints the warnings collected so far before re-throwing the error.
• Test runner bug: test/BuildFail/Tests.hs looked for .flags/.vars files at ../<name>.flags, relative to the repo root, so it never found them. It now looks next to the test directory.

Tests

• test/BuildFail/Issue8875: named project root, warning followed by the ambiguity error.
• test/Fail/Issue8875: root given with -l, warning followed by the ambiguity error.
• test/Succeed/Issue8875-{conflict,unversioned,diamond,same-version}: warning only, the lib-2.0 as [lib] case, the (see above) case, and no warning when two names resolve to the same file.

I also added a CHANGELOG entry and the user-manual entry.

Build note: make quicker-install-bin-no-deps currently fails at link time. The cached text-icu package was built against ICU 77, but Homebrew now defaults to 78. I built with CABAL_FLAG_ICU= CABAL_OPTS=-f-enable-cluster-counting, so the current agda-quicker has no cluster counting. I saved this workaround to memory.

One small cosmetic point: in --build-library mode there is no blank line between the warning and the error that follows.

Your earlier request to review PR #8870 is still open. Should I commit and push this branch, or start that review next?

Prompt 4

I staged your changes but reverted the addition to the emacs mode.
We do not want a specialized parser for markdown-style references there.

Rather, the filenames should be printed in a way we recognize them now.
So, we have to extend them by line and column number.
By default, we can use line 1 and column 1 (start of file).
However, in our case we could link the line where the dependency is mentioned.
Can you make this work?

Answer 4

The library files are now printed as path:line.col-endcol: [label], which the existing Emacs regex already recognises. The Emacs mode stays as you left it (reverted).

On tmp/cover:

Library files:
/Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib:4.3-23: [cover]
/Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/standard-library.agda-lib:1.1: [standard-library-2.4]
/Users/abel/bib/authors/Nachi/frames/frames.agda-lib:4.3-23: [frames]
/Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/standard-library.agda-lib:1.1: [standard-library-2.0]
/Users/abela/agda/ecosystem/agda-categories/agda-categories.agda-lib:6.9-25: [agda-categories]
/Users/abela/agda/std-lib/standard-library.agda-lib:1.1: [standard-library]

I checked the positions against the files: cover.agda-lib:4.3-23 is standard-library-2.4, and agda-categories.agda-lib:6.9-25 is the standard-library after depend: . In emacs --batch, the unmodified regex extracts the file, line, column and end column from these lines. I haven't clicked them in a live Emacs session.

Which line each entry links to

• A library with children in the tree links to the line in its own .agda-lib where it declares its first dependency shown in the tree, i.e. the line you'd edit to fix the conflict. If the tree shows several, only the first is linked (for cover that's standard-library-2.4, not frames).
• A conflicting library at the bottom of the tree links to 1.1.
• The end column is exclusive, the same convention as Agda's own source ranges.
• A path containing spaces won't be clickable, because the regex stops at whitespace.

How the positions are recorded

• AgdaLibFile has a new field _libDependsPos :: Map LibName LibFilePos (line, start column, end column), keeping the first mention of each dependency. _libDepends is unchanged, so no other code is affected.
• In Library/Parse.hs, content lines now carry the column where their text starts. Field parsers receive these as ContentLine values. The depend parser splits entries with a new splitCommasPos, which keeps each word's column; it works for both depend: a, b and indented multi-line lists. splitCommas is now defined via splitCommasPos.
• LibFilePos is printed as line.col-endcol and has an EmbPrj instance. The interface version bump in your staged changes already covers this.

I regenerated the golden files (.warn/.err) with the same by-hand method as before and updated the CHANGELOG example. The existing library tests I spot-checked (installed-libs, BuildFail/LibTooFarDown, a library parse error) behave as before, and whitespace is clean.

These latest edits are not staged, so git diff shows only this round on top of what you staged.

Prompt 5

I rebased this branch onto master, where we reverted the requirement that file positions start at the beginning of the line.

So please also revert printing in the markdown reference style:

[cover]: /Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib:4.3-23:

Answer 5

I changed the library file lines to the format you asked for, [label]: path:L.C-E:. On tmp/cover the --build-library output now reads:

Library files:
[cover]: /Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib:4.3-23:
[standard-library-2.4]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/standard-library.agda-lib:1.1:
[frames]: /Users/abel/bib/authors/Nachi/frames/frames.agda-lib:4.3-23:
[standard-library-2.0]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/standard-library.agda-lib:1.1:
[agda-categories]: /Users/abela/agda/ecosystem/agda-categories/agda-categories.agda-lib:6.9-25:
[standard-library]: /Users/abela/agda/std-lib/standard-library.agda-lib:1.1:

• Code: the only source change is the line in the warning's printer in src/full/Agda/Interaction/Library/Base.hs. The positions are computed as before.
• Expected outputs: I updated the .err/.warn files for the five Issue8875 tests and the CHANGELOG example to the same format.
• Verification: the build succeeds. I ran test/Fail/Issue8875 by hand from the repo root, and the warning part of its output matches the new .err. The error after it doesn't match, because the test runner runs from test/Fail. I haven't run the actual test suite, and I haven't checked in Emacs whether the paths are clickable now that they no longer start the line.

None of these changes are staged yet.

Prompt 6

Two more issues:

1. I am not getting the warning when I call agda without --build-library:

tmp/cover $ agda src/Everything.agda

Checking Everything (/Users/abela/agda-issue-8336/tmp/cover/src/Everything.agda).
 Checking EverythingSafe (/Users/abela/agda-issue-8336/tmp/cover/src/EverythingSafe.agda).
  Checking HeytingAlgebras (/Users/abela/agda-issue-8336/tmp/cover/src/HeytingAlgebras.agda).
/Users/abela/agda-issue-8336/tmp/cover/src/HeytingAlgebras.agda:5.1-35: error: [AmbiguousTopLevelModuleName]
Ambiguous module name. The module name Level could refer to any of
the following files:
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/src/Level.agda
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/src/Level.agda
  /Users/abela/agda/std-lib/src/Level.agda
when scope checking the declaration
  open import Level using (0ℓ; suc)

I am also not getting it in interaction mode (inside emacs).

2. The warning is not separated from the error by a newline:

tmp/cover $ agda --build-library

Checking Context (/Users/abela/agda-issue-8336/tmp/cover/src/Context.agda).
 Checking Context.Properties (/Users/abela/agda-issue-8336/tmp/cover/src/Context/Properties.agda).
warning: -W[no]LibraryVersionConflict
Different versions of the library 'standard-library' depended on:
[cover]
  ├─ [standard-library-2.4]
  ├─ [frames]
  │   └─ [standard-library-2.0]
  └─ [agda-categories]
      └─ standard-library-3.0 as [standard-library]

Library files:
[cover]: /Users/abela/agda-issue-8336/tmp/cover/cover.agda-lib:4.3-23:
[standard-library-2.4]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/standard-library.agda-lib:1.1:
[frames]: /Users/abel/bib/authors/Nachi/frames/frames.agda-lib:4.3-23:
[standard-library-2.0]: /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/standard-library.agda-lib:1.1:
[agda-categories]: /Users/abela/agda/ecosystem/agda-categories/agda-categories.agda-lib:6.9-25:
[standard-library]: /Users/abela/agda/std-lib/standard-library.agda-lib:1.1:
<<BLANK LINE SHOULD BE HERE>>
/Users/abela/agda-issue-8336/tmp/cover/src/Context/Properties.agda:4.1-5.55: error: [AmbiguousTopLevelModuleName]
Ambiguous module name. The module name Data.Product could refer to
any of the following files:
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.4/src/Data/Product.agda
  /Users/abel/.agda/libraries.d/standard-library/agda-stdlib-2.0/src/Data/Product.agda
  /Users/abela/agda/std-lib/src/Data/Product.agda
when scope checking the declaration
  open import Data.Product using (Σ; ∃; ∃₂; _×_; _,_; -,_; proj₁; proj₂)

Answer 6

Both issues are fixed: the warning now shows without --build-library and in Emacs, and it's separated from the error by a blank line.

1. Missing warning. Your project's library dependencies are resolved before anything is checked. But each imported module is checked in a fresh, isolated state, and an error in it only carries that module's own warnings. So the warning appeared when the error was in the file you called agda on, and was lost when the error was in a module it imports (here HeytingAlgebras). In src/full/Agda/Interaction/Imports.hs, createInterfaceIsolated now adds the importing side's library warnings to the error when an imported module fails. Only library warnings are added, so no other warnings from the importing module leak into the error. The command line and Emacs both print the warnings stored with the error, so one change covers both.

2. Blank line. This went away with the fix above. The warning is now printed together with the error by the normal formatter, which puts a blank line between them. That made my extra catch-and-print in BuildLibrary.hs redundant (with it, the warning would be printed twice), so I reverted that file to master.

Verification on tmp/cover:

• agda src/Everything.agda: the warning appears, then a blank line, then the error in HeytingAlgebras.
• agda --build-library: the warning appears exactly once, followed by a blank line.
• Emacs (--interaction, Cmd_load): the *Error* buffer's "Warnings" section contains the warning, both for Everything.agda and when loading HeytingAlgebras.agda directly.

Tests:

• test/BuildFail/Issue8875.err: added the blank line before the error.
• New test/Fail/Issue8875-import.{agda,flags,err}: a module importing the failing Issue8875, i.e. the case that was broken.
• test/Fail/Issue8875 output is unchanged.

As before, I ran these by hand with the runner's arguments, not through agda-tests.

Nothing is staged: the changes are in Imports.hs, BuildLibrary.hs (reverted to master), test/BuildFail/Issue8875.err, and the three new test files.

Prompt 7

Some more issues:

• In the tree, we want to prune duplicate occurrences, like in test/Succeed/Issue8875-diamond.agda, the mid library should only be printed the first time, and then we also do not need to mention b. This information would be enough for the user and clearer:

Different versions of the library 'lib' depended on:
[<root>]
  ├─ [a]
  │   └─ [mid]
  │       └─ [lib-1.0]
  └─ [lib-2.0]
Library files:
[a]: Issue8875/a.agda-lib:2.9-12
[mid]: Issue8875/mid.agda-lib:2.9-16
[lib-1.0]: Issue8875/lib-1.agda-lib:1.1
[lib-2.0]: Issue8875/lib-2.agda-lib:1.1

• LibDepTree should be an instance of Data.Tree (containers).

• The tree rendering should be defined for generic Data.Tree in a place where we define generic pretty printing.
  The actual prettyLibDepTree can be an instance of the generic tree renderer.

Answer 7

All three are done. The diamond warning now prints exactly the tree you sketched, without b or the repeated mid.

The build has no GHC warnings. I re-ran all Issue8875 tests by hand as before, not through agda-tests. Only the diamond output changed, and I updated test/Succeed/Issue8875-diamond.warn to match. The other Succeed, Fail and BuildFail Issue8875 outputs are unchanged, and so are tmp/cover and the --no-unicode output.

1. Pruning duplicates. When the tree is built in Library.hs, two kinds of libraries are now left out:

• a library already shown earlier in the tree;
• a library none of whose branches leads to a conflicting version not shown before. That is why b disappears: its only branch, mid, was already shown.

The conflicting libraries themselves are always kept. The depSeenAbove field and the (see above) marker are gone, and the library files list follows the pruned tree, so b's file is gone too.

2. Data.Tree. LibDepTree is now type LibDepTree = Tree LibDepNode. The .agdai (interface file) serialisation has a generic EmbPrj (Tree a) instance in Serialise/Instances/General.hs. Since LibDepNode lost a field, I bumped the interface version to 20261026 * 10 + 0.

3. Generic renderer. Agda.Syntax.Common.Pretty now has prettyTree :: TreeGlyphs -> Tree Doc -> Doc. The glyphs are a parameter because Glyph imports Pretty, not the other way round. Glyph now exports a single treeGlyphs that respects --no-unicode, in place of the four separate tree glyphs. In Library/Base.hs, prettyLibDepTree is now just prettyTree treeGlyphs . fmap pretty.

Your sketch had a blank line before "Library files:"; the output doesn't, matching your last commit.

These changes are not staged.

Prompt 8

(1)

prettyTree :: TreeGlyphs -> Tree Doc -> Doc

That feels weird. It seems that the following type would be more in our style.
(2)

prettyTree :: Pretty a => TreeGlyphs -> Tree a -> Doc

Are there good reasons for your choice (1)? If not, please switch to (2).

Answer 8

I switched to prettyTree :: Pretty a => TreeGlyphs -> Tree a -> Doc. There was no good reason for the Tree Doc version: Doc has a Pretty instance with pretty = id, so a tree of Docs still works with the new type.

prettyLibDepTree is now just prettyTree treeGlyphs, without the fmap pretty. It builds without warnings, and the diamond test output is unchanged. Not staged.