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

Proper way to upgrade Idris2? #272

Open
mars0i opened this issue Dec 23, 2023 · 3 comments
Open

Proper way to upgrade Idris2? #272

mars0i opened this issue Dec 23, 2023 · 3 comments
Labels
documentation Improvements or additions to documentation

Comments

@mars0i
Copy link

mars0i commented Dec 23, 2023

I had trouble figuring out how to tell pack to install a new release of Idris2. After poking around in the help and trying a few pack commands, I finally discovered that pack switch latest would download, build, and install the latest version (0.7.0, specifically 0.7.0-27780073c at this moment). I might have missed something in the online docs or commandline help, but I didn't find anything that made it clear that this would have the desired effect.

Is this the right way to upgrade Idris2 using pack?

If so, I suggest adding a note somewhere online or in the help docs that clarifies this. I can submit a PR if that would be helpful. I'm not sure what the best documentation strategy is.

Thanks!

@mars0i
Copy link
Author

mars0i commented Dec 23, 2023

(Later I found notes that I wrote to myself earlier suggesting that this in fact the right way to upgrade idris2. I'm not sure where I got the idea from--maybe by the same route as described above, or maybe someone mentioned it on Discord.)

@stefan-hoeck
Copy link
Owner

Using pack switch latest is indeed the correct way to do this. Unfortunately, this is indeed not yet properly documented. It would be great if we had a section about pack switch in the README, probably as a subsection of "Usage". PRs highly welcome.

@mars0i
Copy link
Author

mars0i commented Dec 23, 2023

OK, thanks--I'll submit something when I get a minute. It might not be perfect, but it will be a start, and I won't mind corrections.

@buzden buzden added the documentation Improvements or additions to documentation label Jul 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

No branches or pull requests

3 participants