chore(release): bring develop's execution, migration, extension-library and documentation changes into 0.10.0

.agents/skills/testing-sysml-repl/SKILL.md

@@ -1151,6 +1151,27 @@ changes:
   `unresolved reference: n`; the CLI has **no** flag for action inputs, so exercise `in`/`out`
   parameters by having a caller action invoke `action call = Callee(a = 3, b = 4);`.
 
+## Action fan-out CLI checks
+
+- Use explicit succession syntax in minimal repros: `succession a then done;`
+  or `first a then done;`. A bare `a then done;` inside an action body can be
+  rejected as `expected a body member` before execution; do not mistake that
+  diagnostic for a runtime fan-out refusal.
+- The default scheduler is `reverse`, not `declared`. Compare explicit
+  `-schedule declared` with `-schedule reverse`; a no-flag run normally agrees
+  with reverse.
+- `-engine smt -action <name>` asks whether execution holds, not for the table
+  of final values. Use `-engine smt -action <name> -check-diverge <feature>` to
+  request two witnessed final values. `-engine check` and `-schedule explore`
+  expose outcomes directly. SMT may explicitly refuse an implicit join at a
+  plain node, whereas the runtime supports it; use an explicit join for a
+  cross-engine scheduling comparison.
+- Bound adversarial loops with `OPENSYSML_MAX_ACTION_STEPS=200`, and wrap the
+  command with `timeout 30`. Assert the step-limit diagnostic and exit 2,
+  not watchdog exit 124. Report CLI diagnostics separately from Go error
+  identity: the CLI does not expose `errors.Is`, and static merge/join
+  validation may prevent reaching the runtime guard.
+
 ## Control flow inside an action node body
 
 `while`, `loop … until` (braced and unbraced), `for … in` and `if`/`else` execute inside an
