_why 3.05 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
#compdef why
##
## zsh completion for why
## generated by ocompl

##
##
##
##

local curcontext state line cmds ret=1

##
_arguments -s -S \
     '(- *)'{-h,--help}'[Brief help message]' \
     '-'"[Read the input file from stdin]"\
     '*-T'"[<theory> Select <theory> in the input file or in the library]:<theory>:"\
     '*--theory'"[same as -T]:<theory>:"\
     '*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:"\
     '*--goal'"[same as -G]:<goal>:"\
     '-C'"[<file> Read configuration from <file>]:Configuration File:_files  -g '*.conf'"\
     '--config'"[same as -C]:Configuration File:_files  -g '*.conf'"\
     "(-L --library -I)"'-L'"[<dir> Add <dir> to the library search path]:Mlpost lib path:_files -/  "\
     "(-L --library -I)"'--library'"[same as -L]:Mlpost lib path:_files -/  "\
     "(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/  "\
     "(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:compadd $(why --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3)"\
     "(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:compadd $(why --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3)"\
     "(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
     "(-F --format)"'--format'"[same as -F]:<input format>:"\
     "(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
     "(-t --timelimit)"'--timelimit'"[same as -t]:<timeout s>:"\
     "(-m --memlimit)"'-m'"[<MiB> Set the prover\'s memory limit (default: no limit)]:<memory limit M>:"\
     "(-m --memlimit)"'--memlimit'"[same as -m]:<memory limit M>:"\
     "(-D --driver -P -prover)"'-D'"[<file> Specify a prover\'s driver (conflicts with -P)]:Prover\'s driver:_files  -g '*.drv'"\
     "(-D --driver -P -prover)"'--driver'"[same as -D]:Prover\'s driver:_files  -g '*.drv'"\
     "(-o --output)"'-o'"[<dir> Print the selected goals to separate files in <dir>]:directory output:_files -/  "\
     "(-o --output)"'--output'"[same as -o]:directory output:_files -/  "\
     '--print-theory'"[Print the selected theories]"\
     '--print-namespace'"[Print the namespaces of selected theories]"\
     '--list-transforms'"[List the registered transformations]"\
     '--list-printers'"[List the registered printers]"\
     '--list-provers'"[List the known provers]"\
     '--list-formats'"[List the known input formats]"\
     "(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--parse-only'"[Stop after parsing]"\
     "(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
     '--debug'"[Set the debug flag]"\
     '*-a'"[<transformation> Add a transformation to apply to the task]:<transformation>:compadd $(why --list-transforms | grep -e "^  ")"\
     '*--apply-transform'"[same as -a]:<transformation>:compadd $(why --list-transforms | grep -e "^  ")"\
     "*:The why file:_files  -g '*.why'" \
     && ret=0

return ret

_why "$@"