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

agda: fix code snippet for installing Agda #110491

Merged
merged 1 commit into from Apr 27, 2021

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'

@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?

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?

doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
@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
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
doc/languages-frameworks/agda.section.md Outdated Show resolved Hide resolved
@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
Copy link
Contributor

turion commented Apr 22, 2021

Can you rebase?

- 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
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.

None yet

7 participants