Initial commit

Changes

5 changed files (+40/-0)

• .gitignore (new)
  • @@ -0,0 +1,1 @@
    + /.lake
• Main.lean (new)
  • @@ -0,0 +1,26 @@
    + import Std + open Std.Internal.IO.Async.TCP.Socket + + instance : ToString Std.Net.SocketAddress where + toString a := s!"{a.ipAddr}:{a.port}" + + def handler (conn : Client) := do + IO.println s!"Connection from {← conn.getPeerName}" + match ← (← conn.recv? 65536).block with + | some data => + match String.fromUTF8? data with + | some dataStr => + let filename := (← IO.rand 0 <| 2 ^ 32 - 1).toInt32.toBitVec.toHex + IO.println s!"Writing to {filename}" + IO.FS.writeFile filename dataStr + | none => return + | none => return + + def main := do + let server ← Server.mk + server.bind <| .v4 ⟨⟨Vector.replicate 4 0⟩, 1349⟩ + server.listen 32 + IO.println s!"Listening on {← server.getSockName}" + while true do + let conn ← (← server.accept).block + _ ← IO.asTask <| handler conn
• lake-manifest.json (new)
  • @@ -0,0 +1,5 @@
    + {"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "leanet", + "lakeDir": ".lake"}
• lakefile.toml (new)
  • @@ -0,0 +1,7 @@
    + name = "leanet" + version = "0.1.0" + defaultTargets = ["leanet"] + + [[lean_exe]] + name = "leanet" + root = "Main"
• lean-toolchain (new)
  • @@ -0,0 +1,1 @@
    + leanprover/lean4:v4.22.0-rc3