8000 feat: add system information functions to the standard library by algebraic-dev · Pull Request #8109 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: add system information functions to the standard library #8109

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

feat: add system information functions to the standard library #8109

wants to merge 14 commits into from
+1,685 −1

Conversation

algebraic-dev
Copy link
Member

This PR adds system information functions to the standard library

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 25, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Apr 25, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7feb583b9e4ca5b2958f993a578d4bd9d8ca3f48 --onto 416e07a68e5d9b884de8af4836497a7cc2414c8f. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-25 22:31:48)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ebf455a13780ea508abee8016b8bb6c5549bf9d7 --onto 4eccb5b4792c270ad10ac059b9672a8845961079. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-23 22:43:58)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ebf5fbd294b379dcaf4a7a6da0a6934b035e61d4 --onto 3b2990b3816b7e7ec289ad498496a61d18bd85f4. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-18 06:10:36)

@algebraic-dev algebraic-dev marked this pull request as ready for review May 23, 2025 23:17
@algebraic-dev algebraic-dev requested a review from TwoFX as a code owner May 23, 2025 23:17
@TwoFX TwoFX added the release-ci Enable all CI checks for a PR, like is done for releases label Jun 10, 2025
TwoFX
TwoFX reviewed Jun 10, 2025
View reviewed changes
@algebraic-dev algebraic-dev mentioned this pull request Jun 16, 2025
Open
@algebraic-dev algebraic-dev requested a review from TwoFX June 18, 2025 16:02
@TwoFX TwoFX self-assigned this Jun 18, 2025
TwoFX
TwoFX reviewed Jun 25, 2025
View reviewed changes
src/Std/Internal/Async/Process.lean
/--
CPU time spent in user mode (milliseconds)
-/
cpuUserTimeMs : Time.Millisecond.Offset
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's drop the Ms suffix, it's part of the type now.

src/Std/Internal/Async/Process.lean


/--
A process identifier, typically a numeric ID like in UNIX (e.g. 1001).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do you mean by "typically" here (and elsewhere)?

src/Std/Internal/Async/Process.lean
Returns the absolute path of the current executable.
-/
@[inline]
def getExecutablePath : IO String :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is there a specific reason while this is not a System.FilePath?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX left review comments

Assignees

@TwoFX TwoFX

Labels
changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@algebraic-dev @leanprover-community-bot @TwoFX
0