Osiris.SettingsThe prefix that must be inserted in front of the name of every translated file. E.g., foo.ml in the project directory becomes <mark>foo.v in the destination directory. It is set by --mark.
decorate determines whether expressions in the output .v file should be decorated with location information.
debug format ... sends output to stderr only if --debug is set.
say format ... sends output to stderr only if --verbose is set.
warn format ... sends output to stderr only if --warnings is set.