You're viewing the discuss.systems public feed.

Federated feed Local feed

Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:35 PM
@mcc @dysfun couple things:
- idris2 and pack documentation were written independently of each other so they don't explain how to properly delete both
- here are the docs for what pack uninstall does and doesn't do https://github.com/stefan-hoeck/idris2-pack#uninstallation notably it won't change the existing config file
- idris2 itself can be installed via your OS's package manager so removing it depends on how it was installed in the first place, but pack won't interfere with that by default
💬 1🔄 0⭐ 2

Replies

mccmcc@mastodon.social
Oct 14, 2026, 10:42 PM
@Andrev @dysfun apt-cache search idris doesn't turn anything up. I'm using Debian Trixie. Everyone said pack was pretty good so I'd be happy to use pack if it can work.
In my opinion, it should be possible to move from a racket install to a chez install without the assistance of idris2 staff. IMO the bash script, when it fails noting a duplicate install, should recommend pack uninstall instead of removing one folder, and pack uninstall should kill (or offer to kill) the config file.
💬 2🔄 0⭐ 1
mccmcc@mastodon.social
Oct 14, 2026, 10:43 PM
@Andrev @dysfun Would it be helpful for me to file an issue noting the friction I encountered here?
💬 1🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:43 PM
@mcc @dysfun 20'000'000'00%
💬 1🔄 0⭐ 0
mccmcc@mastodon.social
Oct 14, 2026, 10:45 PM
@Andrev @dysfun i think i will file it on pack rather than idris.
💬 2🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:49 PM
@mcc @dysfun Good call, it's also quite likely to be fixed with pack. Idris repo is much slower. Also the maintainer of pack also wrote the better idris2 tutorial so feedback there will also be welcome https://github.com/idris-community/idris2-tutorial
💬 1🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:51 PM
@mcc @dysfun I forgot a crucial piece of information: If you use the repl, please use it with rlwrap. it's unusable without it. There is an option in pack.toml to make that the default
💬 0🔄 0⭐ 1
mccmcc@mastodon.social
Oct 14, 2026, 11:49 PM
@Andrev @dysfun I filed this bug on Idris:
https://github.com/idris-lang/Idris2/issues/3875
And a second bug on Pack:
https://github.com/stefan-hoeck/idris2-pack/issues/409
💬 1🔄 0⭐ 1
gaytabasedysfun@treehouse.systems
Oct 14, 2026, 11:54 PM
@mcc @Andrev i agree, if racket is going to be this slow, we may as well not support it.
💬 1🔄 0⭐ 0
mccmcc@mastodon.social
Oct 14, 2026, 11:57 PM
@dysfun @Andrev like, listing it as an *option* might be ok, but not as an equal alternative to chez. i'd still be surprised if the racket slowdown is "expected" however.
💬 1🔄 0⭐ 0
gaytabasedysfun@treehouse.systems
Oct 15, 2026, 12:00 AM
@mcc @Andrev we expect it to be slower, just not by that much...
💬 1🔄 0⭐ 0
mccmcc@mastodon.social
Oct 15, 2026, 12:06 AM
@dysfun @Andrev If it had been like, 1.7 seconds in chezscheme, 9 seconds in racket, I wouldn't have complained. Well, OK, I absolutely would have complained, but I probably wouldn't have switched to chezscheme.
💬 0🔄 0⭐ 1
gaytabasedysfun@treehouse.systems
Oct 14, 2026, 10:45 PM
@mcc @Andrev yes i think you've only got the pack version installed
i absolutely agree with you. i think we should document switching (was it really just the pack.toml needed?) and i think pack should be more helpful in its setup script about telling you about the config file.
💬 0🔄 0⭐ 1