flake: fetch inputs via git+https so nix develop works behind the Claude web proxy (#1254) by williamdemeo · Pull Request #1255 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-07-08T06:51:04Z

Description

Addresses #1254. In Claude Code web sandboxes, nix develop fails immediately: the sandbox's GitHub proxy returns 403 for the github: flake-ref shorthand (the tarball endpoints are scoped to the session's own repo), but serves plain git-over-https for any public repo. This PR re-declares the flake inputs as git+https://github.com/... accordingly. The narHash of every pinned rev is identical between the two fetchers, so no dependency changes — same revs, same hashes, a no-op on unrestricted networks (empirical before/after in the comment below).

Commit 1 converts the three direct inputs and pins every flake.lock node (direct + transitive) to the git fetcher; nixpkgs also gets shallow=1, so a binary-cache miss fetches one rev rather than full history. Commit 2 future-proofs updates: a plain nix flake update would regress transitive nodes to github: (their upstream flakes still declare them that way), so flake.nix documents a tested --override-input update invocation plus a one-line check for inputs upstreams add later.

Verified in the web sandbox (comment below) and locally: nix develop --command agda --version → Agda version 2.8.0, everything substituted from cache.nixos.org / cache.iog.io.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md — n/a, infrastructure-only change with no semantic changes to the specifications
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

🤖 Generated with Claude Code

williamdemeo · 2026-07-28T06:28:41Z

Empirical test in the environment this PR targets

(Edited 2026-08-10: trimmed to the flake evidence after the PR was reduced to its flake-only commits; the dev-shell prefetch script this comment also covered was dropped from the PR.)

Ran 2026-07-28 in a fresh Claude Code web sandbox for this repo: recycled container, completely empty /nix; Nix 2.24.9 bootstrapped by hand from releases.nixos.org (allowed by the sandbox proxy, as are cache.nixos.org and cache.iog.io).

#	Scenario	Command	Result
A	master flake (`github:` inputs)	`nix develop --command true`	Fails in <1 s — the first input fetch (`flake-parts`) gets HTTP 403 from the session proxy: "GitHub access to this repository is not enabled for this session"
B	this PR's flake (`git+https` inputs), stone-cold empty store	`nix develop --command agda --version`	≈90 s, success: `Agda version 2.8.0` — all inputs resolved over `git+https`, ~5.6 GB / 110+ store paths substituted from `cache.nixos.org` + `cache.iog.io`, nothing compiled locally. Repeat runs on the warm store: ~2 s

Direct endpoint probes confirm the mechanism: codeload.github.com / api.github.com → 403 for any repo not attached to the session, while git ls-remote https://github.com/input-output-hk/agda.nix succeeds through the same proxy.

Two readings worth keeping: the flake change is the on/off switch, not an optimization (A vs B) — and with identical narHashes it is a no-op elsewhere. Also, nix substituted the nixpkgs source itself by narHash from the binary cache, so no nixpkgs clone happened at all; the shallow=1 on the nixpkgs input is the fallback for when source substitution misses.

🤖 Posted from a Claude Code session that ran the experiments above.

The `github:` flake-ref shorthand fetches source as tarballs from api.github.com / codeload.github.com. In the Claude Code web sandbox these endpoints are served by a GitHub proxy that scopes access to the session's own repositories and returns HTTP 403 for every other repo, so `nix develop` fails while resolving third-party inputs (flake-parts, nixpkgs, agda.nix and its transitive Agda libraries). Plain git-over-https, by contrast, is served by that proxy for any public repo. Declaring the inputs as `git+https://github.com/...` and pinning the lock nodes to the `git` fetcher routes resolution through the working path. The narHash for each rev is identical between the two fetchers, so the pins are unchanged and this is a no-op on unrestricted networks. nixpkgs additionally sets `shallow=1`: when the pinned source cannot be substituted by narHash from a binary cache, a shallow fetch of the locked rev avoids cloning nixpkgs' full history. Verified with `nix develop --command agda --version` (Agda 2.8.0). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01B1ArmS9aNbCxuwhC7zYLBx

A plain `nix flake update` re-reads transitive inputs from their upstream flakes, whose declarations still use the `github:` shorthand, so the lock's locked entries for them would regress to the github fetcher and 403 behind the Claude web sandbox proxy. Record the tested `--override-input` invocation that keeps every node on the git fetcher, the check that catches inputs upstream flakes gain later (exercised for real: agda.nix has grown a categorical-crypto input since our pin), and the note that regressed *original* fields after an update are harmless because consumers fetch by the *locked* entries. Verified 2026-08-10 in a scratch copy: the documented command produces a lock with zero github-locked nodes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

carlostome · 2026-08-12T14:29:33Z

If it is this complicated to update the flake I suggest adding a script (preferably bash + jq) to be able to update the inputs.

Also add a reference to this script in the CONTRIBUTING in how to update the nix flake inputs,

Done: build-tools/nix/update-flake-inputs.sh (bash + jq).

It derives the github-to-git+https conversions from flake.lock itself rather than a fixed list, so it stays valid when upstream flakes gain inputs.

CONTRIBUTING.md has a new "Updating Nix flake inputs" section, and the existing single-dependency example there now uses the git+https form as well.

carlostome · 2026-08-12T14:30:28Z

+  # NOTE: inputs use git+https://... instead of the github: shorthand.
+  # The github: fetcher pulls tarballs from api.github.com / codeload.github.com,
+  # which the Claude Code web sandbox proxy 403s for third-party repos; plain
+  # git-over-https works there for any public repo.
+  #
+  # narHashes are identical between the two fetchers, so the pins are unchanged.
+  #
+  # nixpkgs adds `shallow=1` so a binary-cache miss fetches only the locked rev.
+  #
+  # UPDATING: a plain `nix flake update` re-reads transitive inputs from their
+  # upstream flakes (still declared github:) and would regress the lock.  Use:
+  #
+  #   nix flake update \
+  #     --override-input agda-nix/abstract-set-theory git+https://github.com/input-output-hk/agda-sets \
+  #     --override-input agda-nix/categorical-crypto git+https://github.com/input-output-hk/categorical-crypto \
+  #     --override-input agda-nix/flake-utils git+https://github.com/numtide/flake-utils \
+  #     --override-input agda-nix/flake-utils/systems git+https://github.com/nix-systems/default \
+  #     --override-input agda-nix/iog-prelude git+https://github.com/input-output-hk/iog-agda-prelude \
+  #     --override-input agda-nix/standard-library-classes git+https://github.com/agda/agda-stdlib-classes \
+  #     --override-input agda-nix/standard-library-meta git+https://github.com/agda/agda-stdlib-meta \
+  #     --override-input flake-parts/nixpkgs-lib git+https://github.com/nix-community/nixpkgs.lib
+  #
+  # then verify nothing github-locked slipped in (upstreams gain inputs over time;
+  # `nix flake metadata` shows a new input's path; append an override):
+  #
+  #   python3 -c "import json; L=json.load(open('flake.lock'))['nodes']; \
+  #     print(*[k for k,v in L.items() if v.get('locked',{}).get('type')=='github'] or ['OK'])"
+  #
+  # (Transitive *original* fields read github after an update; harmless since fetches go by *locked* entries.)


I don't think this documentation belongs here. Maybe only a pointer to CONTRIBUTING and how to update the flakes

Agreed. The update documentation moved to CONTRIBUTING.md; the flake.nix note is now the short "why" plus a pointer.

Adds build-tools/nix/update-flake-inputs.sh (bash + jq). It runs `nix flake update`, then derives from flake.lock the input path of every github:-typed entry and re-locks it as git+https, repeating until the lock is clean. Deriving the conversions from the lock keeps the script valid when upstream flakes gain inputs; the update in fact picks up a new agda.nix input (categorical-crypto) and converts it unaided. A --convert-only mode skips the update, for use after re-locking a single input, which can regress sibling entries. CONTRIBUTING gains "Updating Nix flake inputs", and the existing single-dependency example now uses the git+https form so it no longer reintroduces a github: entry. The flake.nix comment shrinks to a pointer, as requested in review. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Copilot

Pull request overview

Routes Nix flake inputs through Git-over-HTTPS for sandbox compatibility while retaining existing dependency revisions and hashes.

Changes:

Converts direct and transitive inputs from github: to Git fetchers.
Adds an input-update and conversion script.
Documents the new update workflow.

Reviewed changes

Copilot reviewed 3 out of 4 changed files in this pull request and generated 1 comment.

File	Description
`flake.nix`	Declares direct inputs using Git-over-HTTPS.
`flake.lock`	Converts all locked inputs to Git fetchers.
`CONTRIBUTING.md`	Documents dependency-update procedures.
`build-tools/nix/update-flake-inputs.sh`	Automates updates and fetcher conversion.

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

williamdemeo · 2026-08-13T03:27:53Z

+      .nodes[$k]
+      | select(.locked.type == "github")
+      | (if .original.type == "github" then .original else .locked end) as $o
+      | ([$o.ref // empty | "ref=\(.)"] + [$o.dir // empty | "dir=\(.)"]) as $q


Confirmed, and reproduced before fixing: pinning agda-nix/abstract-set-theory to an old rev via github:input-output-hk/agda-sets/bbaa00ab… and running --convert-only converted the fetcher but re-resolved the revision (bbaa00a became 2253231). The overrides now pin rev=<locked.rev> (plus ref/dir when declared), so conversion changes the fetcher and nothing else. The same fixture now preserves the old revision, and the full-update mode was re-verified end to end (one conversion pass, no github-typed entries remain). Fixed in a7dd792.

Per Copilot review: the generated overrides carried only ref/dir, so `nix flake lock` re-resolved each converted node and could silently change revisions. --convert-only in particular promised a pure fetcher conversion but bumped any node whose github-locked rev was not the current head (reproduced with a rev-pinned github: entry). Include rev=<locked.rev> in every override so conversion changes the fetcher and nothing else. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

carlostome · 2026-08-13T13:51:16Z

+  # The github: fetcher pulls tarballs from api.github.com / codeload.github.com,
+  # which the Claude Code web sandbox proxy 403s for third-party repos; plain
+  # git-over-https works there for any public repo.
+  #
+  # narHashes are identical between the two fetchers, so the pins are unchanged.
+  #
+  # nixpkgs adds `shallow=1` so a binary-cache miss fetches only the locked rev.
+  #


I'd say to remove this since the motivation is already clear enough in CONTRIBUTING

carlostome · 2026-08-13T13:52:45Z

+
+The flake inputs are declared as `git+https://...` URLs rather than the
+`github:` shorthand, because some sandboxed environments block the GitHub
+tarball endpoints that `github:` uses (see the note in `flake.nix`). A plain


Suggested change

tarball endpoints that `github:` uses (see the note in `flake.nix`). A plain

tarball endpoints that `github:` uses. A plain

carlostome · 2026-08-13T13:55:18Z

+  # To update the inputs, run build-tools/nix/update-flake-inputs.sh (see
+  # "Updating Nix flake inputs" in CONTRIBUTING.md); a plain `nix flake
+  # update` would regress transitive inputs to github:.


I'd change this to a more noticeable comment:

Suggested change

# To update the inputs, run build-tools/nix/update-flake-inputs.sh (see

# "Updating Nix flake inputs" in CONTRIBUTING.md); a plain `nix flake

# update` would regress transitive inputs to github:.

# !WARNING!:

# To update the flake's inputs, DO NOT USE `nix flake update`. Instead run build-tools/nix/update-flake-inputs.sh (see

# "Updating Nix flake inputs" in CONTRIBUTING.md for more info).

williamdemeo · 2026-08-24T18:42:11Z

We've decided to put off supporting web-ui. We can resurrect this PR if/when that changes.

williamdemeo self-assigned this Jul 8, 2026

williamdemeo added discussion 🛠️ infrastructure labels Jul 8, 2026

williamdemeo mentioned this pull request Jul 28, 2026

[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203

Merged

4 tasks

williamdemeo force-pushed the claude/env-config-test-zheoxs branch from af5212a to 34470a6 Compare July 28, 2026 06:48

williamdemeo marked this pull request as ready for review July 28, 2026 06:50

williamdemeo requested a review from carlostome July 28, 2026 06:50

williamdemeo changed the title ~~WIP - flake: fetch inputs via git+https + dev-shell prefetch for cloud proxy (#1254)~~ flake: fetch inputs via git+https + dev-shell prefetch for cloud proxy (#1254) Jul 28, 2026

williamdemeo changed the title ~~flake: fetch inputs via git+https + dev-shell prefetch for cloud proxy (#1254)~~ WIP -- flake: fetch inputs via git+https + dev-shell prefetch for cloud proxy (#1254) Jul 29, 2026

williamdemeo marked this pull request as draft July 29, 2026 14:51

williamdemeo force-pushed the claude/env-config-test-zheoxs branch 2 times, most recently from fe966e4 to 750e405 Compare August 10, 2026 23:06

williamdemeo changed the title ~~WIP -- flake: fetch inputs via git+https + dev-shell prefetch for cloud proxy (#1254)~~ flake: fetch inputs via git+https so nix develop works behind the Claude web proxy (#1254) Aug 10, 2026

williamdemeo force-pushed the claude/env-config-test-zheoxs branch from 750e405 to fcbaaa9 Compare August 10, 2026 23:43

williamdemeo force-pushed the claude/env-config-test-zheoxs branch from fcbaaa9 to b8f9b41 Compare August 10, 2026 23:50

williamdemeo marked this pull request as ready for review August 10, 2026 23:51

carlostome reviewed Aug 12, 2026

View reviewed changes

williamdemeo requested a balanced review from Copilot August 13, 2026 03:17

Copilot started reviewing on behalf of williamdemeo August 13, 2026 03:18 View session

Copilot AI reviewed Aug 13, 2026

View reviewed changes

williamdemeo requested a review from carlostome August 13, 2026 03:37

carlostome reviewed Aug 13, 2026

View reviewed changes

williamdemeo closed this Aug 24, 2026

Navigation Menu

Uh oh!

flake: fetch inputs via git+https so nix develop works behind the Claude web proxy (#1254) - #1255

flake: fetch inputs via git+https so nix develop works behind the Claude web proxy (#1254)#1255
williamdemeo wants to merge 4 commits into
masterfrom
claude/env-config-test-zheoxs

williamdemeo commented Jul 8, 2026 •

edited

Loading

Uh oh!

williamdemeo commented Jul 28, 2026 •

edited

Loading

Uh oh!

carlostome Aug 12, 2026

Uh oh!

williamdemeo Aug 13, 2026

Uh oh!

carlostome Aug 12, 2026

Uh oh!

williamdemeo Aug 13, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

williamdemeo Aug 13, 2026

Uh oh!

carlostome Aug 13, 2026

Uh oh!

carlostome Aug 13, 2026

Uh oh!

carlostome Aug 13, 2026

Uh oh!

williamdemeo commented Aug 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

	tarball endpoints that `github:` uses (see the note in `flake.nix`). A plain
	tarball endpoints that `github:` uses. A plain

Uh oh!

Conversation

williamdemeo commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Checklist

Uh oh!

williamdemeo commented Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Empirical test in the environment this PR targets

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

williamdemeo commented Aug 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

williamdemeo commented Jul 8, 2026 •

edited

Loading

williamdemeo commented Jul 28, 2026 •

edited

Loading