tutorial-rc6

SpecTecX hands-on session

Everything you need for the SpecTecX hands-on. You'll read, run, and extend Typed Imp (a small typed imperative language) using the spectecx tool.

Setup is three steps: (1) download the materials, (2) install the spectecx binary, (3) follow the bundled README.md.

Pick your setup

Decide based on what your machine already has:

Path	Works on	What you need	Effort
Prebuilt binary (recommended)	macOS Apple Silicon, Linux x86_64	a code editor	~2 min
Docker image	any platform	Docker	3.16GB pull
Build from source	any platform	opam, OCaml >= 5.1, GMP headers	~10 min

If a native binary covers your platform, take the prebuilt path. On macOS Intel or Windows, choose Docker (easiest) or build from source.

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-rc6/spectecx-tutorial.tar.gz
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. (Using Docker? Skip ahead, the image already contains the materials.)

2. Install the tool

Two prebuilt binaries are attached. Pick yours and download it into the unpacked bundle directory as spectecx:

macOS (Apple Silicon / M-series):

curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc6/spectecx-darwin-arm64

Linux (x86_64):

curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc6/spectecx-linux-x64

macOS Intel or Windows: no native binary, use Docker or build from source (below).

Then make it executable and check it runs:

chmod +x spectecx
./spectecx help

Downloaded with the browser instead? The file keeps its asset name, so rename it to spectecx (e.g. mv spectecx-darwin-arm64 spectecx) before chmod. On macOS, clear the quarantine flag with xattr -d com.apple.quarantine spectecx.

Every command runs the binary as ./spectecx.

Alternatives

Docker: a prebuilt, self-contained image (tool, materials, vim, and asciidoctor), for anyone without a native binary. Pull and run:

docker pull kaistplrg/spectecx:tutorial
docker run -it kaistplrg/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 -b tutorial-pldi26 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 in the repo root

Then copy the binary into your unpacked bundle, so ./spectecx works there:

cp spectecx /path/to/spectecx-tutorial/spectecx

3. Editor syntax highlighting (recommended)

Highlighters for four editors come with this release. The VS Code, Emacs, and Vim highlighters already sit in your unpacked bundle. All three are also attached to this release page as standalone assets (spectecx.vsix, spectec-ts-mode.el, spectec-vim.tar.gz) if you'd rather grab them directly; Neovim builds from its own grammar repo.

VS Code: install the bundled spectecx.vsix (also on this release page):

code --install-extension spectecx.vsix

If code is not on your PATH, run "Shell Command: Install 'code' command in PATH" from the command palette first. For VSCodium, use codium --install-extension spectecx.vsix.

Neovim (0.9+): self-contained tree-sitter plugin (needs a C compiler; no nvim-treesitter required). With lazy.nvim:

{ "KunJeong/tree-sitter-spectec", build = "make parser" }

See the grammar repo for other plugin managers.

Vim, or Neovim before 0.9: a lightweight regex highlighter without build or dependencies. It ships in the bundle; run it on a spec directly:

vim --cmd 'set rtp^=editors/vim' impty.spectec

Or install it permanently: download spectec-vim.tar.gz and unpack it into your Vim runtime (~/.config/nvim for Neovim):

mkdir -p ~/.vim && tar -xzf spectec-vim.tar.gz -C ~/.vim

Emacs: (29+ with tree-sitter, plus a C compiler) spectec-ts-mode.el ships in the bundle (and on this release page). Run it on a spec; it offers to build the grammar on first use:

emacs -l spectec-ts-mode.el impty.spectec

To make it permanent, load it from your init instead, so every .spectec file opens highlighted:

