From 1ea200b2d9ba327d9e79e3731d64710695b32735 Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 29 May 2024 17:17:45 +0000 Subject: [PATCH] feat: `lake exe mk_all` as a Lean executable (#11853) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies --- lakefile.lean | 5 ++ scripts/mk_all.lean | 113 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 118 insertions(+) create mode 100644 scripts/mk_all.lean diff --git a/lakefile.lean b/lakefile.lean index cf31e9282deef..f01e781c5b81f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -56,6 +56,11 @@ lean_exe checkYaml where srcDir := "scripts" supportInterpreter := true +/-- `lake exe mk_all` constructs the files containing all imports for a project. -/ +lean_exe mk_all where + srcDir := "scripts" + supportInterpreter := true + /-- `lake exe shake` checks files for unnecessary imports. -/ lean_exe shake where root := `Shake.Main diff --git a/scripts/mk_all.lean b/scripts/mk_all.lean new file mode 100644 index 0000000000000..be8131e1d777b --- /dev/null +++ b/scripts/mk_all.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2024 Yaël Dillies, Damiano Testa. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yaël Dillies, Damiano Testa +-/ +import Cli.Basic +import Lean.Util.Path +import Lake.CLI.Main + +/-! +# Script to create a file importing all files from a folder + +This file declares a command to gather all Lean files from a folder into a single Lean file. + +TODO: +`getLeanLibs` contains a hard-coded choice of which dependencies should be built and which ones +should not. Could this be made more structural and robust, possibly with extra `Lake` support? +-/ + +open Lean System.FilePath + +/-- `getAll git ml` takes all `.lean` files in the dir `ml` (recursing into sub-dirs) and +returns the `Array` of `String`s +``` +#[file₁, ..., fileₙ] +``` +where each `fileᵢ` is of the form `"Mathlib.Algebra.Algebra.Basic"`. + +The input `git` is a `Bool`ean flag: +* `true` means that the command uses `git ls-files` to find the relevant files; +* `false` means that the command recursively scans all dirs searching for `.lean` files. +-/ +def getAll (git : Bool) (ml : String) : IO (Array String) := do + let ml.lean := addExtension ⟨ml⟩ "lean" -- for example, `Mathlib.lean` + let allModules : Array System.FilePath ← (do + if git then + let mlDir := ml.push pathSeparator -- for example, `Mathlib/` + let allLean ← IO.Process.run { cmd := "git", args := #["ls-files", mlDir ++ "*.lean"] } + return (((allLean.dropRightWhile (· == '\n')).splitOn "\n").map (⟨·⟩)).toArray + else do + let all ← walkDir ml + return all.filter (·.extension == some "lean")) + let files := (allModules.erase ml.lean).qsort (·.toString < ·.toString) + let withImport ← files.mapM fun f => do + -- this check is helpful in case the `git` option is on and a local file has been removed + if ← pathExists f then + return (← moduleNameOfFileName f none).toString + else return "" + return withImport.filter (· != "") + +open Lake in +/-- `getLeanLibs` returns the names (as an `Array` of `String`s) of all the libraries +on which the current project depends. +If the current project is `mathlib`, then it excludes the libraries `Cache` and `LongestPole` and +it includes `Mathlib/Tactic`. -/ +def getLeanLibs : IO (Array String) := do + let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall? + let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? } + let ws ← MonadError.runEIO (MainM.runLogIO (loadWorkspace config)).toEIO + let package := ws.root + let libs := (package.leanLibs.map (·.name)).map (·.toString) + return if package.name == `mathlib then + libs.erase "Cache" |>.erase "LongestPole" |>.push ("Mathlib".push pathSeparator ++ "Tactic") + else + libs + +open IO.FS IO.Process Name Cli in +/-- Implementation of the `mk_all` command line program. +The exit code is the number of files that the command updates/creates. -/ +def mkAllCLI (args : Parsed) : IO UInt32 := do + -- Check whether the `--git` flag was set + let git := (args.flag? "git").isSome + -- Check whether the `--lib` flag was set. If so, build the file corresponding to the library + -- passed to `--lib`. Else build all the libraries of the package. + -- If the package is `mathlib`, then it removes the libraries `Cache` and `LongestPole` and it + -- adds `Mathlib/Tactic`. + let libs := ← match args.flag? "lib" with + | some lib => return #[lib.as! String] + | none => getLeanLibs + let mut updates := 0 + for d in libs.reverse do -- reverse to create `Mathlib/Tactic.lean` before `Mathlib.lean` + let fileName := addExtension d "lean" + let allFiles ← getAll git d + let fileContent := ("\n".intercalate (allFiles.map ("import " ++ ·)).toList).push '\n' + if !(← pathExists fileName) then + IO.println s!"Creating '{fileName}'" + updates := updates + 1 + IO.FS.writeFile fileName fileContent + else if (← IO.FS.readFile fileName) != fileContent then + IO.println s!"Updating '{fileName}'" + updates := updates + 1 + IO.FS.writeFile fileName fileContent + if updates == 0 then + IO.println "No update necessary" + return updates + +open Cli in +/-- Setting up command line options and help text for `lake exe mk_all`. -/ +def mkAll : Cmd := `[Cli| + mk_all VIA mkAllCLI; ["0.0.1"] + "Generate a file importing all the files of a Lean folder. \ + By default, it generates the files for the Lean libraries of the package.\ + In the case of `Mathlib`, it removes the libraries `Cache` and `LongestPole`\ + and it adds `Mathlib/Tactic`. \ + If you are working in a project downstream of mathlib, use `lake exe mk_all --lib MyProject`." + + FLAGS: + lib : String; "Create a folder importing all Lean files from the specified library/subfolder." + git; "Use the folder content information from git." +] + +/-- The entrypoint to the `lake exe mk_all` command. -/ +def main (args : List String) : IO UInt32 := mkAll.validate args