Feature request: Progress Bar when Translation

[ssyram]

Now for quite some large crate (several hundred MB), Charon usually takes quite a long time to process (or simply when generate-ml in my Mac). This appears as a pure freezing in the console.

Is it possible to have a progress bar to show the general progress so that the users are reassured everything is going fine inside? I also suggest a status showing the number of found errors / warnings.

[sonmarcho]

That would be nice indeed.

[Nadrieril]

That would be quite delightful. While we probably can't predict the number of items we'll extract, we could show a count of "items extracted/items left to extract", which is observable from the size of ctx.items_to_translate.

I'm sure there are many crates that display nice progress bars, do you want to try making this?

[ssyram]

Thanks for the discussion. I think the bar should also show the progress of Cleanups to be made?

BTW, I would focus on the vtable and DST restructuring on the Eurydice side for now, haha.

[Nadrieril]

I think the bar should also show the progress of Cleanups to be made?

Oh yeah, that too

[Nadrieril]

More detailed instructions:

• First challenge is finding a Rust library that does this nicely (https://crates.io/crates/tqdm or https://crates.io/crates/kdam look good);
• Then, there are two places where we could track progress:

  • The main translation loop: https://github.com/AeneasVerif/charon/blob/05817c42b8ceb6045051d7e35f09a9f0179b7db9/charon/src/bin/charon-driver/translate/translate_crate.rs#L674-L679 Here the remaining number of items is items_to_translate.len(), so we could show e.g. "items_translated / items_translated + items_to_translate.len()".

  • The main transformation loop: https://github.com/AeneasVerif/charon/blob/05817c42b8ceb6045051d7e35f09a9f0179b7db9/charon/src/bin/charon-driver/main.rs#L118-L121 Here we can show "how many passes we've run / total number of passes". We could even display the current pass, if the library allows it.