Skip to content

feat: add lean4 to nixpkgs packages - #1754

Merged
shunkakinoki merged 8 commits into
mainfrom
feat/add-lean4
May 11, 2026
Merged

feat: add lean4 to nixpkgs packages#1754
shunkakinoki merged 8 commits into
mainfrom
feat/add-lean4

Conversation

@shunkakinoki

@shunkakinoki shunkakinoki commented May 11, 2026

Copy link
Copy Markdown
Owner

Summary

  • Adds lean4 to the home-manager packages list in alphabetical order

Test plan

  • nixos-rebuild switch or home-manager switch builds successfully with lean4 available

Summary by cubic

Add lean4 to home-manager packages and simplify ghostty config to use a static file with fish --login. Fix input on Framework by having keyd grab 32ac:0006, add a systemctl-noctalia-shell Makefile target (restart quickshell on matic), and suppress gtk4 theme warnings.

Written for commit 7120479. Summary will update on new commits.

@indent-zero

indent-zero Bot commented May 11, 2026

Copy link
Copy Markdown
Contributor
PR Summary

Originally a single-line lean4 package addition, this PR has grown to 8 commits across 5 unrelated subsystems. New changes since the last review include a default-agent flip, a noctalia-shell systemd-restart Makefile target, a ghostty config refactor (drops Nix-time ${pkgs.fish}/bin/fish substitution in favor of a bare fish --login), and a gtk4.theme = null warning suppression.

  • home-manager/packages/default.nix: add lean4 (alphabetically placed).
  • config/keyd/default.conf: explicitly grab Framework 13 AI 300 EC 32ac:0006 since keyd's * wildcard skips I2C HID consumer-control devices.
  • .roborev.toml: change default agent from gemini to codex.
  • Makefile: add systemctl-noctalia-shell target (no-ops off matic/no WAYLAND_DISPLAY) and wire it into the systemctl aggregator.
  • config/ghostty/config & config/ghostty/default.nix: drop __FISH_PATH__ placeholder substitution; the file is now sourced verbatim with command = fish --login (PATH-resolved instead of absolute Nix store path). gtk-single-instance = false was added then removed.
  • config/gtk/default.nix: set gtk4.theme = null to suppress home-manager's gtk4 default-changed warning, removing the explicit Adwaita assignment.

Issues

2 potential issues found:

  • Scope drift: PR titled feat: add lean4 to nixpkgs packages now spans 8 commits across 5 unrelated subsystems (lean4, keyd, gtk, ghostty, roborev, Makefile/systemd) — four of which are empty chore: update messages with no archaeology hint. → Autofix
  • Ghostty command = fish --login now relies on PATH instead of the absolute Nix store path; on macOS, GUI launches (Finder/Spotlight/dock) inherit launchd's PATH, which by default does not include ~/.nix-profile/bin where home-manager installs fish, so the terminal may fail to start a shell. → Autofix

CI Checks

shell-check fails because the dependent shell-lint job reports ShellCheck errors in spec/activate_roborev_spec.sh (SC2148 missing shebang/shell directive on line 1, SC2016 info on line 33). This file was added on main in PR #1751 (904429f) and is not modified by this PR — PR #1754 only touches home-manager/packages/default.nix and config/keyd/default.conf. The failure is pre-existing on main and unrelated to the lean4/keyd changes here.

Failing shell-check→ Autofix
  • The shell-check aggregator fails because shell-lint reports ShellCheck violations in spec/activate_roborev_spec.shSC2148 (missing shebang/shell directive on line 1) and SC2016 (single-quoted expression on line 33). This spec file was introduced on main in PR fix(test): add roborev to shell coverage spec #1751 (commit 904429f) and is not touched by PR feat: add lean4 to nixpkgs packages #1754, so the failure is pre-existing and unrelated to the lean4/keyd changes.

⚡ Autofix All

@mesa-dot-dev

mesa-dot-dev Bot commented May 11, 2026

Copy link
Copy Markdown

You do not have enough credits to review this pull request. Please purchase more credits to continue.

@coderabbitai

coderabbitai Bot commented May 11, 2026

Copy link
Copy Markdown

Review Change Stack

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 54d50506-ecf5-4fe4-8cc3-6cca9d8d3424

📥 Commits

Reviewing files that changed from the base of the PR and between 134574e and 7120479.

📒 Files selected for processing (6)
  • .roborev.toml
  • Makefile
  • config/ghostty/config
  • config/ghostty/default.nix
  • config/gtk/default.nix
  • config/keyd/default.conf

Disabled knowledge base sources:

  • Linear integration is disabled

You can enable these sources in your CodeRabbit configuration.


📝 Walkthrough

Summary by CodeRabbit

  • Configuration Updates

    • Updated terminal shell launch configuration
    • Adjusted GTK4 theme settings
    • Enhanced keyboard input device support for Framework controller
  • Chores

    • Added Lean4 development tooling to default packages
    • Improved system service restart automation
    • Updated default system configuration settings

