		Search-engine friendly clone of the ACL2 documentation.

Command-line

Getopt

A library for processing command-line option.

Introduction

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 program, etc.
You get excellent integration with xdoc, i.e., documentation is mostly automated.
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.
--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:

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

Using Getopts

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.

Subtopics

Demo-p: A basic demo of using getopt to parse command-line options.
Defoptions: Define a structure for representing command line options, and a command-line parser that creates this structure.
Demo2: Demonstration of how to use getopt and argv to create a working command-line program from ACL2.
Parsers: Parsers for various kinds of command-line options.
Sanity-check-formals: Make sure longnames and aliases are unique, every field has a parser, and so forth. This only applies to visible options.
Formal->parser
Formal->argname
Formal->longname
Formal->alias
Formal->usage
Formal->merge
Formal->hiddenp