You're viewing the discuss.systems public feed.

Federated feed Local feed

gaytabasedysfun@treehouse.systems
Oct 14, 2026, 10:30 PM
@mcc @Andrev no, that's just the instructions were shit and you're still using racket. but andre said earlier that you can just change it to use chez. and set codegen to chez just in case.
worth a shot anyway.
💬 3🔄 0⭐ 1

Replies

mccmcc@mastodon.social
Oct 14, 2026, 10:31 PM
@dysfun @Andrev this is the messaging i got https://files.mastodon.social/media_attachments/files/117/441/439/551/038/778/original/98b051da6f63d494.png
💬 2🔄 0⭐ 0
gaytabasedysfun@treehouse.systems
Oct 14, 2026, 10:34 PM
@mcc @Andrev yes, that's what i mean by the instructions are shit. it isn't a full uninstall because of that pack.toml it isn't telling you about.
💬 0🔄 0⭐ 0
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
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
mccmcc@mastodon.social
Oct 14, 2026, 10:34 PM
@dysfun @Andrev setting scheme = "chezscheme" and codegen = "chez" appears to have fixed the problem. i can now use either idris2 or pack and it works. no #!/usr/bin bug. i am a little concerned whether other things are subtly broken somewhere.
💬 2🔄 0⭐ 1
gaytabasedysfun@treehouse.systems
Oct 14, 2026, 10:36 PM
@mcc @Andrev tbh, if it works at all and isn't using racket, that's the bit i'd have expected to break.
💬 0🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:37 PM
@mcc @dysfun In case things break pack --bootstrap update can fix a lot of things.
💬 1🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:41 PM
@mcc @dysfun By the way, since you mentionned you don't have an ipkg file: You will need one to use lsp, you can try:
- idris2 --init and set the source directory in src and place your .idr files there
- pack new bin helloWorld and that will setup a whole project for you including pack.toml, helloWorld.ipkg and test folders
💬 1🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 14, 2026, 10:42 PM
@mcc @dysfun ah and finally, to install lsp, try
```
pack install-app idris2-lsp
```
The name of the binary is idris2-lsp, that's the main piece of info your editor needs to have LSP work. The compiler will run on save
💬 0🔄 0⭐ 0
MHC Levinmhcat@neuromatch.social
Oct 15, 2026, 12:14 AM
@dysfun @mcc @Andrev
to chez or to the name of the chez binary?
💬 1🔄 0⭐ 0
Andre VidelaAndrev@types.pl
Oct 15, 2026, 8:16 AM
@mhcat @dysfun @mcc Just to be clear, there are two options here:
- the first one expect the name of the chez binary
- The second one expect the name of the codegen used by idris, either "chez", "racket" "node" or "javascript"
💬 1🔄 0⭐ 0
mccmcc@mastodon.social
Oct 15, 2026, 9:15 PM
@Andrev @mhcat @dysfun ok so on that note
$ pack exec src/puzzle.idr abcd
abcd
# At this moment I edit puzzle.idr so it no longer compiles
$ pack exec src/puzzle.idr abcd
[ fatal ] Error when executing system command.
Command: "/home/mcc/.local/state/pack/install/b6cbc25d5cd2ef2a250556266fd7b68dfc360f8b/idris2/bin/idris2" "--cg" "chez" "--source-dir" "src" "--cg" "chez" "-o" "_tmppack" "src/puzzle.idr"
Error code: 1
# Is this error messaging surprising?
💬 0🔄 0⭐ 0