Kontrol Build Options
Option | Description |
---|---|
| Show this help message and exit |
| Verbose output |
| Debug output |
| Directories to lookup K definitions in |
| Name of the main module |
| Name of the syntax module |
| Code selector expression to use when reading markdown. |
| Maximum depth to execute to |
| Extra K requires to include in generated output |
| Extra modules to import into generated main module |
| Path to kompile definition to |
| K backend to target with compilation |
| Mode for doing K rule type inference in |
| Emit JSON definition after compilation |
| Additional arguments to pass to llvm-kompile |
| Do not run llvm-kompile process |
| Make generate a dynamic llvm library |
| Make kompile generate debug symbols for llvm |
| Mode to kompile LLVM backend in |
| Location to put kompiled LLVM backend at |
| Generated a kompiled directory that K will not attempt to write to afterwards |
| Optimization level 0 |
| Optimization level 1 |
| Optimization level 2 |
| Optimization level 3 |
| Enable search mode on LLVM backend krun |
| Enable logging semantic rule coverage measurement |
| Generate standalone Bison parser for program sort |
| Disable List{Sort} parsing to make grammar LR(1) for Bison parser |
| Enable proof hint generation in LLVM backend kompilation |
| Do not wrap the output on the CLI |
| Path to Foundry project root directory |
| [haskell|maude] |
| Regenerate foundry.k even if it already exists |
| Rekompile foundry.k even if kompiled definition already exists |
| Do not call 'forge build' during kompilation |
Last updated