# Kontrol Build Options

| Option                                                            | Description                                                                       |
| ----------------------------------------------------------------- | --------------------------------------------------------------------------------- |
| `-h`, `--help`                                                    | Show this help message and exit                                                   |
| `--verbose`, `-v`                                                 | Verbose output                                                                    |
| `--debug`                                                         | Debug output                                                                      |
| `-I INCLUDES`                                                     | Directories to lookup **K** definitions in                                        |
| `--main-module MAIN_MODULE`                                       | Name of the main module                                                           |
| `--syntax-module SYNTAX_MODULE`                                   | Name of the syntax module                                                         |
| `--md-selector MD_SELECTOR`                                       | Code selector expression to use when reading markdown.                            |
| `--depth DEPTH`                                                   | Maximum depth to execute to                                                       |
| `--require REQUIRES`                                              | Extra **K** requires to include in generated output                               |
| `--module-import IMPORTS`                                         | Extra modules to import into generated main module                                |
| `--output-definition DEFINITION_DIR, --definition DEFINITION_DIR` | Path to kompile definition to                                                     |
| `--backend BACKEND`                                               | **K** backend to target with compilation                                          |
| `--type-inference-mode TYPE_INFERENCE_MODE`                       | Mode for doing **K** rule type inference in                                       |
| `--emit-json`                                                     | Emit JSON definition after compilation                                            |
| `-ccopt CCOPTS`                                                   | Additional arguments to pass to llvm-kompile                                      |
| `--no-llvm-kompile`                                               | Do not run llvm-kompile process                                                   |
| `--with-llvm-library`                                             | Make kompile[^1] generate a dynamic llvm library                                  |
| `--enable-llvm-debug`                                             | Make kompile generate debug symbols for llvm                                      |
| `--llvm-kompile-type LLVM_KOMPILE_TYPE`                           | Mode to kompile LLVM backend in                                                   |
| `--llvm-kompile-output LLVM_KOMPILE_OUTPUT`                       | Location to put kompiled LLVM backend at                                          |
| `--read-only-kompiled-directory`                                  | Generated a kompiled directory that **K** will not attempt to write to afterwards |
| `-O0`                                                             | Optimization level 0                                                              |
| `-O1`                                                             | Optimization level 1                                                              |
| `-O2`                                                             | Optimization level 2                                                              |
| `-O3`                                                             | Optimization level 3                                                              |
| `--enable-search`                                                 | Enable search mode on LLVM backend krun                                           |
| `--coverage`                                                      | Enable logging semantic rule coverage measurement                                 |
| `--gen-bison-parser`                                              | Generate standalone Bison parser for program sort                                 |
| `--bison-lists`                                                   | Disable List{Sort} parsing to make grammar LR(1) for Bison parser                 |
| `--llvm-proof-hint-instrumentation`                               | Enable proof hint generation in LLVM backend kompilation                          |
| `--no-exc-wrap`                                                   | Do not wrap the output on the CLI                                                 |
| `--foundry-project-root FOUNDRY_ROOT`                             | Path to Foundry project root directory                                            |
| `--target {KompileTarget.HASKELL,KompileTarget.MAUDE}`            | \[haskell\|maude]                                                                 |
| `--regen`                                                         | Regenerate foundry.k even if it already exists                                    |
| `--rekompile`                                                     | Rekompile foundry.k even if kompiled definition already exists                    |
| `--no-forge-build`                                                | Do not call 'forge build' during kompilation                                      |

[^1]:


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/kontrol/glossary/kontrol-build-options.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.