Lean aims to be a general purpose language, but I haven't seen people actually write HTTP servers in it. If Leo de Moura really wanted it to be general purpose, what does the concurrent runtime look like then? To my knowledge, there isn't one?
That's why I've been writing an HTTP server in Idris2 instead. Here's a todo list demo app[1] and a hello world demo[2]. The advantage of Idris is that it compiles to e.g. Racket, a high level language with a concurrent runtime you can bind to from Idris.
It's also interesting how languages don't need their own hosting (e.g. Hackage) any more. Idris packages are just listed in a TOML file[3] (like Stackage) but still hosted on GitHub. No need for versions, just use git commit hashes. It's all experimental anyway.
There are tasks, which are implemented as part of the runtime and they appear to plan to integrate libuv in the future. Some of the runtime seems to be fairly easy to hack and have somewhat nice ways of interoperating with both C, C++ and Rust.
I don't have much experience with Haskell, but one of the worst experiences has been Stack's compile time dependency on GitHub. GitHub rate limits you and builds take forever.
That's interesting. Could you say more? This is something that we (speaking as part of the Haskell community) should fix. As far as I know Stack/Stackage should pick up packages from Hackage. What does it use GitHub for?
And a few more. The "fix" is having Stack impersonate the user (https://github.com/commercialhaskell/stack/pull/6036) and authenticate to the API. This unblocks progress, but this is really a design bug and not something I think people should emulate.
Every other language I've used allows you to build code without authenticating to a remote service.
> Every other language I've used allows you to build code without authenticating to a remote service.
Sure, the problem here wasn't "building". It was downloading a package template (which one doesn't tend to do 60 times per hour). I agree packages shouldn't be fetched from GitHub.
> and this comment suggests it wasn't GitHub doing the rate limiting after all
That comment is from someone other than the ticket filer who was seeing another issue even after sending the GitHub token. It was this second issue that wasn't caused by GitHub rate limiting -- the original one was.
> It was downloading a package template (which one doesn't tend to do 60 times per hour).
I've personally had Stack-related GitHub API rate limiting delay builds by at least an hour due to extreme slowness. So whatever the rate limits are, Stack occasionally hits them.
This is not related to Lean or Haskell. I'm just wondering why when people are curious about a new general-purpose language, the first thing they test is an HTTP server.
That's why I've been writing an HTTP server in Idris2 instead. Here's a todo list demo app[1] and a hello world demo[2]. The advantage of Idris is that it compiles to e.g. Racket, a high level language with a concurrent runtime you can bind to from Idris.
It's also interesting how languages don't need their own hosting (e.g. Hackage) any more. Idris packages are just listed in a TOML file[3] (like Stackage) but still hosted on GitHub. No need for versions, just use git commit hashes. It's all experimental anyway.
[1]: https://janus.srht.site/docs/todolist.html [2]: https://git.sr.ht/~janus/web-server-racket-hello-world/tree/... [3]: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...