Skip to content

Commit

Permalink
feat: mk_all script implemented in Lean
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani authored and grunweg committed May 31, 2024
1 parent 86ab5d5 commit e5bf1a7
Showing 1 changed file with 45 additions and 0 deletions.
45 changes: 45 additions & 0 deletions scripts/mkAll.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
/-
Copyright (c) 2024 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import Lean.Util.Path

/-!
# An implementation of the `mk_all.sh` script in Lean
-/

namespace Mathlib.mkAll

/-- the command `git ls-files '*.lean'` -/
def gitLSFiles : IO.Process.SpawnArgs where
cmd := "git"
args := #["ls-files", "*.lean"]

open Lean System.FilePath in
/-- `getAll str` takes all Git-managed `.lean` files in the repository in the dir `str` and
returns the string
```
import file₁
...
import fileₙ
```
The string `str` is optional and the stript defaults to `Mathlib` if unprovided. -/
def getAll (ml : String := "Mathlib") : IO String := do
let ml.lean := addExtension ⟨ml⟩ "lean" -- `Mathlib.lean`
let mlDir := ml.push pathSeparator -- `Mathlib/`
let allLean ← IO.Process.run gitLSFiles
let files : List System.FilePath := ((allLean.splitOn "\n").filter mlDir.isPrefixOf).map (⟨·⟩)
let files := (files.erase ml.lean).toArray.qsort (·.toString < ·.toString)
let withImport ← files.mapM fun f => return "import " ++ (← moduleNameOfFileName f none).toString
return ("\n".intercalate withImport.toList).push '\n'

/-- the "Mathlib usual suspects" for "import all" files. -/
abbrev candidates := #["Mathlib", "MathlibExtras", "Mathlib/Tactic", "Counterexamples", "Archive"]

open System.FilePath in
/-- running `#eval mkAll arr` creates an "import all" file for each of the roots in the array `arr`.
The input `arr` is optional and `mkAll` defaults to using `candidates`, if unprovided. -/
def mkAll (cands : Array String := candidates) : IO Unit := do
for d in cands do
IO.FS.writeFile (addExtension ⟨d⟩ "lean") (← getAll d)

0 comments on commit e5bf1a7

Please sign in to comment.