hs-to-rocq: Command for Claude Code

New hs-to-rocq Example

Create a new hs-to-rocq example that translates a Haskell library to Coq. This skill sets up the directory structure, configures the build system, and iteratively translates the library following the Translation Principles from CLAUDE.md.

Arguments

The argument should be the library name and its Git repository URL, e.g.:

/new-example mtl https://github.com/haskell/mtl.git

If only a name is given, ask the user for the repository URL.

Phase 1: Setup

1.1 Create directory structure

examples/<name>/
├── Makefile
├── README.md
├── edits                    # Start empty
├── <name>/                  # Git submodule
├── lib/                     # Generated output (created by make)
├── module-edits/            # Per-module edits (created as needed)
└── theories/                # Proofs (created later if needed)

1.2 Add Git submodule

git submodule add <REPO_URL> examples/<name>/<name>

Pin to a specific tag/commit if the user specifies one. Ask:

• "Which version/tag/commit of the library should I use?"

1.3 Identify Haskell source files

Explore the submodule to find:

• The src/ or lib/ directory containing Haskell sources
• The .cabal file to understand module structure and dependencies
• Which modules are "exposed" (public API) vs internal

Ask the user:

• "I found N modules. Should I translate all of them, or start with a subset?"

1.4 Create Makefile

Use the graph/containers Makefile as a template. The Makefile must:

include ../../common.mk

ifeq (,$(wildcard <name>))
$(error Please run git submodule update --init examples/<name>/<name>)
endif

OUT=lib

MODULES = \
  Module/Path/One \
  Module/Path/Two

VFILES_GEN = $(addprefix $(OUT)/,$(addsuffix .v,$(MODULES)))
VFILES = $(VFILES_GEN)

all: vfiles coq

vfiles: $(OUT)/edits $(OUT)/_CoqProject $(OUT)/README.md $(VFILES)

$(OUT)/_CoqProject: Makefile
	mkdir -p $(OUT)
	> $@
	echo '-Q . ""' >> $@
	echo '-Q ../../../base ""' >> $@
	$(foreach f,$(addsuffix .v,$(MODULES)),echo '$(f)' >> $@;)

$(OUT)/edits:
	ln -fs ../edits $(OUT)/edits

$(OUT)/README.md:
	mkdir -p $(OUT)
	> $@
	echo 'This directory contains generated Coq files. Do not edit directly.' >> $@

coq: $(OUT)/_CoqProject $(VFILES)
	cd $(OUT) && coq_makefile -f _CoqProject -o Makefile
	$(MAKE) -C $(OUT)

HS_TO_ROCQ_OPTS := \
  -e ../../base/edits \
  -e edits \
  --iface-dir ../../base/ \
  --iface-dir $(OUT) \
  -N \
  -i <name>/<src-path>

.SECONDEXPANSION:
$(VFILES_GEN): $(OUT)/%.v : $$(wildcard module-edits/$$*/preamble.v) \
                            $$(wildcard module-edits/$$*/midamble.v) \
                            $$(wildcard module-edits/$$*/edits) \
                            $$(wildcard module-edits/$$*/flags) \
                            edits $(OUT)/README.md
	$(HS_TO_ROCQ) $(addprefix -e , $(wildcard module-edits/$*/edits)) \
	             $(addprefix -p , $(wildcard module-edits/$*/preamble.v)) \
	             $(addprefix --midamble , $(wildcard module-edits/$*/midamble.v)) \
	             $(HS_TO_ROCQ_OPTS) \
	             -o $(OUT) \
	             <name>/<src-path>/$*.hs
	test -e $@

clean:
	rm -rf $(OUT) hs-spec

theories: coq
	@if test -f theories/_CoqProject; then \
	  cd theories && coq_makefile -f _CoqProject -o Makefile && $(MAKE); \
	fi