def Lake.hexEncodeByte (b : UInt8) : Char

def Lake.uriEscapeByte (b : UInt8) (s : String := "") : String

Encode a byte as a URI escape code (e.g., %20).

@[specialize #[]]

def Lake.foldlUtf8M {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ

Folds a monadic function over the UTF-8 bytes of Char from most significant to least significant.

@[reducible, inline]

abbrev Lake.foldlUtf8 {σ : Type u_1} (c : Char) (f : σ → UInt8 → σ) (init : σ) : σ

def Lake.uriEscapeChar (c : Char) (s : String := "") : String

Encode a character as a sequence of URI escape codes representing its UTF8 encoding.

def Lake.isUriUnreservedMark (c : Char) : Bool

A URI unreserved mark as specified in RFC3986. Unlike the older RFC2396, RFC2396 also reserves !, *, ', (, and ).

Lake uses RFC3986 here because the curl implementation of AWS Sigv4 that Lake uses to upload artifacts requires these additional characters to be escaped.

def Lake.uriEncodeChar (c : Char) (s : String := "") : String

Encodes anything but a URI unreserved character as a URI escape sequences.

def Lake.uriEncode (s : String) (init : String := "") : String

Encodes a string as an ASCII URI component, escaping special characters (and unicode).

def Lake.getUrl? (url : String) (headers : Array String := #[]) : LogIO (Option String)

Performs a HTTP GET request of a URL (using curl with JSON output) and, if successful, return the body. Otherwise, returns none on a 404 and errors on anything else.

def Lake.getUrl (url : String) (headers : Array String := #[]) : LogIO String

Perform a HTTP GET request of a URL (using curl) and return the body.