Demonstration of how to use getopt and argv to create a working command-line program from ACL2.
This is an example of how to write an extremely basic command-line program in ACL2 that parses some options from the command-line.
Note: our focus in this demo is to show how getopt and argv and save-exec work together. Our program takes just a few basic options. If you want to see a demo of how to parse fancier command-line options, see demo instead.
Depending on its input, our program will print out:
Our top-level program is demo2-main.
To see how to turn
On some Lisps the program may also print out a Lisp banner. Most Lisps can be instructed to suppress such a banner via additional command-line options (which vary from Lisp to Lisp). A notable exception is Lispworks, where the banner cannot be suppressed. So depending on your host Lisp, you may be able to edit the resulting shell script to disable the banner, but unfortunately ACL2's save-exec has no portable way to do this.