search

leanprover / elan

The Lean version manager
Apache License 2.0
292 stars 34 forks source link

fix display glitch of download progress #101

Closed mkckr0 closed 1 year ago

mkckr0 commented 1 year ago 
$ elan update stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0-m5
info: downloading component 'lean'
  6.9 MiB / 139.1 MiB (  5 %)   0 B/s ETA: Unknown                 19.1 MiB / 139.1 MiB ( 14 %)   6.9 MiB/s ETA:  17 s
               30.2 MiB / 139.1 MiB ( 22 %)   9.5 MiB/s ETA:  11 s                 41.4 MiB / 139.1 MiB ( 30 %)  10.1 MiB/s ETA:  10 s                 52.5 MiB / 139.1 MiB ( 38 %)  10.3 MiB/s ETA:   8 s                 63.6 MiB / 139.1 MiB ( 46 %)  10.5 MiB/s ETA:   7 s                 74.7 MiB / 139.1 MiB ( 54 %)  11.3 MiB/s ETA:   6 s                 86.0 MiB / 139.1 MiB ( 62 %)  11.1 MiB/s ETA:   5 s                 97.1 MiB / 139.1 MiB ( 70 %)  11.2 MiB/s ETA:   4 s
          108.3 MiB / 139.1 MiB ( 78 %)  11.2 MiB/s ETA:   3 s                119.4 MiB / 139.1 MiB ( 86 %)  11.2 MiB/s ETA:   2 s                130.6 MiB / 139.1 MiB ( 94 %)  11.2 MiB/s ETA:   1 s                139.1 MiB / 139.1 MiB (100 %)  11.2 MiB/s ETA:   0 s
info: installing component 'lean'

  stable installed - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

The download progress is bad displayed. Add carriage return (\x0d) to fix it.

$ elan update stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0-m5
info: downloading component 'lean'
139.1 MiB / 139.1 MiB (100 %)  11.0 MiB/s ETA:   0 s
info: installing component 'lean'

  stable installed - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
Kha commented 1 year ago

Pull requests without meaningful description are not acceptable

mkckr0 commented 1 year ago

Description has been updated.

Kha commented 1 year ago

There is already a call to term.carriage_return(), is it clear why that doesn't work? When in doubt, please instead port over fixes from rustup upstream, who seem to have relevant changes.

mkckr0 commented 1 year ago

Rustup implements a new terminal interface by themself. They also use ANSI escape code \r or \x0d to achieve carriage return.

terminalsource.rs#L172-L180

Copying this file and dealing with all dependencies and references is a hard work. So I only copy some snippets, and use \r directly.

For filling spaces with a carriage return, it is because last line may be longer than next line, then the trailing chars may still be showed. So filling a fixed quantity of spaces is not enough in this case. Use displayed_charcount to count the spaces of last line instead.

Kha commented 1 year ago

Okay, looks reasonable to me. Thanks for investigating.

I assume you sucessfully tested it on Windows?

mkckr0 commented 1 year ago

Okay, looks reasonable to me. Thanks for investigating.

I assume you sucessfully tested it on Windows?

Yes, it's latest Windows 10.

Kha commented 1 year ago

Looks good on Linux as well