IntersectMBO / IntersectMBO/formal-ledger-specifications

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

Open
#1,315 0 comments 0 reactions 0 assignees Claimed by @williamdemeo View on GitHub
🛠️ infrastructure bug documentation
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.