search

algebraic-dev / melp

🕸️ | Incomplete HTTP/1.1 Server in Lean4 for Rinha de backends
16 stars 1 forks source link

Merging melp and requests #1

Open chuwy opened 11 months ago

chuwy commented 11 months ago

Hey @algebraic-sofia! Seems you're the first one to create a working HTTP ecosystem in Lean 4! Looks cool!

I'm wondering if you think it's a sane idea to collect all related stuff under one umbrella (let's assume it's going to be Melp), like it's done in http4s (Scala), where they have a single core (http4s-core), describing the whole domain of HTTP primitives like methods, statuses, requests, responses etc, then http4s-client (that is your requests) to operate those entities to make requests and http4s-server to accept those requests (more melp rather than ash).

Asking because I'm trying to write a Servant analog in lean4 and looking for unified description of HTTP domain and there's bit of duplication between requests and melp. Obviously not critical now, but trying to imagine what future might look like.

I can send a PR if you think it would work out for you.

algebraic-dev commented 11 months ago

Hi, these libraries are just prototypes. I'm planing on rewriting them as soon as possible, if you have any ideas on how to improve the code I would love to receive PRs or if you just start a new project I think I can just archive ash, melp and requests in favour of your project.

If you want to create an organization for it in order to organize all of these things, I would love to participate :)

chuwy commented 11 months ago

If you want to create an organization for it in order to organize all of these things, I would love to participate :)

You said that! Let's try :) https://github.com/axiomed

Do you mind if I copy-paste some of your code then?

P.S. Feel free too to share ideas on naming, I'm not very good at it.

algebraic-dev commented 11 months ago

Do you mind if I copy-paste some of your code then?

Not a problem!

algebraic-dev commented 11 months ago

So lets organize this thing @chuwy. I saw that you created a repo called Http.lean, It's going to be both the client and the server implementation? and the core that you mentioned? Can you create a repo for client, server and the core so we can just can make everything in parallel?