http requests

Stream: lean4

[Adam Topaz]

What's the state of the art for making http(s) requests using lean4? I remember that someone was working on an http library a while ago, but I can't seem to find it. Is this the best approach? If I understand correctly, lake has some wrappers around curl for such requests, is that right?

[Matthew Ballard]

https://github.com/xubaiw/Socket.lean/tree/main/examples/http-server ?

[Adam Topaz]

yeah I think that's the repo I was thinking of. Thanks. I guess what I'm looking for is something with a similar functionality as python's requests package.

[Adam Topaz]

I suppose such a thing doesn't exist.

[Henrik Böving]

Such a thing does indeed not exist yet.

[Joachim Breitner]

The repo you linked above archived now. Are there “serious” lean4 libraries for Sockets/TCP/HTTP already?

[François G. Dorais]

Not that I know of but this is something I seriously considered doing, I gave up thinking that somebody with better knowledge than me would eventually do it. I'm still very interested though!

[Henrik Böving]

The above is the only one that I am aware of. And getting this done in an async fashion is even further out of reach right now.

[Henrik Böving]

That said my reason for not doing it is the same as @François G. Dorais so maybe someone :tm: should just do it :D

[Adam Topaz]

Presumably it should be relatively easy to make a wrapper around the curl c api

[Adam Topaz]

Anyway, it would be great to have such a thing.

[Pim Otte]

As far as I know, https://github.com/lurk-lab/Http.lean is state of the art (and building on a fork of repo archived above)

[Henrik Böving]

Henrik Böving said:

That said my reason for not doing it is the same as François G. Dorais so maybe someone :tm: should just do it :D

I'll do it to learn alloy now^^

[Arthur Paulino]

Developing a proper HTTP request API for Lean 4 is definitely something I've wanted to do for a while. If someone is going to spearhead such a project and needs an extra pair of hands, just ping me or send a DM

[Henrik Böving]

@Mac Malone i've got this setup so far: https://github.com/hargoniX/socket.lean and I tried to compile just to see if it works and am getting

ld.lld: error: relocation R_X86_64_32S cannot be used against local symbol; recompile with -fPIC
>>> defined in ./build/ir/Socket.alloy.c.o
>>> referenced by Socket.alloy.c
>>>               ./build/ir/Socket.alloy.c.o:(lean_mk_socket)

ld.lld: error: relocation R_X86_64_32S cannot be used against local symbol; recompile with -fPIC
>>> defined in ./build/ir/Socket.alloy.c.o
>>> referenced by Socket.alloy.c
>>>               ./build/ir/Socket.alloy.c.o:(lean_mk_socket)

ld.lld: error: relocation R_X86_64_32 cannot be used against local symbol; recompile with -fPIC
>>> defined in ./build/ir/Socket.alloy.c.o
>>> referenced by Socket.alloy.c
>>>               ./build/ir/Socket.alloy.c.o:(lean_mk_socket)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/nix/.elan/toolchains/leanprover--lean4---nightly-2023-08-19/bin/leanc` exited with code 1

any idea? do I have to sneak -fPIC in?

[Mac Malone]

@Henrik Böving I would certainly give-fPIC a try (via moreLeancArgs).

[Henrik Böving]

That seems to work indeed

[Henrik Böving]

Can a linker magician tell me why I need FPIC? :D

[Mac Malone]

@Henrik Böving It sounds like it may be due to mixing shared and static libraries based on this StackOverflow question.

[Mac Malone]

However, I am curious why I never encountered this problem in the Alloy S test.

[Mac Malone]

@Henrik Böving A more generally comment on your code. One of the advantages of Alloy is that C code is now Lean code, so you can use Lean metaprogramming to generate definitions. For instance, you could define some custom syntax/elaborator to map your enums to C and back instead of having to write it all manually.

[Henrik Böving]

Oh :eyes: that's a good idea yeah, i'll try that

[Mac Malone]

@Henrik Böving Also, if anything breaks, report it! I have only tested Alloy on a few examples, so you are essentially an Alloy beta tester. Thus, I would appreciate any feedback you can provide (both bugs and feature requests). Also, do not be hesitant to blame any breakage on Alloy. :laughing:

[Henrik Böving]

:D sure!

[Henrik Böving]

@Mac Malone I have one right away!

  `(command|
    alloy c section
      static inline $cType $leanToC($ffiType arg) {

      }
    end
   )

