Open jbclements opened 3 hours ago
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.
... and naturally, if you prefer tgz
well then that sounds perfect as well!
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 usingagda --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 thereadthedocs.io
site?Apologies if I'm wading into a religious debate that I'm not aware of :).