Local Setup

This repo does not require Codex, Claude Code, or an agent runtime.

Requirements

Node.js 20 or newer
opam
Z3
F* installed through opam or exposed with FSTAR=/path/to/fstar.exe

Commands

git clone https://github.com/danbri/wikifn-fstar.git
cd wikifn-fstar
make setup-fstar
make doctor
make import-vendored-dump
node ./bin/wikifn.js db build

make setup-fstar uses an opam switch named fstar by default. Override it with:

OPAM_SWITCH=my-switch make setup-fstar

Checks

npm test
node ./bin/wikifn.js eval-example --trace --profile
node ./bin/wikifn.js analyze Z22294
node ./bin/wikifn.js cache stats
node ./bin/wikifn.js db stats
make fstar-check
make fstar-js-demo

analyze uses the local cache by default. Pass --live or --refresh-cache only when you intentionally want public API access. It reads only seed functions and their listed implementations unless --follow-calls is passed. Keep --max-objects bounded when following calls.

Cache

The default cache is cache/wikifunctions/.

node ./bin/wikifn.js cache stats
make import-vendored-dump
make download-dump
node ./bin/wikifn.js cache import-xml cache/dumps/wikifunctionswiki/20260801/wikifunctionswiki-20260801-pages-meta-current.xml.bz2
node ./bin/wikifn.js cache fetch --follow-calls --max-objects 500 --max-network-objects 100 Z22294
node ./bin/wikifn.js analyze --follow-calls --max-objects 500 Z22294

make import-vendored-dump uses the snapshot in third_party/wikifunctions-dumps/ and does not contact Wikimedia. make download-dump is for intentional refreshes.

Cache modes:

default for analyze: local cache only
--live: trust cached latest revisions and fetch only misses
--refresh-cache: check current revision IDs and fetch changed objects
--offline: use only the cache
--no-cache: bypass cache

--max-objects caps the analysis corpus. --max-network-objects caps new full-object network fetches; cache hits do not count against it.

Rendered from setup.md by make docs. That file is the source; this page is generated.