where

ffiType : Ident

application type mismatch
  ffiType.raw
argument
  ffiType
has type
  Ident : Type
but is expected to have type
  TSyntax `Alloy.C.pointer : Type

is there a nice way to make these or do I go the raw route?

[Mac Malone]

@Henrik Böving Could you give a full #mwe? (i.e., with an example of what cType and leanToC are as well)

[Henrik Böving]

syntax "alloy" "c" "enum" ident " : " ident "translators" ident " ↔ " ident "where" ("| " ident " = " ident)+ : command

macro_rules
| `(command| alloy c enum $name:ident : $cType:ident translators $leanToC:ident ↔ $cToLean:ident where $[| $leanVariant:ident = $cVariant:ident]*) => do
  let ffiType ←
    if leanVariant.size <= 2^8 then
      pure <| mkIdent `uint8_t
    else if leanVariant.size <= 2^16 then
      pure <| mkIdent `uint16_t
    else if leanVariant.size <= 2^32 then
      pure <| mkIdent `uint32_t
    else
      Macro.throwError s!"Enum {name} has more than 2^32 variants, this is not supported"
  `(command|
    alloy c section
      static inline $cType $leanToC($ffiType arg) {
      }
    end
   )

[Mac Malone]

@Henrik Böving It is clear I am missing some TSyntax Coe instance, the question is: which ones/ Currently working on it.

[Henrik Böving]

I'll use the fast forward button (formely known as "sleeping") in that case :P

[Mac Malone]

@Henrik Böving Having finished investigating, this is actually just due to ambiguities of the C grammar. You just need to be explicit about the syntax kind:

 static inline $cType $leanToC:ident($ffiType:ident arg) {}

[Mac Malone]

Also, out of curiosity, @Henrik Böving, are you making use of Alloy's clangd LSP integration (i.e., do you see semantic highlighting, hovers, go-to-def, etc. in C code)?

[Joachim Breitner]

After seeing your message I tried it in loogle (by changing the nix shell to use the clang-stdenv, so any problems may be nix-related), but I get

Lean (version 4.0.0-nightly-2023-08-15, commit b5a736708f40, Release)
E[10:35:06.889] Trying to remove file from TUScheduler that is not tracked: /dev/null
[Error - 10:35:06] Request textDocument/semanticTokens/range failed.
  Message: C language server request 3 failed: trying to get AST for non-added document
  Code: -32602

[Henrik Böving]

Mac Malone said:

Also, out of curiosity, Henrik Böving, are you making use of Alloy's clangd LSP integration (i.e., do you see semantic highlighting, hovers, go-to-def, etc. in C code)?

I do see proper highlighting of the code yes, didn't try the rest yet

[Henrik Böving]

I present the final:

macro_rules
| `(command| alloy c enum $name:ident : $cType:ident translators $leanToC:ident ↔ $cToLean:ident where $[| $leanVariant:ident = $cVariant:ident]*) => do
  let ffiType ←
    if leanVariant.size <= 2^8 then
      pure <| mkIdent `uint8_t
    else if leanVariant.size <= 2^16 then
      pure <| mkIdent `uint16_t
    else if leanVariant.size <= 2^32 then
      pure <| mkIdent `uint32_t
    else
      Macro.throwError s!"Enum {name} has more than 2^32 variants, this is not supported"
  let counter := Array.range leanVariant.size |>.map (Syntax.mkNumLit <| toString ·)
  `(
    inductive $name : Type where $[ | $leanVariant:ident]*
    alloy c section
      static inline $cType $leanToC:ident($ffiType:ident arg) {
        switch (arg) {
          $[
            case $counter:num:
              return $cVariant:ident;
          ]*
          default:
            lean_panic_fn(lean_box(-1), lean_mk_string("illegal C value"));
        }
      }

      static inline $ffiType $cToLean:ident($cType:ident arg) {
        switch (arg) {
          $[
            case $cVariant:ident:
              return $counter:num;
          ]*
          default:
            lean_panic_fn(lean_box(-1), lean_mk_string("illegal Lean value"));
        }
      }
    end
   )

Sadly all of those annotations are necessary right now. But I'm quite happy it just seems to work out! The highlighting also works very nicely!

image.png

[Mac Malone]

@Henrik Böving I added a many more coercions last night and one more right now which allowed me to get it down to this:

case $counter:constExpr:
    return $cVariant;
[...]
case $cVariant:constExpr:
   return $counter;

But sadly many of those annotations don't seem removable.

[Henrik Böving]

That's fine for me right now, If you know about it it becomes trivial^^

I do have a second idea already as well, for the sockaddr_in and sockaddr_in6 i essentially just need to manage a void pointer with Lean so I wrote this:

scoped syntax "alloy" "c" "alloc" ident " = " ident "as" ident "translators" ident " ↔ " ident "finalize" ident : command

macro_rules
| `(command| alloy c alloc $name:ident = $cName:ident as $externClass:ident translators $leanToC:ident ↔ $cToLean:ident finalize $finalizer:ident) =>
  let nonemptyType := mkIdent <| name.getId.append `nonemptyType
  `(
    opaque $nonemptyType : NonemptyType
    def $name : Type := NonemptyType.type $nonemptyType
    instance : Nonempty $name := Subtype.property $nonemptyType

    alloy c section
      static lean_external_class* $externClass:ident = NULL;

      static void $finalizer:ident(void* ptr) {
        free(($cName:ident*)ptr);
      }

      static inline lean_object* $cToLean:ident($cName:ident* ptr) {
        if ($externClass:ident == NULL) {
          $externClass:ident = lean_register_external_class($finalizer:ident, NULL);
        }
        return lean_alloc_external($externClass:ident, ptr);
      }

      static inline $cName:ident* $leanToC:ident(b_lean_obj_arg ptr) {
        return ($cName:ident*)(lean_get_external_data(ptr));
      }
    end
  )

used like so

alloy c alloc SockAddr4 = sockaddr_in as g_sockaddr_in_external_class translators sockaddr_in_to_lean ↔ lean_to_sockaddr_in finalize sockaddr_in_finalize

which gives me the new and exciting!

command is ill-formed (cannot be reprinted)

how do I go from here? :D

[Mac Malone]

@Henrik Böving To fix it, use $cToLean:ident($cName* ptr) instead of $cToLean:ident($cName:ident* ptr). Why this is happening I am not quite sure.

[Mac Malone]

Somehow the annotation is producing some syntax it cannot reprint.

[Henrik Böving]

That works indeed, next question! Since sockaddr_in is a struct that is not typedef-ed I need to struct sockaddr_in in my generated C code. What is the proper category to replace ident on the cName variable with? @Mac Malone

[Mac Malone]

@Henrik Böving If you update, it should figure that one out automatically (I tested that so it should hopefully work).

[Mac Malone]

(For reference though, the kind is aggrSig.)

[Henrik Böving]

Is it not cTypeSpec?

[Mac Malone]

Oh, maybe I am misunderstanding. What do you want to exactly?

[Mac Malone]

I thought you just wanted to do struct $var:kind

[Henrik Böving]

Ah that is also an option yes. But I was thinking about keeping it generic maybe? So turning:

scoped syntax "alloy" "c" "enum" ident " : " ident "translators" ident " ↔ " ident "where" ("| " ident " = " ident)+ : command

into a syntax that accepts (syntactically) both:

alloy c alloc SockAddr4 = sockaddr_in as struct g_sockaddr_in_external_class translators sockaddr_in_to_lean ↔ lean_to_sockaddr_in finalize sockaddr_in_finalize

and

alloy c alloc SockAddr4 = sockaddr_in as g_sockaddr_in_external_class translators sockaddr_in_to_lean ↔ lean_to_sockaddr_in finalize sockaddr_in_finalize

such that a user is not necessarily forced to use it with structs

[Henrik Böving]

So my question is what do I have to replace the second ident in the syntax decl with such that it captures struct sockaddr_in and also just a basic sockaddr_in? Or in general any valid c type I guess.

[Mac Malone]

Oh, that is actually a bit complicated depending on the generality you are going for. The C grammar is weird.

[Henrik Böving]

:sad: maybe just struct ident and ident then? :D Do we have something for that?

[Mac Malone]

However, I think in your case what you want is cDeclSpec+.

[Henrik Böving]

O_o why the +?

[Mac Malone]

What makes it interesting is you then want to to put a pointer after it, which happens to be be the convenient boundary point.

[Mac Malone]

Henrik Böving said:

O_o why the +?

Because your presumable also want to accept thins like const struct sockaddr_in.

[Mac Malone]

however, if you do just want plain types, you are correct that the category iscTypeSpec.

[Henrik Böving]

Hurray it works indeed. This is the most fun i've had with C in a while :D

[Mac Malone]

@Henrik Böving It is worth noting that this will not accept a pointer type like char* for instance.

[Henrik Böving]

I hope that I won't want to box pointers for now :D

[Mac Malone]

@Henrik Böving Well, with that done, I will myself be heading to sleep myself (that is time zone differences for you).

[Mac Malone]

Happy I was able to help you have some fun with C!

[Mac Malone]

@Henrik Böving One final note: For lean_register_external_class, I was under the impression you had to provide handler for both (i.e., NULL was not a valid option). If you want it to be a no-op, you needed to define a no-op handler.

[Henrik Böving]

I might have found a bug in your grammar now^^

def IPv4Addr := UInt32
def IPv4Addr.mk (first second third fourth : UInt8) : IPv4Addr :=
  first.toUInt32 <<< 24 ||| second.toUInt32 <<< 16 ||| third.toUInt32 <<< 8 ||| fourth.toUInt32

alloy c extern "lean_mk_sockaddr_in"
def SockAddr4.mk (ip : IPv4Addr) (port : UInt16) : Unit := {
  struct sockaddr_in* sa = malloc(sizeof(struct sockaddr_in));
   .......
}

This fails to parse but if I turn the malloc into: malloc(sizeof(sockaddr_in)) it parses although now the c compiler is of course very unhappy. I'll work around it with a typedef for now.

[Henrik Böving]

image.png
:sparkles:

[Sebastian Ullrich]

This is a nice thread, it's great to see what is already possible. We should also document what is missing in the FFI to make this feasible purely in Lean.

[Henrik Böving]

To make what exactly feasible purely in Lean? @Sebastian Ullrich Do you want to get to the point where we don't have to write C at all?

[Sebastian Ullrich]

Yes, that's what I would expect from a complete FFI, no?

[Henrik Böving]

Hm, not really no. For example in OCaml it is very common to write C code still. They also have absolutely awesome docs on their FFI: https://v2.ocaml.org/manual/intfc.html I think if we can get to the level of this document we should be fine for a while^^

[Sebastian Ullrich]

So OCaml supports only homogeneous value FFI signatures? We are already beyond that, and I see no reason not to move even further.

[Henrik Böving]

No, they do also have unboxed values (namely everything <= 63 bit can be unboxed, 63 because the 64th bit is used for the box/unbox tag) and external allocations just like we do. They also have a bunch of special stuff like float arrays without indirection just like we do. In general I feel like modulo the garbage collector vs RC stuff our FFI is actually not that different from OCaml.

And on top of that they have Eisenberg (the GHC Eisenberg) working on more unboxed stuff at JaneStreet so I would expect something to come out of that in the not too distant future as well.

[Sebastian Ullrich]

