No documented devShell type-checks `formal-ledger-test`

[williamdemeo]

Problem

In the default dev shell every module under formal-ledger-test fails to load, while modules under src load normally.

$ nix develop
$ cd formal-ledger-test && agda src/Test/Prelude.lagda.md
error: [LibraryError]
Library 'formal-ledger' not found.
Add the path to its .agda-lib file to
  '/nix/store/…-libraries'
to install.
Installed libraries:
  standard-library-2.3
  standard-library-classes
  standard-library-meta
  abstract-set-theory
  iog-prelude

It is the same in Emacs, which is how this surfaced: C-c C-l on any file under formal-ledger-test reports the error above.

Thanks to Tudor Ferariu (@tferariu) for reporting this issue.

Why

formal-ledger-test/formal-ledger-test.agda-lib declares depend: … formal-ledger, and the default shell registers only the five upstream libraries, not formal-ledger itself. Two changes combined to produce this.

• #1175 moved src/Test/* into the separate formal-ledger-test library. Before that the test modules were part of formal-ledger, and the default shell served them.
• #1177 removed formal-ledger-test from devShells.default's inputsFrom; that is right on its own (otherwise entering the default shell first waits for the fully type-checked ledger) but it left the test library with no shell.

Two things a contributor is likely to try cannot work, for reasons worth recording.

• Adding a line to ~/.config/agda/libraries has no effect. The shell's agda is a wrapper that passes --library-file=/nix/store/…-libraries on every invocation, which overrides the user's own library file entirely.
• Running nix develop from inside formal-ledger-test gives the identical shell, since Nix searches upward for flake.nix and the shell does not depend on the working directory.

What to do

• Expose a dev shell for the test library (devShells.formal-ledger-test). Entering that environment already works by package attribute, since formal-ledger-test is a flake package and nix develop accepts one, but nothing advertises it: nix flake show lists only default, fls-agda, fls-shake, and fls-shake-agdaWithPackages.
• Document the split in CONTRIBUTING.md, together with two facts that cost time to rediscover: Agda selects the governing .agda-lib by searching the current directory and its parents, so the test library must be type-checked from inside its own directory (from the repository root Agda picks the root library and reports ModuleNameDoesntMatchFileName); and a command-line --library-file overrides the wrapper's, which is how to check the test library against a working copy of src rather than against the built ledger.

Adjacent staleness in CONTRIBUTING

These were found while diagnosing this.

• The Agda pin moved to 2.8.0 in d8eb89d, a year ago; §Setup Without Nix still says "Install Agda 2.7.0.1", and the Emacs snippet still labels ~/ledger-agda as 2.7.0.1.
• §Using update-alternatives tells the reader to register ~/ledger-agda/bin/agda-mode, which does not exist. Our agda provides no agda-mode, and that executable is deprecated as of Agda 2.8.0 in favour of agda --emacs-mode. An Emacs whose agda2-mode elisp comes from a different Agda then fails with The Agda mode's version (X) does not match that of agda (2.8.0)., and the guide says nothing about where matching elisp comes from.
• §Setup Without Nix pins agda-stdlib at v2.2 (we use 2.3) and gives four commit hashes that all differ from flake.lock, referring the reader to a build-tools/nix/sources.json that no longer exists.
• The same section type-checks src/Everything.agda, which does not exist.
• scripts/plot_typecheck_time.py moved to build-tools/scripts/plot_typecheck_time.py.

Not covered here

TROUBLESHOOTING.md is still pre-flake: it recommends nix-shell -A devShells.ci and nix-build -A formalLedger, neither of which exists.