8000 Agda stdlib installation instructions broken link · Issue #6957 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Agda stdlib installation instructions broken link #6957

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
Closed
patrick-nicodemus opened this issue Nov 7, 2023 · 3 comments · Fixed by #6973
Closed

Agda stdlib installation instructions broken link #6957

patrick-nicodemus opened this issue Nov 7, 2023 · 3 comments · Fixed by #6973
Assignees
@andreasabel
Labels
std-lib Issue affecting the standard library ux: documentation Issues relating to Agda's documentation
Milestone
2.6.4.1

Comments

@patrick-nicodemus
Copy link

This page
https://agda.readthedocs.io/en/v2.6.4/getting-started/a-taste-of-agda.html#a-taste-of-agda
links to installation instructions for the standard library but the link is broken.
@jamesmckinna
Copy link
Contributor

Specifically, v1.7.* releases of the library do point to the notes/ subdirectory for additional ancillary documentation, but this is being moved to doc/ for the v2.0 release, and that change has already been propagated on master by agda/agda-stdlib#2184

@andreasabel andreasabel added this to the 2.6.4.1 milestone Nov 8, 2023
@andreasabel
Copy link
Member

Thanks for the heads up!

We should only use time-resistant links... These don't rot as references per se, only as pointers to relevant content. 😆

@andreasabel andreasabel self-assigned this Nov 9, 2023
@andreasabel andreasabel added ux: documentation Issues relating to Agda's documentation std-lib Issue affecting the standard library labels Nov 9, 2023
@andreasabel andreasabel mentioned this issue Nov 9, 2023
Merged
@jamesmckinna
Copy link
Contributor

Re: time-resistant links. how would that cash out in terms of the stdlib documentation? or is this comment local to the user-manual/ documentation (it would in any case be nice, for developers and end-users/readers alike, if we can try to keep these as loosely coupled as possible...)

@andreasabel andreasabel mentioned this issue Feb 7, 2024
Closed
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
@andreasabel @JobPetrovcic
Fix agda#6957: user-manual: link to std-lib installation instructions
d0630b4 
Not using a permalink since the content it points to could get outdated.
Rather risking that the link will break as a whole again in the future.

Closes agda#6957.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
std-lib Issue affecting the standard library ux: documentation Issues relating to Agda's documentation
Projects
None yet
Milestone
2.6.4.1
3 participants
@andreasabel @jamesmckinna @patrick-nicodemus
0