Skip to content

Conversation

@andrevidela
Copy link
Contributor

addresses one of the points for andrevidela/idris-documentation-tracking#1

  • removes the disclaimer about the instructions not being up to date, we're updating them now
  • Add basic instructions to use pack like pack switch latest and pack build
  • Link to the pack collection

Using `pack switch latest` does indeed update one's installed version of
Idris 2, however, it updates it to the latest git commit (the latest
HEAD) and not the latest release. This is worth clarifying.
This is some larger rewording compared to the previous commit. However,
it felt better to immediately point people to `pack` as the least
painful install process. Mentioning that one can use releases with
`pack`, but that this requires some care, also seemed sensible.
Although both `pack` and Idris2's repo mention needing Chez or Racket at
some point, having this at the very start means people don't get halfway
through the install procedure, only for it to then go "And what Scheme
have you got installed?", which might lead to confusion and/or
frustration. This way, new users will know to set up Chez Scheme or
Racket first, and then return to the Idris install instructions.
@CodingCellist
Copy link
Member

There were some more things that snuck in there whilst editing, sorry... I tried to be careful to have them in separate commits though, so if you dislike any of the changes @andrevidela , please feel free to revert them (or edit the text if that's straightforward) : )

@andrevidela
Copy link
Contributor Author

andrevidela commented Aug 20, 2025

Thanks! I think all changes are good. I slightly reworded the bit about the git commit because it felt strange to suddently talk about git in the middle of the instructions for pack so I moved the original text in a footnote and said it switches to the version of idris that's currently in development. Are we good to merge?

@CodingCellist
Copy link
Member

Thanks, that 100% reads better. Just pushed a tiny fix to the footnote (it seemed to interact weirdly with the monospace markers when running Pelican locally).

I think we're good to merge : )

@stefan-hoeck
Copy link

Thanks for doing this. Looks good to me.

@andrevidela andrevidela merged commit 3978a61 into idris-lang:main Aug 20, 2025
@andrevidela andrevidela deleted the pack-documentation-download branch August 20, 2025 12:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants