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:
- Argument parsing gives you an ordinary aggregate that can have nice, strong
type guarantees on its fields.
- It's very easy to add new options, pass the arguments throughout your
- You get excellent integration with xdoc, i.e., documentation is
- We can automatically generate usage messages that stay up to date as you
add new arguments.
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.
-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:
- A proper options structure with depth 3, verbose t,
and output report.txt.
- The "extra" arguments, i.e., ("foo.java" "bar.java").
For rare cases where you need to process a file that starts with -, the
special syntax -- is a marker that means "stop looking for options
Getopts is an ordinary library with no ttags. To load it, just include the
(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.
- A basic demo of using getopt to parse command-line options.
- Define a structure for representing command line options, and a
command-line parser that creates this structure.
- Demonstration of how to use getopt and argv to create a
working command-line program from ACL2.
- Parsers for various kinds of command-line options.
- Make sure longnames and aliases are unique, every field has a parser,
and so forth. This only applies to visible options.