diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index ed207066b1..c01aae4a70 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/src/lake/Lake/Load/Materialize.lean @@ -45,6 +45,7 @@ def updateGitRepo (repo : GitRepo) (url : String) (rev? : Option String) (name : String) : LogIO Unit := do let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do let some remoteUrl ← repo.getRemoteUrl? | return false + if remoteUrl = url then return true return (← IO.FS.realPath remoteUrl) = (← IO.FS.realPath url) if sameUrl then updateGitPkg repo rev? name diff --git a/src/lake/tests/clone/test.sh b/src/lake/tests/clone/test.sh index cb92251121..d1da54ad3a 100755 --- a/src/lake/tests/clone/test.sh +++ b/src/lake/tests/clone/test.sh @@ -20,12 +20,22 @@ git add --all git commit -m "initial commit" popd +HELLO_URL="file://$(pwd)/hello" + cd test +$LAKE -R -Kurl="$HELLO_URL" update +# test that a second `lake update` is a no-op (with URLs) +# see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901 +$LAKE -R -Kurl="$HELLO_URL" update | diff - /dev/null +rm -rf lake-packages + # Test that Lake produces no warnings on a `lake build` after a `lake update` # See https://github.com/leanprover/lean4/issues/2427 -$LAKE update +$LAKE -R update +# test that a second `lake update` is a no-op (with file paths) +$LAKE -R update | diff - /dev/null test -d lake-packages/hello # test that Lake produces no warnings $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null