Skip to content

openkal.exec,以及一种规范没有覆盖的偏性(6.5) #41

openkal.exec,以及一种规范没有覆盖的偏性(6.5)

openkal.exec,以及一种规范没有覆盖的偏性(6.5) #41

Workflow file for this run

name: CI
# What this workflow asserts about the specification.
#
# A specification is a claim about programs, so the claims are tested by
# building and running programs rather than by reading the text. There are four:
#
# declarations the two forms compile, under three compiler families and on
# three systems, and declare the same entities
# substitution a program's source is invariant under a change of
# implementation, and the check that says so fails when it should
# conformance the suite in this repository runs against the implementation
# for each system and every observation holds
# composability an implementation that provides three interfaces is examined
# for three, rather than failing to link
#
# The three compiler families are covered because the specification is a
# contract and a contract that holds only under the compiler its author used is
# a description of that compiler.
on:
push:
branches: [main]
pull_request:
workflow_dispatch:
env:
# A version verified to build these packages, not a measured minimum. The pin
# exists for reproducibility rather than because an older mcpp is known to
# fail.
MCPP_VERSION: 2026.8.19.4
XLINGS_VERSION: v2026.8.17.2
XLINGS_NON_INTERACTIVE: '1'
jobs:
# ---------------------------------------------------------------------------
# The declarations compile, everywhere, in both forms.
declarations:
name: declarations (${{ matrix.os }}, ${{ matrix.toolchain }})
runs-on: ${{ matrix.os }}
timeout-minutes: 45
strategy:
fail-fast: false
matrix:
include:
- { os: ubuntu-24.04, toolchain: 'gcc@16.1.0' }
- { os: ubuntu-24.04, toolchain: 'llvm@22.1.8' }
- { os: macos-14, toolchain: 'llvm@20.1.7' }
- { os: windows-2022, toolchain: 'llvm@20.1.7' }
- { os: windows-2022, toolchain: 'msvc@system' }
defaults:
run:
shell: bash
steps:
- uses: actions/checkout@v4
- name: Install xlings and mcpp (Unix)
if: runner.os != 'Windows'
run: |
curl -fsSL 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 and mcpp (Windows)
if: runner.os == 'Windows'
shell: pwsh
run: |
irm https://d2learn.org/xlings-install.ps1.txt | iex
# The installer amends the user's environment; a later step in this
# job reads none of it, so the directory is named here.
"$env:USERPROFILE\.xlings\subos\current\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
- name: Install mcpp
run: |
# ⚠️ A LOOP, BECAUSE ONE `xlings update` CAN RETURN A STALE INDEX
# WITHOUT SAYING SO.
#
# The index is published as an artifact behind a pointer, and that
# pointer propagates asynchronously after a version bump is merged.
# Measured on release day: an update run four minutes after the merge
# printed `index updated`, and the install then failed with
#
# package 'mcpp@<ver>' not found in the synced index
# (xim@artifact:<an older sha>, ...), synced 0 seconds ago
#
# Nothing had gone wrong. The update fetched the PREVIOUS artifact,
# and "synced 0 seconds ago" describes when it was fetched rather than
# what it contains — which is why the message reads as freshness.
#
# So this is not a retry around flakiness; it is the wait that a
# single update does not perform. A pin naming a version that was
# never published still fails, after the last attempt, and says which
# of the two situations it is.
for attempt in 1 2 3 4 5 6; do
xlings update > /dev/null 2>&1 || true
if xlings install "mcpp@$MCPP_VERSION" -y -g; then break; fi
if [ "$attempt" = 6 ]; then
echo "::error::mcpp@$MCPP_VERSION never appeared in the index (6 attempts over 5 minutes). If it was just released, the pointer has not propagated; if the pin names a version that was never published, it never will."
exit 1
fi
echo "the index has not caught up yet (attempt $attempt of 6); waiting 60s"
sleep 60
done
mcpp --version
mcpp self config --mirror GLOBAL
# The compiler family and version for this row. mcpp keeps its toolchains
# in a sandbox of its own, so this selects rather than installs into the
# system, and `mcpp test' and `mcpp run' have no flag for it --- which is
# why it is set once here rather than passed to each command.
- name: Select the toolchain
run: |
spec='${{ matrix.toolchain }}'
case "$spec" in
msvc*) mcpp toolchain default msvc ;;
*) mcpp toolchain install "${spec%@*}" "${spec#*@}"
mcpp toolchain default "$spec" ;;
esac
mcpp toolchain list
# The C++ form. The modules are the artefact a C++ consumer imports, and
# building them is what proves the compiler accepts them.
# ⚠️ A 32-BIT TARGET, AND NOTHING ELSE IN THIS REPOSITORY IS ONE.
#
# Every row of every job here is hosted, and every hosted target this
# specification serves is 64-bit. That is a structural blind spot rather
# than an omission: the C ABI this repository freezes is instantiated at
# two pointer widths, and only one of them was ever compiled.
#
# Measured 2026-08-20: `kal_node_info`'s frozen-layout assertion read
# `offsetof(modified_ns) == sizeof(kal_uintptr)`, which is true at 64 bits
# and false at 32 — the timestamp is a naturally-aligned `kal_u64`, so a
# 32-bit `size` is followed by four bytes of padding and the offset stays
# at eight. The failure surfaced in a CONSUMER (`mcpplibs/riscv-virt-rt`,
# whose rv32 leg activates the openkal feature), which is the only place
# the 32-bit layout existed at all.
#
# Compile-only: there is no 32-bit implementation to run against, and the
# claim under test is about layout rather than behaviour.
# ⚠️ A 32-BIT TARGET, AND NOTHING ELSE IN THIS REPOSITORY IS ONE.
#
# Every other row here is hosted, and every hosted target this
# specification serves is 64-bit. That is a structural blind spot: the C
# ABI this repository freezes is instantiated at two pointer widths, and
# only one of them was ever compiled.
#
# Measured 2026-08-20: `kal_node_info`'s frozen-layout assertion read
# `offsetof(modified_ns) == sizeof(kal_uintptr)`, true at 64 bits and
# false at 32 — the timestamp is a naturally-aligned `kal_u64`, so a
# 32-bit `size` is followed by four bytes of padding and the offset stays
# at eight. It surfaced in a CONSUMER (`mcpplibs/riscv-virt-rt`'s rv32
# leg), the only place the 32-bit layout existed at all.
#
# ⚠️ THROUGH `mcpp`, NOT THROUGH A BORROWED clang. The first version of
# this step globbed the LLVM payload for `clang++` — which is absent on
# the gcc and msvc rows, and is named `clang++.exe` on Windows, so the
# command expanded to nothing and the step died with `: command not
# found` on four rows. mcpp resolves the toolchain for a target itself;
# asking it is the only spelling that holds on every row.
# ⚠️ A 32-BIT TARGET, AND NOTHING ELSE IN THIS REPOSITORY IS ONE.
#
# Every other row here is hosted, and every hosted target this
# specification serves is 64-bit. That is a structural blind spot: the C
# ABI this repository freezes is instantiated at two pointer widths, and
# only one of them was ever compiled.
#
# Measured 2026-08-20: `kal_node_info`'s frozen-layout assertion read
# `offsetof(modified_ns) == sizeof(kal_uintptr)`, true at 64 bits and
# false at 32 — the timestamp is a naturally-aligned `kal_u64`, so a
# 32-bit `size` is followed by four bytes of padding and the offset stays
# at eight. It surfaced in a CONSUMER (`mcpplibs/riscv-virt-rt`'s rv32
# leg), the only place the 32-bit layout existed at all.
#
# ⚠️ THE PROBE LIVES INSIDE THE CHECKOUT AND USES A RELATIVE PATH. Two
# earlier spellings failed for reasons that had nothing to do with the
# ABI: globbing the LLVM payload for `clang++` died with `: command not
# found` on the rows whose toolchain is gcc or msvc, and interpolating
# `$GITHUB_WORKSPACE` into a C++ string literal produced
# `"D:\a\openkal\openkal/include"`, whose backslashes the compiler read
# as escape sequences. A relative directory has neither problem, and
# `include_dir` resolves it against the package root.
- name: The C ABI holds at thirty-two bits as well as sixty-four
run: |
set -euo pipefail
rm -rf .abi-probe && mkdir -p .abi-probe/src
cat > .abi-probe/mcpp.toml <<'EOF'
[package]
name = "abi"
version = "0.1.0"
EOF
cat > .abi-probe/build.mcpp <<'EOF'
import mcpp;
int main() { mcpp::include_dir("../include"); return 0; }
EOF
cat > .abi-probe/src/main.cpp <<'EOF'
#include <openkal/types.h>
#include <openkal/fs.h>
static_assert(__builtin_offsetof(kal_node_info, size) == 0);
static_assert(__builtin_offsetof(kal_node_info, modified_ns) == 8);
static_assert(sizeof(kal_node_info) == 24);
static_assert(sizeof(kal_dir) == sizeof(kal_uintptr));
static_assert(sizeof(kal_file) == sizeof(kal_uintptr));
extern "C" void _start() { for (;;) {} }
EOF
for t in riscv64-none-elf riscv32-none-elf; do
( cd .abi-probe && rm -rf target && mcpp build --target "$t" ) \
|| { echo "the frozen layout does not hold for $t"; exit 1; }
echo "$t: layout holds"
done
rm -rf .abi-probe
- name: The module form compiles
run: mcpp build
# The C form, with the environment's own headers excluded --- because the
# consumer this form exists for, a C library being ported onto openkal, is
# compiled that way. The tool needs a driver it can pass -nostdinc to; the
# toolchain that has no such spelling compiles the same declarations in
# the translation unit the conformance suite carries, which every row of
# the conformance job below builds.
- name: The C form compiles without the environment's headers
if: runner.os != 'Windows'
run: |
CC=cc bash tools/check-declarations.sh
command -v clang >/dev/null && CC=clang bash tools/check-declarations.sh || true
# ---------------------------------------------------------------------------
# The property the specification exists for.
substitution:
name: substitution holds (${{ matrix.toolchain }})
runs-on: ubuntu-24.04
timeout-minutes: 40
strategy:
fail-fast: false
matrix:
toolchain: ['gcc@16.1.0', 'llvm@22.1.8']
steps:
- uses: actions/checkout@v4
- name: Install xlings
run: |
curl -fsSL 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 mcpp
run: |
# ⚠️ A LOOP, BECAUSE ONE `xlings update` CAN RETURN A STALE INDEX
# WITHOUT SAYING SO.
#
# The index is published as an artifact behind a pointer, and that
# pointer propagates asynchronously after a version bump is merged.
# Measured on release day: an update run four minutes after the merge
# printed `index updated`, and the install then failed with
#
# package 'mcpp@<ver>' not found in the synced index
# (xim@artifact:<an older sha>, ...), synced 0 seconds ago
#
# Nothing had gone wrong. The update fetched the PREVIOUS artifact,
# and "synced 0 seconds ago" describes when it was fetched rather than
# what it contains — which is why the message reads as freshness.
#
# So this is not a retry around flakiness; it is the wait that a
# single update does not perform. A pin naming a version that was
# never published still fails, after the last attempt, and says which
# of the two situations it is.
for attempt in 1 2 3 4 5 6; do
xlings update > /dev/null 2>&1 || true
if xlings install "mcpp@$MCPP_VERSION" -y -g; then break; fi
if [ "$attempt" = 6 ]; then
echo "::error::mcpp@$MCPP_VERSION never appeared in the index (6 attempts over 5 minutes). If it was just released, the pointer has not propagated; if the pin names a version that was never published, it never will."
exit 1
fi
echo "the index has not caught up yet (attempt $attempt of 6); waiting 60s"
sleep 60
done
mcpp self config --mirror GLOBAL
# The compiler family and version for this row. mcpp keeps its toolchains
# in a sandbox of its own, so this selects rather than installs into the
# system, and `mcpp test' and `mcpp run' have no flag for it --- which is
# why it is set once here rather than passed to each command.
- name: Select the toolchain
run: |
spec='${{ matrix.toolchain }}'
case "$spec" in
msvc*) mcpp toolchain default msvc ;;
*) mcpp toolchain install "${spec%@*}" "${spec#*@}"
mcpp toolchain default "$spec" ;;
esac
mcpp toolchain list
- name: Substitution holds
working-directory: examples/substitution/app
run: |
# The property under test is that the source is invariant. The
# checksum is taken before the first build and compared after the
# second, so that a change made by either build would be detected.
before="$(sha256sum src/main.cpp | cut -d' ' -f1)"
mcpp build > /dev/null
./target/*/*/bin/app > with-fd.log 2>&1
grep -q 'the application produced this line' with-fd.log
sed -i 's|openkal-fd = { path = "../impl-fd" }|openkal-discard = { path = "../impl-discard" }|' mcpp.toml
rm -rf target
mcpp build > /dev/null
./target/*/*/bin/app > with-discard.log 2>&1
if grep -q 'the application produced this line' with-discard.log; then
echo "the discarding implementation produced output"; exit 1
fi
after="$(sha256sum src/main.cpp | cut -d' ' -f1)"
[ "$before" = "$after" ] || { echo "the source changed between builds"; exit 1; }
- name: The surface checker detects an addition
working-directory: examples/substitution/impl-fd
run: |
# The checker is only useful if it fails when it should. An
# unspecified name is introduced, the checker is required to reject
# it, and the name is then removed.
mcpp build > /dev/null
bash ../../../tools/check-surface.sh ../../../SURFACE.txt \
$(find target -name '*.o' | tr '\n' ' ')
printf 'extern "C" void kal_vendor_extension(void) {}\n' > src/extra.cpp
mcpp build > /dev/null
if bash ../../../tools/check-surface.sh ../../../SURFACE.txt \
$(find target -name '*.o' | tr '\n' ' '); then
echo "the checker accepted an unspecified name"; exit 1
fi
rm -f src/extra.cpp
# ---------------------------------------------------------------------------
# The suite, against the implementation for each system.
#
# The implementations are checked out at the branch under test where they have
# one and at their default branch otherwise, so that this job asserts what it
# is for: that the specification as written here and the implementations as
# written there agree today.
conformance:
name: conformance (${{ matrix.implementation }}, ${{ matrix.toolchain }})
runs-on: ${{ matrix.os }}
timeout-minutes: 60
strategy:
fail-fast: false
matrix:
include:
# `features' names the optional interfaces the implementation in that
# row provides, on top of `full'. It is per-row rather than global
# because clause 6.1 makes a missing optional interface not a
# deviation: a set that demanded every one of them from every
# implementation would report a link failure where the specification
# says there is nothing to report.
- { os: ubuntu-24.04, toolchain: 'gcc@16.1.0', implementation: openkal-linux, features: 'full,optional' }
- { os: ubuntu-24.04, toolchain: 'llvm@22.1.8', implementation: openkal-linux, features: 'full,optional' }
- { os: macos-14, toolchain: 'llvm@20.1.7', implementation: openkal-macos, features: 'full' }
- { os: windows-2022, toolchain: 'llvm@20.1.7', implementation: openkal-windows, features: 'full' }
- { os: windows-2022, toolchain: 'msvc@system', implementation: openkal-windows, features: 'full' }
defaults:
run:
shell: bash
steps:
- uses: actions/checkout@v4
- name: The implementation
run: |
git clone --quiet https://github.com/mcpplibs/${{ matrix.implementation }}.git .impl
branch='${{ github.head_ref || github.ref_name }}'
if git -C .impl rev-parse --verify --quiet "origin/$branch" > /dev/null; then
git -C .impl checkout --quiet "origin/$branch"
echo "the implementation is at $branch $(git -C .impl rev-parse --short HEAD)"
else
echo "the implementation has no $branch; its default branch is used" \
"($(git -C .impl rev-parse --short HEAD))"
fi
# Whether the two are describing the same version of the contract.
#
# This job asserts that the specification as written here and the
# implementation as written there agree today, and that assertion is
# only meaningful when the implementation is written against this
# version. During a release across five repositories they are out of
# step for the seconds between one merge and the next, and the
# compiler's report on that is a hundred errors about names a header
# no longer has --- which names the symptom and not the cause.
# An implementation states which openkal it is written against in one
# of two forms, and the question the check asks is different in each.
#
# openkal = "0.5.2" a released version. The question is
# whether it is this one.
# openkal = { git = …, branch = … }
# a development line. The version is
# not stated and cannot be; what makes
# the two in step is that the branch is
# this branch, and that is what to ask.
#
# The second form was not anticipated when this check was written, and
# the check then extracted nothing and reported a mismatch against the
# empty string --- which named neither the cause nor the symptom.
here="$(sed -n 's/^version[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' mcpp.toml | head -1)"
there="$(sed -n 's/^openkal[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' .impl/mcpp.toml | head -1)"
if [ -n "$there" ]; then
if [ "$here" != "$there" ]; then
echo "::error::this is openkal $here and ${{ matrix.implementation }} is written against openkal $there. Nothing is wrong with either; they are not in step. Re-run after the implementation's branch has the matching version." >&2
exit 1
fi
echo "both describe openkal $here"
else
impl_branch="$(sed -n 's/^openkal[[:space:]]*=[[:space:]]*{.*branch[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' .impl/mcpp.toml | head -1)"
if [ -z "$impl_branch" ]; then
echo "::error::${{ matrix.implementation }} states neither a version nor a branch for openkal, so there is nothing to be in step with." >&2
exit 1
fi
if [ "$impl_branch" != "$branch" ]; then
echo "::error::this is $branch and ${{ matrix.implementation }} follows $impl_branch. They are not in step." >&2
exit 1
fi
echo "both follow $branch; this is openkal $here"
fi
- name: Install xlings and mcpp (Unix)
if: runner.os != 'Windows'
run: |
curl -fsSL 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 and mcpp (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: |
# ⚠️ A LOOP, BECAUSE ONE `xlings update` CAN RETURN A STALE INDEX
# WITHOUT SAYING SO.
#
# The index is published as an artifact behind a pointer, and that
# pointer propagates asynchronously after a version bump is merged.
# Measured on release day: an update run four minutes after the merge
# printed `index updated`, and the install then failed with
#
# package 'mcpp@<ver>' not found in the synced index
# (xim@artifact:<an older sha>, ...), synced 0 seconds ago
#
# Nothing had gone wrong. The update fetched the PREVIOUS artifact,
# and "synced 0 seconds ago" describes when it was fetched rather than
# what it contains — which is why the message reads as freshness.
#
# So this is not a retry around flakiness; it is the wait that a
# single update does not perform. A pin naming a version that was
# never published still fails, after the last attempt, and says which
# of the two situations it is.
for attempt in 1 2 3 4 5 6; do
xlings update > /dev/null 2>&1 || true
if xlings install "mcpp@$MCPP_VERSION" -y -g; then break; fi
if [ "$attempt" = 6 ]; then
echo "::error::mcpp@$MCPP_VERSION never appeared in the index (6 attempts over 5 minutes). If it was just released, the pointer has not propagated; if the pin names a version that was never published, it never will."
exit 1
fi
echo "the index has not caught up yet (attempt $attempt of 6); waiting 60s"
sleep 60
done
mcpp self config --mirror GLOBAL
# The compiler family and version for this row. mcpp keeps its toolchains
# in a sandbox of its own, so this selects rather than installs into the
# system, and `mcpp test' and `mcpp run' have no flag for it --- which is
# why it is set once here rather than passed to each command.
- name: Select the toolchain
run: |
spec='${{ matrix.toolchain }}'
case "$spec" in
msvc*) mcpp toolchain default msvc ;;
*) mcpp toolchain install "${spec%@*}" "${spec#*@}"
mcpp toolchain default "$spec" ;;
esac
mcpp toolchain list
# Every interface and every kind of examination. The exit status is the
# verdict: 0 when every observation held, 1 when one did not, and 2 when
# nothing was observed --- the last being the outcome a run that selected
# no interface would otherwise pass silently.
- name: Every interface, every kind of examination
run: |
bash tools/run-conformance.sh '${{ matrix.implementation }}' .impl '${{ matrix.features }}'
# The suite is composable because openkal is: an implementation provides
# an interface in whole or not at all, and a suite that examined all eight
# unconditionally would fail to link against a conforming implementation
# of three. Selecting three is therefore asserted to produce a report
# rather than a link failure.
- name: A selection of three interfaces is examined, not refused
run: |
rm -rf conformance/target
bash tools/run-conformance.sh '${{ matrix.implementation }}' .impl core,fs,task \
| tee selected.log
# A report was produced, and nothing in it failed.
grep -qE 'observations: [0-9]+ held, 0 did not hold' selected.log
# An interface that was not selected is reported as not examined and
# carries the reason, rather than being absent --- a report that
# omitted it could not be distinguished from a report on an
# implementation that provides it.
grep -q 'openkal.process --- the interface was not selected' selected.log
# And an interface that was selected was examined.
grep -qE 'held +\[behaviour\].*' selected.log