IntersectMBO / IntersectMBO/formal-ledger-specifications
No documented devShell type-checks `formal-ledger-test`
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
## 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](https://github.com/IntersectMBO/formal-ledger-specifications/pull/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](https://github.com/IntersectMBO/formal-ledger-specifications/pull/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 d8eb89d1a, 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.
Contributor guide
Research direction
Start with the flake's devShells configuration and formal-ledger-test/formal-ledger-test.agda-lib, then read the relevant setup sections in CONTRIBUTING.md. Enter the test library's shell and type-check from its directory, including the documented library-file override. Done means devShells.formal-ledger-test is advertised and CONTRIBUTING.md explains the split and current Agda setup.
Written by the indexing model from the issue text.
Assessment
- Domain
- build-system, documentation
- Issue type
- Feature
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Activity status
- Active
- Clarity
- Clearly specified
- Newbie friendliness
- 67/100