3 ms·

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,

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. [1]: https://janus.srht.site/docs/todolist.html https://janus.srht.site/docs/todolist.html [2]: https://git.sr.ht/~janus/web-server-racket-hello-world/tree/master/item/src/HelloWorld.idr https://git.sr.ht/~janus/web-server-racket-hello-world/tree/... [3]: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...

drzzhan 2y ago
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.
ants_everywhere 2y ago
> (like Stackage) but still hosted on GitHub 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.
- tome 2y ago
  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?
  - ants_everywhere 2y ago
    I'm not entirely sure where it uses GitHub and where Hackage, but there are a few GitHub issues on the Stack repo about it: - Binary upgrade of Stack fails due to GitHub API request limit #4979 (https://github.com/commercialhaskell/stack/issues/4979 https://github.com/commercialhaskell/stack/issues/4979) - GitHub rate limiting can affect Stack CI #6034 (https://github.com/commercialhaskell/stack/issues/6034 https://github.com/commercialhaskell/stack/issues/6034) And a few more. The "fix" is having Stack impersonate the user (https://github.com/commercialhaskell/stack/pull/6036 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.
    - tome 2y ago
      Thanks! So it seems to be not packages, but templates, and this comment suggests it wasn't GitHub doing the rate limiting after all: https://github.com/commercialhaskell/stack/issues/4979#issuecomment-1603388213 https://github.com/commercialhaskell/stack/issues/4979#issue... > 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.
      - ants_everywhere 2y ago
        > 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.
orbifold 2y ago
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.

drzzhan 2y ago

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.

ants_everywhere 2y ago

> (like Stackage) but still hosted on GitHub 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.

tome 2y ago
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?
- ants_everywhere 2y ago
  I'm not entirely sure where it uses GitHub and where Hackage, but there are a few GitHub issues on the Stack repo about it: - Binary upgrade of Stack fails due to GitHub API request limit #4979 (https://github.com/commercialhaskell/stack/issues/4979 https://github.com/commercialhaskell/stack/issues/4979) - GitHub rate limiting can affect Stack CI #6034 (https://github.com/commercialhaskell/stack/issues/6034 https://github.com/commercialhaskell/stack/issues/6034) And a few more. The "fix" is having Stack impersonate the user (https://github.com/commercialhaskell/stack/pull/6036 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.
  - tome 2y ago
    Thanks! So it seems to be not packages, but templates, and this comment suggests it wasn't GitHub doing the rate limiting after all: https://github.com/commercialhaskell/stack/issues/4979#issuecomment-1603388213 https://github.com/commercialhaskell/stack/issues/4979#issue... > 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.
    - ants_everywhere 2y ago
      > 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.

orbifold 2y ago

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.