User primitives with arity n ≤ 5 are implemented by C functions that take n arguments of type value, and return a result of type value

This seems quite clear to me. In any case, OCaml appears to be a relative outlier here, I can't think of any other compiled language that wants you to write C code for interfacing (of course, OCaml is not exclusively compiled, which might be one reason for this design).

[MangoIV]

You will find many libraries in the Haskell ecosystem that uses generated c compatibility shims e g https://github.com/haskell/hsc2hs generates c code, too

[Henrik Böving]

Which languages are you thinking about here? The ones that come to mind for me instantly would be C, C++, Rust, Golang and Haskell.
C/C++ are obviously not relevant here.

With Rust you can do everything in Rust indeed but they also have support for C constructs that we don't afaik?:

• directly integrated pointers
• unions
• the #[repr(C)]
• on top of that you usually use an FFI generator but that's more of a bonus.

Golang has cgo which is effectively an FFI generator that spits out both golang and C files as well.

For haskell I don't quite know what they do

[Mac Malone]

Sebastian Ullrich said:

Yes, that's what I would expect from a complete FFI, no?

While a great feature, having it would be surprising. Rust is the only language I know of that has something close to this and that is because it supports exact C calling conventions and data representations (so you do essentially write C in Rust). Every other major language language I know of, both compiled and interpreted, use C shims to fill in gaps in the FFI: Haskell, Java, PHP, Python, Ruby, JavaScript, , etc.

[Mac Malone]

Henrik Böving said:

I might have found a bug in your grammar now^^

Fixed. This grammar mistake was a result of me misreading a formatting error in Microsoft's C Language Syntax Summary. Its grammar for the type-based sizeof is written as follows:

unary-expression:
 postfix-expression
 ++ unary-expression
 -- unary-expression
 unary-operator cast-expression
 sizeof unary-expression
 sizeof ( type-name )  _Alignof ( type-name )

Where the final sizeof and _Alignof should be on separate lines.

[Henrik Böving]

I have new cursed stuff for you! @Mac Malone The manpages for unix domain sockets demonstrate this syntax:

  strncpy(sa->sun_path, lean_string_cstr(path), sizeof(sa->sun_path) - 1);

like so for example:

alloy c extern "lean_mk_sockaddr_un"
def SockAddrUnix.unix (path : @& System.FilePath) : SockAddrUnix := {
  struct sockaddr_un* sa = malloc(sizeof(struct sockaddr_un));
  sa->sun_family = AF_UNIX;
  strncpy(sa->sun_path, lean_string_cstr(path), sizeof(sa->sun_path) - 1);
  return sockaddr_un_to_lean(sa);
}

your sizeof grammar does not approve

[Richard Copley]

What goes wrong? (sa->sun_path) is a fine unary-expression, and (sa->sun_path) - 1 is not; and sa->sun_path isn't a type-name. (However, strncpy is cursed.)

[Henrik Böving]

It complains at the - of the ->sun_path that it expects a )

[Henrik Böving]

It being alloy, so the grammar implemented in alloy still seems to be flawed

[Mac Malone]

@Henrik Böving Fixed. My implementation was missing an atomic.

[Henrik Böving]

Yay that works

[Henrik Böving]

Okay I think I got a basic socket API for UNIX based systems working and documented now. Next thing would of course be :window: @Mac Malone do you have a particular story for cross platform in mind with alloy? Or is it also intended as an ifdef macro massacre?

[Mac Malone]

@Henrik Böving ifdef is how it is done in core, so at least for now, that is how I would assume FFIs would do it.

[Henrik Böving]

Okay. But #ifdef doesn't seem to work with alloy code blocks (probably given that it is not valid C but preprocessor C?) so what is the intended integration way here?

[Henrik Böving]

In particular also with #include's given that I need to work with the win32 header files to get sockets going properly.

[Mario Carneiro]

the lean 4 equivalent of #ifdef is meta if, not sure if it is applicable here

[Mac Malone]

Henrik Böving said:

