Documentation

Lake.Reservoir

Package Registries #

This module contains definitions for fetching Lake package information from a online registry (e.g., Reservoir).

Package source information from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

Instances For
    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For

                Package metadata from a Lake registry (e.g., Reservoir). Only contains the subset of fields useful to Lake.

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

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

                          Equations
                            Instances For
                              @[specialize #[]]
                              def Lake.foldlUtf8M {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] (c : Char) (f : σUInt8m σ) (init : σ) :
                              m σ

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

                              Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev Lake.foldlUtf8 {σ : Type u_1} (c : Char) (f : σUInt8σ) (init : σ) :
                                  σ
                                  Equations
                                    Instances For
                                      def Lake.uriEscapeChar (c : Char) (s : String := "") :

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

                                      Equations
                                        Instances For

                                          A URI unreserved mark as specified in RFC2396.

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

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

                                              Equations
                                                Instances For

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

                                                  Equations
                                                    Instances For
                                                      def Lake.getUrl (url : String) (headers : Array String := #[]) :

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

                                                      Equations
                                                        Instances For
                                                          inductive Lake.ReservoirResp (α : Type u) :

                                                          A Reservoir API response object.

                                                          Instances For
                                                            Equations
                                                              Instances For
                                                                def Lake.Reservoir.pkgApiUrl (lakeEnv : Env) (owner pkg : String) :
                                                                Equations
                                                                  Instances For
                                                                    Equations
                                                                      Instances For
                                                                        def Lake.Reservoir.fetchPkg? (lakeEnv : Env) (owner pkg : String) :
                                                                        Equations
                                                                          Instances For