perennial-cli

Tool to manage perennial-based verification projects.

Install with go install github.com/mit-pdos/perennial-cli@latest.

Features

Run perennial-cli help for more detailed help.

Create a new project

Run go run github.com/mit-pdos/perennial-cli@latest init <url> to create a brand-new perennial project, with a Makefile and goose.toml setup. After setup, you can run the CLI with go tool perennial-cli using the newly-created go.mod file. Run go get -u tool to keep the version up-to-date.

Manage opam files

Perennial projects use an opam file to specify their dependencies, notably the version of perennial. These dependencies are specified using a git hash using opam's pin-depends feature. While pin-depends allows depending on specific commits and removes the need for a custom opam repository, it has some quirks: opam upgrade does not update pin-depends, and opam does not install transitive pin-depends for a dependency.

We handle this by providing perennial-cli opam update, which can (a) update the pin-depends field to the latest commit, and (b) automatically maintain all indirect dependencies.

To add a new dependency, use perennial-cli opam add. Takes a URL and pins the dependency to the current commit.

Run goose

perennial-cli goose will run goose. Write a goose.toml file to configure the translation:

rocq = "src"
go_path = "."
packages = ["./..."]

All of these fields are optional; an empty file is enough to direct perennial-cli. If go_path is not specified, the default behavior is to search for go.mod, so your code can be in a subdirectory.

Note

This functionality should be integrated into the goose binary.

Install and uninstall files

perennial-cli install implements the functionality of make install when using rocq makefile. It has some extra features: it takes a list of files to install and uses .rocqdeps.d (generated as part of our Makefile setup) to automatically extend that list with all dependencies.

perennial-cli uninstall does the same as make uninstall.

This command is intended to be called by the opam file, but it can be run manually (with the caveat that the installed files may not match what opam thinks is installed).

Shell completion

You can install shell completions for perennial-cli. Follow the cobra instructions for your shell.

For fish you just need perennial-cli completion fish > ~/.config/fish/completions/perennial-cli.fish.

Developing

perennial-cli requires Go 1.24+.