Upload the first half of the boolin draft

1 files changed, 231 insertions, 0 deletions

diff --git a/blog/boolin.md b/blog/boolin.md
new file mode 100644
index 0000000..6acae55
--- /dev/null
+++ b/blog/boolin.md
@@ -0,0 +1,231 @@
+<!--
+  -- title = "Inclusion in Python Environment Algebra"
+  -- rss = "Specifying a subset of environment constraints for Python packages"
+  -- date = Date(2021, 11, 26)
+  -- tags = ["fun", "math", "packaging", "python"]
+  -->
+# Inclusion in Python Environment Algebra
+
+!!! note "Note"
+
+    If you do not want to hear me rambling about the shortcomings
+    of Python packaging metadata standards, feel free to skip
+    to section [1.c](#objective).
+
+\toc
+
+## Background
+
+### Motivation
+
+I sometimes [praise] Python wheels as the best binary packaging format
+for cross-platform delivery.  It truly is, at least to my limited knowledge.
+Via compatibility tags, the constraints for the target environment
+can be exclusively specified.  Even though {{pep 425 compressed-tag-sets}}
+was introduced
+
+> to allow for compact filenames of bdists[^bdists]
+> that work with more than one compatibility tag triple,
+
+the filenames are not always *compact* and it is not always possible
+to specify all environments a module can work on either.  For instance,
+there's no direct answer for one of the FAQ:
+
+> **What tag do I use if my distribution uses
+> a feature exclusive to the newest version of Python?**
+
+I have seen workarounds like `cp35.cp36.cp37.cp38.cp39`, which accept
+CPython from version 3.5, but not 3.10, which is the topic of the next Q&A:
+
+> **Why isn't there a `.` in the Python version number?**
+>
+> CPython has lasted 20+ years without a 3-digit major release.
+> This should continue for some time.  Other implementations may use `_`
+> as a delimiter, since both `-` and `.` delimit the surrounding filename.
+
+The platform tag was not carefully standardized either,
+which gives us inconsistent cyphers such as `win32`, `win_amd64`
+and `manylinux2010_x86_64`.[^glibc]
+
+### Inspiration
+
+A few years later, {{pep 508 environment-markers}} came along after multiple
+iterations ({{pep 345}}, {{pep 426}}) with a much more human-readable format,
+which is essentially a Boolean algebra of comparisons.  With this,
+the aforementioned CPython constraint can be correctly expressed as
+
+```python
+platform_python_implementation == 'CPython'
+and python_version >= '3.5'
+```
+
+Unfortunately, they are only standardized for marking dependencies,
+usually to watch out for environments where a library is either unnecessary
+or unusable.  But *who watches the watchers*?  While it is possible
+to [specify Python and platform tags when building wheels][params], the feature
+is undocumented and almost unknown.  Therefore, many, if not most,
+platform-specific pure-Python wheels are tagged as `none` platform and all
+their dependents needs to have the same redundant markers.  Furthermore,
+due to the exclusive nature of compatibility tags, a GNU/Linux-only
+purelib wheel should be tagged with something like the following abomination:
+
+```
+manylinux_2_17_x86_64.manylinux_2_17_i686.manylinux_2_17_aarch64.manylinux_2_17_armv7l.manylinux_2_17_ppc64.manylinux_2_17_ppc64le.manylinux_2_17_s390x
+```
+
+Now imagine the filename of a wheel that only works on Unix-like systems.
+`uvloop` is one and it is among the 500 [most-downloaded on PyPI][3719394]
+at the time of writing.
+
+### Objective
+
+This article is, though, not going to sell you the idea of porting
+environment markers to top-level `WHEEL` metadata.  I should sit down
+with the [PyPA] people and [discuss] it one day, but the currently defined
+markers are lacking CPU and ABI information.  The reason for this is that
+Python's standard library does not implement a way to retrieve such information,
+and for completeness, the operating system's version is not meaningfully
+available either.  If we want to redo this right, I highly recommend
+looking into [Zig]'s [std.Target], which was designed from the start
+for cross-compilation.  Whatever we will come up with, it shall not be
+done overnight.
+
+Instead, right now I need to solve a more immediate problem.  For the last
+few months, I have been working on [IPWHL][ipwhl], a downstream repository for
+Python distributions.  Since we enforce that all dependencies to be satisfied,
+packages with too strict or too lax environment declaration will break
+the automated tests, even though effectively the declared packages integrate
+well with each other.  We came to a conclusion that adding information would
+improve the checks' accuracy and decided to use the [floating cheeses][ipwhl]
+as a testbed for [top-level environment specifiers][proposal].
+
+In short, we are going to merge the `METADATA` field `Requires-Python`
+with other environmental information to a single field `environment`.
+Since other information may or may not be present in the filename,
+during metadata integrity check we can only check if what declared
+is [included][inclusion] by what found from the original wheel.
+
+### Theory
+
+Ignoring `extra`, a Python environment can be represented as a 11-tuple of
+
+```python
+(python_version, python_full_version, os_name, sys_platform,
+ platform_release, platform_system, platform_version,
+ platform_machine, platform_python_implementation,
+ implementation_name, implementation_version)
+```
+
+Denote $S$ as the set of all strings, then the set of all environments
+$E \subset S^{11}$.  Let
+\[O = \{\le, <, \ne, =, \ge, >, \cong, \equiv, \in, \notin, \ni, \notni\}\]
+the set of all marker expressions[^var] can be defined as
+\[X = \{e \mapsto e \bigcirc s \mid \bigcirc \in O \land s \in S\}\]
+and the set of all environment markers[^markers] can be recursively defined as
+\[\begin{aligned}
+  M = \{c_\top\} &\cup \{(e_1, \ldots, e_{11})
+                         \mapsto m(e_1, \ldots, e_{11}) \land x(e_{\imath})
+                         \mid m \in M \land x \in X \land \imath \in I\}\\
+                 &\cup \{(e_1, \ldots, e_{11})
+                         \mapsto m(e_1, \ldots, e_{11}) \lor x(e_{\imath})
+                         \mid m \in M \land x \in X \land \imath \in I\}
+\end{aligned}\]
+where $\top$ is the *top* element in Boolean algebra, $c_\top: E \to \{\top\}$
+is a constant function and $I = [1, 11]$.  With all Boolean expressions
+converted into one of their standard forms, we have the following alternative
+definitions of an environment marker
+\[\begin{aligned}
+  (e_1, \ldots, e_{11})
+  &\mapsto \bigvee_{\imath = 1}^n\bigwedge_{\jmath = 1}^{f(\imath)}
+  x(\jmath)\left(e_{k(\jmath)}\right)\\
+  (e_1, \ldots, e_{11})
+  &\mapsto \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
+  x(\jmath)\left(e_{k(\jmath)}\right)
+\end{aligned}\]
+where $n \in \N$, $f: \N^* \to \N^*$, $x: \N^* \to X$, $k: \N^* \to I$
+and an empty Boolean expression is implicitly $c_\top$.
+
+Now it is possible to formalize inclusion for markers as
+\[\forall\,\{m, n\} \subset M: (m \le n) = (\forall\,e \in E: m(e) \le n(e))\]
+
+Thus, checking if a marker includes another is equivalent to evaluating
+the following expression, for all $(e_1, \ldots, e_{11}) \in E$
+\[\begin{aligned}
+  r &= \bigvee_{\imath' = 1}^{n'}\bigwedge_{\jmath' = 1}^{f'(\imath')}
+       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
+       x(\jmath)\left(e_{k(\jmath)}\right)\\
+    &= \bigwedge_{\imath' = 1}^{n'}\left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
+       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
+       x(\jmath)\left(e_{k(\jmath)}\right)\right)\\
+    &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n
+       \left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
+       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       \le \bigvee_{\jmath = 1}^{f(\imath)}
+       x(\jmath)\left(e_{k(\jmath)}\right)\right)
+\end{aligned}\]
+where $r$ is whether the original marker (defined by $n$, $f$, $x$ and $k$)
+includes the declared one (defined by $n'$, $f'$, $x'$ and $k'$). Let
+\[\begin{aligned}
+  g(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f(\imath)]
+                              \land k(\jmath) = \ell\}\\
+  g'(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f'(\imath)]
+                               \land k'(\jmath) = \ell\}
+\end{aligned}\]
+and assume $e_1, \ldots, e_{11}$ are orthogonal, we have
+\[\begin{aligned}
+  r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
+       \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
+       x'(\jmath')\left(e_{\ell}\right)
+       \le \bigvee_{\jmath \in g(\imath, \ell)}
+       x(\jmath)\left(e_{\ell}\right)\right)\\
+    &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
+       \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
+       x'(\jmath')\left(e_{\ell}\right)
+       \land \lnot \bigvee_{\jmath \in g(\imath, \ell)}
+       x(\jmath)\left(e_{\ell}\right) = \bot\right)
+\end{aligned}\]
+where $\bot$ is the Boolean algebra bottom element.  By [De Morgan's laws],
+\[\begin{aligned}
+  r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
+       \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
+       x'(\jmath')\left(e_{\ell}\right)
+       \land \bigwedge_{\jmath \in g(\imath, \ell)}
+       \lnot x(\jmath)\left(e_{\ell}\right) = \bot\right)
+\end{aligned}\]
+
+Essentially, checking if
+\[\bigwedge_{\jmath' \in g'(\imath', \ell)} x'(\jmath')\left(e_{\ell}\right)
+  \land \bigwedge_{\jmath \in g(\imath, \ell)}
+  \lnot x(\jmath)\left(e_{\ell}\right)\]
+is unsatisfiable for all $e_{\ell}$ is a [SAT problem] which we can write
+a solver for.
+
+## Implementation
+
+### Generation
+
+### Conversion
+
+### Verification
+
+[^bdists]: [Built distributions][bdist], as opposed to [sdist]
+[^glibc]: Bonus: try to sort `manylinux1`, `manylinux_2_24` and `manylinux2014`
+[^var]: Ignoring relations between two variables or two strings
+[^markers]: Or *environment specifiers* when [not marking anything][proposal]
+
+[praise]: https://nixnet.social/notice/A9GyFTnNnQDVZrmtUm
+[bdist]: https://packaging.python.org/glossary/#term-Built-Distribution
+[sdist]: https://packaging.python.org/glossary/#term-Source-Distribution-or-sdist
+[params]: https://github.com/pypa/wheel/blob/0.37.0/src/wheel/bdist_wheel.py#L136-L164
+[3719394]: https://hugovk.github.io/top-pypi-packages
+[PyPA]: https://pypa.io
+[discuss]: https://discuss.python.org/t/7831
+[Zig]: https://ziglang.org
+[std.Target]: https://ziglang.org/documentation/master/std/#std;Target
+[ipwhl]: https://man.sr.ht/~cnx/ipwhl
+[proposal]: https://lists.sr.ht/~cnx/ipwhl-discuss/%3CCEP1VQH719Y4.1EX12MJII0WVE%40nix%3E
+[inclusion]: https://en.wikipedia.org/wiki/Inclusion_(Boolean_algebra)
+[De Morgan's laws]: https://en.wikipedia.org/wiki/De_Morgan%27s_laws
+[SAT problem]: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem