Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revamp Agda builder, add documentation #39318

Closed
wants to merge 1 commit into from

Conversation

langston-barrett
Copy link
Contributor

@langston-barrett langston-barrett commented Apr 22, 2018

The build process for Agda packages now mirrors that of Idris packages. There is an agda.withPackages attribute that works like ghcWithPackages.

This should make it easier to implement building Agda binaries, since that process can reuse agdaWithPackages.

Motivation for this change

Fixes #19434

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option build-use-sandbox in nix.conf on non-NixOS)
  • 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 nox --run "nox-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Fits CONTRIBUTING.md.

The build process for Agda packages now mirrors that of Idris packages.
There is an agdaWithPackages attribute that works like ghcWithPackages.
This should make it easier to implement building Agda binaries, since that
process can reuse agdaWithPackages.
@langston-barrett
Copy link
Contributor Author

cc: @Fuuzetsu @copumpkin

Copy link
Member

@Fuuzetsu Fuuzetsu left a comment

Choose a reason for hiding this comment

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

Seems it removes the interactive part which is needed for nix-based Agda with emacs for example

@langston-barrett
Copy link
Contributor Author

@Fuuzetsu Can you point that part out to me? Is it the passthru bit? Thanks for taking a look.

@Fuuzetsu
Copy link
Member

Yes precisely the passthru, being able to load stuff into emacs was actually the main motivation for original version of builder (not the one you're changing)

@langston-barrett
Copy link
Contributor Author

@Fuuzetsu Can you describe the use-case in a little more detail? It seems to me like the user could use agda.withPackages, since emacs will find the wrapped agda binary.

@Fuuzetsu
Copy link
Member

emacs needs to know where to find sources and compiled sources, it's not enough that agda binary sees it

@mpickering
Copy link
Contributor

Does this break or improve the way we can package cedille? I didn't know there were any other agda binaries packaged in nixpkgs.

@alexarice
Copy link
Contributor

Is there any reason the documentation and withPackages part of this can't be added without changing the agda mkderivation part? Otherwise I feel I'm missing something as I can't see how you can currently load any agda packages in emacs.

@turion
Copy link
Contributor

turion commented May 15, 2020

@langston-barrett I believe this is now superseded by #76653. Shall we close?

@langston-barrett
Copy link
Contributor Author

@turion Yes, agreed! 🎉

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Documentation for Agda packages?
7 participants