Login
You're viewing the discuss.systems public feed.
  • 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

Replies

  • 💬 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