tutorial-rc3
SpecTecX hands-on session
Tool and materials for the SpecTecX hands-on: the spectecx binary and a small typed imperative language ("Typed Imp") to read, run, and extend.
1. Get the materials
Download spectecx-tutorial.tar.gz (spec skeleton, tests, README, and prose document) and unpack it:
curl -L -O https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc3/spectecx-tutorial.tar.gz
tar -xzf spectecx-tutorial.tar.gz && cd spectecx-tutorialThe unpacked README.md drives the session; the steps below just put the spectecx binary alongside it first.
2. Install the tool
Pick the binary for your platform:
- macOS Apple Silicon (M series):
spectecx-darwin-arm64 - Linux x86_64:
spectecx-linux-x64 - macOS Intel: no native binary; use Docker or build from source (below).
- Windows: use WSL2 with the Linux binary, or Docker.
Download it into the unpacked bundle directory as spectecx, make it executable, and check it runs:
curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc3/spectecx-<your-platform>
chmod +x spectecx
./spectecx helpDownloaded with the browser instead? Rename the file to spectecx (mv spectecx-<your-platform> spectecx) before chmod. On macOS, clear the quarantine flag with xattr -d com.apple.quarantine spectecx.
Every command runs the binary as ./spectecx, so there is no PATH setup to do.
For the optional prose build (make doc-html), also install asciidoctor: gem install asciidoctor asciidoctor-pdf. The Docker image below already bundles it.
Alternatives
Docker -- a prebuilt, self-contained image (tool, materials, an editor, and asciidoctor), for anyone without a native binary. No download needed -- pull and run:
docker pull kaist-plrg/spectecx:tutorial
docker run -it kaist-plrg/spectecx:tutorialThis opens a shell in the bundle; from there step 3 and the whole README run exactly as written (./spectecx ..., make test, ...).
Build from source -- opam, OCaml >= 5.1, GMP headers:
git clone https://github.com/kaist-plrg/spectecx.git && cd spectecx
opam switch create spectecx 5.1.0
opam install -y --switch=spectecx --deps-only ./spectec
make exe # produces ./spectecx3. Start the session
From the unpacked bundle, follow README.md from the top:
./spectecx impty eval -p tests/base/hello.impFull Changelog: tutorial-rc2...tutorial-rc3