Login
You're viewing the f.duriansoftware.com public feed.
  • mccmcc@mastodon.social
    Oct 14, 2026, 10:37 PM

    After some poking, it turns out that installing Idris2 in Racket mode, then uninstalling with the given instructions, then re-installing in Chez mode, leaves the system in an inconsistent state where it sometimes uses Racket and sometimes doesn't work at all. I need to stress I have various community members and maintainers in my mentions trying to help me and they're being very nice. They give me hand-surgery to perform on a TOML file. It ixes it. Compiling takes 1.4s instead of over 2 minutes.

    running idris2 and pack at the command line
    💬 2🔄 0⭐ 0

Replies

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

    Furthermore, it appears that in addition to the two tutorials I mention above, the ones linked from the regular Idris website, there is a third, secret tutorial, and this one explains how to actually execute a piece of code, explains why readline isn't working right in the idris2 repl, etc. codeberg.org/jjl/tutorials/src

    I guess I can move on now. Hopefully there aren't more nasty surprises lurking in my toml configuration file (presumably lying in wait to blow up if I attempt to configure an LSP).

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 15, 2026, 1:38 AM

    So Sublime Text doesn't have an Idris LSP package-- only an Idris syntax highlighting package.

    But it turns out if I `pack install-app idris2-lsp, then in Sublime go to Package Settings -> LSP -> Server Configurations

    {
    "idris2-lsp": {
    "enabled": true,
    "command": ["/home/mcc/.local/bin/idris2-lsp"], // Update the PATH
    "selector": "source.idris"
    }
    }

    It just like… magically works. I have type-on-hover now. As long as I create a .lidr file with idris2 --init.

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

    @dysfun one thing i notice was that there was *NO* codegen option selected. like it didn't say codegen=racket, codegen was just commented out. Maybe whatever codegen is just wasn't happening

    💬 1🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 10:48 PM

    @mcc yes, so i think it should default to the codegen for whatever it's currently running on (so chez would default to chez and racket to racket), but i only use chez so i figured changing that was easier than debugging if for some reason it wasn't that.

    codegens are just the final step in the compiler. you use exactly one at a time. idris itself comes with several (chez, racket, javascript etc.). every idris has all of those built in. the code they produce is intended for different runtimes, obviously.

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

    @dysfun also I think it's weird my chez is named chezscheme but the toml file key is chez

    💬 1🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 10:51 PM

    @mcc the codegen is called chez, that's the internal name. the scheme should match whatever the binary name is on your system.

    💬 0🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 10:42 PM

    @mcc mmm, the only other option i ever touch is 'bootstrap'. you might want to have a look, like you can enable rlwrap for example. i don't think there are any more surprises.

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

    @dysfun bootstrap and bootstrap-stage3 are not set at all. they are commented out. what would enabling one of these do for me?

    💬 1🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 10:49 PM

    @mcc i don't know what the stage 3 thing is.

    pack will let you use your existing idris to build idris. if it's too old to compile the new idris you will be forced to bootstrap (which uses the precompiled chez version in the repo)

    💬 0🔄 0⭐ 0