Walkthrough

This PR adds Lean4 to Home Manager defaults, adds a conditional noctalia-shell restart Makefile target, switches Ghostty to use a local config file and fish --login, sets GTK4 theme to null, adds a keyd device id, and changes .roborev.toml agent to codex.

Changes

Repository configuration updates

Layer / File(s) Summary
Default Package List
home-manager/packages/default.nix
Adds lean4 to the default Home Manager package list.
Makefile systemctl target
Makefile
systemctl target now depends on systemctl-noctalia-shell; new target conditionally restarts noctalia-shell/quickshell on matic when WAYLAND_DISPLAY is set.
Ghostty: Nix sourcing & command
config/ghostty/default.nix, config/ghostty/config
Stop templating config text; use source = ./config (including macOS path). Set Ghostty command to fish --login.
GTK config
config/gtk/default.nix
Set gtk4.theme = null (remove explicit Adwaita package).
keyd device IDs
config/keyd/default.conf
Add explicit I2C HID device id 32ac:0006 to [ids].
Tooling config
.roborev.toml
Change agent from gemini to codex.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~10 minutes

Possibly related PRs

Poem

🐰 I hopped through dotfiles, line by line,
Lean4 tucked in, configs now align,
Shells that restart when Wayland's near,
Ghostty reads a file, fish appears,
Codex hums — the rabbit gives a cheer!

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Title check ✅ Passed The title directly describes the main change: adding lean4 to the nixpkgs packages in home-manager configuration.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.
Description check ✅ Passed The pull request description accurately describes the changeset, which adds lean4 to the home-manager packages list in alphabetical order, matching the implemented changes.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/add-lean4

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

@mesa-dot-dev

mesa-dot-dev Bot commented May 11, 2026

Copy link
Copy Markdown

Mesa Description

TL;DR

Adds lean4 to the home-manager packages and updates keyd configuration to correctly remap the Framework key on certain devices.

What changed?

  • home-manager/packages/default.nix: Added the lean4 package to the list of available packages.
  • config/keyd/default.conf: Updated to explicitly include device ID 32ac:0006 for the Framework 13 AI 300 embedded controller, ensuring keyd processes the Framework key (an I2C HID consumer control device) for correct remapping.

Description generated by Mesa. Update settings

@cubic-dev-ai cubic-dev-ai Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

No issues found across 1 file

@gemini-code-assist gemini-code-assist Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Code Review

This pull request adds the lean4 package to the home-manager configuration. There are no review comments, and I have no feedback to provide.

Comment thread config/keyd/default.conf
# Framework 13 AI 300 embedded controller (I2C HID). keyd's `*` wildcard
# does not grab I2C HID consumer control devices, so the Framework key
# bypasses keyd unless this id is listed explicitly.
32ac:0006

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Scope drift (nit): This keyd fix is unrelated to the PR's stated purpose (feat: add lean4 to nixpkgs packages). The change itself looks correct — keyd's * wildcard does not grab I2C HID consumer-control devices, so explicitly listing 32ac:0006 (Framework 13 AI 300 EC) is the right way to make the leftmeta/prog1/f13cmd_hyper remaps in [main] apply to the Framework key. But it would be easier to find this fix in git log if it lived in its own PR (or if PR #1754's title/description called it out).

@shunkakinoki
shunkakinoki enabled auto-merge (squash) May 11, 2026 19:02
@shunkakinoki
shunkakinoki disabled auto-merge May 11, 2026 19:04
@shunkakinoki
shunkakinoki merged commit 1936965 into main May 11, 2026
29 of 32 checks passed
@shunkakinoki
shunkakinoki deleted the feat/add-lean4 branch May 11, 2026 19:04
Comment thread config/ghostty/config
macos-titlebar-style = "tabs"
shell-integration = fish
command = __FISH_PATH__ --login
command = fish --login

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Latent regression on macOS GUI launches: Previously config/ghostty/default.nix substituted __FISH_PATH__ with ${pkgs.fish}/bin/fish at build time, so this line was an absolute Nix store path. Now ghostty must resolve fish via PATH (execvp). On macOS, ghostty.app launched from Finder/Spotlight/dock inherits launchd's PATH, which by default contains only /usr/bin:/bin:/usr/sbin:/sbin plus entries in /etc/paths.d/*. The nix multi-user installer adds /nix/var/nix/profiles/default/bin there, but ~/.nix-profile/bin — where home-manager installs fish — is not on launchd's PATH unless the user manually ran launchctl setenv PATH .... Result: ghostty may fail to spawn the shell. On Linux desktop sessions this is fine because Hyprland/etc. inherit the user's session PATH. Either restore the ${pkgs.fish}/bin/fish substitution or document the launchd PATH requirement.

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.

1 participant