Okay. But #ifdef doesn't seem to work with alloy code blocks (probably given that it is not valid C but preprocessor C?) so what is the intended integration way here?

It should work. #ifdef is part of the Alloy's C grammar. Do you have an example breakage?

[Henrik Böving]

Mac Malone said:

Henrik Böving said:

Okay. But #ifdef doesn't seem to work with alloy code blocks (probably given that it is not valid C but preprocessor C?) so what is the intended integration way here?

It should work. #ifdef is part of the Alloy's C grammar. Do you have an example breakage?

alloy c extern "lean_mk_socket"
def mk (family : @& AddressFamily) (type : @& Typ) : IO Socket := {
  int af = lean_to_socket_af(family);
  int typ = lean_to_socket_type(type);
  #ifdef FOO
    int* fd = malloc(sizeof(int));
  #endif
  *fd = socket(af, typ, 0);
  if (*fd < 0) {
    free(fd);
    return lean_io_result_mk_error(lean_decode_io_error(errno, NULL));
  } else {
    return lean_io_result_mk_ok(socket_to_lean(fd));
  }
}

[Mac Malone]

Oh, yeah, I made pp directives just commands, not statements. Need to fix that.

[Mac Malone]

@Henrik Böving Examples like yours should now work.

[Henrik Böving]

Nice. What about the include lines? Do I meta if those?

[Mac Malone]

@Henrik Böving No, this should work:

alloy c section
#ifdef WIN32
#include <windows/windows.h>
#else
#include <unistd.h>
#endif
end

[Henrik Böving]

Ah of course^^

[Henrik Böving]

@Mac Malone do we have a story for injecting linker arguments to leanc based on platform or is this a meta if job? It's because I gotta -lws2_32 but of course only on windows

[Mac Malone]

@Henrik Böving You can just us normal Lean syntax for that (i.e., if Platform.isWindows then ... else ...)

[Henrik Böving]

Mac Malone said:

Henrik Böving You can just us normal Lean syntax for that (i.e., if Platform.isWindows then ... else ...)

I got this now: https://github.com/hargoniX/socket.lean/blob/main/lakefile.lean#L14 but the flag is not properly injected into the leanc call that is used to build the alloy shim:

[89/95] Compiling Socket
[89/95] Generating Socket alloy
[90/95] Compiling Socket alloy
error: > c:\Users\runneradmin\.elan\toolchains\leanprover--lean4---nightly-2023-08-19\bin\leanc.exe -shared -o .\build\lib\Socket-1.dll .\build\ir\Socket.o .\build\ir\Socket.alloy.c.o -L.\lake-packages\alloy\build\lib -L.\lake-packages\std\build\lib -L.\build\lib -lAlloy-Util-Parser-1 -lAlloy-C-Grammar-1 -lAlloy-C-Syntax-1 -lAlloy-C-IR-1 -lAlloy-C-Shim-1 -lAlloy-Util-Extension-1 -lAlloy-C-Extension-1 -lAlloy-Util-Syntax-1 -lAlloy-Util-Binder-1 -lAlloy-C-Command-1 -lAlloy-Util-Server-Capabilities-1 -lAlloy-Util-Server-Initialize-1 -lAlloy-Util-Server-Methods-1 -lAlloy-C-Server-Clangd-1 -lAlloy-Util-Server-Worker-1 -lAlloy-C-Server-Worker-1 -lAlloy-C-Server-Utils-1 -lAlloy-Util-Server-1 -lAlloy-C-Server-Hover-1 -lAlloy-C-Server-SemanticTokens-1 -lAlloy-C-Server-1 -lAlloy-C-1 -lStd-Tactic-OpenPrivate-1 -lStd-Tactic-NoMatch-1 -lStd-Data-List-Init-Lemmas-1 -lStd-Data-Array-Init-Basic-1 -lStd-Data-Ord-1 -lStd-Data-Array-Basic-1
error: stderr:

I'm assuming I have to do something additional?

[Mac Malone]