(add-to-list 'load-path "/directory/holding/spectec-ts-mode.el")
(require 'spectec-ts-mode)

4. Prose document (optional)

make doc splices the spec into AsciiDoc at documentation/impty.adoc with no extra tools -- read it in any editor, or preview it with the VS Code / JetBrains AsciiDoc extension. For HTML or PDF (make doc-html / make doc-pdf), install asciidoctor:

gem install asciidoctor asciidoctor-pdf

It is already present in the Docker image.

5. Verification

From the unpacked bundle, run:

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

The hands-on exercise will proceed after the demo.

Full Changelog: tutorial-rc5...tutorial-rc6

tutorial-rc5

SpecTecX hands-on session

Everything you need for the SpecTecX hands-on. You'll read, run, and extend Typed Imp (a small typed imperative language) using the spectecx tool.

Setup is three steps: (1) download the materials, (2) install the spectecx binary, (3) follow the bundled README.md.

Pick your setup

Decide based on what your machine already has:

Path	Works on	What you need	Effort
Prebuilt binary (recommended)	macOS Apple Silicon, Linux x86_64	a code editor	~2 min
Docker image	any platform	Docker	3.16GB pull
Build from source	any platform	opam, OCaml >= 5.1, GMP headers	~10 min

If a native binary covers your platform, take the prebuilt path. On macOS Intel or Windows, choose Docker (easiest) or build from source.

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-rc5/spectecx-tutorial.tar.gz
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. (Using Docker? Skip ahead, the image already contains the materials.)

2. Install the tool

Two prebuilt binaries are attached. Pick yours and download it into the unpacked bundle directory as spectecx:

macOS (Apple Silicon / M-series):

curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc5/spectecx-darwin-arm64

Linux (x86_64):

curl -L -o spectecx https://github.com/kaist-plrg/spectecx/releases/download/tutorial-rc5/spectecx-linux-x64

macOS Intel or Windows: no native binary -- use Docker or build from source (below).

Then make it executable and check it runs:

chmod +x spectecx
./spectecx help

Downloaded with the browser instead? The file keeps its asset name, so rename it to spectecx (e.g. mv spectecx-darwin-arm64 spectecx) before chmod. On macOS, clear the quarantine flag with xattr -d com.apple.quarantine spectecx.

Every command runs the binary as ./spectecx.

Alternatives

Docker: a prebuilt, self-contained image (tool, materials, vim, and asciidoctor), for anyone without a native binary. Pull and run:

docker pull kaistplrg/spectecx:tutorial
docker run -it kaistplrg/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 -b tutorial-pldi26 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 in the repo root

Then copy the binary into your unpacked bundle, so ./spectecx works there:

cp spectecx /path/to/spectecx-tutorial/spectecx

3. Editor syntax highlighting (recommended)

Highlighters for four editors come with this release. The VS Code, Emacs, and Vim highlighters already sit in your unpacked bundle. All three are also attached to this release page as standalone assets (spectecx.vsix, spectec-ts-mode.el, spectec-vim.tar.gz) if you'd rather grab them directly; Neovim builds from its own grammar repo.

VS Code: install the bundled spectecx.vsix (also on this release page):

code --install-extension spectecx.vsix

If code is not on your PATH, run "Shell Command: Install 'code' command in PATH" from the command palette first. For VSCodium, use codium --install-extension spectecx.vsix.

Neovim (0.9+): self-contained tree-sitter plugin (needs a C compiler; no nvim-treesitter required). With lazy.nvim:

{ "KunJeong/tree-sitter-spectec", build = "make parser" }

See the grammar repo for other plugin managers.

Vim, or Neovim before 0.9: a lightweight regex highlighter without build or dependencies. It ships in the bundle; run it on a spec directly:

vim --cmd 'set rtp^=editors/vim' impty.spectec

Or install it permanently: download spectec-vim.tar.gz and unpack it into your Vim runtime (~/.config/nvim for Neovim):

mkdir -p ~/.vim && tar -xzf spectec-vim.tar.gz -C ~/.vim

Emacs: (29+ with tree-sitter, plus a C compiler) spectec-ts-mode.el ships in the bundle (and on this release page). Run it on a spec; it offers to build the grammar on first use:

emacs -l spectec-ts-mode.el impty.spectec

To make it permanent, load it from your init instead, so every .spectec file opens highlighted:

(add-to-list 'load-path "/directory/holding/spectec-ts-mode.el")
(require 'spectec-ts-mode)

4. Prose document (optional)

make doc splices the spec into AsciiDoc at documentation/impty.adoc with no extra tools -- read it in any editor, or preview it with the VS Code / JetBrains AsciiDoc extension. For HTML or PDF (make doc-html / make doc-pdf), install asciidoctor:

gem install asciidoctor asciidoctor-pdf

It is already present in the Docker image.

5. Verification

From the unpacked bundle, run:

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

The hands-on exercise will proceed after the demo.

What's Changed

• Fix property parsing and sample-count behavior by @KunJeong in #74
• feat(impty): save quickcheck counterexamples as runnable tests by @jihongmin63 in #75
• Add quickcheck support for the type preservation property by @jihongmin63 in #76
• Refactor backtick escape into per-kind atom markers by @KunJeong in #77

Full Changelog: tutorial-rc4...tutorial-rc5

tutorial-rc4

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-rc4/spectecx-tutorial.tar.gz
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-rc4/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 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 kunjeong/spectecx:tutorial
docker run -it kunjeong/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

Full Changelog: tutorial-rc3...tutorial-rc4

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-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-rc3/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 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: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

Full Changelog: tutorial-rc2...tutorial-rc3

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

tutorial-rc1

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-rc1/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

• Prune non-applicable rules from interpreter failtraces by @KunJeong in #65
• refactor(il): unify relation-call premises into binding and assertion forms by @KunJeong in #66
• Record provenance on each premise by @KunJeong in #67
• Add EL unparser and roundtrip test by @KunJeong in #68

Full Changelog: tutorial-rc0...tutorial-rc1

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