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

Enhance the Agda builder #60271

Closed
michaelpj opened this issue Apr 26, 2019 · 3 comments · Fixed by #76653
Closed

Enhance the Agda builder #60271

michaelpj opened this issue Apr 26, 2019 · 3 comments · Fixed by #76653
Labels
0.kind: enhancement Add something new 6.topic: agda "A dependently typed programming language / interactive theorem prover" 9.needs: community feedback

Comments

@michaelpj
Copy link
Contributor

michaelpj commented Apr 26, 2019

For my sins, I'm trying to integrate some Agda code into the testing part of a production system. I'd like to use the Agda builder from Nixpkgs, but it could do with a few enhancements. I thought I'd open an issue discussing those so I can see whether other people agree before I try to actually implement anything.

Things I would like:

  • Support for library files.
    • The current builder passes all dependencies using -i, we could probably use AGDA_DIR or --library-file now for many libraries.
    • Would need to think of how to handle fallback for libraries that don't use library files yet.
  • agdaWithPackages
    • Obviously we'd want to preserve the existing ability for emacs to pick things up, but I think might be easier with AGDA_DIR now.
  • Easier configuration of build flags.
    • It's a bit annoying to try and override buildFlags at the moment.
  • Some simple enable/disable options for generating html/latex literate Agda output, and for producing compiled outputs via one of the backends.

Mentioning some people who seem to be involved: @Fuuzetsu @siddharthist

@Fuuzetsu
Copy link
Member

I haven't used Agda for few years so I'm not really up to date on the current build system in nix but the suggestions sound fine I think.

@langston-barrett
Copy link
Contributor

@turion
Copy link
Contributor

turion commented Dec 13, 2019

@langston-barrett can your project be merged into nixpkgs? Also, there is a PR here: #39318

@alexarice alexarice mentioned this issue Dec 29, 2019
10 tasks
@veprbl veprbl added the 6.topic: agda "A dependently typed programming language / interactive theorem prover" label Feb 3, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
0.kind: enhancement Add something new 6.topic: agda "A dependently typed programming language / interactive theorem prover" 9.needs: community feedback
Projects
None yet
Development

Successfully merging a pull request may close this issue.

6 participants