Skip to content

Build system gardening 🪴#589

Merged
ncfavier merged 9 commits intothe1lab:mainfrom
ncfavier:no-nix
Jan 27, 2026
Merged

Build system gardening 🪴#589
ncfavier merged 9 commits intothe1lab:mainfrom
ncfavier:no-nix

Conversation

@ncfavier
Copy link
Member

@ncfavier ncfavier commented Jan 25, 2026

Warning: boring PR.

This makes cabal build 1lab-shake succeed (without warnings), so that one can build the 1Lab outside of the provided Nix shell by following the instructions in the (updated) README, should one choose to inflict this upon oneself. To prevent further bitrot in 1lab-shake.cabal, I also replaced the bespoke mkDerivation for building the shakefile with an equivalent callCabal2nix; this means that dependencies and other build options are only tracked in one place.

These changes are made with four use cases in mind:

  • nix-build for building the 1Lab;
  • nix-shell --run '1lab-shake all' for working on the 1Lab interactively;
  • nix-shell -A shakefile --run 'cabal run 1lab-shake -- all' for working on the 1Lab and the build system interactively;
  • cabal run 1lab-shake -- all outside of a Nix shell, after following the instructions in the README for setting up dependencies.

Also removes support/check.sh as discussed in #587, since the same thing can be achieved with agda --build-library.

Also bumps GHC to 9.10 to get dependencies from cache.nixos.org.

Also contains other trivial changes. The only breaking changes should be:

  • The shake Cabal target is renamed to 1lab-shake.
  • nix-shell -A shakefile no longer exposes ghcide (possibly other stuff as well). If needed, this can be added in shell.nix. HLS is still included.

Let me know if you find anything else.

@4e554c4c Does this work for your use cases?

@ncfavier ncfavier requested review from TOTBWF and plt-amy January 25, 2026 19:10
@Lavenza
Copy link
Member

Lavenza commented Jan 25, 2026

Pull request preview

@ncfavier ncfavier force-pushed the no-nix branch 4 times, most recently from 1b5b637 to 1676cdb Compare January 25, 2026 22:07
@4e554c4c
Copy link
Contributor

4e554c4c commented Jan 26, 2026

Most things appear to be building, thank you

it's a bit annoying to have to manually modify cabal.project. My main concern here is accidently committing something, so I would hope that one of the three following options could be done:

  1. add cabal.project to the .gitignore so change to it aren't committed
  2. add the rev in support/nix/dep/Agda/github.json to cabal.project so it builds by default, and then add a check to the build script to make sure the two match, e.g.
#!/bin/sh
set -e

if [ "$(awk -F': ' '/tag/ {print $2}' cabal.project)" != "$(jq -r '.rev' support/nix/dep/Agda/github.json)" ]; then
  echo "Mismatching revs" > /dev/stderr
  exit 1;
fi
  1. Parse the rev out of cabal.project with cabal2nix and use that in support/nix/dep/Agda/github.json (this one sounds like a pain).

@ncfavier
Copy link
Member Author

I don't think 1 works: if I add cabal.project to .gitignore and make a change to cabal.project, git still tracks it. I think .gitignore only dictates which files become tracked in the first place, but once a file is tracked it's tracked.

2 doesn't play nicely with the third use case above: running cabal inside a Nix shell should use the Nix-provided Agda by default.

For 3, I don't think cabal2nix can do this but we could write a script using cabal-install-parsers and call it from Nix. It's a bit weird to have the information go from cabal.project to Nix though, since Nix also requires a hash that's not present in the cabal.project file. I'm also not sure this is worth the extra complexity.

@TOTBWF
Copy link
Collaborator

TOTBWF commented Jan 26, 2026

We definitely want to keep cabal.project tracked by git. @4e554c4c you can use cabal.project.local to override things, see https://cabal.readthedocs.io/en/3.4/cabal-project.html

Copy link
Collaborator

@TOTBWF TOTBWF left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can deal with synchronizing the revs in the cabal file in later work, as it looks pretty non-trivial.

This ensures that `cabal build shake` succeeds without warnings, as a
first step towards making it possible to build the 1Lab without Nix.
Replace the bespoke `mkDerivation` with an equivalent `callCabal2nix`
so that dependencies and other build options are only tracked in one
place.

These changes are made with *four* use cases in mind:

- `nix-build` for building the 1Lab;
- `nix-shell --run '1lab-shake all'` for working on the 1Lab
  interactively;
- `nix-shell -A shakefile --run 'cabal run 1lab-shake -- all'` for
  working on the 1Lab *and the build script* interactively;
- `cabal run 1lab-shake -- all` outside of a Nix shell, after following
  the instructions in the README for setting up dependencies.
Since 9.10 is the default version in nixpkgs, Haskell dependencies are
now available from cache.nixos.org.
`all-pages.agda` is already generated by the shakefile. To build the
1Lab as an Agda library, one can use `agda --build-library`.
Both available mechanisms for determining whether we are in a
nix-shell invocation are currently broken:

- the `inNixShell` argument is not set by nix-direnv;
- the `IN_NIX_SHELL` environment variable is an environment variable,
  so it affects nix-build calls inside nix shells.

So we keep the shells separate instead.
@ncfavier ncfavier enabled auto-merge (rebase) January 27, 2026 11:24
@ncfavier ncfavier merged commit 8d0128c into the1lab:main Jan 27, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants