0.12.0 --- the working directory reaches the program, and a unit can … #165
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| # What this workflow asserts. | |
| # | |
| # The claim this package makes is that a C library ported once onto openkal runs | |
| # above every implementation of the specification, so the claim is tested by | |
| # running the same two programs on three systems and comparing what they produce | |
| # against what the system's own tools produce. | |
| # | |
| # posix a program that opens a file by an absolute name, reads a | |
| # variable, measures an interval, starts another program and waits | |
| # for it --- thirty-two observations, none of which the program | |
| # contains an implementation of | |
| # wordcount the same counts as the system's own `wc' | |
| # | |
| # Two compiler families, gcc and llvm. The third of the three mcpp offers is | |
| # absent from this package and the reason is recorded in the manifest: musl's | |
| # four remaining assembly definitions are in an object format that toolchain | |
| # does not assemble, so the question that toolchain would answer is not one this | |
| # package can ask. | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| inputs: | |
| mcpp_ref: | |
| description: "Branch of mcpp-community/mcpp to build and test against (empty = the released pin)" | |
| required: false | |
| default: "" | |
| env: | |
| MCPP_SOURCE_REF: ${{ github.event.inputs.mcpp_ref || vars.MCPP_SOURCE_REF }} | |
| MCPP_VERSION: 2026.8.27.1 | |
| XLINGS_VERSION: v2026.8.17.2 | |
| XLINGS_NON_INTERACTIVE: '1' | |
| jobs: | |
| programs: | |
| name: ${{ matrix.name }} | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 90 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| # ⭐ `net`, `fork` and `shell` STATE WHAT THE BACKEND BENEATH THIS ROW | |
| # PROVIDES, and they are part of the criterion rather than a | |
| # convenience. openkal permits an implementation to decline an | |
| # interface in whole (clause 3), so "the probe was not run" and "the | |
| # probe was run and the refusal was the expected answer" are | |
| # different outcomes, and only the second is evidence. | |
| # | |
| # ⭐⭐ `abort` NAMES WHAT EACH BACKEND'S `kal_abort` PRODUCES, AND IT IS | |
| # THREE DIFFERENT THINGS ON PURPOSE. | |
| # | |
| # Until 0.6.0 `abort` did not end the program at all: musl's `raise` is | |
| # `tkill`, this port had no case for it, and `abort` fell through to | |
| # musl's own `a_crash()` --- `hlt` on x86_64 --- so every uncaught | |
| # exception and every `assert` reported a segmentation fault. A row | |
| # asserting only "the end was not an ordinary one" would have passed | |
| # throughout that, because a fault is not an ordinary end either. So | |
| # each row asserts the PARTICULAR end its implementation produces: | |
| # | |
| # --abort-signal SIGABRT: openkal-linux raises it with tgkill | |
| # --abort-status exit 134: openkal-macos ends with a status no | |
| # program returns | |
| # --abort-terminated a termination rather than a return: Windows | |
| # fail-fasts, and the fault this replaces was | |
| # reported there as an exit | |
| - { name: 'linux, gcc', os: ubuntu-24.04, toolchain: 'gcc@16.1.0', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-signal', dirtime: '--dir-time' } | |
| - { name: 'linux, llvm', os: ubuntu-24.04, toolchain: 'llvm@22.1.8', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-signal', dirtime: '--dir-time' } | |
| - { name: 'macos, llvm', os: macos-14, toolchain: 'llvm@20.1.7', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-status', dirtime: '--dir-time' } | |
| # ⚠️ openkal-windows declines `openkal.space`: this system has no | |
| # primitive that copies an address space and starts a context in the | |
| # copy, and inventing one would be the simulation clause 3.1 | |
| # forbids. `--no-fork` asserts the refusal. | |
| - { name: 'windows, gcc', os: windows-2022, toolchain: 'gcc@16.1.0', target: 'x86_64-windows-gnu', net: 'yes', fork: '--no-fork', shell: '--no-shell', abort: '--abort-terminated', dirtime: '--dir-time' } | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # WHAT IS COMMITTED NAMES NO DIRECTORY OF ANYBODY'S MACHINE. | |
| # | |
| # tools/working-trees.sh rewrites this manifest to name working trees and | |
| # deliberately does not restore it: the rewrite must survive for the rest | |
| # of the job. A run by hand therefore leaves the manifest naming absolute | |
| # paths, and committing that publishes them --- a consumer resolving from | |
| # the index is handed a manifest pointing at a directory that exists | |
| # nowhere. | |
| # | |
| # ⚠️ THAT HAS HAPPENED. This step runs BEFORE the rewrite, so what it | |
| # examines is what the commit contains rather than what the job has done | |
| # to it. | |
| - name: The committed manifest names no local directory | |
| run: | | |
| set -euo pipefail | |
| bad=$(grep -nE '^[a-z-]+ = \{[^}]*path = "(/|[A-Za-z]:)' mcpp.toml || true) | |
| if [ -n "$bad" ]; then | |
| echo "::error::the committed manifest names an absolute path" | |
| printf '%s\n' "$bad" | sed 's/^/ /' | |
| echo " tools/working-trees.sh rewrites these and does not restore them;" | |
| echo " run 'git checkout -- mcpp.toml' after using it by hand." | |
| exit 1 | |
| fi | |
| echo " ok every dependency is named by version or by a relative path" | |
| - name: The specification and the implementation for this system | |
| run: | | |
| bash tools/working-trees.sh '${{ github.head_ref || github.ref_name }}' \ | |
| '${{ matrix.target }}' | |
| - name: Install xlings (Unix) | |
| if: runner.os != 'Windows' | |
| run: | | |
| # --retry-all-errors AND NOT --retry ALONE. `--retry` covers a | |
| # transient HTTP status and a timeout; it does not cover a failure of | |
| # the transport, which is what this step meets. Measured on this | |
| # branch, one row of the matrix, with nothing wrong in it: | |
| # | |
| # curl: (35) Recv failure: Connection reset by peer | |
| # ##[error]Process completed with exit code 35 | |
| # | |
| # A red row that names a defect nobody introduced costs a reader the | |
| # time it takes to establish that, every time. | |
| curl -fsSL --retry 3 --retry-all-errors --retry-delay 2 \ | |
| https://raw.githubusercontent.com/openxlings/xlings/main/tools/other/quick_install.sh \ | |
| | bash -s "$XLINGS_VERSION" | |
| echo "$HOME/.xlings/subos/current/bin" >> "$GITHUB_PATH" | |
| - name: Install xlings (Windows) | |
| if: runner.os == 'Windows' | |
| shell: pwsh | |
| run: | | |
| irm https://d2learn.org/xlings-install.ps1.txt | iex | |
| "$env:USERPROFILE\.xlings\subos\current\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append | |
| - name: Install mcpp | |
| run: | | |
| xlings update | |
| # ⚠️ THE PIN MAY NAME THE RELEASE THIS RUN IS VALIDATING, which does | |
| # not exist yet — that is the whole point of MCPP_SOURCE_REF. Bootstrap | |
| # from whatever the index has; the step below replaces it with the | |
| # build under review, and the pin is what an ordinary run tests. | |
| if [ -n "${MCPP_SOURCE_REF:-}" ]; then | |
| xlings install mcpp -y -g | |
| else | |
| xlings install "mcpp@$MCPP_VERSION" -y -g | |
| fi | |
| mcpp --version | |
| mcpp self config --mirror GLOBAL | |
| # ⭐⭐ CROSS-VALIDATION: BUILD THE mcpp UNDER REVIEW AND USE THAT ONE. | |
| # | |
| # Empty in the ordinary run, so this job keeps testing the RELEASED | |
| # mcpp the pin above names. Set it — `workflow_dispatch` input, or the | |
| # repository variable — and the same job runs against that source. | |
| # | |
| # ⚠️ THIS EXISTS BECAUSE THE ORDER USED TO BE WRONG. Several mcpp | |
| # releases went out green and only then turned this ecosystem red: the | |
| # engine's own CI cannot see a defect that appears only in a real | |
| # dependency graph, and this repository could not see the engine until | |
| # it had been published. Validating before the release closes that gap. | |
| # | |
| # The released mcpp installed just above is the bootstrap that compiles | |
| # it; mcpp builds itself and there is no other compiler for it here. | |
| if [ -n "${MCPP_SOURCE_REF:-}" ]; then | |
| src="$RUNNER_TEMP/mcpp-src" | |
| [ -d "$src" ] || git clone --quiet --depth 1 \ | |
| --branch "$MCPP_SOURCE_REF" \ | |
| https://github.com/mcpp-community/mcpp.git "$src" | |
| # ⚠️ THE CLONE'S OWN WORKSPACE PIN MUST NOT DECIDE WHICH mcpp | |
| # BUILDS IT. `.xlings.json` at mcpp's root pins the mcpp that | |
| # compiles mcpp, and that pin does not move when mcpp is released — | |
| # so a build inside the checkout obeys it and tries to install a | |
| # version the index may no longer carry: | |
| # | |
| # [error] xlings: version '2026.8.17.1' not found for 'mcpp' | |
| # available: 2026.8.25.1 | |
| # | |
| # What is wanted here is the source compiled by the mcpp installed | |
| # above, which is exactly what removing the file leaves. | |
| rm -f "$src/.xlings.json" | |
| ( cd "$src" && mcpp build --release ) | |
| # ⚠️ BOTH SPELLINGS, AND NO `-perm`. The matrix reaches Windows and | |
| # macOS runners too: on Windows the artefact is `mcpp.exe`, and | |
| # `-perm -u+x` is not a question that filesystem answers the way this | |
| # expects. Measured: `Finished release [optimized] in 173.44s` | |
| # followed by "mcpp did not build" — the build had succeeded and the | |
| # search was looking for the wrong name. | |
| # | |
| # `$src` is a FRESH clone each run, so `target/` holds exactly what | |
| # this step just built; `-printf` would be the safer form on a cached | |
| # tree and is a GNU extension this must not use. | |
| built=$(find "$src/target" -type f \ | |
| \( -name mcpp -o -name mcpp.exe \) | head -1) | |
| [ -n "$built" ] || { echo "::error::mcpp did not build from $MCPP_SOURCE_REF"; exit 1; } | |
| echo "$(cd "$(dirname "$built")" && pwd)" >> "$GITHUB_PATH" | |
| # ⚠️ Reported, because a PATH entry that does not win looks exactly | |
| # like one that does until something built with the wrong engine. | |
| echo "under review: $("$built" --version) (from $MCPP_SOURCE_REF)" | |
| fi | |
| - name: Select the toolchain | |
| run: | | |
| spec='${{ matrix.toolchain }}' | |
| mcpp toolchain install "${spec%@*}" "${spec#*@}" | |
| mcpp toolchain default "$spec" | |
| mcpp toolchain list | |
| - name: The library builds | |
| run: | | |
| extra='' | |
| [ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}' | |
| mcpp build $extra | |
| # ⭐ AN OPTIONAL INTERFACE IS REFERENCED WEAKLY, WHICH IS A PROPERTY OF | |
| # THE OBJECT AND NOT OF ANY ONE LINK. | |
| # | |
| # `openkal.random` is optional, and clause 6.1 expresses an | |
| # implementation that does not provide it as the absence of a link-time | |
| # definition. This dispatcher is linked into every program, so a strong | |
| # reference to `kal_random_fill` makes an optional interface mandatory: | |
| # every program over a backend without it fails to link, whether or not | |
| # it wanted a random byte. | |
| # | |
| # ⚠️ THAT DEFECT SHIPPED, AND NOTHING HERE SAW IT. It was found one | |
| # repository downstream, by a bare-metal program in openkal-llvm-runtime | |
| # linking over openkal-opensbi: | |
| # | |
| # ld.lld: error: undefined symbol: kal_random_fill | |
| # | |
| # Reproducing it here would need a bare-metal toolchain and a backend | |
| # that declines the interface. The symbol class needs neither, and states | |
| # the invariant more directly than a link would: `w` for the optional | |
| # one, `U` for a required one beside it. | |
| - name: An optional interface is referenced weakly | |
| if: runner.os == 'Linux' | |
| run: | | |
| set -euo pipefail | |
| # ⚠️ ONE FINGERPRINT DIRECTORY, ASSERTED BEFORE ANYTHING IS READ. | |
| # `target/` accumulates one per configuration, and a search across all | |
| # of them answers for a build that is not this one. The step that | |
| # checks the withheld set already learned this; the assertion is made | |
| # here for the same reason and not by reference to that one. | |
| fps=$(ls -d target/*/*/ 2>/dev/null | wc -l) | |
| [ "$fps" = 1 ] || { echo "::error::expected one fingerprint directory under target/, found $fps" | |
| ls -d target/*/*/ 2>/dev/null | sed 's/^/ /' | |
| exit 1; } | |
| # ⚠️⚠️ AND THIS PACKAGE'S OWN OBJECTS, WHICH IS NOT WHAT A SEARCH UNDER | |
| # `target/` FINDS. Measured while this step was extended: a search of | |
| # everything under `target/` reported `kal_net_accept` and | |
| # `kal_datagram_recv_from` as undefined STRONG references and the other | |
| # nine as weak — because the DEPENDENCY's objects are there too, under | |
| # `obj/mcpplibs_*`, and openkal-linux's `kal_timeout_accept` refers to | |
| # its own `kal_net_accept` strongly. That is correct for an | |
| # implementation and says nothing about this port. | |
| objs=$(find target/*/*/obj -maxdepth 1 -name '*.o') | |
| n=$(printf '%s\n' "$objs" | grep -c . || true) | |
| echo " examining $n of this package's own objects" | |
| [ "$n" -gt 100 ] || { echo "::error::only $n objects; nothing was examined"; exit 1; } | |
| nm="$(command -v llvm-nm || command -v nm)" | |
| "$nm" $objs > syms.txt 2>/dev/null || true | |
| # The control: a required interface must still be a strong reference, | |
| # so that a backend failing to provide one is still a link error. | |
| grep -qE '^ *U kal_time_sleep$' syms.txt \ | |
| || { echo "::error::kal_time_sleep is not an undefined strong reference — the check below proves nothing" | |
| grep kal_time syms.txt; exit 1; } | |
| grep -qE '^ *w kal_random_fill$' syms.txt \ | |
| || { echo "::error::kal_random_fill is not a weak reference; an optional interface has been made mandatory" | |
| grep kal_random syms.txt; exit 1; } | |
| # ⭐⭐ AND THE SAME FOR EVERY INTERFACE THE 0.8 ROUTES REACH, WHICH IS | |
| # WHY THIS STEP IS NOT A SINGLE ASSERTION ANY MORE. | |
| # | |
| # `openkal.net`, `openkal.datagram`, `openkal.timeout` and | |
| # `openkal.space` are optional in exactly the sense `openkal.random` | |
| # is, and openkal-opensbi and openkal-uefi decline all four. A strong | |
| # reference to any one of them would make a bare-metal program that | |
| # never opens a socket fail to link — which is the defect this step | |
| # already exists because of, arriving through a different name. | |
| # | |
| # ⚠️ THE SYMBOL IS SOUGHT ACROSS THE PORT'S OBJECTS RATHER THAN IN ONE, | |
| # because the routes are spread over three sources: okm_net.c, | |
| # okm_poll.c and okm_fork.c. Naming one file would assert a property of | |
| # that file and report nothing about the others. | |
| weakfail=0 | |
| for name in kal_net_connect kal_net_listen kal_net_accept kal_net_close \ | |
| kal_datagram_open kal_datagram_recv_from \ | |
| kal_timeout_read kal_timeout_write kal_timeout_accept \ | |
| kal_timeout_wait_process \ | |
| kal_space_start kal_process_channel; do | |
| if grep -qE "^ *U $name\$" syms.txt; then | |
| echo "::error::$name is an undefined STRONG reference; an interface a backend may decline has been made mandatory" | |
| weakfail=1 | |
| elif grep -qE "^ *w $name\$" syms.txt; then | |
| echo " weak: $name" | |
| else | |
| echo "::error::$name is referenced nowhere; the route that was added does not call it" | |
| weakfail=1 | |
| fi | |
| done | |
| [ "$weakfail" = 0 ] || exit 1 | |
| echo " ok every optional interface is referenced weakly, and kal_time_sleep is strong" | |
| # ⚠️⚠️ AND ONE OF THEM IS AN OBJECT, WHICH IS NOT TESTED THE WAY THE | |
| # ELEVEN ABOVE ARE. | |
| # | |
| # Every name above is a function, so `if (kal_net_connect)` tests the | |
| # ADDRESS and is correct. `kal_process_props` is a capability word: | |
| # the same spelling would READ it, and where the definition is absent | |
| # the object sits at address zero --- so the test written to prevent a | |
| # null dereference would be one. okm_opt.h takes the address, once, and | |
| # every caller reaches the word through that. | |
| # | |
| # ⚠️ WHAT THIS STEP CAN AND CANNOT SEE. That the reference is weak, it | |
| # can. That the source takes the address rather than reading the value, | |
| # it cannot --- both forms leave a relocation. The rule is stated where | |
| # it is used and asserted here only against the failure a link can | |
| # produce: a strong reference, which would make a backend that declines | |
| # `openkal.process` fail to link every program. | |
| case "$(grep -E '^ *[wv] kal_process_props$' syms.txt | wc -l)" in | |
| 0) echo "::error::kal_process_props is not a weak reference in these objects" | |
| grep kal_process_props syms.txt || echo " (it is referenced nowhere)" | |
| exit 1 ;; | |
| *) echo " weak object: kal_process_props" ;; | |
| esac | |
| # ⭐⭐ ASKING WHETHER A STREAM IS A TERMINAL GETS THE RIGHT ANSWER. | |
| # | |
| # musl's `isatty' asks with TIOCGWINSZ; this port answered only TCGETS, | |
| # so every `isatty' returned 0 — for a real terminal as readily as for a | |
| # pipe. Nothing failed: `std::print' simply never took its terminal path, | |
| # and a program deciding on colour or on line buffering decided wrongly | |
| # and in silence. | |
| # | |
| # ⭐ THE CRITERION IS A RELATION, NOT A VALUE. `isatty` under a pipe and | |
| # under a pseudo-terminal must DIFFER, and must differ the same way the | |
| # system's own C library does. A test asserting "0 in a pipe" alone would | |
| # have passed throughout the defect. | |
| - name: Asking whether a stream is a terminal is answered, not refused | |
| if: runner.os == 'Linux' && matrix.target == '' | |
| run: | | |
| d="$(mktemp -d)"; mkdir -p "$d/src" | |
| cat > "$d/mcpp.toml" <<TOML | |
| [package] | |
| name = "isattyprobe" | |
| version = "0.1.0" | |
| [dependencies] | |
| openkal-musl = { path = "$PWD" } | |
| [targets.isattyprobe] | |
| kind = "bin" | |
| main = "src/main.c" | |
| [build] | |
| cxx_runtime = "host-coupled" | |
| TOML | |
| sed -i 's/^ //' "$d/mcpp.toml" | |
| printf '#include <unistd.h>\n#include <stdio.h>\nint main(void){ printf("%%d\\n", isatty(1)); return 0; }\n' > "$d/src/main.c" | |
| ( cd "$d" && mcpp build --toolchain '${{ matrix.toolchain }}' ) | |
| bin="$(find "$d/target" -name isattyprobe -type f | head -1)" | |
| test -n "$bin" || { echo "::error::the probe did not build"; exit 1; } | |
| # The control: the system's own C library, through the same harness. | |
| # Without it a `script` that fails to allocate a pty would make the | |
| # port look broken. | |
| printf '#include <unistd.h>\n#include <stdio.h>\nint main(void){ printf("%%d\\n", isatty(1)); return 0; }\n' > "$d/ctrl.c" | |
| cc "$d/ctrl.c" -o "$d/ctrl" | |
| ctrl_pipe="$("$d/ctrl" | cat | tr -d '\r')" | |
| ctrl_tty="$(script -qec "$d/ctrl" /dev/null | tr -d '\r' | head -1)" | |
| [ "$ctrl_pipe" = 0 ] && [ "$ctrl_tty" = 1 ] \ | |
| || { echo "::error::the harness cannot tell a pty from a pipe (control gave $ctrl_pipe/$ctrl_tty) — this check would prove nothing" | |
| exit 1; } | |
| port_pipe="$("$bin" | cat | tr -d '\r')" | |
| port_tty="$(script -qec "$bin" /dev/null | tr -d '\r' | head -1)" | |
| echo " control: pipe=$ctrl_pipe tty=$ctrl_tty port: pipe=$port_pipe tty=$port_tty" | |
| [ "$port_pipe" = "$ctrl_pipe" ] && [ "$port_tty" = "$ctrl_tty" ] \ | |
| || { echo "::error::isatty over this port disagrees with the system's own C library"; exit 1; } | |
| echo " ok isatty answers the same as the system's own C library" | |
| # ⭐⭐ THE INTERNAL OVERLAY STOPS AT THIS PACKAGE'S BOUNDARY. | |
| # | |
| # musl reaches its own declarations through `src/include`, whose headers | |
| # define `hidden`, `weak` and `weak_alias` — names that mean something | |
| # only to musl's own sources. This package publishes the path it is built | |
| # from, so every consumer used to see them too, and which consumer broke | |
| # on which name was found one at a time (openkal-musl#13). | |
| # | |
| # `[build] private_include_dirs` (mcpp 2026.8.27.1) says which entries of | |
| # `include_dirs` stop here. This asserts the DIRECTORY is absent from a | |
| # consumer's command line — not that one macro no longer collides, which | |
| # would go green again the moment the package patched that macro while | |
| # the leak stayed. | |
| # WHAT IS WITHHELD IS NOT DEFINED BY THIS PACKAGE, AND WHAT IS NOT | |
| # WITHHELD IS. | |
| # | |
| # ⚠️⚠️ THE CRITERION IS THE PACKAGE'S OWN OBJECTS, NOT A PROGRAM'S LINK. | |
| # | |
| # It was a program's link, and that measured the wrong thing. Under one | |
| # toolchain the probe built successfully for symbols this package does not | |
| # define at all --- something else on the link line supplied them --- so | |
| # the check reported "did not fail at the link" for a facility that had in | |
| # fact been withheld. A program's link is closed over this port only when | |
| # nothing else answers, and that is a property of the toolchain rather than | |
| # of this package. | |
| # | |
| # A definition either is in these objects or is not. That holds under every | |
| # toolchain and cannot be satisfied by a host C library. | |
| # | |
| # ⚠️ AND THE OBJECTS ARE SCOPED TO ONE FINGERPRINT DIRECTORY. `target/` | |
| # accumulates one per configuration, so a search across all of them reads | |
| # definitions from a build made before the change --- which is how this | |
| # check first reported every withheld symbol as still present. | |
| - name: What is withheld is not defined, and what is not withheld is | |
| if: runner.os == 'Linux' && matrix.target == '' | |
| run: | | |
| set -euo pipefail | |
| fps=$(ls -d target/*/*/ 2>/dev/null | wc -l) | |
| [ "$fps" = 1 ] || { echo "::error::expected one fingerprint directory under target/, found $fps" | |
| ls -d target/*/*/ 2>/dev/null | sed 's/^/ /' | |
| exit 1; } | |
| objs=$(find target -name '*.o') | |
| n=$(printf '%s\n' "$objs" | grep -c . || true) | |
| echo " examining $n objects in $(ls -d target/*/*/)" | |
| [ "$n" -gt 100 ] || { echo "::error::only $n objects; nothing was examined"; exit 1; } | |
| defines() { # symbol -> the number of definitions in these objects | |
| nm $objs 2>/dev/null | grep -cE "^[0-9a-f]+ [TWi] $1\$" || true | |
| } | |
| fail=0 | |
| for s in epoll_create1 eventfd timerfd_create inotify_init signalfd; do | |
| d=$(defines "$s") | |
| if [ "$d" = 0 ]; then echo " withheld, not defined: $s" | |
| else echo "::error::$s is withheld and yet defined $d time(s)"; fail=1; fi | |
| done | |
| # The other half. Without it the check above would pass for a package | |
| # that had stopped compiling anything at all. `pipe` is here because | |
| # openkal 0.8 made it expressible; `socket` and `fork` because their | |
| # closures reach the password functions and the thread implementation, | |
| # so they are deliberately NOT withheld and the manifest says why. | |
| for s in printf malloc open pipe faccessat chmod socket fork; do | |
| d=$(defines "$s") | |
| if [ "$d" -ge 1 ]; then echo " defined here: $s" | |
| else echo "::error::$s is not withheld and yet is not defined"; fail=1; fi | |
| done | |
| [ "$fail" = 0 ] || exit 1 | |
| echo " ok the withheld set is exactly what the manifest names" | |
| - name: What this package is built from is not what it publishes | |
| working-directory: examples/cross-hello | |
| run: | | |
| extra='' | |
| [ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}' | |
| mcpp build --toolchain '${{ matrix.toolchain }}' $extra | |
| test -s compile_commands.json \ | |
| || { echo "::error::no compile_commands.json — nothing to check"; exit 1; } | |
| # ⚠️⚠️ PER ROW, NOT OVER THE FILE. This example depends on the | |
| # package by path, so THE PROVIDER'S OWN ROWS ARE IN THIS SAME FILE | |
| # and they carry the overlay legitimately — that is what "private, | |
| # not unused" means. A `grep` over the whole file cannot tell the two | |
| # apart and would call the package's own build a leak. | |
| # | |
| # ⚠️ Separators are normalised because the Windows runner writes | |
| # `…\musl\src\include`, and a check that silently stops matching on | |
| # one platform is a check that platform does not have. | |
| norm='(.arguments // (.command | split(" "))) | join(" ") | gsub("\\\\"; "/")' | |
| jq -r ".[] | select((.file | gsub(\"\\\\\\\\\"; \"/\")) | test(\"examples/cross-hello\")) | $norm" \ | |
| compile_commands.json > consumer.txt | |
| jq -r ".[] | select((.file | gsub(\"\\\\\\\\\"; \"/\")) | test(\"examples/cross-hello\") | not) | $norm" \ | |
| compile_commands.json > provider.txt | |
| # ⚠️ DENOMINATORS ON BOTH SIDES. With no consumer row every absence | |
| # below is vacuously true; with no provider row the control is. | |
| cons="$(wc -l < consumer.txt)"; prov="$(wc -l < provider.txt)" | |
| echo " rows: consumer=$cons provider=$prov" | |
| [ "$cons" -ge 1 ] && [ "$prov" -ge 1 ] \ | |
| || { echo "::error::consumer=$cons provider=$prov — nothing was checked"; exit 1; } | |
| bad=0 | |
| for d in musl/src/include musl/src/internal musl-generated/internal; do | |
| if grep -q -- "$d" consumer.txt; then | |
| echo "::error::the internal overlay '$d' reached a consumer" | |
| bad=1 | |
| fi | |
| # The other half of the same key: private is not the same as | |
| # dropped. musl's own sources must still reach their declarations. | |
| grep -q -- "$d" provider.txt \ | |
| || { echo "::error::'$d' is on nobody's command line — private_include_dirs withheld it from this package too" | |
| bad=1; } | |
| done | |
| # And something PUBLIC must still cross the boundary, or this check | |
| # would pass for a build that published nothing at all. | |
| grep -q -- 'port/include' consumer.txt \ | |
| || { echo "::error::no public include directory reached the consumer — the check above proves nothing" | |
| exit 1; } | |
| [ "$bad" = 0 ] || exit 1 | |
| echo " ok the internal overlay stops here; the public headers do not" | |
| # A program above this package names one package. It does not name | |
| # openkal, it does not name an implementation, and it says nothing about | |
| # the platform. | |
| # | |
| # ⚠️ FOUR PROBES, ONE RUNNER. tools/run-probe.sh holds the watchdog, the | |
| # report of where a program that stopped was, and the two readings of the | |
| # output. Four copies of that would be four places for one of them to fall | |
| # behind. | |
| - name: The posix probe | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: bash tools/run-probe.sh examples/posix posix | |
| # A BUILD STATES WHICH VERSION OF THIS LIBRARY IT HOLDS, AND THE STATEMENT | |
| # IS COMPARED WITH THE MANIFEST RATHER THAN READ. | |
| # | |
| # This step exists because of what its absence cost. Two rounds of | |
| # mcpplibs/openkal-linux#13 were answered against the wrong version: the | |
| # only version-shaped thing a program could read was `uname`'s release | |
| # field, which was the literal "0.5.0" through every release after 0.5.0, | |
| # so a consumer who checked it was told a version and the version was | |
| # wrong. The report that followed named versions its author believed in | |
| # and could not verify, and neither could we. | |
| # | |
| # Three observations, and the third is the one that keeps this honest for | |
| # everybody who is NOT debugging: | |
| # | |
| # 1. the banner names exactly what mcpp.toml says | |
| # 2. `uname` reports the same string | |
| # 3. WITHOUT the variable, the program writes nothing to the error | |
| # stream at all | |
| # | |
| # Without (3) this feature would be free to become noise in every | |
| # ordinary run, and nothing would say so. | |
| - name: A build states its own version, and says nothing when not asked | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: | | |
| set -euo pipefail | |
| want="$(sed -n 's/^version *= *"\(.*\)"/\1/p' mcpp.toml | head -1)" | |
| [ -n "$want" ] || { echo "::error::no version in mcpp.toml"; exit 1; } | |
| echo " the manifest says $want" | |
| cd examples/posix | |
| binary="$(bash "$GITHUB_WORKSPACE/tools/one-artifact.sh" posix)" | |
| # (3) first, because it is the property an ordinary run depends on. | |
| # | |
| # `-eq' AND NOT `='. This step runs on every row, and BSD `wc' pads its | |
| # count with spaces where GNU `wc' does not, so a string comparison | |
| # reads " 0" and fails on a program that wrote nothing: | |
| # | |
| # ##[error]the program wrote 0 line(s) to the error stream | |
| # | |
| # The step above that does the same thing is `if: runner.os == Linux', | |
| # which is why it never met this. | |
| quiet="$("./$binary" 2>&1 >/dev/null | wc -l)" | |
| [ "$quiet" -eq 0 ] || { | |
| echo "::error::the program wrote $quiet line(s) to the error stream without being asked" | |
| "./$binary" 2>&1 >/dev/null | sed 's/^/ /'; exit 1; } | |
| echo " ok silent unless asked" | |
| # (1) the banner. Each process announces itself once, so a program | |
| # that starts another produces more than one line; they must agree. | |
| banners="$(OPENKAL_MUSL_TRACE=enosys "./$binary" 2>&1 >/dev/null | grep '^openkal-musl [0-9]' | sort -u)" | |
| [ "$banners" = "openkal-musl $want" ] || { | |
| echo "::error::expected exactly 'openkal-musl $want'; got:" | |
| printf '%s\n' "$banners" | sed 's/^/ /'; exit 1; } | |
| echo " ok the banner names $want" | |
| # (2) and the field a program reads without setting anything. | |
| got="$("./$binary" 2>/dev/null | sed -n 's/^note: release=//p' | head -1)" | |
| [ "$got" = "$want" ] || { | |
| echo "::error::uname reports '$got' and the manifest says '$want'"; exit 1; } | |
| echo " ok uname reports $want" | |
| # ⭐ THE NAMES THIS LIBRARY MUST NOT TAKE FROM A PROGRAM ABOVE IT. | |
| # | |
| # Reported as openkal-musl#13. This one is a COMPILE-TIME criterion: the | |
| # source declares `hidden`, `weak` and `weak_alias` as ordinary | |
| # identifiers, and if any of the three is a macro again the file does not | |
| # compile. It is run as well as built so that something links afterwards, | |
| # which is what distinguishes a source that compiles from a package that | |
| # works. | |
| - name: A program may use the names the internal overlay defines | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: | | |
| bash tools/run-probe.sh examples/identifiers identifiers | |
| grep -q 'hidden+weak+weak_alias = 41' examples/identifiers/run.log | |
| # ⭐⭐ THE ROUTES openkal 0.8 MADE POSSIBLE, EXERCISED THROUGH POSIX. | |
| # | |
| # `socket`, `bind`, `listen`, `accept`, `connect`, `sendto`, `recvfrom`, | |
| # `poll` and `select` reached this port's default arm and returned ENOSYS | |
| # until `openkal.net`, `openkal.datagram` and `openkal.timeout` existed to | |
| # route them onto (openkal-linux#13). The probe names no openkal symbol: | |
| # a probe that called `kal_net_connect` to check that `connect` works | |
| # would be checking the wrong thing. | |
| # | |
| # ⚠️ `matrix.net` DECIDES WHETHER THE ROW RUNS IT, and the value is a | |
| # property of the BACKEND rather than of the system. A backend that | |
| # declines `openkal.net` is behaving correctly; a row that expected it and | |
| # silently did not get it is what this must not read as a pass. | |
| - name: The network probe | |
| if: matrix.net == 'yes' | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: bash tools/run-probe.sh examples/net net | |
| # Another program, started three ways. ⭐ WHAT IS EXPECTED IS PASSED IN | |
| # RATHER THAN INFERRED: `--no-fork` requires that duplicating the calling | |
| # image be REFUSED, so a system whose backend declines `openkal.space` is | |
| # asserted to decline it rather than merely not asked. | |
| - name: The subprocess probe | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: bash tools/run-probe.sh examples/subprocess subprocess ${{ matrix.fork }} ${{ matrix.shell }} ${{ matrix.abort }} | |
| # ⭐⭐ WHETHER AN ANSWER IS TRUE, WHICH IS A DIFFERENT QUESTION FROM | |
| # WHETHER AN OPERATION WORKS --- AND THE ONE NO PROBE HERE WAS ASKING. | |
| # | |
| # Every probe above starts something, opens something or transfers | |
| # something and asserts that it happened. A whole family of defects lived | |
| # underneath that: `fcntl(F_SETLK)' granted every lock and took none, so | |
| # two programs held one exclusive lock; `F_GETLK' left the caller's word | |
| # untouched, so the answer read "somebody holds this" for ever; | |
| # `getppid' returned -38 AS AN IDENTIFIER; `sigaltstack' reported an | |
| # installation it had not performed; `sysconf(_SC_OPEN_MAX)' answered 0 | |
| # for a bound this library sets itself. | |
| # | |
| # ⚠️ NOT ONE OF THEM IS A MISSING OPERATION, so not one appears in | |
| # `OPENKAL_MUSL_TRACE=enosys'. They were found by comparing every answer | |
| # against the host's, and this probe is that comparison kept. | |
| - name: The surface probe | |
| env: | |
| MCPP_TARGET: ${{ matrix.target }} | |
| run: bash tools/run-probe.sh examples/surface surface ${{ matrix.dirtime }} | |
| # ⭐⭐ WHERE A STARTED PROGRAM'S OUTPUT WENT, WHICH THE PROBE CANNOT ASK | |
| # ABOUT ITSELF. | |
| # | |
| # A caller that redirects descriptor 1 and then starts a program used to | |
| # get the program's bytes on the stream IT had been started with, and the | |
| # file it had redirected onto stayed empty (openkal-linux#13). The probe | |
| # asserts the file; it cannot assert the other half, because a program | |
| # cannot read its own output. This log is that output. | |
| # | |
| # ⚠️ BOTH DIRECTIONS, AND THE SECOND IS NOT DECORATION. Requiring only that | |
| # the redirected markers are absent would pass for a library that had | |
| # stopped letting a started program write anywhere at all; requiring only | |
| # that the inherited one is present would pass for the defect. The probe's | |
| # own messages are worded so that neither token can appear in one. | |
| - name: A started program's output went where the caller sent it | |
| working-directory: examples/subprocess | |
| run: | | |
| set -euo pipefail | |
| test -s run.log || { echo "::error::no run.log — nothing to read"; exit 1; } | |
| if grep -q 'redirected-bytes' run.log; then | |
| echo "::error::a started program's output arrived on the caller's own stream" | |
| grep -n 'redirected-bytes' run.log | sed 's/^/ /' | |
| exit 1 | |
| fi | |
| grep -q 'inherited-child-bytes' run.log \ | |
| || { echo "::error::a started program that redirected nothing wrote nowhere; the check above proves nothing" | |
| exit 1; } | |
| echo " ok redirected output reached the file; inherited output reached the caller" | |
| # ⭐ AN OPERATION THIS LIBRARY DOES NOT HAVE CAN SAY SO WHEN ASKED. | |
| # | |
| # The default arm of the dispatcher answers ENOSYS in silence, and the only | |
| # way a consumer could learn WHICH operation was missing was to read | |
| # port/src/okm_syscall.c. Two rounds of openkal-linux#13 went on that | |
| # question. | |
| # | |
| # ⚠️ THREE OBSERVATIONS, BECAUSE THE INTERESTING FAILURES ARE THE QUIET | |
| # ONES: a channel that reports nothing when asked, a channel that reports | |
| # when it was not asked, and a channel that reports the same thing once per | |
| # attempt so that a reader counting lines concludes it happened once. | |
| - name: An absent operation reports which one it was, and only when asked | |
| if: runner.os == 'Linux' && matrix.target == '' | |
| run: | | |
| set -euo pipefail | |
| d="$(mktemp -d)"; mkdir -p "$d/src" | |
| cat > "$d/mcpp.toml" <<TOML | |
| [package] | |
| name = "traceprobe" | |
| version = "0.1.0" | |
| [dependencies] | |
| openkal-musl = { path = "$PWD" } | |
| [targets.traceprobe] | |
| kind = "bin" | |
| main = "src/main.c" | |
| [build] | |
| cxx_runtime = "host-coupled" | |
| TOML | |
| sed -i 's/^ //' "$d/mcpp.toml" | |
| # ⚠️⚠️ THE OPERATION THIS PROBE NAMES MUST STILL BE ABSENT, AND THE | |
| # ONE IT NAMED STOPPED BEING SO. | |
| # | |
| # It was `symlinkat`, chosen because openkal had no atom that creates a | |
| # link. openkal 0.9 added `kal_fs_link_create`, this dispatcher gained | |
| # a case for it, and the probe --- unchanged, still green in intent --- | |
| # began exercising an operation that now SUCCEEDS. It reported zero | |
| # diagnostics for a hundred attempts, which is the same reading a | |
| # broken diagnostic channel gives. | |
| # | |
| # ⭐ SO THE ABSENCE IS NOW ASSERTED RATHER THAN ASSUMED. `mknodat` | |
| # creates a device node, which openkal does not express and is not | |
| # going to; if a case for it ever appears, the grep below fails and | |
| # says to pick another operation --- instead of this step passing | |
| # while measuring nothing. | |
| if grep -q 'SYS_mknodat' port/src/okm_syscall.c; then | |
| echo "::error::the dispatcher now handles mknodat, so this probe no" | |
| echo "::error::longer exercises an absent operation. Pick another" | |
| echo "::error::operation openkal has no atom for and name it here." | |
| exit 1 | |
| fi | |
| # The number is printed by the probe rather than computed here, so the | |
| # expectation comes from the same headers the dispatcher was compiled | |
| # with; a number worked out on the host would answer for the host's C | |
| # library. | |
| printf '%s\n' \ | |
| '#include <sys/syscall.h>' \ | |
| '#include <sys/stat.h>' \ | |
| '#include <fcntl.h>' \ | |
| '#include <unistd.h>' \ | |
| '#include <stdio.h>' \ | |
| 'int main(void) {' \ | |
| ' for (int i = 0; i < 100; i++)' \ | |
| ' (void)!mknodat(AT_FDCWD, "node", S_IFIFO | 0600, 0);' \ | |
| ' printf("%ld\n", (long)SYS_mknodat);' \ | |
| ' return 0;' \ | |
| '}' > "$d/src/main.c" | |
| ( cd "$d" && mcpp build --toolchain '${{ matrix.toolchain }}' ) | |
| bin="$(find "$d/target" -name traceprobe -type f | head -1)" | |
| test -n "$bin" || { echo "::error::the probe did not build"; exit 1; } | |
| want="$("$bin" 2> /dev/null)" | |
| [ -n "$want" ] || { echo "::error::the probe printed no operation number"; exit 1; } | |
| quiet="$("$bin" 2>&1 > /dev/null | wc -l)" | |
| [ "$quiet" = 0 ] \ | |
| || { echo "::error::the channel reported $quiet line(s) without being asked" | |
| "$bin" 2>&1 > /dev/null | sed 's/^/ /'; exit 1; } | |
| asked="$(OPENKAL_MUSL_TRACE=enosys "$bin" 2>&1 > /dev/null)" | |
| echo " what it reported: $asked" | |
| n="$(printf '%s\n' "$asked" | grep -c 'no operation for system call' || true)" | |
| [ "$n" = 1 ] \ | |
| || { echo "::error::expected exactly one report for one hundred attempts, got $n" | |
| exit 1; } | |
| printf '%s\n' "$asked" | grep -q "no operation for system call $want\$" \ | |
| || { echo "::error::the report does not name the operation the probe asked for ($want)" | |
| exit 1; } | |
| echo " ok silent unless asked, one line per operation, and it names the operation" | |
| - name: The same program, built the ordinary way, as a control | |
| run: | | |
| # ⚠️ THIS STEP EXISTS BECAUSE IT ALREADY EARNED ITS PLACE. | |
| # | |
| # The cross-built copy failed on a machine of the other system, and the | |
| # obvious reading was a defect in this port or in the way it was | |
| # cross-built. A native build of the SAME source reproduced it here --- | |
| # which said it was neither, and the defect was in the program's own | |
| # assertion macro, which evaluated its condition twice and so closed a | |
| # stream that was already closed. | |
| # | |
| # Two failures that look alike are told apart by building the same | |
| # source two ways, and that is cheap enough to do every time. | |
| # ⚠️ The target has to be named here as it is everywhere else in this | |
| # job: one system needs it, and a step that omitted it built for that | |
| # system's other toolchain and failed at the link with names kernel32 | |
| # supplies. Measured, on the first run of this step. | |
| extra='' | |
| [ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}' | |
| cd examples/cross-hello | |
| mcpp build $extra | |
| binary="$(bash "$GITHUB_WORKSPACE/tools/one-artifact.sh" cross-hello)" | |
| "./$binary" 2>&1 | tee out.log | |
| grep -q -- '-- failures: 0 --' out.log | |
| - name: The counts agree with the system's own | |
| working-directory: examples/wordcount | |
| run: | | |
| printf 'alpha beta\ngamma\n' > sample.txt | |
| expected="$(wc < sample.txt | tr -s ' ' | sed 's/^ //')" | |
| extra='' | |
| [ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}' | |
| mcpp build $extra | |
| binary="$(bash "$GITHUB_WORKSPACE/tools/one-artifact.sh" wordcount)" | |
| WORDCOUNT_VERBOSE=1 "$binary" sample.txt 2>&1 | tee run.log | |
| counts="$(sed -n 's/^lines \([0-9]*\) words \([0-9]*\) bytes \([0-9]*\)$/\1 \2 \3/p' run.log)" | |
| test -n "$counts" || { echo "the program printed no count" >&2; exit 1; } | |
| echo "wordcount: $counts" | |
| echo "wc: $expected" | |
| test "$counts" = "$expected" | |
| # The variable was consulted, and the interval was measured. | |
| grep -q 'elapsed .* nanoseconds' run.log | |
| # --------------------------------------------------------------------------- | |
| # The measurement musl/PATCHES.md records, made from a machine that is not the | |
| # system it is about. | |
| # | |
| # It is a job rather than a note because the claim it supports --- that a | |
| # program for that system can be built, and linked, without any file that | |
| # system supplies --- is one that a change to this port could silently undo. | |
| # The two numbers it asserts are zero indirect symbols and exactly two names. | |
| cross-macos: | |
| name: cross-link for the other system, from this one | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 30 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: The implementation for that system | |
| run: | | |
| branch='${{ github.head_ref || github.ref_name }}' | |
| git clone --quiet https://github.com/mcpplibs/openkal-macos.git ../openkal-macos | |
| git -C ../openkal-macos checkout --quiet "origin/$branch" 2>/dev/null || true | |
| git clone --quiet https://github.com/mcpplibs/openkal.git ../openkal | |
| git -C ../openkal checkout --quiet "origin/$branch" 2>/dev/null || true | |
| - name: Install LLVM | |
| run: | | |
| sudo apt-get update -qq | |
| sudo apt-get install -y -qq clang lld llvm | |
| # ld64.lld is the Mach-O driver of the same binary; Ubuntu's package | |
| # installs it under a version suffix and without the plain name. | |
| v=$(ls /usr/lib/llvm-*/bin/ld64.lld 2>/dev/null | sort -V | tail -1) | |
| test -n "$v" || { echo "::error::this image has no ld64.lld"; exit 1; } | |
| d=$(dirname "$v") | |
| echo "LD64=$v" >> "$GITHUB_ENV" | |
| # The tools are installed under a version suffix and the probe asks for | |
| # them by their plain names, so the directory that has both spellings | |
| # is named rather than assumed. | |
| echo "NM=$d/llvm-nm" >> "$GITHUB_ENV" | |
| echo "$d" >> "$GITHUB_PATH" | |
| "$d/llvm-nm" --version | head -1 | |
| clang --version | head -1 | |
| - name: Zero indirect symbols, and two names | |
| run: | | |
| bash tools/probe-cross-macos.sh aarch64 | |
| bash tools/probe-cross-macos.sh x86_64 | |
| # ⚠️ LINKING IS NOT RUNNING, AND THIS IS WHERE THAT IS ADMITTED. | |
| # | |
| # Everything above happens on a machine that is not the system in | |
| # question, and everything above is about the objects and the link. Whether | |
| # the result STARTS is a different question, and it cannot be asked here: | |
| # that system's 64-bit ARM variant refuses to start an image that is not | |
| # signed, and the signature can only be made on a machine of that system. | |
| # | |
| # So the artifact is carried there. The job that receives it is the only | |
| # place in this workflow where the claim becomes "a program built here | |
| # runs there" rather than "a program built here links". | |
| - name: A program for that system, built here | |
| run: | | |
| bash tools/cross-build-macos.sh aarch64 examples/cross-hello/src/main.c cross-hello-arm64 | |
| file cross-hello-arm64 | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: cross-hello-arm64 | |
| path: cross-hello-arm64 | |
| retention-days: 1 | |
| # --------------------------------------------------------------------------- | |
| # The other half of the claim, on a machine of that system. | |
| cross-macos-run: | |
| name: what was cross-built starts, on that system | |
| needs: cross-macos | |
| runs-on: macos-14 | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/download-artifact@v4 | |
| with: | |
| name: cross-hello-arm64 | |
| - name: Sign it, because this system will not start it otherwise | |
| run: | | |
| chmod +x cross-hello-arm64 | |
| # Ad hoc: the identity is `-', which asserts nothing about who made | |
| # the program and is exactly what this system requires before it will | |
| # start one on this architecture. A program that is distributed needs | |
| # more; a program that is checked needs this. | |
| codesign -s - --force cross-hello-arm64 | |
| codesign -dv cross-hello-arm64 2>&1 | head -3 | |
| - name: It starts, and the C library beneath it came up | |
| run: | | |
| ./cross-hello-arm64 | tee run.log | |
| grep -q -- '-- failures: 0 --' run.log |