@Henrik Böving Actually that is a bug in Lake with precompiled modules. I did not include the module's moreLinkArgs. Oops!

[Henrik Böving]

I shall await the next nightly then^^

[Siddharth Bhat]

@Tomas Skrivan I suspect this will fix our eigen bindings also!

[Mac Malone]

@Henrik Böving However, you should still be able to build the executable.

[Henrik Böving]

if I add the linker flags there?

[Henrik Böving]

let's see

[Henrik Böving]

No it does seem to forcibly want to link Socket before but that's fine I have time^^

[Mac Malone]

@Henrik Böving Could you try turning off precompileModules? I want to verify my suspicion that that is the problem.

[Henrik Böving]

sure

[Henrik Böving]

Mac Malone said:

Henrik Böving Could you try turning off precompileModules? I want to verify my suspicion that that is the problem.

yes

[Mac Malone]

@Henrik Böving Yes, it worked without precompileModules?

[Henrik Böving]

Yes

[Mac Malone]

@Henrik Böving Thanks! :thumbs_up:

[Henrik Böving]

(note that work means: it manages to pass the linker argument through, windows is of course ridiculing me and telling me that it cannot find that library)

Which is why i checked the docs and for some god-forsaken reason they (https://learn.microsoft.com/en-us/windows/win32/winsock/creating-a-basic-winsock-application) want you to do it like this:

#ifndef WIN32_LEAN_AND_MEAN
#define WIN32_LEAN_AND_MEAN
#endif

#include <windows.h>
#include <winsock2.h>
#include <ws2tcpip.h>
#include <iphlpapi.h>
#include <stdio.h>

#pragma comment(lib, "Ws2_32.lib")

int main() {
  return 0;
}

and i tried that:

#ifndef WIN32_LEAN_AND_MEAN
#define WIN32_LEAN_AND_MEAN
#endif

#include <windows.h>
#include <winsock2.h>
#include <ws2tcpip.h>
#include <iphlpapi.h>
#include <stdio.h>

#pragma comment(lib, "Ws2_32.lib")

int main() {
  return 0;
}

but alloy does not like the pragma syntax as it aborts at the " of "ws2..." so that's another grammar issue for your^^ @Mac Malone

:fast_forward:

[Mac Malone]

@Henrik Böving Fixed.

[Mac Malone]

Also, lean4#2447

[Siddharth Bhat]

@Mac Malone does it suffice to checkout the latest lean, build it, and /path/to/checkout/bin/lake build to test this?

[Mac Malone]

@Siddharth Bhat Sure, you shouldn't even need to build Lean itself, just building lake with a recent Lean toolchain should work.

[James Gallicchio]

So... suppose I wanted to be able to handle https traffic........ I assume there's a lot of work before socket.lean could support https? :stuck_out_tongue:

[Henrik Böving]

There are basically two requirements for this.

1. Someone needs to write an HTTP parser. Parsing HTTP 1.1 is actually completely trivial and I claim most FP interested people on this server could get it done with parser combinators in a few days based on the RFC: https://www.rfc-editor.org/rfc/rfc2616 Implementing everything the standard tells you is another thing but many things in the HTTP 1.1 standard are very simple (deliberately). If we want a modern HTTP library we'll at least have to parse HTTP 2...if we want to do that you can throw the idea of "deliberate simplicity" completely out of the window since they employ lots funky mechanisms such as: Multiplexing multiple connections through the same socket as "streams, Compressing headers in such a way that you basically only get differential update on what headers changed and many more fun things. So getting a compliant HTTP 2 implementation is actually something where you kind of need to know what you are doing
2. the TLS/SSL part, this is in theory easy as we "just need to bind OpenSSL" since it provides the necessary API for wrapping a regular socket with a TLS/SSL context such that the encryption/decryption just works :tm:. Then again binding OpenSSL especially in such a way that it is secure and safe is also not very trivial. However this second half can be ignored for a long while as it is rather common to have a reverse proxy like nginx today that receives the TLS connection which can then forward it to us in clear text.

@James Gallicchio

[Sebastian Ullrich]

Note that this topic originally was about making HTTP requests, not accepting them :) . For which, as pointed out, binding to libcurl should indeed be vastly easier.

[Mac Malone]

Joachim Breitner said:

After seeing your message I tried it in loogle (by changing the nix shell to use the clang-stdenv, so any problems may be nix-related), but I get

I just realized I somehow overlooked this message. Sorry! That error is unfortunately an expected one but fortunately should not actually cause any problems.

[James Gallicchio]

@Arthur Paulino I see Http.lean has an http parser and the relevant types -- do you think we could separate those into a package independent of Socket? (is the package worth reviving?)

[Arthur Paulino]

We're not maintaining the repo right now, but feel free to open PRs to organize it in a way that you see fit and I can review

[Arthur Paulino]

It's also, obviously, fine to maintain a fork of your own for the sake of agility on your side

[James Gallicchio]

(frankly, I don't really want to maintain an http library, so if lurk could maintain it longterm I'd prefer that, but I suspect you're not using it right now? :joy:)

[James Gallicchio]

I'll fork it for now, and we can figure out long term maintenance later

[Sebastian Ullrich]

Interesting JEP in the context of this thread: https://openjdk.org/jeps/454

Replace the brittle machinery of native methods and the Java Native Interface (JNI) with a concise, readable, and pure-Java API.

JNI involves several tedious artifacts: a Java API (native methods), a C header file derived from the Java API, and a C implementation that calls the native library of interest. Java developers must work across multiple toolchains to keep platform-dependent artifacts in sync, which is especially burdensome when the native library evolves rapidly.

[James Gallicchio]

Ok, I have updated and pretty much rewritten/overhauled the http library here: https://github.com/JamesGallicchio/http

[Scott Morrison]

Looks like you can remove the "When running lake update ..." note in the README!

[James Gallicchio]

wha-- I just put that there! :racecar:

[James Gallicchio]

wait, https://github.com/fgdorais/lean4-unicode-basic/blob/main/lake-manifest.json is still out of date

[Scott Morrison]

Sorry, my mistake!

[Scott Morrison]

Great example of the automatic version bumping / notification we need all across the ecosystem. :-)

[James Gallicchio]

if i make enough libraries on my way to the github bot, i'll have no path forward except through!

[James Gallicchio]

<---- I am a clown

[Siddhartha Gadgil]

@James Gallicchio
Is this ready to replace curl calls? If so is there an example?

[James Gallicchio]

No -- part of the rewrite's purpose was to get rid of dependence on Socket.lean. It only defines types for representing HTTP, not how to send them over the wire. The second half is honestly pretty straightforward to do from scratch, and is somewhat opinionated on what's the best API, so it makes sense to stay separate.

[James Gallicchio]

I can add some examples to the README. The types are fairly straightforward, but the documentation is definitely lacking...

[Henrik Böving]

James Gallicchio said:

No -- part of the rewrite's purpose was to get rid of dependence on Socket.lean. It only defines types for representing HTTP, not how to send them over the wire. The second half is honestly pretty straightforward to do from scratch, and is somewhat opinionated on what's the best API, so it makes sense to stay separate.

But you don't really want to have this separation with HTTP right? Like even very basic HTTP already has a concept of keeping connections alive and things like that.

[Schrodinger ZHU Yifan]

Henrik Böving said:

James Gallicchio said:

No -- part of the rewrite's purpose was to get rid of dependence on Socket.lean. It only defines types for representing HTTP, not how to send them over the wire. The second half is honestly pretty straightforward to do from scratch, and is somewhat opinionated on what's the best API, so it makes sense to stay separate.

But you don't really want to have this separation with HTTP right? Like even very basic HTTP already has a concept of keeping connections alive and things like that.

I think separate abstraction is actually common?
https://crates.io/crates/http/0.2.9

[Henrik Böving]

Interesting I see

[James Gallicchio]

yeah an HTTP server is super complicated compared to anything in this package