Skip to content

Files

Latest commit

54cf68b · Apr 29, 2024

History

History

.completion

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 

Completion of fstar.exe flags

If you want completion of arguments to fstar.exe for your shell, you can find completion scripts to do so here. We don't yet automatically install these where your shell will pick them up, so you'll have to manually install them using instructions for your shell.

In the below descriptions, $FSTAR_HOME is the path to the F* source directory.

bash

Bash completion uses the external package bash-completion. Once bash-completion is setup, you can get completion working by adding the following line to your ~/.bash_completion:

source $FSTAR_HOME/.completion/bash/fstar.exe.bash

This completion script parses the output of fstar.exe --help dynamically.

zsh

ZSH has builtin completion support; you may have to enable it if you didn't during the initial setup, by adding the following lines to ~/.zshrc:

autoload -Uz compinit
compinit

If you're using oh-my-zsh, it already enables completion.

Next, you'll need to put $FSTAR_HOME/.completion/zsh/__fstar.exe somewhere on your $fpath. You can add the directory to your $fpath by adding the following to your ~/.zshrc:

fpath=($FSTAR_HOME/.completion/zsh $fpath)

If you prefer, you can create a new directory for user-defined ZSH functions instead, for example:

$ mkdir -p ~/.zsh/functions
$ ln -s $FSTAR_HOME/.completion/zsh/__fstar.exe ~/.zsh/functions/

and then add fpath=(~/.zsh/functions $fpath) to your ~/.zshrc.

The ZSH completion uses ZSH's builtin support for parsing fstar.exe --help.

fish

fish has builtin support for completion that is enabled by default. Install the completion script where fish will find it:

$ ln -s $FSTAR_HOME/.completion/fish/fstar.exe.fish ~/.config/fish/completions/

The completions file for fish is generated by parsing fstar.exe --help with $FSTAR_HOME/.scripts/fstar_fish_completions.py.