tutorial-rc2

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:

tar -xzf spectecx-tutorial.tar.gz && cd spectecx-tutorial

The 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-rc2/spectecx-<your-platform>
chmod +x spectecx
./spectecx --help

Downloaded 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 splice-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:tutorial

This 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 ./spectecx

3. Start the session

From the unpacked bundle, follow README.md from the top:

./spectecx impty eval -p tests/base/hello.imp

What's Changed

• Add premise level to derivation-tree handler by @KunJeong in #69
• Fix the batch command by @KunJeong in #71

Full Changelog: tutorial-rc1...tutorial-rc2