Skip to content

agda: fix code snippet for installing Agda #110491

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Apr 27, 2021
Merged

agda: fix code snippet for installing Agda #110491

merged 1 commit into from
Apr 27, 2021
+90 −9

Conversation

neosimsim
Copy link
Contributor

Hi @alexarice @turion, I try to improve the usability of nix for Agda projects. This PR fixes I minor issue I encountered on the way. I few more PRs will follow.

Motivation for this change

The documentation nix command does not work.

Things done

Replaced the shell snippet

neosimsim@relaxo$ nix-env -iA agda
error: attribute 'agda' in selection path 'agda' not found

by

neosimsim@relaxo$ nix-env -f '<nixpkgs>' -iA agda
installing 'agdaWithPackages-2.6.1'

@ofborg ofborg bot added 8.has: documentation This PR adds or changes documentation 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux labels Jan 22, 2021
@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch from 71e75de to 80f96de Compare January 22, 2021 15:00
@neosimsim neosimsim marked this pull request as ready for review January 22, 2021 15:02
@veprbl veprbl added the 6.topic: agda "A dependently typed programming language / interactive theorem prover" label Feb 3, 2021
@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch from 80f96de to 994b969 Compare February 12, 2021 10:45
@neosimsim
Copy link
Contributor Author

I finally managed to extend the manual with information I thought would have helped me getting started with nix+Agda. Most importantly code snippets. This change is now what I had in mind for an upcoming PR before the quickfix escalated.

@neosimsim
Copy link
Contributor Author

Next I would like to add the example preBuild to agda.lib as mkSimpleEverything. Should I do so as part of this PR?

alexarice
alexarice reviewed Feb 12, 2021
View reviewed changes
Copy link
Contributor

@alexarice alexarice left a comment

Choose a reason for hiding this comment

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

I am unconvinced by having a tutorial for how to use nix-shell inside the agda documentation. I just feel that it makes it harder to actually access the information about agda?

@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch from 994b969 to 05836d9 Compare March 1, 2021 14:29
@neosimsim
Copy link
Contributor Author

I'm still unsure about

  • documenting how to use libs from GitHub repositories. Maybe we should not encourage this.
  • the example preBuild. Might be to overwhelming.

@turion
Copy link
Contributor

turion commented Mar 1, 2021

documenting how to use libs from GitHub repositories

I think that's fine. The python section also has references to concrete PyPi versions of some packages. Or what exactly is bothering you?

@neosimsim
Copy link
Contributor Author

documenting how to use libs from GitHub repositories

I think that's fine. The python section also has references to concrete PyPi versions of some packages. Or what exactly is bothering you?

I feel this might discourage people from contributing to agdaPackages.

@turion
Copy link
Contributor

turion commented Mar 1, 2021

documenting how to use libs from GitHub repositories

I think that's fine. The python section also has references to concrete PyPi versions of some packages. Or what exactly is bothering you?

I feel this might discourage people from contributing to agdaPackages.

Because they will then find it too easy to simply pin versions on their own? I wouldn't be afraid of that. They should use agdaPackages because it offers additional value above pinning versions yourself: Namely compatibility between libraries and agda versions.

@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch 2 times, most recently from 2680fe0 to aeffcee Compare March 1, 2021 14:50
@alexarice alexarice mentioned this pull request Mar 2, 2021
Closed
SuperSandro2000
SuperSandro2000 requested changes Mar 21, 2021
View reviewed changes
@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch from aeffcee to 6eb0c37 Compare March 27, 2021 17:15
@neosimsim
Copy link
Contributor Author

I think I’m happy now.

@turion turion requested a review from SuperSandro2000 March 28, 2021 16:50
@turion
Copy link
Contributor

turion commented Apr 22, 2021

Can you rebase?

@SuperSandro2000 SuperSandro2000 added the 2.status: merge conflict This PR has merge conflicts with the target branch label Apr 22, 2021
@neosimsim
agda: extend agda language frameworks manual section

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode
4e8641a 
- add code snippets
- be more detailed on some aspects
@neosimsim neosimsim force-pushed the agda-doc-fix-install-command branch from 6eb0c37 to 4e8641a Compare April 23, 2021 16:31
@neosimsim
Copy link
Contributor Author

Can you rebase?

I sure can.

@turion
Copy link
Contributor

turion commented Apr 25, 2021

@SuperSandro2000 I think all your requests were incorporated?

@SuperSandro2000
Copy link
Member

What happened to the CI?

@alexarice
Copy link
Contributor

What happened to the CI?

Something is wrong with ghc on aarch64 and none of us know how to start debugging it

@turion
Copy link
Contributor

turion commented Apr 27, 2021

@SuperSandro2000 this is #111738

@domenkozar domenkozar closed this Apr 27, 2021
@domenkozar domenkozar reopened this Apr 27, 2021
@domenkozar domenkozar merged commit ba6f0e8 into NixOS:master Apr 27, 2021
@Janik-Haag Janik-Haag added the 12. first-time contribution This PR is the author's first one; please be gentle! label Jun 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alexarice alexarice

@turion turion

@SuperSandro2000 SuperSandro2000

Assignees
No one assigned
Labels
2.status: merge conflict This PR has merge conflicts with the target branch 6.topic: agda "A dependently typed programming language / interactive theorem prover" 8.has: documentation This PR adds or changes documentation 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux 12. first-time contribution This PR is the author's first one; please be gentle!
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@neosimsim @turion @SuperSandro2000 @alexarice @domenkozar @veprbl @Janik-Haag