[docs] Bring conclusions.rst up to speed, fix links in packages.rst
#3653
+30
−24
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* Point people at the mailing list rather than just mentioning it exists. * Fix the discord invite link. * Fix the IRC link (we moved off freenode alongside everyone else, and that was years ago).
The website is not really related to questions, so it makes more sense to group the mailing list with the discord. As part of that separation, then, add a brief sentence on what the website does. Similar to the website, mention that the discord is currently the most active interactive discussion place.
This is likely the closest one can come to a "Type-Driven Development with Idris **2**" book, so it should be near the top. Huge props to Stefan Höck for writing the original, and to the community for turning it into an mdBook and now having stewardship of it.
Having the original Idris papers on the readthedocs is probably manageable. However, to save us having to keep multiple "Papers" pages in sync, I'm pointing back to the website for papers involving Idris in general.
CodingCellist
added
documentation
mattpolzin
approved these changes
Oct 17, 2025
As listed, they were showing as Idris1 ^3 ^2 , which was just slightly bothering me.
The links for "pack collection" and "third-party libraries" were missing a space between the display text and the ref, leading to incorrect hyperlinks in the readthedocs output.
CodingCellist
changed the title
conclusions.rst up to speedconclusions.rst up to speed, fix links in packages.rst
|
Sorry, should have looked into how to do this before submitting the PR: I built the readthedocs locally, and had a nit-pick with the order of the footnotes for Idris1 (they now appear in numeric order), but also got a warning that the links to |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
The final page under the "Crash Course in Idris2" was severely out of date, for example it mentioned the freenode IRC channel, which we moved off of years ago.
This PR updates:
Paperspage idris-lang.github.io#16 )(Related: andrevidela/idris-documentation-tracking#7 )