tutorial-rc0

Download

Pick the binary for your operating system:

• macOS Apple Silicon (M Series): spectecx-darwin-arm64
• Linux x86_64: spectecx-linux-x64
• macOS Intel: build from source per the README, or run the
  Linux binary in a VM (UTM, Lima).
• Windows: use WSL2 + the Linux binary.

Tutorial materials

spectecx-tutorial.tar.gz -- participant materials for the MechSpec
tutorial (spec skeleton, tests, README, prose document).

Install (Unix)

curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc0/spectecx-<your-target>
chmod +x spectecx
./spectecx --help

macOS Gatekeeper

If the binary was downloaded via a browser, macOS will quarantine
it. Either right-click and choose Open the first time, or strip
the attribute:

xattr -d com.apple.quarantine spectecx

What's Changed

• refactor: Better APIs for builtins, value construction and state manipulation by @KunJeong in #1
• feat/refactor: Add SL interpreter and test scripts, modularize exceptions by @KunJeong in #2
• refactor: Organize modules to simplify dependencies by @KunJeong in #3
• fix(cache): Structural hash to match compare by @KunJeong in #7
• feat(interp): Hook system and hook-based tracing/profiling by @KunJeong in #8
• refactor(cache): Wrapper for cache usage, prevent HOF caching by @KunJeong in #10
• refactor(test): move test data under dune project directory by @KunJeong in #28
• Sync P4-SpecTec interpreter and AST changes by @KunJeong in #29
• Simplify elaboration using IL types by @KunJeong in #30
• Refactor mixfix representation and make atoms lossless by @KunJeong in #31
• Refactor instrumentation architecture and make lifecycle exception-safe by @KunJeong in #32
• Refactor CLI into per-target modules by @KunJeong in #34
• Sync new P4 concrete spec by @KunJeong in #35
• Sync P4 SL fixes by @KunJeong in #36
• Intermediate trace levels and a derivation-tree handler by @KunJeong in #37
• Sync premise coverage report improvements by @KunJeong in #38
• Structured diagnostics for elaboration by @KunJeong in #43
• Add CI and supporting tooling by @KunJeong in #44
• fix(ci): adjust workflow to setup-ocaml@v3 by @KunJeong in #45
• Sync mixfix API and atom representation by @KunJeong in #46
• refactor(il): convert positional fields to named records in rules, declarations, and types by @KunJeong in #47
• Refactor quickcheck to fit the target architecture by @KunJeong in #49
• Rename SpecTec-Core to SpecTecX by @KunJeong in #50
• feat(ci): add release workflow for prebuilt spectecx binaries by @KunJeong in #51
• Measure coverage during quickcheck runs by @jihongmin63 in #54
• Polish diagnostic rendering by @KunJeong in #55
• Prose rendering pipeline by @KunJeong in #57
• Refactor IL relation notation to inline input/output direction by @KunJeong in #58
• Structured diagnostics for interpreter failtraces by @KunJeong in #59
• Refine the impty spec and tests by @KunJeong in #60

New Contributors

• @jihongmin63 made their first contribution in #54

Full Changelog: https://github.com/kaist-plrg/spectecx/commits/tutorial-rc0