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

feat: Fix free_simps

Browse source
This commit is contained in:
jstoobysmith 2025-03-10 13:07:07 +00:00
parent 5530a33d27
commit f50c0383fe
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/MetaPrograms/free_simps.lean
View file

@ -64,7 +64,7 @@ unsafe def processAllFiles : IO Unit := do
let tasks := files.map fun f => let tasks := files.map fun f =>
((IO.asTask $ IO.Process.run ((IO.asTask $ IO.Process.run
{cmd := "lake", args := #["exe", "free_simps", f.toString]}), f) {cmd := "lake", args := #["exe", "free_simps", f.toString]}), f)
tasks.toList.enum.forM fun (n, (t, path)) => do tasks.toList.zipIdx.forM fun ((t, path), n) => do
let tn ← IO.wait (← t) let tn ← IO.wait (← t)
match tn with match tn with
| .ok x => | .ok x =>
@ -87,7 +87,7 @@ unsafe def processFileArray (files : Array FilePath) : IO Unit := do
let tasks := files.map fun f => let tasks := files.map fun f =>
((IO.asTask $ IO.Process.run ((IO.asTask $ IO.Process.run
{cmd := "lake", args := #["exe", "free_simps","-file", f.toString]}), f) {cmd := "lake", args := #["exe", "free_simps","-file", f.toString]}), f)
tasks.toList.enum.forM fun (n, (t, path)) => do tasks.toList.zipIdx.forM fun ((t, path), n) => do
let tn ← IO.wait (← t) let tn ← IO.wait (← t)
match tn with match tn with
| .ok x => | .ok x =>