Login
You're viewing the discuss.systems public feed.

Replies

  • mccmcc@mastodon.social
    Oct 14, 2026, 8:48 PM

    Among the things not mentioned in either Idris tutorial

    - What file extension is used for Idris files? (it's .idr)

    - How do you execute an idris file?

    Running idris2 puts you at a REPL. Running "idris2 src/puzzle.idr" churns a long time, creates a series of utterly baffling files in a build/ subdirectory, then drops you at the same repl. "-c" does this then quits; but it still does nothing useful.

    One tutorial implies "pack -o hello exec src/puzzle.idr" will do something; this hangs forever

    💬 3🔄 0⭐ 3
  • mccmcc@mastodon.social
    Oct 14, 2026, 8:50 PM

    I understand true LISP heads are comfortable just spending all their time in a REPL forever. I am not a true LISP head. I'm an ocaml poser.

    I *think* the mysterious "pack" command, while hanging, created in the mysterious "build" subdirectory a "hello.rkt" file that wouldn't have been there otherwise. I remember someone saying idris works by transpiling itself to a "backend" lang, so maybe I'm supposed to figure out the non-hanging args to "pack", transpile, then execute the rkt file in racket.

    💬 3🔄 0⭐ 4
  • mccmcc@mastodon.social
    Oct 14, 2026, 9:04 PM

    *Rubbing eyes* okay, so

    idris2's command line --help lists a "-o <file>" flag, which "specifies output file". Output file for what? Apparently this actually means "build an executable, put it in ./build/exec [path non-negotiable], and name it <file>".

    I run this. I run it in `time`. It does create a runnable Linux executable.

    It takes it one minute and fifty-three seconds to compile the program:

    main : IO ()
    main = putStrLn "Help"

    During which time I sincerely could not tell if it had hung

    💬 2🔄 0⭐ 4
  • mccmcc@mastodon.social
    Oct 14, 2026, 10:30 PM

    So after a brief conversation with Idris2 maintainers

    - Idris can run on top of either "Racket" or "Chez". I went with Racket because I thought it was the fast one. This is no longer true. The maintainers expect Chez to be a little faster. In fact it's hundreds of times faster. This surprises the maintainers.

    - Additionally, in Debian, Chez takes up 10% the disk space of Racket.

    After what I'd consider a somewhat unfriendly uninstall procedure, I re-install idris2, atop Chez.

    It doesn't work

    long bunch of bash garbage. toward the end it says to delete /home/mcc/.local/state/pack.
    idris2 -o puzzle src/puzzle.idr Error loading file "src/puzzle.idr#!/bin/sh": File not found
    💬 2🔄 1⭐ 2
  • 💬 2🔄 0⭐ 0
  • 💬 1🔄 0⭐ 1
  • Michelle HughesMegaMichelle@a2mi.social
    Oct 14, 2026, 8:27 PM

    @mcc

    I used to be afraid of functional programming languages like Haskell and erlang because I thought they were logic solvers like prolog, and I was not able to wrap my head around prolog. But no, erlang just turned out to be just a different way to express imperatives. Then I was using prolog to solve the "murdle" logic game puzzles for awhile, so I'm less scared of it than I was, but I still don't think I could make a web application with it.

    💬 1🔄 0⭐ 1
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • d@nny disc@hipsterelectron@circumstances.run
    Oct 14, 2026, 8:31 PM

    @MegaMichelle @mcc idris is the one programming language with a theory of dependent types which can be used in very interesting ways and the language comes from an academic community very close to interactive theorem provers although the proof community will tell you its theory isn't quite sound

    💬 1🔄 0⭐ 1
  • d@nny disc@hipsterelectron@circumstances.run
    Oct 14, 2026, 8:33 PM

    @MegaMichelle @mcc unsure if andi mentioned this yet but the language is VERY stridently anti-LLM and apparently edwin who is credited with starting the project is a nice guy who likes writing music

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

    @mcc pack is just a package manager for idris. all it really does apart from install idris and idris packages is wrap the idris2 command.

    💬 0🔄 0⭐ 0
  • technomancytechnomancy@hey.hagelb.org
    Oct 14, 2026, 8:53 PM

    @mcc yes but with caveats; when people read "spend all day in the repl" it's often read as "spend all day looking at the repl prompt" but the real meaning is more like "your editor is constantly connected to the repl and usually sending entire files over to it"

    (you don't actually spend that much time looking at the repl itself)

    💬 1🔄 1⭐ 0
  • 💬 0🔄 0⭐ 0
  • technomancytechnomancy@hey.hagelb.org
    Oct 15, 2026, 5:44 AM

    @fabiosantoscode just constantly recompiling and running tests as part of the normal feedback loop; editor integration functions allow you to run the currently focused test and see if it passed

    you switch to the repl buffer in cases where you specifically need to see the values, yeah

    💬 0🔄 0⭐ 0
  • 💬 2🔄 0⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 9:06 PM

    @mcc @Andrev although didn't you say something about using the racket backend? it's slower on racket, but surely not that much slower, given racket is also based on chez now.

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

    @dysfun @Andrev It also takes 1 minute and 53 seconds on an incremental build if I change the string "Help" to "Helx".

    The way I installed idris2 was I installed Racket via apt, and then I ran a bashfile curled from the "pack" website. On the first step, it asked me my scheme interpreter, [racket] was the default [possibly because chez was not installed]. It was *very* slow.

    How do I switch from "racket" to "chez"? Do I rerun the bash? Do I have to uninstall the old version first?

    💬 3🔄 1⭐ 1
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 9:24 PM

    @mcc @Andrev yes, rerun the bash after installing chez. if memory serves, it will complain that the installation already exists at a given path if you're not sure where it is to remove it.

    💬 0🔄 0⭐ 1
  • Samael :therian:Kishi@meow.social
    Oct 14, 2026, 9:28 PM

    @mcc @dysfun @Andrev

    I have had no luck getting idris2 built and running. There are chez-related test errors in channels (and this is pulling both chez-scheme and idris2 from latest git sources), and it appears to have been this way for some time (unclear how long, and I do not currently have the spoons to dig). I did not try a Racket-based situation, so I may attempt that later.

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

    @Kishi @mcc @Andrev what are you running on? like if pack doesn't work (happened a few weeks ago), it should still be trivial to build idris out of the repo like we used to have to. they ship a precompiled version for bootstrapping.

    💬 2🔄 0⭐ 1
  • 💬 0🔄 0⭐ 1
  • Samael :therian:Kishi@meow.social
    Oct 14, 2026, 10:24 PM

    @dysfun @mcc @Andrev

    Arch derivative, unfortunately. I haven't been able to push myself back to Gentoo.

    idris2-git, chez-scheme-git, idris2-pack-git (all AUR because apparently nobody at arch packages it), though pack never happened because idris2 never succeeded in tests, and pack depends on it. I would attempt to debug, but I'm sick today and don't have the energy.

    There's an issue somewhere in one of idris2 or chez-scheme which describes test failures in a container, and that issue perfectly describes the symptoms I see.

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

    @Kishi @mcc @Andrev i mean ideally we'd like it to just work everywhere. when you're feeling better, try cloning the idris repo and following the build instructions and see if it still fails.

    💬 0🔄 0⭐ 1
  • 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
  • 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
  • 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
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 9:17 PM

    @dysfun @mcc oh my god what is going on with racket? Yeah using chez scheme takes 0.36s (of which 0.3 is spinning up the chez runtime), but using racket takes 7.68s


    time idris2 hello.idr -o program
    idris2 hello.idr -o program  0.36s user 0.08s system 96% cpu 0.452 total

    time idris2 --cg racket hello.idr -o program
    idris2 --cg racket hello.idr -o program  7.68s user 0.62s system 96% cpu 8.560 total
    💬 1🔄 1⭐ 0
  • gaytabasedysfun@treehouse.systems
    Oct 14, 2026, 9:19 PM

    @Andrev @mcc huh? isn't that just running the racket backend under chez? why is the backend for racket so much slower under chez?!

    💬 1🔄 0⭐ 0
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 9:22 PM

    @dysfun @mcc No clue, I don’t remember being such a big difference in the past. This must have happened in the last year or two. I’m sure this is something we can ask the racket people about, we’re probably passing incorrect arguments to racket (or overly conservative ones)

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

    @Andrev @mcc the only thing i remember was some comment a couple of years back (i think it was edwin?) saying he had to change the gc options to make performance better?

    but like 2 minutes to compile hello world is clearly beyond the pale. even idris1 didn't take that long!

    💬 1🔄 0⭐ 0
  • Andre VidelaAndrev@types.pl
    Oct 14, 2026, 9:31 PM

    @dysfun @mcc

    Here is what I know of what’s going on for chez cheme, and how that relates to other codegens:

    • The compiler being a scheme program needs to start the scheme runtime. Chez sheme takes about 300ms to bootup, so every invocation of the compiler takes at least that much
    • typechecking of such programs is essentially instantaneous
    • compilation takes a while. we generate scheme code and then we rely on chez to compile it and optimise it.

    once we emit scheme code we call racket or chezscheme and have them compile and optimise the executable, this can take a while especially when linking large projects.

    For a hello world this should be fast, no idea why racket is so slow. Chezscheme performs as expected (0.36s) where 0.3 is taken by booting up the runtime, and 0.06 by compiling the executable

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

    @Andrev @mcc yes, sorry, what i mean is selecting the racket codegen is still running it under chez, no? just like i can select the javascript codegen and it's still running under chez? i guess it has to call racket afterwards?

    but that's clearly a lot slower. and apparently on the scale of compiling hello world entirely on racket, that's 2 minutes.

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