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.

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

chore: bump toolchain to v4.3.0-rc2 #367

Merged
merged 92 commits into from
Nov 17, 2023
Merged
Changes from 1 commit
Commits
Show all changes
92 commits
Select commit Hold shift + click to select a range
b4d59a9
testing leanprover/lean4#2688
kim-em Oct 16, 2023
f9614a5
fix
kim-em Oct 16, 2023
8e33f88
merge
kim-em Oct 21, 2023
23bc3e4
Run CI against core PR 2721 (do not merge)
bustercopley Oct 21, 2023
597fdf1
fix: use version number from EditableDocument for WorkspaceEdit
bustercopley Oct 20, 2023
3d66565
fixes for leanprover/lean4#2734
kim-em Oct 23, 2023
2ff2c56
merge fixes for leanprover/lean4#2688
kim-em Oct 23, 2023
76dc5e1
new lake-manifest.json
kim-em Oct 23, 2023
961c6b2
Update Std/Tactic/Ext/Attr.lean
kim-em Oct 23, 2023
71ccc03
chore: move to latest nightly
kim-em Oct 23, 2023
4b8dc14
empty lake-manifest.json
kim-em Oct 23, 2023
a75a594
merge lean-pr-testing-2688
kim-em Oct 23, 2023
3fa2bbd
chore: bump toolchain to nightly-2023-10-23
kim-em Oct 23, 2023
b128c19
Apply suggestions from code review
digama0 Oct 23, 2023
03c9aa9
Merge remote-tracking branch 'origin/main' into nightly-testing
kim-em Oct 24, 2023
a717993
Merge remote-tracking branch 'origin/main' into lean-pr-testing-2734
kim-em Oct 24, 2023
094b08e
bump toolchain
kim-em Oct 25, 2023
b869351
merge #306
kim-em Oct 25, 2023
97d30e5
bump toolchain
kim-em Oct 26, 2023
e3d90c3
merge #316
kim-em Oct 26, 2023
a2e2fc5
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 27, 2023
a18c5fa
chore: bump to nightly-2023-10-27
leanprover-community-mathlib4-bot Oct 27, 2023
1f7b317
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 27, 2023
5175eba
chore: bump to nightly-2023-10-28
leanprover-community-mathlib4-bot Oct 28, 2023
5cd3d13
chore: changes required for leanprover/lean4#2783
kim-em Oct 30, 2023
34cd9a4
chore: bump to nightly-2023-10-30
leanprover-community-mathlib4-bot Oct 30, 2023
f8f886e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 30, 2023
e1f9766
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 31, 2023
145e768
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 31, 2023
e884944
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 31, 2023
7ad8223
Merge main into nightly-testing
leanprover-community-mathlib4-bot Oct 31, 2023
2b65ea9
chore: fixes for new simp default (decide := false) in lean4#2722
collares Oct 21, 2023
6f724a0
use leanprover/lean4-pr-releases:pr-release-2722 toolchain
collares Oct 31, 2023
7b3a210
chore: bump to nightly-2023-10-31
leanprover-community-mathlib4-bot Oct 31, 2023
cf03e8b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
9292734
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
1f719ba
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
7b1e009
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
c7b3745
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
4f16e93
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
363d8d0
chore: bump to nightly-2023-11-01
leanprover-community-mathlib4-bot Nov 1, 2023
569142a
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
677efa9
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
3fc673d
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
ba1a605
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 1, 2023
099e2ce
merge
kim-em Nov 2, 2023
586a7fa
rm lake-manifest
kim-em Nov 2, 2023
a81cb02
Merge remote-tracking branch 'origin/main' into lean-pr-testing-2722
kim-em Nov 2, 2023
c618f3c
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 3, 2023
41a2161
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 3, 2023
253aead
chore: bump to nightly-2023-11-03
leanprover-community-mathlib4-bot Nov 3, 2023
d2df4d4
merge #312
kim-em Nov 3, 2023
07f5bd5
fix
kim-em Nov 3, 2023
a91b93a
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 4, 2023
7fcae40
chore: bump to nightly-2023-11-04
leanprover-community-mathlib4-bot Nov 4, 2023
e63b80e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 4, 2023
824a8f0
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 4, 2023
4167e5e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 5, 2023
27a201c
merge nightly-testing-2023-11-04
kim-em Nov 5, 2023
267d465
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 5, 2023
cced23c
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 5, 2023
4ebec3a
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 5, 2023
f449ab7
chore: bump to nightly-2023-11-05
leanprover-community-mathlib4-bot Nov 5, 2023
716838e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 6, 2023
f292fcc
chore: bump to nightly-2023-11-06
leanprover-community-mathlib4-bot Nov 6, 2023
ccd12a3
chore: bump to nightly-2023-11-07
leanprover-community-mathlib4-bot Nov 7, 2023
c730b95
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 8, 2023
a025356
chore: bump to nightly-2023-11-08
leanprover-community-mathlib4-bot Nov 8, 2023
511ea8e
fix test
kim-em Nov 8, 2023
0938cd3
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 9, 2023
bce5eb1
chore: bump to nightly-2023-11-10
leanprover-community-mathlib4-bot Nov 10, 2023
5e52ffd
merge lean-pr-testing-2783
kim-em Nov 10, 2023
16db66b
Update Std/Classes/LawfulMonad.lean
kim-em Nov 10, 2023
9a7273b
Merge remote-tracking branch 'origin/lean-pr-testing-2783' into night…
kim-em Nov 10, 2023
5a1bbad
infer decidable instances for simp lemmas
kim-em Nov 9, 2023
5e086ed
toolchain
kim-em Nov 11, 2023
7c68b32
chore: bump to nightly-2023-11-11
leanprover-community-mathlib4-bot Nov 11, 2023
309aee1
bump toolchain
kim-em Nov 12, 2023
7d4ddd0
merge lean-pr-testing-2816
kim-em Nov 12, 2023
fade49b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 14, 2023
5954d44
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 14, 2023
aefa41b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 14, 2023
21a207e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Nov 14, 2023
0da7d7e
chore: bump to nightly-2023-11-14
leanprover-community-mathlib4-bot Nov 14, 2023
366988e
.lake
kim-em Nov 14, 2023
03b914b
Merge branch 'nightly-testing' into bump_v4.3.0-rc2
kim-em Nov 16, 2023
d5d3c14
comp_def
kim-em Nov 16, 2023
56a98cd
better gitignore
kim-em Nov 16, 2023
38b376b
smaller diff
kim-em Nov 16, 2023
0c15f35
toolchain
kim-em Nov 16, 2023
adeb7d4
forbidden character
kim-em Nov 16, 2023
660c6d1
style
digama0 Nov 17, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix: use version number from EditableDocument for WorkspaceEdit
bustercopley committed Oct 22, 2023
commit 597fdf1932bc1b2b2ed6d585905ccbb8166229c8
2 changes: 1 addition & 1 deletion Std/CodeAction/Deprecated.lean
Original file line number Diff line number Diff line change
@@ -60,7 +60,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
let pos := doc.meta.text.leanPosToLspPos msg.pos
let endPos' := doc.meta.text.leanPosToLspPos endPos
pure { eager with
edit? := some <| .ofTextEdit params.textDocument.uri {
edit? := some <| .ofTextEdit doc.versionedIdentifier {
range := ⟨pos, endPos'⟩
newText := toString c'
}
23 changes: 13 additions & 10 deletions Std/CodeAction/Misc.lean
Original file line number Diff line number Diff line change
@@ -85,7 +85,7 @@ instance : Monad Id := {
else
str := str ++ indent ++ "}"
pure { eager with
edit? := some <| .ofTextEdit params.textDocument.uri {
edit? := some <| .ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨holePos, info.stx.getTailPos?.get!⟩
newText := str
}
@@ -131,7 +131,7 @@ def foo : Expr → Unit := fun
```

-/
@[hole_code_action] def eqnStub : HoleCodeAction := fun params snap ctx info => do
@[hole_code_action] def eqnStub : HoleCodeAction := fun _ snap ctx info => do
let some ty := info.expectedType? | return #[]
let .forallE _ dom .. ← info.runMetaM ctx (whnf ty) | return #[]
let .const name _ := (← info.runMetaM ctx (whnf dom)).getAppFn | return #[]
@@ -156,22 +156,22 @@ def foo : Expr → Unit := fun
str := str ++ if arg.hasNum || arg.isInternal then " _" else s!" {arg}"
str := str ++ s!" => {holeKindToHoleString info.elaborator ctor}"
pure { eager with
edit? := some <|.ofTextEdit params.textDocument.uri {
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨holePos, info.stx.getTailPos?.get!⟩
newText := str
}
}
}]

/-- Invoking hole code action "Start a tactic proof" will fill in a hole with `by done`. -/
@[hole_code_action] def startTacticStub : HoleCodeAction := fun params _ _ info => do
@[hole_code_action] def startTacticStub : HoleCodeAction := fun _ _ _ info => do
let holePos := info.stx.getPos?.get!
let doc ← readDoc
let indent := (findIndentAndIsStart doc.meta.text.source holePos).1
pure #[{
eager.title := "Start a tactic proof."
eager.kind? := "quickfix"
eager.edit? := some <|.ofTextEdit params.textDocument.uri {
eager.edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨holePos, info.stx.getTailPos?.get!⟩
newText := "by\n".pushn ' ' (indent + 2) ++ "done"
}
@@ -192,7 +192,7 @@ example : True := by
```
-/
@[tactic_code_action*]
def removeAfterDoneAction : TacticCodeAction := fun params _ _ stk node => do
def removeAfterDoneAction : TacticCodeAction := fun _ _ _ stk node => do
let .node (.ofTacticInfo info) _ := node | return #[]
unless info.goalsBefore.isEmpty do return #[]
let _ :: (seq, i) :: _ := stk | return #[]
@@ -203,7 +203,7 @@ def removeAfterDoneAction : TacticCodeAction := fun params _ _ stk node => do
title := "Remove tactics after 'no goals'"
kind? := "quickfix"
isPreferred? := true
edit? := some <|.ofTextEdit params.textDocument.uri {
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨prev, stop⟩
newText := ""
}
@@ -251,7 +251,7 @@ example (x : Nat) : x = x := by
It also works for `cases`.
-/
@[tactic_code_action Parser.Tactic.cases Parser.Tactic.induction]
def casesExpand : TacticCodeAction := fun params snap ctx _ node => do
def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
let .node (.ofTacticInfo info) _ := node | return #[]
let (discr, induction, alts) ← match info.stx with
| `(tactic| cases $[$_ :]? $e $[$alts:inductionAlts]?) => pure (e, false, alts)
@@ -302,7 +302,10 @@ def casesExpand : TacticCodeAction := fun params snap ctx _ node => do
str := str ++ s!" => sorry"
str
pure { eager with
edit? := some <|.ofTextEdit params.textDocument.uri { range := ⟨startPos, endPos⟩, newText }
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := ⟨startPos, endPos⟩
newText
}
}
}]

@@ -356,7 +359,7 @@ def addSubgoalsActionCore (params : Lsp.CodeActionParams)
for _ in goals.tail! do
newText := newText ++ indent ++ "· done"
pure { eager with
edit? := some <|.ofTextEdit params.textDocument.uri {
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange range
newText
}
4 changes: 2 additions & 2 deletions Std/Tactic/GuardMsgs.lean
Original file line number Diff line number Diff line change
@@ -163,7 +163,7 @@ elab_rules : command
open CodeAction Server RequestM in
/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
@[command_code_action guardMsgsCmd]
def guardMsgsCodeAction : CommandCodeAction := fun params _ _ node => do
def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
let .node _ ts := node | return #[]
let res := ts.findSome? fun
| .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
@@ -187,7 +187,7 @@ def guardMsgsCodeAction : CommandCodeAction := fun params _ _ node => do
else
s!"/--\n{res}\n-/\n"
pure { eager with
edit? := some <|.ofTextEdit params.textDocument.uri {
edit? := some <|.ofTextEdit doc.versionedIdentifier {
range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
newText
}
2 changes: 1 addition & 1 deletion Std/Tactic/TryThis.lean
Original file line number Diff line number Diff line change
@@ -62,7 +62,7 @@ apply the replacement.
eager.title := "Apply 'Try this'"
eager.kind? := "quickfix"
eager.isPreferred? := true
eager.edit? := some <| .ofTextEdit params.textDocument.uri { range, newText }
eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText }
}

/-- Replace subexpressions like `?m.1234` with `?_` so it can be copy-pasted. -/