		Search-engine friendly clone of the ACL2 documentation.

Getopt

Defoptions

Define a structure for representing command line options, and a command-line parser that creates this structure.

defoptions is the main command provided by getopt library. It is really a thin wrapper around defaggregate, where each field can have some additional keywords that have certain effects.

A Basic Example

(defoptions myopts
  :parents (myprogram)
  :short "Command line options for my program."
  :tag :myopts
  ((help    booleanp
            "Print a help message and exit with status 0.")
   (outfile stringp
            "Where to write the output."
            :default "a.out")))

So far, this is identical to defaggregate except that we use defoptions instead. Indeed, the first thing the above defoptions form expands into is an ordinary defaggregate call. The defaggregate introduces a myopts-p structure as usual, complete with the usual accessors like myopts->help, a make-myopts macro, etc.

But in addition to introducing an aggregate, defoptions introduces a usage message and a command-line parsing function.

For myopts above, the usage message, *myopts-usage*, will just be:

--help                Print a help message and exit with status 0.
--outfile=ARG         Where to write the output.

So that's handy, and below we'll see how to customize this message a bit. You can probably easily imagine incorporating this into your program's --help message.

Meanwhile, the parsing function, parse-myopts, allows you to parse a string-listp into a myopts-p structure. The signature of parse-myopts is:

(parse-myopts args &key (init '*default-myopts*))
 -->
(mv errmsg result extra)

The args here are just a string list. Normally, if you were writing a real command-line program with ACL2, you would normally get the args to process by calling oslib::argv. But for testing and development, we can just use any old string list we want.

Usually you won't care about the optional :init argument: it just lets you use a custom myopts structure as the starting point, instead of starting from the default structure (which has the :default value for each field.)

Command-line parsing can fail because the user might type in something crazy. For instance, they might try to run myprogram --hlep instead of myprogram --help. The errmsg will be NIL if everything is okay, or else will be an error message produced by msg, which is suitable for printing with the fmt directive ~@. For example:

(b* (((mv errmsg result extra)
       (parse-myopts '("--hlep")))
      ((when errmsg)
       (cw "Error processing options!~%")
       (cw "~@0~%" errmsg)
       nil))
   result)

Will print out:

Error processing options!
Unrecognized option --hlep

When command-line processing is successful, the main return value, result, is a valid myopts-p structure that contains the various settings, and the extra return value is a list of any command-line options that we skipped because they didn't look like options. For example:

(b* (((mv ?errmsg result extra)
      (parse-myopts
       '("foo.java" "--outfile" "report.txt" "bar.java"))))
  (list :result result
        :extra extra))

Will return:

(:RESULT (:MYOPTS (HELP)
                  (OUTFILE . "report.txt"))
 :EXTRA ("foo.java" "bar.java"))

Adding Short Aliases (-h, -o, ...)

Ordinarily a program that takes options like --help and --outfile will also have shorter ways to give these options, e.g., -h and -o. You can set up these short names by just adding an :alias to your fields, like this:

(defoptions myopts
  :parents (myprogram)
  :short "Command line options for my program."
  :tag :myopts
  ((help    booleanp
            "Print a help message and exit with status 0."
            :alias #\h)
   (outfile stringp
            "Where to write the output."
            :default "a.out"
            :alias #\o)))

Note that the usage message gets automatically extended to take these into account. *myopts-usage* becomes:

-h,--help             Print a help message and exit with status 0.
-o,--outfile=ARG      Where to write the output.

Custom Option Types

The myopts-p structure is especially simple in that it only contains booleanp and stringp fields. Getopt has built-in parsers for these types, as well as for natp and posp. But in some cases these may not be sufficient.

If you need something fancier, you can write your own parser. See custom-parser for details. After writing your own parse-foo function, you can either register it as the default for all foo-p fields, or you can install it just as the parser for a particular field using the :parser option. For instance:

(outfile stringp
         "Where to write the output."
         :default "a.out"
         :alias #\o
         ;; redundant, but acceptable, to explicitly say to use the
         ;; default stringp parser
         :parser getopt::parse-string)

Changing Option Names

By default the option name is just automatically inferred from the field name. In rare cases you might want to change this, e.g., perhaps you prefer to use field-names like verbosep instead of verbose. You can accomplish this with a custom :longname for the field, e.g.,

(defoptions myopts
  :parents (myprogram)
  :short "Command line options for my program."
  :tag :myopts
  ((verbosep booleanp
             :longname "verbose"
             "Print excessive debugging information.")
   (help    booleanp
            "Print a help message and exit with status 0."
            :alias #\h)
   (outfile stringp
            "Where to write the output."
            :default "a.out"
            :alias #\o)))

List Types

By default options are unmergeable, meaning that it is an error to try to specify them more than once. This is generally sensible behavior, e.g., you probably don't want to support things like:

myprog --username jared --username sol ...

But occasionally you want to have an option that "stacks" with other options. For instance, in our Verilog parsing stuff we often want a "search path" that is a list of directories.

To facilitate this, the :merge option can be used to specify a custom "merging function" (typically cons) that can extend a field with a new value. For instance, here's basically the canonical way to have an option that lets the user write:

myprog --dir /dir1 --dir /dir2 ...

And turns them into a dirs field:

(dirs string-listp
      :longname "dir"
      :parser getopt::parse-string
      :merge cons)

Note that this will actually accumulate the options in the reverse order (because cons extends the front of a list). This is easily corrected for by using some kind of push function instead of cons, or by reversing the list at the end. See getopt-demo::demo-p for an example.

Customizing Usage Messages

By default we reuse the xdoc documentation for a field as its usage message. If you want to have a separate usage message instead, you can just add one, e.g., via :usage "blah blah".

For options that take arguments, you may occasionally want to name the argument. That is, by default, we will produce usage messages like:

--port ARG      The port to connect to.
--out ARG       Where to write the output.

But maybe you'd rather have this print as:

--port PORT     The port to connect to.
--out FILE      Where to write the output.

You can do this by adding, e.g., :argname "PORT" and :argname "FILE" to the port/out fields.