Long live OpenSysML #11
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: PR | |
| # Pull requests only: pushes and tags are covered by the CircleCI config, and | |
| # this workflow deliberately mirrors only its build-test workflow, not release. | |
| on: | |
| pull_request: | |
| permissions: | |
| contents: read | |
| env: | |
| # The OMG training corpus is not vendored. Requiring it here turns "corpus | |
| # absent" into a test failure instead of a skip, so the gate cannot pass green | |
| # without actually running (see internal/core/model/training_examples_test.go). | |
| OPENSYSML_REQUIRE_TRAINING_CORPUS: "1" | |
| # z3 is installed below, so "no solver, therefore skip" would exercise nothing: | |
| # this turns an absent solver into a failure (see internal/core/solve). | |
| OPENSYSML_REQUIRE_SMT: "1" | |
| jobs: | |
| build-and-test: | |
| name: Build and test | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-go@v5 | |
| with: | |
| go-version-file: go.mod | |
| cache: true | |
| - name: Download modules | |
| run: go mod download | |
| # The solver is an external process, never linked in: the solver-dependent | |
| # tests need one on PATH to run rather than skip. | |
| - name: Install z3 | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y z3 | |
| z3 --version | |
| # The second verified backend, for the portability gate below: cvc5 has no | |
| # apt package, so the official static release is what CI runs, pinned by | |
| # digest so a substituted asset is not run. | |
| - name: Install cvc5 | |
| run: | | |
| curl -fsSL -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 | |
| # Keyed on the download script, so a change to the pinned pilot tag or the | |
| # layout invalidates the cache. A restored cache is still verified below. | |
| - name: Cache the OMG training corpus | |
| uses: actions/cache@v4 | |
| with: | |
| path: examples/sysml-v2-training | |
| key: training-corpus-${{ hashFiles('scripts/download-training-examples.sh') }} | |
| - name: Download the OMG training corpus | |
| run: ./scripts/download-training-examples.sh | |
| - name: Verify the corpus is present | |
| run: | | |
| count=$(find examples/sysml-v2-training -name '*.sysml' | wc -l) | |
| echo "training corpus: $count .sysml files" | |
| if [ "$count" -eq 0 ]; then | |
| echo "error: the training corpus is empty; the corpus gate would not run" >&2 | |
| exit 1 | |
| fi | |
| - name: Check gofmt | |
| run: | | |
| unformatted=$(gofmt -l .) | |
| if [ -n "$unformatted" ]; then | |
| echo "The following files are not gofmt'd:" | |
| echo "$unformatted" | |
| exit 1 | |
| fi | |
| - name: Run go vet | |
| run: go vet ./... | |
| - name: Run static analysis (staticcheck + gosec) | |
| run: make lint | |
| - name: Run tests | |
| run: go test -v -race -coverprofile=coverage.txt -covermode=atomic ./... | |
| # Re-run the corpus gate on its own so its verdict is legible in the log | |
| # and a skip is impossible to miss. | |
| - name: Corpus gate | |
| run: | | |
| set -o pipefail | |
| go test -count=1 -v ./internal/core/model -run 'TestTrainingExamples' | tee corpus-gate.log | |
| grep -E 'training files clean' corpus-gate.log | |
| if grep -qE '^\s*--- SKIP' corpus-gate.log; then | |
| echo "error: the corpus gate skipped" >&2 | |
| exit 1 | |
| fi | |
| # Re-run the solver gate on its own, as the corpus gate is, so a skip | |
| # cannot hide behind a green suite. | |
| - name: Solver gate | |
| run: | | |
| set -o pipefail | |
| go test -count=1 -v ./internal/core/solve ./internal/repl -run 'TestSolver|TestDiscovery|TestSolved|TestDivisor|TestCheck|TestSolve|TestConfigure|TestSynthesis|TestPinned|TestFixed|TestOptimize|TestOptimum' | tee solver-gate.log | |
| if grep -qE '^\s*--- SKIP' solver-gate.log; then | |
| echo "error: a solver-dependent test skipped" >&2 | |
| exit 1 | |
| fi | |
| # The differential gate compares the solver against the normative | |
| # evaluator; its summary counts make coverage drift reviewable in the log. | |
| - name: Differential agreement gate | |
| run: | | |
| set -o pipefail | |
| go test -count=1 -v ./internal/core/solve -run TestDifferential | tee differential-gate.log | |
| grep -E 'differential gate .*: .* elements:' differential-gate.log | |
| if grep -qE '^\s*--- SKIP' differential-gate.log; then | |
| echo "error: a differential gate skipped" >&2 | |
| exit 1 | |
| fi | |
| # Portability: the same subset run against both verified backends, so a | |
| # feature one of them refuses is reported rather than discovered by a user. | |
| # OPENSYSML_REQUIRE_SMT makes an absent solver a failure, not a skip. | |
| - name: Portability gate | |
| run: | | |
| set -o pipefail | |
| for solver in z3 cvc5; do | |
| OPENSYSML_SMT="$solver" go test -count=1 -v ./internal/core/solve \ | |
| -run 'TestPortability' | tee "portability-$solver.log" | |
| grep -E "portability of $solver" "portability-$solver.log" | |
| if grep -qE '^\s*--- SKIP' "portability-$solver.log"; then | |
| echo "error: the portability gate skipped for $solver" >&2 | |
| exit 1 | |
| fi | |
| done | |
| # The solver gate again against the second backend, not only the | |
| # portability subset: what z3 answers, cvc5 must answer too. | |
| - name: Second backend gate | |
| run: | | |
| set -o pipefail | |
| OPENSYSML_SMT=cvc5 go test -count=1 -v ./internal/core/solve ./internal/repl \ | |
| -run 'TestSolver|TestDiscovery|TestSolved|TestDivisor|TestCheck|TestSolve|TestConfigure|TestSynthesis|TestPinned|TestFixed|TestExplain|TestCore' \ | |
| | tee cvc5-gate.log | |
| if grep -qE '^\s*--- SKIP' cvc5-gate.log; then | |
| echo "error: a solver-dependent test skipped under cvc5" >&2 | |
| exit 1 | |
| fi | |
| # The other half of the contract: with no solver to be found, every | |
| # solver-dependent test must skip with a reason and the absent-solver paths | |
| # must still report one. OPENSYSML_SMT names an executable that does not | |
| # exist, which is discovery's absent case, and the requirement flag is | |
| # dropped so a skip is the expected outcome here. | |
| - name: Solver-absent gate | |
| run: | | |
| set -o pipefail | |
| env -u OPENSYSML_REQUIRE_SMT OPENSYSML_SMT=/nonexistent/no-such-solver \ | |
| go test -count=1 -v ./internal/core/solve ./internal/repl | tee no-solver-gate.log | |
| for name in TestCheckReportsAnAbsentSolver TestExplainReportsAnAbsentSolver \ | |
| TestSolveReportsAnAbsentSolver TestConfigureReportsAnAbsentSolver \ | |
| TestOptimizeReportsAnAbsentSolver; do | |
| grep -qE "^\s*--- PASS: $name" no-solver-gate.log || { | |
| echo "error: $name did not run without a solver" >&2 | |
| exit 1 | |
| } | |
| done | |
| - name: Build binaries | |
| run: | | |
| make build \ | |
| VERSION="pr-${{ github.event.pull_request.number }}" \ | |
| COMMIT="$(git rev-parse --short HEAD)" \ | |
| BUILD_TIME="$(date -u '+%Y-%m-%d_%H:%M:%S')" \ | |
| GO_VERSION="$(go version | awk '{print $3}')" | |
| - name: Verify binaries | |
| run: | | |
| ./bin/sysml --version | |
| ./bin/sysml-lsp --version | |
| ls -lh bin/ | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: binaries | |
| path: bin/ | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: coverage | |
| path: coverage.txt | |
| vscode-extension: | |
| name: VS Code extension | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/setup-node@v4 | |
| with: | |
| node-version: '22' | |
| cache: npm | |
| cache-dependency-path: editors/vscode/package-lock.json | |
| # Type-check, bundle and package. The generated TextMate grammars are | |
| # gated by go test ./editors/... in the job above. | |
| - name: Package the extension | |
| working-directory: editors/vscode | |
| run: | | |
| npm ci | |
| npm run package | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: vscode-extension | |
| path: editors/vscode/opensysml-sysml.vsix | |
| python-test: | |
| name: Python client tests | |
| needs: build-and-test | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: actions/download-artifact@v4 | |
| with: | |
| name: binaries | |
| path: bin | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Install sysml-grpc binary | |
| run: | | |
| mkdir -p ~/.opensysml/bin | |
| cp bin/sysml-grpc ~/.opensysml/bin/ | |
| chmod +x ~/.opensysml/bin/sysml-grpc | |
| - name: Install Python package | |
| working-directory: python | |
| run: | | |
| pip install -e . | |
| pip install pytest pytest-mock | |
| # The integration tests need a service to talk to; without one they skip, | |
| # which exercises nothing, so one runs here for the rest of the job. | |
| - name: Start sysml-grpc service | |
| run: | | |
| chmod +x ~/.opensysml/bin/sysml-grpc | |
| nohup ~/.opensysml/bin/sysml-grpc -port 50051 > /tmp/sysml-grpc.log 2>&1 & | |
| python3 - <<'PY' | |
| import socket, sys, time | |
| for _ in range(30): | |
| with socket.socket() as probe: | |
| probe.settimeout(1) | |
| if probe.connect_ex(("localhost", 50051)) == 0: | |
| print("sysml-grpc is listening on 50051") | |
| sys.exit(0) | |
| time.sleep(1) | |
| sys.exit("sysml-grpc never listened on 50051") | |
| PY | |
| # OPENSYSML_REQUIRE_SERVICE turns "no service, so skip" into a failure: a | |
| # service is provided here, so its absence is the bug, not a pass. | |
| - name: Run Python tests | |
| working-directory: python | |
| env: | |
| OPENSYSML_REQUIRE_SERVICE: 1 | |
| run: pytest tests/ -v | |
| - name: Verify import | |
| run: python3 -c "import opensysml; print(f'opensysml {opensysml.__version__} imported successfully')" |