Skip to content

Commit fea9737

Browse files
grunwegadomani
andcommitted
fix(create_deprecated_modules): fix the build again (leanprover-community#37391)
The code needed updating to the new String API; it failed to build before this PR. This also removes uses of deprecated String API. A future PR will add CI to ensure this script builds fine. (Future future: can we test that we tested all .lean scripts? Or have a test which builds all .lean files in scripts?) Co-authored-by: Damiano Testa <adomani@gmail.com>
1 parent 02d8476 commit fea9737

1 file changed

Lines changed: 22 additions & 20 deletions

File tree

scripts/create_deprecated_modules.lean

Lines changed: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ pass `"git commit -m 'message with spaces'`, the command will be split into
3434
`["git", "commit", "-m", "'message", "with", "spaces'"]`, which is not what you want.
3535
-/
3636
def runCmd (s : String) : IO String := do
37-
let cmd::args := s.splitOn | EStateM.throw "Please provide at least one word in your command!"
37+
let cmd::args := s.splitOn | throw <| IO.userError "Please provide at least one word in your command!"
3838
IO.Process.run {cmd := cmd, args := args.toArray}
3939

4040
/--
@@ -123,9 +123,9 @@ formatted as a collapsible message. In practice, `msg` is either `last modified`
123123
it returns the pair `(<hash>, <msg> in <PRdescr> <hash> <diff of file wrt previous commit>)`,
124124
formatted as a collapsible message.
125125
-/
126-
def processPrettyOneLine (log msg fname : String) : IO (String × MessageData) := do
126+
def processPrettyOneLine (log msg fname : String.Slice) : IO (String.Slice × MessageData) := do
127127
let hash := log.takeWhile (!·.isWhitespace)
128-
let PRdescr := (log.drop hash.length).trim
128+
let PRdescr := (log.dropWhile (!·.isWhitespace)).trimAscii
129129
let gitDiffCLI := s!"git diff {hash}^...{hash} -- {fname}"
130130
let diff ← runCmd gitDiffCLI <|> pure s!"{hash}: error in computing '{gitDiffCLI}'"
131131
let diffCollapsed := .trace {cls := .str .anonymous s!"{hash}"} m!"{gitDiffCLI}" #[m!"{diff}"]
@@ -146,11 +146,11 @@ If no input is provided, the default percentage is `100`.
146146
def mkRenamesDict (percent : Nat := 100) : IO (Std.HashMap String String) := do
147147
let mut dict := ∅
148148
let gitDiff ← runCmd s!"git diff --name-status origin/master...HEAD"
149-
let lines := gitDiff.trim.splitOn "\n"
149+
let lines := gitDiff.trimAscii.lines
150150
for git in lines do
151151
-- If `git` corresponds to a rename, it contains `3` segments, separated by a
152152
-- tab character (`\t`): `R%%`, `oldName`, `newName`.
153-
let [pct, oldName, newName] := git.split (· == '\t') | continue
153+
let [pct, oldName, newName] := git.split (· == '\t') |>.toList | continue
154154
if pct.take 1 != "R" then
155155
IO.println
156156
s!"mkRenamesDict: '{pct}' should have been of the form Rxxx, denoting a `R`ename \
@@ -160,7 +160,7 @@ def mkRenamesDict (percent : Nat := 100) : IO (Std.HashMap String String) := do
160160
-- This looks like a rename with a similarity index at least as big as our threshold:
161161
-- we add the rename to our dictionary.
162162
if percent ≤ pctNat then
163-
dict := dict.insert oldName newName
163+
dict := dict.insert oldName.toString newName.toString
164164
-- This looks like a rename, but the similarity index is smaller than our threshold:
165165
-- we report a message and do not add the rename to our dictionary.
166166
else
@@ -183,7 +183,8 @@ def mkModName (fname : System.FilePath) : String :=
183183
match cpts.getLast? with
184184
| none => cpts
185185
| some last =>
186-
cpts.dropLast ++ [if last.endsWith ".lean" then last.dropRight ".lean".length else last]
186+
cpts.dropLast ++
187+
[if last.endsWith ".lean" then last.dropEnd ".lean".length |>.toString else last]
187188
".".intercalate cpts
188189

189190
#guard mkModName ("Mathlib" / "Data" / "Nat" / "Basic.lean") == "Mathlib.Data.Nat.Basic"
@@ -214,16 +215,16 @@ def deprecateFilePath (fname : String) (rename comment : Option String) :
214215
-- Retrieve the last two commits that modified `fname`:
215216
-- the last one is the deletion, the previous one is the last file modification.
216217
let log ← runCmd s!"git log --pretty=oneline -2 -- {fname}"
217-
let [deleted, lastModified] := log.trim.splitOn "\n" |
218-
throwError "Found {(log.trim.splitOn "\n").length} commits, but expected 2! \
218+
let [deleted, lastModified] := log.lines.toList |
219+
throwError "Found {log.lines.length} commits, but expected 2! \
219220
Please make sure the file {fname} existed at some point!"
220221
let (_deleteHash, deletedMsg) ← processPrettyOneLine deleted "deleted" fname
221222
let (modifiedHash, modifiedMsg) ← processPrettyOneLine lastModified "last modified" fname
222223
msgs := msgs.append #[m!"The file {fname} was\n", modifiedMsg, deletedMsg]
223224
-- Get the commit date, in `YYYY-MM-DD` format, of the commit deleting the file.
224225
let log' ← runCmd s!"git log --format=%cs -2 -- {fname}"
225-
let deletionDate := (log'.trim.splitOn "\n")[0]!
226-
let deprecation ← mkDeprecationWithDate deletionDate comment
226+
let deletionDate := log'.lines.first?.get!
227+
let deprecation ← mkDeprecationWithDate deletionDate.toString comment
227228
msgs := msgs.push ""
228229
-- Retrieve the final version of the file, before it was deleted.
229230
let file ← runCmd s!"git show {modifiedHash}:{fname}"
@@ -233,7 +234,7 @@ def deprecateFilePath (fname : String) (rename comment : Option String) :
233234
let modName := mkModName rename
234235
pure s!"import {modName}"
235236
| none => getHeader fname file false
236-
let deprecatedFile := s!"{fileHeader.trimRight}\n\n{deprecation.pretty.trimRight}\n"
237+
let deprecatedFile := s!"{fileHeader.trimAsciiEnd}\n\n{deprecation.pretty.trimAsciiEnd}\n"
237238
msgs := msgs.push <| .trace {cls := `Deprecation} m!"{fname}" #[m!"\n{deprecatedFile}"]
238239
return (msgs, deprecatedFile)
239240

@@ -300,10 +301,10 @@ elab tk:"#find_deleted_files" nc:(ppSpace num)? pct:(ppSpace num)? bang:&"%"? :
300301
-- (throwing an error if that doesn't exist).
301302
let getHashAndMessage (n : Nat) : CommandElabM (String × MessageData) := do
302303
let log ← runCmd s!"git log --pretty=oneline -{n}"
303-
let some last := log.trim.splitOn "\n" |>.getLast? | throwError "Found no commits!"
304-
let commitHash := last.takeWhile (.isWhitespace)
305-
let PRdescr := (last.drop commitHash.length).trim
306-
return (commitHash, .trace {cls := `Commit} m!"{PRdescr}" #[m!"{commitHash}"])
304+
let some last := log.lines.toList.getLast? | throwError "Found no commits!"
305+
let commitHash := last.takeWhile (fun c : Char ↦ !c.isWhitespace)
306+
let PRdescr := (last.dropWhile (fun c : Char ↦ !c.isWhitespace)).trimAscii
307+
return (commitHash.toString, .trace {cls := `Commit} m!"{PRdescr}" #[m!"{commitHash}"])
307308
let getFilesAtHash (hash : String) : CommandElabM (Std.HashSet String) := do
308309
let files ← runCmd s!"git ls-tree -r --name-only {hash} Mathlib/"
309310
return .ofList <| files.splitOn "\n"
@@ -329,10 +330,10 @@ elab tk:"#find_deleted_files" nc:(ppSpace num)? pct:(ppSpace num)? bang:&"%"? :
329330
for fname in onlyPastFiles do
330331
let fnameStx := Syntax.mkStrLit fname
331332
let stx ← if let some newName := dict[fname]? then
332-
let newNameStx := Syntax.mkStrLit newName
333-
`(command|#create_deprecated_module $fnameStx rename_to $newNameStx)
334-
else
335-
`(command|#create_deprecated_module $fnameStx)
333+
let newNameStx := Syntax.mkStrLit newName
334+
`(command|#create_deprecated_module $fnameStx rename_to $newNameStx)
335+
else
336+
`(command|#create_deprecated_module $fnameStx)
336337
suggestions := suggestions.push {
337338
suggestion := (⟨stx.raw.updateTrailing "hello".toRawSubstring⟩ : TSyntax `command)
338339
}
@@ -372,6 +373,7 @@ the deprecations later on.
372373
-/
373374

374375
#find_deleted_files 0
376+
375377
/--
376378
info: import Mathlib.Tactic.Linter.DeprecatedModule
377379
import Std.Time.Zoned

0 commit comments

Comments
 (0)