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 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 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 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.