Command-Line Reference

Table of Contents

• Usage
• Debugging Features

Usage

USAGE:
  thorin [-?|-h|--help] [-v|--version] [-l|--list-search-paths] [-c|--clang <clang>] [-p|--plugin <plugin>] [-P|--plugin-path <path>] [-V|--verbose] [-O|--optimize <level>] [--output-d <file>] [--output-dot <file>] [--output-h <file>] [--output-ll <file>] [--output-md <file>] [-o|--output-thorin <file>] [-a|--ascii] [--bootstrap] [--dot-follow-types] [--dot-all-annexes] [--dump-gid <level>] [--dump-recursive] [--aggr-lam-spec] [--scalerize-threshold <threshold>] [-b|--break <gid>] [--reeval-breakpoints] [--break-on-alpha-unequal] [--break-on-error] [--break-on-warn] [--trace-gids] [<file>]
 
Display usage information.
 
OPTIONS, ARGUMENTS:
  -?, -h, --help          
  -v, --version           Display version info and exit.
  -l, --list-search-paths List search paths in order and exit.
  -c, --clang <clang>     Path to clang executable (default: 'which clang').
  -p, --plugin <plugin>   Dynamically load plugin.
  -P, --plugin-path <path>
                          Path to search for plugins.
  -V, --verbose           Verbose mode. Multiple -V options increase the verbosity. The maximum is 4.
  -O, --optimize <level>  Optimization level (default: 2).
  --output-d <file>       Emits dependency file containing a rule suitable for 'make' describing the dependencies of the source file (requires --output-h).
  --output-dot <file>     Emits the Thorin program as a graph using Graphviz' DOT language.
  --output-h <file>       Emits a header file to be used to interface with a plugin in C++.
  --output-ll <file>      Compiles the Thorin program to LLVM.
  --output-md <file>      Emits the input formatted as Markdown.
  -o, --output-thorin <file>
                          Emits the Thorin program again.
  -a, --ascii             Use ASCII alternatives in output instead of UTF-8.
  --bootstrap             Puts thorin into "bootstrap mode". This means a '.plugin' directive has the same effect as an '.import' and will not load a library. In addition, no standard plugins will be loaded.
  --dot-follow-types      Follow type dependencies in DOT output.
  --dot-all-annexes       Output all annexes - even if unused - in DOT output.
  --dump-gid <level>      Dumps gid of inline expressions as a comment in output if <level> > 0. Use a <level> of 2 to also emit the gid of trivial defs.
  --dump-recursive        Dumps Thorin program with a simple recursive algorithm that is not readable again from Thorin but is less fragile and also works for broken Thorin programs.
  --aggr-lam-spec         Overrides LamSpec behavior to follow recursive calls.
  --scalerize-threshold <threshold>
                          Thorin will not scalerize tuples/packs/sigmas/arrays with a number of elements greater than or equal this threshold.
  -b, --break <gid>       *Triggers breakpoint upon construction of node with global id <gid>. Useful when running in a debugger.
  --reeval-breakpoints    *Triggers breakpoint even upon unfying a node that has already been built.
  --break-on-alpha-unequal
                          *Triggers breakpoint as soon as two expressions turn out to be not alpha-equivalent.
  --break-on-error        *Triggers breakpoint on ELOG.
  --break-on-warn         *Triggers breakpoint on WLOG.
  --trace-gids            *Output gids during World::unify/insert.
  <file>                  Input file.
 
*These are developer options only enabled, if 'THORIN_ENABLE_CHECKS' is ON.
Use "-" as <file> to output to stdout.

In addition, you can specify more search paths using the environment variable THORIN_PLUGIN_PATH. Thorin will look for plugins in this priority:

1. The current working directory.
2. All paths specified via -D (in the given order).
3. All paths specified in the environment variable THORIN_PLUGIN_PATH (in the given order).
4. path/to/thorin.exe/../../lib/thorin
5. CMAKE_INSTALL_PREFIX/lib/thorin

Debugging Features

• You can increase the log level with -V.
  • No -V corresponds to thorin::Log::Level::Error.
  • -V corresponds to thorin::Log::Level::Warn.
  • -VV corresponds to thorin::Log::Level::Info.
  • -VVV corresponds to thorin::Log::Level::Verbose.
  • -VVVV corresponds to thorin::Log::Level::Debug. This output only exists in a Debug build of Thorin.

• You can trigger a breakpoint upon construction of a thorin::Def with a specific global id.

  For example, this will trigger a breakpoint if the thorin::Def with global id 4223 is being created:

  thorin -b 4223 in.thorin

• You can also trigger a breakpoint at some other very specific places like when a check for alpha equivalence fails via --break-on-alpha-unequal.