A library for processing command-line option.
Getopt is a tool for writing command-line programs in ACL2. It is similar in spirit to Getopt::Long for Perl, Trollop for Ruby, and so on.
We basically extend defaggregate with a command-line parsing layer. This has some nice consequences:
To make Getopt more automatic, we insist on some typical Unix conventions. We support options like these:
--help Long names use two dashes. --color red Values can use spaces or = signs. --shape=square -c red Short aliases use one dash. Plain -s=square aliases (with no arguments) can be -xfvz bundled. E.g., -xfvz instead of -x -f -v -z.
We insist on two dashes for long options, and one dash for short options. This lets us support mixing options in with other arguments like file names. For instance, after parsing something like:
myprogram --depth 3 --verbose foo.java bar.java -o report.txt
You get two things out:
For rare cases where you need to process a file that starts with
Getopts is an ordinary library with no ttags. To load it, just include the top book:
(include-book "centaur/getopt/top" :dir :system)
After that, the main command is defoptions.
There is also a demo of how to use Getopt: getopt-demo::demo-p.