Skip to content
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

doc: add docstrings and usage examples in Init.Data.String.Basic #4001

Merged
merged 18 commits into from
May 8, 2024
Merged

doc: add docstrings and usage examples in Init.Data.String.Basic #4001

merged 18 commits into from
May 8, 2024

Conversation

austinletson
Copy link
Contributor

Add docstrings and usage examples for String.length, .push, .append, .get?, .set, .modyify, and .next. Update docstrings and add usage examples for String.toList, .get, and .get!.

@austinletson austinletson requested a review from kim-em as a code owner April 27, 2024 11:51
@austinletson austinletson changed the title docs: add docstrings and usage examples in Init.Data.String.Basic doc: add docstrings and usage examples in Init.Data.String.Basic Apr 27, 2024
@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 27, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Apr 27, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-04-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-04-27 12:12:05)
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but was unexpectedly noisy. (2024-04-28 13:56:23) View Log
  • ✅ Mathlib branch lean-pr-testing-4001 has successfully built against this PR. (2024-04-28 14:39:11) View Log
  • ✅ Mathlib branch lean-pr-testing-4001 has successfully built against this PR. (2024-04-28 15:21:26) View Log
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but was unexpectedly noisy. (2024-04-28 17:31:53) View Log
  • ✅ Mathlib branch lean-pr-testing-4001 has successfully built against this PR. (2024-04-28 18:13:40) View Log
  • ✅ Mathlib branch lean-pr-testing-4001 has successfully built against this PR. (2024-04-28 18:56:24) View Log
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but was unexpectedly noisy. (2024-05-06 14:19:29) View Log
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but lean4checker failed. (2024-05-06 14:50:08) View Log
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but was unexpectedly noisy. (2024-05-06 18:04:09) View Log
  • 🟡 Mathlib branch lean-pr-testing-4001 build against this PR was cancelled. (2024-05-06 23:48:27) View Log
  • ❌ Mathlib branch lean-pr-testing-4001 built against this PR, but was unexpectedly noisy. (2024-05-07 00:49:23) View Log
  • ❗ Std CI can not be attempted yet, as the nightly-testing-2024-05-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-05-07 12:52:48)

@austinletson
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Apr 27, 2024
nomeata
nomeata reviewed Apr 27, 2024
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment

Choose a reason for hiding this comment

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

Thanks!

src/Init/Data/String/Basic.lean Outdated Show resolved Hide resolved
src/Init/Data/String/Basic.lean Show resolved Hide resolved
src/Init/Data/String/Basic.lean Show resolved Hide resolved
@leodemoura leodemoura added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Apr 27, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4001
dcb38a9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4001
1fd77ca
@nomeata
Copy link
Collaborator

nomeata commented Apr 28, 2024

I'm happy. I'd like to give David a chance to have a look (or decline to having a look).

@nomeata nomeata added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
913ed55
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
1dcfaf0
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
f2ee5a0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
490958e
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
b6cbb1c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
d203d99
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
57b7325
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
811076c
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 6, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4001
7aa9631
david-christiansen
david-christiansen reviewed May 7, 2024
View reviewed changes
Copy link
Contributor

@david-christiansen david-christiansen left a comment

Choose a reason for hiding this comment

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

This is looking very good! I think it's almost ready to go. Two final comments.

Thank you very much!

austinletson and others added 17 commits May 7, 2024 08:23
@austinletson
doc: add docstrings and usage examples in Init.Data.String.Basic
ee7019b 
Add docstrings  and usage examples for `String.length`, `.push`,
`.append`, `.get?`, `.set`, `.modyify`, and `.next`. Update docstrings
and add usage examples for `String.toList`, `.get`, and `.get!`.
@austinletson @nomeata
format: lower case String
ac7eabb 
Co-authored-by: Joachim Breitner <[email protected]>
@austinletson @nomeata
doc: add warning about destructive updates to String.set docs
260d01a 
Co-authored-by: Joachim Breitner <[email protected]>
@austinletson
doc: add usage examples for multi-byte chars
6165eb7
@austinletson
doc: updated next to include refernce to valid position
f77bead
@austinletson @nomeata
docs: next wordsmithing
c9f4750 
Co-authored-by: Joachim Breitner <[email protected]>
@austinletson
doc: added case where p = s.endPos to next docstring
808ab0d
@austinletson @david-christiansen
doc: add note of Unicode code points to String.length
96b2c64 
Co-authored-by: David Thrane Christiansen <[email protected]>
@austinletson @david-christiansen
doc: batch apply David's suggestions
cec02c3 
Co-authored-by: David Thrane Christiansen <[email protected]>
@austinletson
doc: add example to String.length which differentiates between code p…
dcd77bf 
…oints and bytes
@austinletson
doc: add context to examples for String.next
f241d83
@austinletson
doc: improve examples
47bbfcc
@austinletson
doc: improve String.next example context
868a1ce
@austinletson
doc: remove white space
72d3d4e
@austinletson
doc: add newlines to lines longer than 100 chars
1c14476
@austinletson @david-christiansen
doc: improve unspecified examples for String.next
48c0723 
Co-authored-by: David Thrane Christiansen <[email protected]>
@austinletson @david-christiansen
doc: fix typo
1f0f5eb 
Co-authored-by: David Thrane Christiansen <[email protected]>
@austinletson
Copy link
Contributor Author

I addressed the two final comments and rebased off of master to try and fix the mathlib builds.

@kim-em
Copy link
Collaborator

kim-em commented May 7, 2024

Don't worry about the Mathlib build for this one, there's been a CI hiccup due to the Std -> Batteries rename. Normal service should resume tomorrow.

@kim-em kim-em added this pull request to the merge queue May 7, 2024
Merged via the queue into leanprover:master with commit b8e67d8 May 8, 2024
11 checks passed
@david-christiansen
Copy link
Contributor

Thanks again!

@austinletson austinletson mentioned this pull request May 18, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata left review comments

@david-christiansen david-christiansen david-christiansen requested changes

Assignees

@david-christiansen david-christiansen

Labels
awaiting-review Waiting for someone to review the PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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.
6 participants
@austinletson @leanprover-community-mathlib4-bot @nomeata @kim-em @david-christiansen @leodemoura