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

Update installation instructions wrt install dir? #2500

Open
jbclements opened this issue Nov 16, 2024 · 3 comments
Open

Update installation instructions wrt install dir? #2500

jbclements opened this issue Nov 16, 2024 · 3 comments

Comments

@jbclements
Copy link

The installation directions suggest that the agda library information directory lives at $HOME/.agda/libraries. However, the documentation at https://agda.readthedocs.io/en/latest/tools/package-system.html suggests that this is out of date (though still supported), and suggests identifying the location using agda --print-agda-app-dir ... which indeed, on my macOS system, returns $HOME/.config/agda rather than $HOME/.agda. So perhaps the installation directions here are out of date? Or perhaps there should just be a link to the readthedocs.io site?

Apologies if I'm wading into a religious debate that I'm not aware of :).

@jbclements
Copy link
Author

While I'm looking at this page, it looks like the command-line comment

wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz

... should instead be

wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.1.1.tar.gz

, and the later command

tar -zxvf agda-stdlib.tar

should instead be

tar -zxvf agda-stdlib.tar.gz

Granted, the current pair of commands works, but it's giving a .tar suffix to something that is definitely not just a tar file, but instead a gzipped tar file.

@jbclements
Copy link
Author

... and naturally, if you prefer tgz well then that sounds perfect as well!

@MatthewDaggitt
Copy link
Contributor

Yes, those both seem reasonable changes to make. Thanks for spotting! Would you be willing to make a PR fixing it?

@MatthewDaggitt MatthewDaggitt added this to the v2.2 milestone Nov 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants