Login
You're viewing the discuss.systems public feed.
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 9:25 PM

    @mcc @dysfun pack is the way to go, you have a pack config file in your .config. it has a scheme field on which you can put the executable name for your version of scheme (assuming its installed). For me it’s “scheme” on the mac and “chezscheme” on linux, might be different for you. There should be nothing else to change, pack will use the right version of scheme onwards

    edit: added screenshot of my config

    Image attached toot
    💬 1🔄 0⭐ 1

Replies

  • mccmcc@mastodon.social
    Oct 14, 2026, 10:05 PM

    @Andrev @dysfun imagine i deleted ~/.local/state/pack, re-ran the bash script that installs pack, and selected chezscheme this time. then i delete my ./build and re-run idris2 -o. And I get this message.

    What do you make of this?

    idris2 -o puzzle src/puzzle.idr Error loading file "src/puzzle.idr#!/bin/sh": File not found
    💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 10:18 PM

    @mcc @dysfun

    this is the error that idris throws when the path given cannot be found. It looks like the argument parser injested the string ending in "#!/bin/sh" which is clearly clearly wrong on multiple aspects.
    2 questions:

    • is if different if you use pack exec src/puzzle.idr?
    • is it different if you type out the command rather than using !?
    💬 2🔄 0⭐ 1
  • mccmcc@mastodon.social
    Oct 14, 2026, 10:26 PM

    @Andrev @dysfun

    1. Typing out the command does not change the outcome.

    2. time pack exec src/puzzle.idr does work. However it takes 1 minute 51 seconds. so i have not solved the problem from the racket version. a 2 minute iteration time is survivable but pretty painful.

    Additionally, although the bash script was told to use chezscheme, when I run "top" while pack is running, I see "racket" is using 100% CPU.

    Note that i do not have an ipkg file anywhere.

    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 14, 2026, 10:29 PM

    @dysfun @Andrev scheme="racket"

    and "codegen" is not set.

    It is increasingly looking like installing idris2 once with racket as your scheme "mines" your system in such a way it is no longer possible to cleanly install a chezscheme version of idris2.

    💬 1🔄 0⭐ 0
  • 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
  • 💬 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 github.com/stefan-hoeck/idris2 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
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 2🔄 0⭐ 0
  • 💬 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
  • 💬 1🔄 0⭐ 1
  • 💬 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
  • 💬 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
  • 💬 0🔄 0⭐ 0
  • 💬 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
  • 💬 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
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 10:22 PM

    @mcc @dysfun Here is another potential source of confusion. your version of idris installed by pack might not be the same as the one installed by the system. here is an example where the version in bin/idris2 is not the same as the version invoked by pack.

    So if you killed pack and reinstalled it, you might not necessarily have killed the old version of idris

    EDIT: This is one of the reasons doing anything via pack is a lot more reliable because it will pick the correct version of idris for you current project and keep that up to date, including libraries and tools like idris2-lsp

    Image attached toot
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 14, 2026, 10:27 PM

    @Andrev @dysfun Looking in ~/.local/bin, I see an "idris2" and a "pack".

    The bash installer for pack said only to delete ~/.local/pack . What is the correct uninstallation procedure for idris/pack? Is it documented somewhere?

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 1