def Lake.hexEncodeByte (b : UInt8) : Char

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lake.uriEscapeByte b s = ((s.push '%').push (Lake.hexEncodeByte (b >>> 4))).push (Lake.hexEncodeByte (b &&& 15))

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• Lake.foldlUtf8 c f init = (Lake.foldlUtf8M c (fun (x1 : σ) (x2 : UInt8) => pure (f x1 x2)) init).run

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

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

Equations

• Lake.uriEscapeChar c s = Lake.foldlUtf8 c (fun (s : String) (b : UInt8) => Lake.uriEscapeByte b s) s

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.

Equations

• Lake.isUriUnreservedMark '-' = true
• Lake.isUriUnreservedMark '_' = true
• Lake.isUriUnreservedMark '.' = true
• Lake.isUriUnreservedMark '~' = true
• Lake.isUriUnreservedMark c = false

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

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

Equations

• Lake.uriEncodeChar c s = if (c.isAlphanum || Lake.isUriUnreservedMark c) = true then s.push c else Lake.uriEscapeChar c s

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

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

Equations

• Lake.uriEncode s init = String.foldl (fun (s : String) (c : Char) => Lake.uriEncodeChar c s) init s

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.