Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

fix: do not suppress git output #67

Closed
wants to merge 1 commit into from

Conversation

gebner
Copy link
Member

@gebner gebner commented May 15, 2022

This makes it easier to debug cases where git fails. The stderr output also shows progress information during git clone.

See #31 (comment)
Split off from #64

This makes it easier to debug cases where git fails.  The stderr output
also shows progress information during git clone.
See leanprover#31 (comment)
@tydeu tydeu added the enhancement New feature or request label May 16, 2022
@tydeu
Copy link
Member

tydeu commented Jun 30, 2022

@gebner Lake now logs Git stdout/stderr on failure. Do you find that sufficient?

@gebner
Copy link
Member Author

gebner commented Jun 30, 2022

It's an improvement, but I'd certainly prefer to get the stderr unfiltered for the live progress report.

@tydeu
Copy link
Member

tydeu commented Jul 1, 2022

@gebner That just does not seem practical to me. Lake needs to capture the output as it needs to determine how and when to print it based on its own settings. This will, for instance, be important when I improve Lake's logging to have format closer to something like CMake and have flags like --quiet and --verbose to toggle how much logging is performed.

@tydeu
Copy link
Member

tydeu commented Aug 2, 2022

I am closing this as I think the current logging approach is sufficient for preserving the output for debugging purposes and the live piping approach used here to preserve progress reports is infeasible for the reasons I mentioned above.

@tydeu tydeu closed this Aug 2, 2022
Kha pushed a commit to Kha/lean4 that referenced this pull request Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants