IntersectMBO / IntersectMBO/formal-ledger-specifications
flake: use git+https for inputs so `nix develop` works behind the GitHub tarball proxy
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
## Summary
`nix develop` fails in the Claude Code web (cloud sandbox) environment because our flake inputs are declared with the `github:` shorthand, which fetches source as tarballs from `api.github.com`/`codeload.github.com`. Those endpoints are repo-scoped by the sandbox's GitHub proxy and return `403` for any repo outside the current session's scope. Switching the inputs to `git+https://github.com/...` resolves this with no change to the pinned revisions. A companion setup-script prefetch then removes the resolution cost entirely for subsequent sessions.
## Symptom
```
$ nix develop --command agda --version
error: unable to download
'https://github.com/hercules-ci/flake-parts/archive/57928607….tar.gz':
HTTP error 403
{"message":"GitHub access to this repository is not enabled for this session…"}
```
Resolution dies on the first third-party input; the same would happen for `nixpkgs`, `agda.nix`, and the transitive Agda libraries.
## Root cause
The sandbox routes outbound traffic through two independent gates:
- **Security proxy** — a host allowlist for plain HTTPS. GitHub *tarball* endpoints go through here and are scoped to the session's own repositories (→ `403` for third-party repos, even public ones).
- **GitHub proxy** — handles *git operations* with a scoped credential that reaches any public repo.
Nix's `github:` fetcher uses the tarball path (the blocked one). Plain `git`-over-https uses the working path. Confirmed empirically:
| Fetch of `hercules-ci/flake-parts` (out of session scope) | Result |
|---|---|
| `curl` archive tarball / `nix flake metadata github:…` | `403` |
| `git ls-remote …` / `nix flake metadata git+https://…` | success |
## Proposed change
Two parts:
1. **Route inputs through git.** Declare each input as `git+https://github.com//` instead of `github:/`, and pin the `flake.lock` nodes to the `git` fetcher. The `narHash` for any given revision is **identical** between the two fetchers, so every pin is preserved — this is a no-op on an unrestricted network and does not bump any dependency. Touches only `flake.nix` (the three direct inputs) and `flake.lock` (all nodes, including transitive ones pulled in via `agda.nix` and `flake-parts`).
2. **Prefetch the dev shell in the setup phase.** Add `build-tools/nix/prefetch-devshell.sh`, which realises the `nix develop` shell into `/nix/store` and pins a gc-root. Wired into the cloud environment's *setup script* (whose filesystem output is snapshotted and reused), it moves the one-time resolution/build off the interactive session: later sessions find every store path already present and fetch nothing. The script is idempotent, keeps its gc-root outside the working tree, and no-ops cleanly when `nix` is absent. Setup instructions and caching behaviour are in `build-tools/nix/README-prefetch.md`.
Part 1 makes resolution *possible* behind the proxy; part 2 makes it *instant* for subsequent sessions.
## Verification
`nix develop --command agda --version` → `Agda version 2.8.0`, with inputs fetched over git and binaries substituted from `cache.nixos.org` / `cache.iog.io`. The prefetch script reproduces the same result and completes in seconds against a warm store.
## Caveat / follow-up
`flake.lock` nodes for the *transitive* inputs are pinned to `git`, but their upstream flakes (e.g. `agda.nix`) still declare them with `github:`. A future `nix flake update` will therefore re-introduce `github:`-typed nodes and reintroduce the problem until re-converted. A durable upstream fix would be to adopt the `git+https` convention in `agda.nix` itself; until then, re-running the conversion after a dependency bump (and relying on the prefetch cache in day-to-day use) keeps sessions working.
Contributor guide
Research direction
Start with flake.nix and flake.lock to inspect the direct and transitive input nodes, then read the setup-script integration and build-tools/nix/README-prefetch.md. Verify with nix develop --command agda --version and the prefetch script. Done means inputs resolve through git, the setup phase warms the dev shell, and the documented warm-store behavior works.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- git, shell
- Domain
- build-system, devops, infrastructure
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Quiet
- Clarity
- Clearly specified
- Newbie friendliness
- 55/100