@@ -4139,10 +4160,10 @@ Traps and recipes:
 - Error wordings to assert: non-Boolean guard →
   `error: execution failed: type mismatch: node s1: guard must evaluate to boolean, got constant`;
   unresolvable name in a guard → `error: execution failed: eval guard of node s1: unresolved
-  reference: nosuch`. Two guards out of one action node that both hold →
-  `error: execution failed: more than one succession is enabled: action node check has multiple
-  successors` (wraps the `ErrAmbiguousSuccession` sentinel; the run stops with the token still on the
-  node and neither branch's attribute written — assert that with `%tokens`, not just the message).
+  reference: nosuch`. Two guards out of one ordinary action node that both hold are no error: each
+  succession is its own `HappensBefore` link, so the token splits as a fork's does and both branch
+  attributes are written (assert both in `Results:`). Only a `decide` node picks one of several
+  holding guards; a `join` or `merge` with two outgoing successions is still refused.
 - Places a guard could still be silently ignored, all worth a one-liner fixture: succession out of a
   real initial node (`then start s1 if …;`), out of a `merge`, out of a `join` (must not deadlock —
   the branch tokens are consumed either way), and one whose target is `done`.

.circleci/config.yml

@@ -17,7 +17,7 @@ executors:
       # It carries Node LTS, 24 or later, which the gate needs.
       - image: cimg/go:1.25-node
     resource_class: medium
-  
+
   python-executor:
     docker:
       - image: cimg/python:3.11
@@ -1047,7 +1047,7 @@ jobs:
     executor: python-executor
     steps:
       - checkout
-      
+
       - attach_workspace:
           at: .
 
@@ -1070,7 +1070,7 @@ jobs:
             mkdir -p ~/.opensysml/bin
             cp bin/sysml-grpc ~/.opensysml/bin/
             chmod +x ~/.opensysml/bin/sysml-grpc
-      
+
       - run:
           name: Install Python client
           command: |
@@ -1083,7 +1083,7 @@ jobs:
             # its wheels with python -m build.
             pip install --only-binary :all: jupyter_client==8.10.0 build==1.6.1
             make jupyter-kernel-install
-      
+
       # The integration tests connect to a service on the standard port with
       # auto_start=False, which is the explicit opt-in to one the client does not
       # manage; without it they skip, exercising nothing, so one runs here for
@@ -2251,66 +2251,66 @@ jobs:
       - go/load-cache
       - go/mod-download
       - go/save-cache
-      
+
       - run:
           name: Build release binaries
           command: |
             VERSION=${CIRCLE_TAG}
             COMMIT=${CIRCLE_SHA1}
             BUILD_TIME=$(date -u '+%Y-%m-%d_%H:%M:%S')
             GO_VERSION=$(go version | awk '{print $3}')
-            
+
             # Build for multiple platforms using make
             mkdir -p dist
-            
+
             GOOS=linux GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml dist/sysml-linux-amd64
-            
+
             GOOS=linux GOARCH=arm64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml dist/sysml-linux-arm64
-            
+
             GOOS=darwin GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml dist/sysml-darwin-amd64
-            
+
             GOOS=darwin GOARCH=arm64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml dist/sysml-darwin-arm64
-            
+
             GOOS=windows GOARCH=amd64 make build-sysml VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml dist/sysml-windows-amd64.exe
-            
+
             GOOS=linux GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-lsp dist/sysml-lsp-linux-amd64
-            
+
             GOOS=linux GOARCH=arm64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-lsp dist/sysml-lsp-linux-arm64
-            
+
             GOOS=darwin GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-lsp dist/sysml-lsp-darwin-amd64
-            
+
             GOOS=darwin GOARCH=arm64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-lsp dist/sysml-lsp-darwin-arm64
-            
+
             GOOS=windows GOARCH=amd64 make build-lsp VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-lsp dist/sysml-lsp-windows-amd64.exe
-            
+
             # The gRPC service backs the Python client, which downloads one
             # file per platform and verifies it against a .sha256 sidecar, so
             # these are published raw rather than archived. They are built into
             # a subdirectory to keep them out of the archive globs below.
             mkdir -p dist/grpc
-            
+
             GOOS=linux GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-grpc dist/grpc/sysml-grpc-linux-amd64
-            
+
             GOOS=linux GOARCH=arm64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-grpc dist/grpc/sysml-grpc-linux-arm64
-            
+
             GOOS=darwin GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-grpc dist/grpc/sysml-grpc-darwin-amd64
-            
+
             GOOS=darwin GOARCH=arm64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-grpc dist/grpc/sysml-grpc-darwin-arm64
-            
+
             GOOS=windows GOARCH=amd64 make build-grpc VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/sysml-grpc dist/grpc/sysml-grpc-windows-amd64.exe
 
@@ -2345,7 +2345,7 @@ jobs:
             mkdir -p dist/wasm
             make build-release-wasm VERSION="$VERSION" COMMIT="$COMMIT" BUILD_TIME="$BUILD_TIME" GO_VERSION="$GO_VERSION"
             mv bin/wasm/release/sysml-wasm.wasm bin/wasm/release/wasm_exec.js dist/wasm/
-            
+
             # Create tarballs
             cd dist
             for binary in sysml-*; do
@@ -2355,7 +2355,7 @@ jobs:
                 tar czf "${binary}.tar.gz" "$binary"
               fi
             done
-            
+
             # Bundle archives: both binaries under their plain names
             # (sysml, sysml-lsp), which is the layout a Homebrew formula or a
             # PATH install expects, with their manual pages beside them under
@@ -2376,7 +2376,7 @@ jobs:
             cp sysml-lsp-windows-amd64.exe stage/windows-amd64/sysml-lsp.exe
             (cd stage/windows-amd64 && zip -q ../../opensysml-windows-amd64.zip sysml.exe sysml-lsp.exe)
             rm -rf stage
-            
+
             # The checksum manifest and the per-file sidecars are
             # build-release's, once the Python distributions exist to list.
             ls -l . grpc jupyter
@@ -2457,17 +2457,17 @@ jobs:
           name: Assemble the release and write its checksum manifest
           command: |
             cd dist
-            
+
             # The opensysml wheel and sdist, released with the binaries they drive,
             # and the jupyter-opensysml-kernel platform wheels and sdist likewise.
             cp ../client/python/dist/opensysml-*.whl ../client/python/dist/opensysml-*.tar.gz .
             cp ../client/jupyter-kernel/dist/jupyter_opensysml_kernel-*.whl \
                ../client/jupyter-kernel/dist/jupyter_opensysml_kernel-*.tar.gz .
-            
+
             # Checksums over every published archive, so a Homebrew formula
             # (or a careful user) can verify a download.
             sha256sum ./*.tar.gz ./*.zip ./*.whl | sed 's|\./||' > SHA256SUMS.txt
-            
+
             # Same for the raw gRPC binaries, through the per-file sidecars
             # written beside them when they were built, the only checksum
             # opensysml reads: checked against the bytes here, then folded in.
@@ -2623,7 +2623,7 @@ jobs:
                        <(jq -r '.dsseEnvelope.payload' provenance.intoto.json.bundle | base64 -d \
                          | jq -r '.subject[] | "\(.name) \(.digest.sha256)"' | sort)
 
-      
+
       - rehearsal-skip:
           what: "cosign keyless signing and attestation (they write to the public Rekor log)"
       - run:
@@ -3311,7 +3311,7 @@ jobs:
             - rehearsal-tag
       - attach_workspace:
           at: .
-      
+
       - unless:
           condition: << pipeline.parameters.release_rehearsal >>
           steps:
@@ -3325,7 +3325,7 @@ jobs:
                   fi
                   echo "Publishing release $VERSION"
                   ls -la dist/
-            
+
                   # Move only tarballs to a release directory
                   mkdir -p dist/release
                   mv dist/*.tar.gz dist/*.zip dist/release/ 2>/dev/null || true
@@ -3343,14 +3343,14 @@ jobs:
                   mv dist/provenance.intoto.json dist/provenance.intoto.json.bundle dist/release/
                   echo "Release artifacts:"
                   ls -la dist/release/
-            
+
                   # Try different token variable names
                   TOKEN="${GITHUB_TOKEN:-${GH_TOKEN:-${CIRCLE_TOKEN}}}"
                   if [ -z "$TOKEN" ]; then
                     echo "Error: No GitHub token found. Tried GITHUB_TOKEN, GH_TOKEN, CIRCLE_TOKEN"
                     exit 1
                   fi
-            
+
                   # '-replace' reuses an existing release and only re-uploads assets of
                   # the same name, so hand-written notes, title and prerelease/latest
                   # flags survive a re-run. Never '-delete': that is an alias of

.github/workflows/extension-libraries-upstream.yml

@@ -0,0 +1,97 @@
+name: Extension libraries upstream
+
+# Advisory: does the extension-libraries upstream's ref still run under
+# OpenSysML? It syncs the ref into the vendored directory and runs the whole
+# suite. It is scheduled rather than a required check: it downloads from
+# upstream and takes minutes, so a failure here surfaces what broke without
+# blocking pull requests. It never pushes and never opens issues.
+on:
+  schedule:
+    - cron: '41 4 * * *'
+  workflow_dispatch:
+    inputs:
+      ref:
+        description: 'Extension-libraries ref to sync (branch or tag)'
+        required: true
+        default: main
+
+permissions:
+  contents: read
+
+jobs:
+  upstream:
+    name: OpenSysML against upstream extension libraries
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    env:
+      REF: ${{ inputs.ref || 'main' }}
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v4
+
+      - name: Set up Go
+        uses: actions/setup-go@v5
+        with:
+          go-version-file: go.mod
+          cache: true
+
+      - name: Install Z3
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y z3
+          z3 --version
+
+      - name: Install cvc5
+        run: |
+          curl -fsSL --proto '=https' --proto-redir '=https' -o /tmp/cvc5.zip \
+            https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.4/cvc5-Linux-x86_64-static.zip
+          echo "dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6  /tmp/cvc5.zip" | sha256sum --check --strict
+          unzip -p /tmp/cvc5.zip '*/bin/cvc5' > /tmp/cvc5-bin
+          sudo install -m 0755 /tmp/cvc5-bin /usr/local/bin/cvc5
+          cvc5 --version | head -1
+
+      - name: Sync the upstream ref
+        id: sync
+        run: |
+          out="$(scripts/sync-extension-libraries.sh --ref "$REF" | tee /dev/stderr)"
+          sha="$(sed -n 's/^Resolved .* to \([0-9a-f]*\)$/\1/p' <<<"$out" | tail -1)"
+          {
+            echo "### Synced upstream \`$REF\` at \`$sha\`"
+            echo '```'
+            git status --porcelain -- "internal/workspace/libs/stdlib/OpenSysML Libraries/"
+            echo '```'
+          } >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Check the library snapshot
+        id: snapshot
+        run: |
+          if make stdlib-snapshot-check; then
+            echo "Snapshot unchanged." >> "$GITHUB_STEP_SUMMARY"
+          else
+            echo "Snapshot regenerated for the synced libraries." >> "$GITHUB_STEP_SUMMARY"
+            make stdlib-snapshot
+          fi
+
+      - name: Run the test suite
+        id: tests
+        run: |
+          go test ./...
+          go test -C tools ./...
+
+      - name: Report the verdict
+        if: always()
+        run: |
+          if [ "${{ steps.tests.outcome }}" = "success" ]; then
+            echo "Upstream \`$REF\` runs clean under OpenSysML." >> "$GITHUB_STEP_SUMMARY"
+          else
+            {
+              echo "**Upstream \`$REF\` breaks OpenSysML.**"
+              echo ""
+              echo "| step | outcome |"
+              echo "| --- | --- |"
+              echo "| sync | ${{ steps.sync.outcome }} |"
+              echo "| snapshot | ${{ steps.snapshot.outcome }} |"
+              echo "| tests | ${{ steps.tests.outcome }} |"
+            } >> "$GITHUB_STEP_SUMMARY"
+          fi
+          git checkout -- "internal/workspace/libs/stdlib/OpenSysML Libraries/" 2>/dev/null || true

.github/workflows/pr.yml

@@ -73,6 +73,12 @@ jobs:
           BASE_REF: ${{ github.base_ref }}
         run: scripts/ci-changed-areas.sh "origin/$BASE_REF" HEAD | tee -a "$GITHUB_OUTPUT"
 
+      # The vendored copy is checked in this job, not static-and-integrity: the
+      # changed-areas filter may skip that job for a non-Go change, but drift
+      # between the vendored libraries and their pin must always fail.
+      - name: Check the vendored extension libraries against their pin
+        run: make extension-libraries-check
+
   race-tests:
     name: Go race tests (${{ matrix.shard }})
     needs: changes