Dev agda shellfor

[turion]

Motivation for this change

Things done

• Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
• Built on platform(s)
  • NixOS
  • macOS
  • other Linux distributions
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• Determined the impact on package closure size (by running nix path-info -S before and after)
• Ensured that relevant documentation is up to date
• Fits CONTRIBUTING.md.

CC @alexarice

#98084 should be merged first

[turion]

/marvin opt-in
/status needs_reviewer

[marvin-mk2]

Hi! I'm an experimental bot. My goal is to guide this PR through its stages, hopefully ending with a merge. You can read up on the usage here.

[alexarice]

What does this do that

mkShell {
  buildInputs = [
    (agda.withPackages (p: [ ... ])
  ];
}

doesn't?

[turion]

It doesn't build the package itself, but only its dependencies. See updated docs.

[alexarice]

Ah right I understand. Perhaps we should follow what haskell does and have this under packageName.passthru.env

[turion]

Aha. I hadn't even heard of passthru.env until now. It seems undocumented. There is a shellFor as well for Haskell, though. Not sure which one is more general, but I believe shellFor. It at least has a test, it seems.

In Haskell's shellFor it's possible to add a list of packages, in fact, and also further dev tools like editors, linters etc., maybe we want that here as well?

We could actually have both, a shellFor and an env which calls shellFor. What do you think?

[alexarice]

I think having the env attribute is nice, as then you can just put library.env in your shell

[turion]

@alexarice Like this?

[turion]

This doesn't work, it seems.

[alexarice]

Does that actually work, I'd have thought you need some sort of mkShell command (as you did for the original shellFor). I thought the plan was to keep both

[turion]

I thought the plan was to keep both

Ah ok, I misunderstood you then 😅 Ok I'll bring back both.

[alexarice]

I was thinking of the sort of thing in pkgs/development/haskell-modules/generic-builder.nix

[alexarice]

nixpkgs/pkgs/development/haskell-modules/generic-builder.nix

Line 635 in d851140

env = envFunc { };

[turion]

Ok, I should be able to make something from that, thanks!

[marvin-mk2]

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be should be put back in the needs_reviewer queue in one day.

---

Note: This feature is currently broken. The bot will not actually change the status. If you see this message multiple times, please request a status change manually.

[marvin-mk2]

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be should be put back in the needs_reviewer queue in one day.

---

Note: This feature is currently broken. The bot will not actually change the status. If you see this message multiple times, please request a status change manually.

[marvin-mk2]

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be should be put back in the needs_reviewer queue in one day.

---

Note: This feature is currently broken. The bot will not actually change the status. If you see this message multiple times, please request a status change manually.

[marvin-mk2]

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be should be put back in the needs_reviewer queue in one day.

---

Note: This feature is currently broken. The bot will not actually change the status. If you see this message multiple times, please request a status change manually.

[marvin-mk2]

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be should be put back in the needs_reviewer queue in one day.

---

Note: This feature is currently broken. The bot will not actually change the status. If you see this message multiple times, please request a status change manually.

[timokau]

Sorry for the bot spam (see timokau/marvin-mk2#90 and #121518 (comment)).

/status awaiting_changes

[timokau]

Hi!

The marvin-mk2 bot is now discontinued. I have removed the relevant tags from this PR. If you still need someone to look at it, one option would be to ask in this discourse thread.

I am posting this notice to all open PRs with the marvin tag. Please understand that following all of these discussions would take too much time, so I will unsubscribe from this PR unless I have already been involved in it before this message.