fix: mk_all ignores locally removed files

[adomani]

@YaelDillies pointed out that their preference was to exclude files that are removed, but not yet staged.

From the point of view of CI, the change should be invisible, since CI acts on an unmodified branch.

---

[YaelDillies]

Maybe this could be a flag to the command? Namely ./scripts/mk_all.sh takes unstaged changed into account, but .scripts/mk_all.sh --ignore-unstaged ignores them.

I also wonder whether we could write the script in Lean so that any downstream project can create their all file as lake exe mk-all.

[adomani]

I can easily implement the flag. As for writing the function in Lean, this is a first possibility:

def mkAll (mathlib : String := "Mathlib") : IO Unit := do
  let pth ← System.FilePath.walkDir mathlib
  let files := (pth.filter (·.extension == some "lean")).qsort (·.toString < ·.toString)
  let withImport ← files.mapM fun f => do
    return "import " ++ (← Lean.moduleNameOfFileName f none).toString
  IO.FS.writeFile (mathlib ++ ".lean") (String.intercalate "\n" withImport.toList)

After that, running #eval mkAll would create the Mathlib.lean file with all the imports.

However, all really means all (.lean) files in the Mathlib folder, whether or not they are in the output of git ls-files or not. I asked a question about running git ls-files from Lean here.

EDIT: this is a way of getting git ls-files to work "in Lean".

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

open Lean System.FilePath in
def mkAll (ml : String := "Mathlib") : IO Unit := 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
  IO.FS.writeFile ml.lean <| ("\n".intercalate withImport.toList).push '\n'

[YaelDillies]

Given that Lean libraries aren't necessarily backed by a git repository, so I think not using the information from git is the correct default behaviour. You could recover the current behaviour by adding a --git flag to get the information from git.

[adomani]

I am implementing the simple version of the mk_all script at #11853. There, you can find the flag:

-- use git
run_cmd mkAll (git? := true) (cands := candidates)

-- recurse into dirs
run_cmd mkAll (git? := false) (cands := candidates)

(The argument are actually not optional, but the explicit labels make them clearer, I hope!)

[grunweg]

Let's mark this as blocked on #11853 (which has been approved, but not yet merged) --- that PR would certainly fix the issue this is solving.

[YaelDillies]

I believe this PR could simply be closed since we will soon remove ./scripts/mk_all.sh entirely

[grunweg]

Since #11853 has landed, this PR can be closed, right?

[YaelDillies]

I think we should just delete mk_all.sh now, yes

[adomani]

@YaelDillies should I deleteclose this PR? Is there some extra functionality that you would like lake exe mk_all to have that should be rescued from here?

If you are ok with closing, feel free to do so yourself as well!

[YaelDillies]

Yes, let's close this PR