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

fix: mk_all ignores locally removed files #11850

Closed
wants to merge 1 commit into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 2, 2024

@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.


Open in Gitpod

@YaelDillies
Copy link
Collaborator

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
Copy link
Collaborator Author

adomani commented Apr 2, 2024

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
Copy link
Collaborator

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
Copy link
Collaborator Author

adomani commented Apr 2, 2024

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 grunweg added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 24, 2024
@grunweg
Copy link
Collaborator

grunweg commented May 24, 2024

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
Copy link
Collaborator

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

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 24, 2024
@grunweg
Copy link
Collaborator

grunweg commented May 31, 2024

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

@YaelDillies
Copy link
Collaborator

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

@adomani adomani added the WIP Work in progress label Jul 2, 2024
@adomani
Copy link
Collaborator Author

adomani commented Jul 2, 2024

@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
Copy link
Collaborator

Yes, let's close this PR

@YaelDillies YaelDillies closed this Jul 2, 2024
@YaelDillies YaelDillies deleted the adomani/mk_all_erases_locally_deleted_files branch July 2, 2024 18:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
WIP Work in progress
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants