Skip to content

Commit 6c62f09

Browse files
fix: don't run 'lake update subverso' in IO example projects
The temporary project generated for an IO example does not depend on SubVerso, so there is nothing to update. Recent versions of Lake reject updating a package that the project does not require.
1 parent 755ccbe commit 6c62f09

1 file changed

Lines changed: 0 additions & 5 deletions

File tree

  • src/verso-manual/VersoManual/InlineLean

src/verso-manual/VersoManual/InlineLean/IO.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -428,11 +428,6 @@ meta def check
428428
logErrorAt (loc (some o)) s!"Output file {f} mismatch. Got:\n{contents}"
429429
else Lean.logError s!"Output file {f} not found"
430430

431-
let out ← IO.Process.output {cmd := "lake", args := #["update", "subverso"], cwd := some dirname}
432-
if out.exitCode != 0 then
433-
throwError
434-
m!"When running 'lake update subverso' in {dirname}, the exit code was {out.exitCode}\n" ++
435-
m!"Stderr:\n{out.stderr}\n\nStdout:\n{out.stdout}\n\n"
436431
let jsonFile := s!"{leanCodeName}.json"
437432
let out ← IO.Process.output {cmd := toString «subverso-extract-mod» , args := #[leanCodeName, jsonFile], cwd := some dirname}
438433
if out.exitCode != 0 then

0 commit comments

Comments
 (0)