Progress bar - #1061
Draft
ArkadySkv wants to merge 7 commits into
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add
--progressflag with dynamic progress bar for symbolic executionThis PR adds a
--progressflag to theowi symcommand, displaying a live‑updating progress bar during symbolic execution. The progress bar shows the number of completed tasks, total tasks, and a visual progress indicator.OCaml Version
Motivation
Currently, there is no way to see the progress of symbolic execution without enabling
--debug, which floods the output and significantly slows down execution. This feature provides a lightweight, user‑friendly progress indicator that updates in place.Fixes: #458, #575
Changes
New Module:
src/infra/progress.ml#‑filled bar showing completion percentagecompleted / total)Modified Files
src/bin/owi.ml--progressCLI flag, included insymbolic_parameterssrc/symbolic/symbolic_parameters.mlprogress : boolfieldsrc/symbolic/symbolic_parameters.mliprogress : boolto interfacesrc/symbolic/symbolic_driver.mlsrc/symbolic/symbolic_driver.mliprogress:booltorunsignaturesrc/cmd/cmd_sym.ml~progressfrom parameters to driversrc/cmd/cmd_iso.ml~progressfrom parameters to driversrc/cmd/cmd_iso.mliprogress:booltocmdsignaturesrc/owi.mliSymbolic_parametersrecord definitionsrc/duneprogress.mlto build systemTesting
Test File:
example.watCommand & Output
The progress bar updates as symbolic execution explores each path:
Expected Behavior
TTY output: Live‑updating progress bar with # characters, percentage, and task counts.
Non‑TTY output (redirected to file or pipe): Plain log messages like Progress: 3 / 5 tasks completed.
Unknown total: Shows "Waiting for tasks..." until the first task is counted.
Usage
Examples
Implementation Details
The progress bar is implemented using:
Atomic counters for thread‑safe updates across workers.
Logs.app for output (follows Owi's logging system).
Carriage return (\r) for in‑place terminal updates.
Unix.isatty to detect TTY vs. non‑TTY output.
Tasks are counted at two points:
Total tasks incremented when a new task is pushed (Yield).
Completed tasks incremented when a task finishes (Ok or Error).
The reporter is enabled only when --progress is passed and output is a TTY.
Future Work
Add --progress support to other subcommands (owi c, owi c++, owi rust, owi go, owi zig).
Add customizable progress bar style (e.g., spinner for unknown total).
Related Issues
Closes #458 – add an option to display progress
Closes #575 – make a shiny terminal progress interface (partial)
Checklist
☑ Build passes (dune build @ALL)
☑ Tests pass (dune runtest) – except pre‑existing failures
☑ Code follows Owi style and uses the prelude library
☑ Documentation updated (usage examples)
☑ --progress flag appears in --help