Adjust docs for proxying (#523)

Update/polish up the documentation around http proxying

docs/modules/pkl-cli/pages/index.adoc

@@ -831,16 +831,46 @@ The CLI option takes precedence over the certificates in `~/.pkl/cacerts/`. +
 Certificates need to be X.509 certificates in PEM format.
 
 [[http-proxy]]
-== HTTP Proxy
+== HTTP Proxying
 
-When making HTTP(S) requests, Pkl can use a proxy.
-By default, no proxy is configured.
-A proxy can be configured as follows:
+When making HTTP(s) requests, Pkl can possibly make use of an HTTP proxy.
 
-- Using `--proxy <uri>`.
-  The URI must (currently) have scheme `http`, and may not contain anything other than a host and port.
-- Using `--no-proxy <hosts>`.
-  The given (comma separated list of) hosts bypass the proxy.
-  Hosts can be specified by domain name (in which case all subdomains also bypass the proxy), IP addresses, or IP ranges (using link:https://en.wikipedia.org/wiki/Classless_Inter-Domain_Routing#CIDR_notation[CIDR notation]).
-  For individual hosts (not CIDRs), ports can be specified.
-  When no port is specified for a given host, connections to all ports bypass the proxy.
+There are two values that determine proxy settings; the proxy address and list of noproxy rules.
+When determining proxy settings, Pkl will look at the following locations, in order of precedence (lowest to highest):
+
+1. OS settings (on macOS, Windows, and GNOME environments)
+2. <<settings-file,Settings file>>
+3. xref:language-reference:index.adoc#projects[PklProject file]
+4. `--proxy` and `--no-proxy` CLI flags
+
+[NOTE]
+====
+The proxy and noproxy values are individually set.
+For example, using the `--no-proxy` flag but not the `--proxy` flag will cause Pkl to look at the PklProject file, then the settings file, then system settings for the proxy address.
+
+One exception to this rule is that setting a proxy address will cause Pkl to ignore any noproxy values set at the OS level.
+====
+
+Pkl only supports HTTP proxies, so neither HTTPS nor SOCKS proxies are supported.
+Pkl does not support authentication with a proxy.
+
+When specifying a proxy address, it must have scheme `http`, and may not contain anything other than a host and port.
+
+=== Proxy exclusions
+
+Pkl can be configured to bypass the proxy for specific requests via a proxy exclusion rule (i.e. the `--no-proxy` flag).
+It may be provided either as a hostname, an IP address, or an IP range via https://en.wikipedia.org/wiki/Classless_Inter-Domain_Routing#CIDR_notation[CIDR notation].
+When determining whether a proxy should be excluded, hostnames do not get resolved to their IP address.
+For example, a request to `localhost` will not match `--no-proxy=127.0.0.1`.
+
+For individual hosts (not CIDRs), ports can be specified.
+When no port is specified for a given host, connections to all ports bypass the proxy.
+
+A hostname will match all of its subdomains.
+For example, `example.com` will match `foo.example.com`, and `bar.foo.example.com`, but not `fooexample.com`.
+
+The value `*` is a special wildcard that matches all hosts.
+
+A port can optionally be specified. If omitted, it matches all ports.
+
+NOTE: Pkl follows the rules described in https://about.gitlab.com/blog/2021/01/27/we-need-to-talk-no-proxy/#standardizing-no_proxy[Standardizing `no_proxy`], except it does not look at environment variables.

docs/modules/pkl-cli/partials/cli-common-options.adoc

@@ -127,7 +127,7 @@ For other methods of configuring certificates, see xref:pkl-cli:index.adoc#ca-ce
 [%collapsible]
 ====
 Default: (none) +
-Example: `http://proxy.example.com:1234` +
+Example: `\http://proxy.example.com:1234` +
 Configures HTTP connections to connect to the provided proxy address.
 The URI must have scheme `http`, and may not contain anything other than a host and port.
 ====

docs/modules/pkl-gradle/partials/gradle-common-properties.adoc

@@ -88,7 +88,7 @@ Relative paths are resolved against the project directory.
 [%collapsible]
 ====
 Default: `null` +
-Example: `http://proxy.example.com:1234` +
+Example: `proxy = uri("http://proxy.example.com:1234")` +
 Configures HTTP connections to connect to the provided proxy address.
 The URI must have scheme `http`, and may not contain anything other than a host and port.
 ====
@@ -97,7 +97,7 @@ The URI must have scheme `http`, and may not contain anything other than a host
 [%collapsible]
 ====
 Default: `null` +
-Example: `example.com,169.254.0.0/16` +
+Example: `noProxy = ["example.com", "169.254.0.0/16"]` +
 Hosts to which all connections should bypass the proxy.
 Hosts can be specified by name, IP address, or IP range using https://en.wikipedia.org/wiki/Classless_Inter-Domain_Routing#CIDR_notation[CIDR notation].
 ====

stdlib/EvaluatorSettings.pkl

@@ -94,8 +94,6 @@ http: Http?
 /// Settings that control how Pkl talks to HTTP(S) servers.
 class Http {
   /// Configuration of the HTTP proxy to use.
-  ///
-  /// If [null], uses the operating system's proxy configuration.
   proxy: Proxy?
 }
 
@@ -103,7 +101,11 @@ class Http {
 class Proxy {
   /// The proxy to use for HTTP(S) connections.
   ///
-  /// At the moment, only HTTP proxies are supported.
+  /// Only HTTP proxies are supported.
+  /// The proxy address must start with `http://`, and can only contain a host and a port.
+  /// If a port is omitted, it defaults to port `80`.
+  ///
+  /// Proxy authentication is not supported.
   ///
   /// Example:
   /// ```
@@ -114,15 +116,19 @@ class Proxy {
   /// Hosts to which all connections should bypass a proxy.
   ///
   /// Values can be either hostnames, or IP addresses.
-  /// IP addresses can optionally be provided using [CIDR notation](https://en.wikipedia.org/wiki/Classless_Inter-Domain_Routing#CIDR_notation).
+  /// IP addresses can optionally be provided using
+  /// [CIDR notation](https://en.wikipedia.org/wiki/Classless_Inter-Domain_Routing#CIDR_notation).
   ///
-  /// The only wildcard is `"*"`, which disables all proxying.
+  /// The value `"*"` is a wildcard that disables proxying for all hosts.
   ///
   /// A hostname matches all subdomains.
   /// For example, `example.com` matches `foo.example.com`, but not `fooexample.com`.
   /// A hostname that is prefixed with a dot matches the hostname itself,
   /// so `.example.com` matches `example.com`.
   ///
+  /// Hostnames do not match their resolved IP addresses.
+  /// For example, the hostname `localhost` will not match `127.0.0.1`.
+  ///
   /// Optionally, a port can be specified.
   /// If a port is omitted, all ports are matched.
   ///