Description
In ProbeLean/Verify.lean, the pathsMatch function uses String.endsWith without a directory boundary guard:
def pathsMatch (path1 : String) (path2 : String) : Bool :=
path1 == path2 ||
path1.endsWith path2 ||
path2.endsWith path1 ||
normalizePathForMatch path1 == normalizePathForMatch path2
Example: pathsMatch "ATest.lean" "Test.lean" returns true even though they are different files. This could cause sorry warnings from one file to be incorrectly attributed to atoms in another file with a similar-suffix name.
Suggested Fix
Check for a path separator before the suffix match:
path1.endsWith ("/" ++ path2) || path1 == path2
Description
In
ProbeLean/Verify.lean, thepathsMatchfunction usesString.endsWithwithout a directory boundary guard:Example:
pathsMatch "ATest.lean" "Test.lean"returnstrueeven though they are different files. This could cause sorry warnings from one file to be incorrectly attributed to atoms in another file with a similar-suffix name.Suggested Fix
Check for a path separator before the suffix match:
path1.endsWith ("/" ++ path2) || path1 == path2