DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Update meta programs

Browse source
This commit is contained in:
jstoobysmith 2024-09-04 08:20:10 -04:00
parent fccb283a5c
commit bbe507360e
5 changed files with 221 additions and 124 deletions
Download patch file Download diff file Expand all files Collapse all files

28
HepLean/Meta/AllFilePaths.lean Normal file
View file

@ -0,0 +1,28 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Batteries.Lean.HashSet
import Lean
/-!
## Getting an array of all file paths in HepLean.
-/
open Lean Elab System
/-! TODO: Make this definition more functional in style. -/
/-- Gets an array of all file paths in `HepLean`. -/
partial def allFilePaths : IO (Array FilePath) := do
go (#[] : Array FilePath) `HepLean ("./HepLean" : FilePath)
where go prev root path := do
let mut r := prev
for entry in ← path.readDir do
if ← entry.path.isDir then
r ← go r (root.mkStr entry.fileName) entry.path
else
r := r.push (root.toString.replace "." "/" ++ "/" ++ entry.fileName)
pure r

119
HepLean/Meta/TransverseTactics.lean Normal file
View file

@ -0,0 +1,119 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Batteries.Lean.HashSet
import Lean
import HepLean.Meta.AllFilePaths
/-!
This file enables us to transverse tactics and test for conditions.
## References
The content of this file is based on the following sources (released under the Apache 2.0 license):
- https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
- https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
Modifications have been made to the original content of these files here.
See also:
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
-/
open Lean Elab System
namespace transverseTactics
partial def processCommands : Frontend.FrontendM (List (Environment × InfoState)) := do
/- Very roughly, `Frontend.FrontendM (List (Environment × InfoState))` is equivalent
to `Frontend.Context → Frontend.state → List (Environment × InfoState)`.
The `←get` here is returning the inputted value of `Frontend.state`,
from which we get the enviroment.
-/
let env := (←get).commandState.env
/- Processes a single command, adding it to `env`. This is done using
`modify fun s => { s with commands := s.commands.push cmd }` as part of
`Frontend.processCommand`. -/
let done ← Frontend.processCommand
/- Gets the updated `Frontend.state`. -/
let st := ← get
/- Gets the infostate associated with the single command. -/
let infoState := st.commandState.infoState
set {st with commandState := {st.commandState with infoState := {}}}
if done
then return [(env, infoState)]
else
/- For each command, we return the enviroment before the command is processed,
and the `infoState` associated with that command. -/
return (env, infoState) :: (←processCommands)
def visitInfo (file : FilePath) (env : Environment)
(visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) (ci : ContextInfo)
(info : Info) (acc : List (IO Unit)) : List (IO Unit) :=
match info with
| .ofTacticInfo ti =>
(ci.runMetaM default
(do setEnv env
try visitTacticInfo file ci ti
catch e =>
println! "caught: {←e.toMessageData.toString}")) :: acc
| _ => acc
def traverseForest (file : FilePath)
(visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit)
(steps : List (Environment × InfoState)) : List (IO Unit) :=
let t := steps.map fun (env, infoState) ↦
(infoState.trees.toList.map fun t ↦
(Lean.Elab.InfoTree.foldInfo (visitInfo file env visitTacticInfo) [] t).reverse)
t.join.join
end transverseTactics
open transverseTactics in
unsafe def transverseTactics (file : FilePath)
(visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) : IO Unit := do
searchPathRef.set compile_time_search_path%
/- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`. -/
let fileContent ← IO.FS.readFile file
enableInitializersExecution
/- Get `Parser.InputContext` from file. -/
let inputCtx := Parser.mkInputContext fileContent file.toString -- The input content of the file
/- We parse the header. Recall that the parser is takes a string and
outputs a Lean syntax object. -/
let (header, parserState, messages) ← Parser.parseHeader inputCtx
/- Recall that the elborator turns a Lean syntax object into a Lean Expr object.
In the below, we process the header, creating an enviroment with the relevent imports.
This can be thought of as creating an import only file. -/
if messages.hasErrors then
for msg in messages.toList do
if msg.severity == .error then
println! "ERROR: {← msg.toString}"
throw $ IO.userError "Errors during import; aborting"
for msg in messages.toList do
println! "{← msg.toString}"
let (env, messages) ← processHeader header {} messages inputCtx
if messages.hasErrors then
for msg in messages.toList do
if msg.severity == .error then
println! "ERROR: {← msg.toString}"
throw $ IO.userError "Errors during import; aborting"
/- As part of the enviroment header is the module name. This is not included
in our current `env`. So we include it now. -/
let env1 := env.setMainModule (← moduleNameOfFileName file none)
/- From the enviroment, we create a state of the `Command` monad. -/
let commandState := {Command.mkState env1 messages {} with infoState.enabled := true}
/- We create a state of the `Frontend` monad-/
/- Runs the `processCommands` function on the context defined by `inputCtx`, and the
state defined by `frontendState`. -/
let (steps, _frontendState) ← (processCommands.run { inputCtx := inputCtx }).run
{ commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
/- Note that for us, each `infoState.trees` is actually of length 1. -/
for t in traverseForest file visitTacticInfo steps do
try t
catch e =>
println! "caught top level: {e}"
pure ()

4
lakefile.toml
View file

@ -60,6 +60,10 @@ srcDir = "scripts"
name = "stats"
srcDir = "scripts"
[[lean_exe]]
name = "free_simps"
srcDir = "scripts/MetaPrograms"
# -- Optional inclusion of openAI_doc_check. Needs `llm` above.
#[[lean_exe]]
#name = "openAI_doc_check"

127
scripts/MetaPrograms/check_rfl.lean
View file

@ -5,49 +5,17 @@ Authors: Joseph Tooby-Smith
-/
import Batteries.Lean.HashSet
import Lean
import HepLean.Meta.AllFilePaths
import HepLean.Meta.TransverseTactics
/-!
This file produces a list of places where `rfl` will complete the goal.
## References
The content of this file is based on the following sources (released under the Apache 2.0 license):
- https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
- https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
Modifications have been made to the original content of these files here.
See also:
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
-/
open Lean Elab System
partial def processCommands : Frontend.FrontendM (List (Environment × InfoState)) := do
/- Very roughly, `Frontend.FrontendM (List (Environment × InfoState))` is equivalent
to `Frontend.Context → Frontend.state → List (Environment × InfoState)`.
The `←get` here is returning the inputted value of `Frontend.state`,
from which we get the enviroment.
-/
let env := (←get).commandState.env
/- Processes a single command, adding it to `env`. This is done using
`modify fun s => { s with commands := s.commands.push cmd }` as part of
`Frontend.processCommand`. -/
let done ← Frontend.processCommand
/- Gets the updated `Frontend.state`. -/
let st := ← get
/- Gets the infostate associated with the single command. -/
let infoState := st.commandState.infoState
set {st with commandState := {st.commandState with infoState := {}}}
if done
then return [(env, infoState)]
else
/- For each command, we return the enviroment before the command is processed,
and the `infoState` associated with that command. -/
return (env, infoState) :: (←processCommands)
namespace Lean.Elab.TacticInfo
def name? (t : TacticInfo) : Option Name :=
@ -73,7 +41,6 @@ def isSubstantive (t : TacticInfo) : Bool :=
| some ``Lean.Parser.Tactic.exact => false
| _ => true
end Lean.Elab.TacticInfo
def visitTacticInfo (file : FilePath) (ci : ContextInfo) (ti : TacticInfo) : MetaM Unit := do
@ -105,94 +72,6 @@ def visitTacticInfo (file : FilePath) (ci : ContextInfo) (ti : TacticInfo) : Met
pure ()
pure ()
def visitInfo (file : FilePath) (env : Environment) (ci : ContextInfo)
(info : Info) (acc : List (IO Unit))
: List (IO Unit) :=
match info with
| .ofTacticInfo ti =>
(ci.runMetaM default
(do setEnv env
try visitTacticInfo file ci ti
catch e =>
println! "caught: {←e.toMessageData.toString}")) :: acc
| _ => acc
def traverseForest (file : FilePath) (steps : List (Environment × InfoState)) : List (IO Unit) :=
let t := steps.map fun (env, infoState) ↦
(infoState.trees.toList.map fun t ↦
(Lean.Elab.InfoTree.foldInfo (visitInfo file env) [] t).reverse)
t.join.join
unsafe def checkRfl (file : FilePath) : IO Unit := do
searchPathRef.set compile_time_search_path%
/- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`. -/
let fileContent ← IO.FS.readFile file
enableInitializersExecution
/- Get `Parser.InputContext` from file. -/
let inputCtx := Parser.mkInputContext fileContent file.toString -- The input content of the file
/- We parse the header. Recall that the parser is takes a string and
outputs a Lean syntax object. -/
let (header, parserState, messages) ← Parser.parseHeader inputCtx
/- Recall that the elborator turns a Lean syntax object into a Lean Expr object.
In the below, we process the header, creating an enviroment with the relevent imports.
This can be thought of as creating an import only file. -/
if messages.hasErrors then
for msg in messages.toList do
if msg.severity == .error then
println! "ERROR: {← msg.toString}"
throw $ IO.userError "Errors during import; aborting"
for msg in messages.toList do
println! "{← msg.toString}"
let (env, messages) ← processHeader header {} messages inputCtx
if messages.hasErrors then
for msg in messages.toList do
if msg.severity == .error then
println! "ERROR: {← msg.toString}"
throw $ IO.userError "Errors during import; aborting"
/- As part of the enviroment header is the module name. This is not included
in our current `env`. So we include it now. -/
let env1 := env.setMainModule (← moduleNameOfFileName file none)
/- From the enviroment, we create a state of the `Command` monad. -/
let commandState := {Command.mkState env1 messages {} with infoState.enabled := true}
/- We create a state of the `Frontend` monad-/
/- Runs the `processCommands` function on the context defined by `inputCtx`, and the
state defined by `frontendState`. -/
let (steps, _frontendState) ← (processCommands.run { inputCtx := inputCtx }).run
{ commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
/- Note that for us, each `infoState.trees` is actually of length 1. -/
for t in traverseForest file steps do
try t
catch e =>
println! "caught top level: {e}"
pure ()
/-- Recursively finds files in directory. -/
partial def addModulesIn (recurse : Bool) (prev : Array FilePath) (root : Name := .anonymous)
(path : FilePath) : IO (Array FilePath) := do
let mut r := prev
let rootStr := root.toString.replace "." "/"
for entry in ← path.readDir do
if ← entry.path.isDir then
if recurse then
r ← addModulesIn recurse r (root.mkStr entry.fileName) entry.path
else
r := r.push (rootStr ++ "/" ++ entry.fileName)
pure r
/-- Compute imports expected by `HepLean.lean` by looking at file structure. -/
def allFilePaths : IO (Array FilePath) := do
let mut needed := #[]
for top in ← FilePath.readDir "HepLean" do
let nm := `HepLean
let rootname := FilePath.withExtension top.fileName ""
let root := nm.mkStr rootname.toString
if ← top.path.isDir then
needed ← addModulesIn (recurse := true) needed (root := root) top.path
else
needed := needed
pure needed
/- See conversation here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E -/
unsafe def processAllFiles : IO Unit := do
@ -209,5 +88,5 @@ unsafe def processAllFiles : IO Unit := do
unsafe def main (args : List String) : IO Unit := do
match args with
| [path] => checkRfl path
| [path] => transverseTactics path visitTacticInfo
| _ => processAllFiles

67
scripts/MetaPrograms/free_simps.lean Normal file
View file

@ -0,0 +1,67 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Batteries.Lean.HashSet
import Batteries.Data.String.Matcher
import Lean
import HepLean.Meta.AllFilePaths
import HepLean.Meta.TransverseTactics
/-!
This file checks for non-terminating `simp` tactics which do not appear as `simp only`.
See also:
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
-/
open Lean Elab System
namespace Lean.Elab.TacticInfo
def name? (t : TacticInfo) : Option Name :=
match t.stx with
| Syntax.node _ n _ => some n
| _ => none
/-- Decide whether a tactic is "substantive",
or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
def isSimp (t : TacticInfo) : Bool :=
match t.name? with
| some ``Lean.Parser.Tactic.simp => true
| _ => false
end Lean.Elab.TacticInfo
def visitTacticInfo (file : FilePath) (ci : ContextInfo) (ti : TacticInfo) : MetaM Unit := do
if not ti.isSimp then return ()
let stx := ti.stx
match stx.getHeadInfo? with
| .some (.synthetic ..) =>
-- Not actual concrete syntax the user wrote. Ignore.
return ()
| _ => pure ()
let some sp := stx.getPos? | return ()
let startPosition := ci.fileMap.toPosition sp
let some ep := stx.getTailPos? | return ()
let s := Substring.mk ci.fileMap.source sp ep
if ti.goalsAfter.length ≠ 0 ∧ ¬ String.containsSubstr s.toString "only" then
println! "./{file}:{startPosition.line}"
/- See conversation here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E -/
unsafe def processAllFiles : IO Unit := do
let files ← allFilePaths
let tasks := files.map fun f =>
((IO.asTask $ IO.Process.run
{cmd := "lake", args := #["exe", "free_simps", f.toString]}), f)
tasks.toList.enum.forM fun (n, (t, path)) => do
println! "{n} of {tasks.toList.length}: {path}"
let tn ← IO.wait (← t)
match tn with
| .ok x => println! x
| .error _ => println! "Error"
unsafe def main (args : List String) : IO Unit := do
match args with
| [path] => transverseTactics path visitTacticInfo
| _ => processAllFiles