A/B/C.lean and A/C/B.lean

Stream: mathlib4

[Johan Commelin]

Kevin Buzzard said:

Do we have any more pairs of files called A/B/C.lean and A/C/B.lean??

I just ran a quick check, and I think the answer is "no".

[Johan Commelin]

#!/usr/bin/env bash


# Find all directories
directories=$(find . -type d | sed 's|^\./||')

# Loop through each directory
for dir in $directories; do
  # Extract the base name of the directory
  base_name=$(basename $dir)
  # Extract the parent directory
  parent_dir=$(dirname $dir)
  # Extract the grandparent directory
  grandparent_dir=$(dirname $parent_dir)

  # Skip if parent_dir is '.'
  if [[ $parent_dir == "." ]]; then
    continue
  fi

  # Check if the directory matches the pattern */A/B
  if [[ -d "$parent_dir" && -d "$grandparent_dir/$base_name/$parent_dir" ]]; then
    echo "Match found: $dir and $grandparent_dir/$base_name/$parent_dir"
  fi
done

[Damiano Testa]

I actually found

Mathlib/Data/Finite/Set.lean
Mathlib/Data/Set/Finite.lean

Mathlib/Algebra/BigOperators/Module.lean
Mathlib/Algebra/Module/BigOperators.lean

Mathlib/CategoryTheory/Limits/MorphismProperty.lean
Mathlib/CategoryTheory/MorphismProperty/Limits.lean

plus some close calls whose "A" is not identical.

[Damiano Testa]

This is the script that I used:

while read -r first second
do
  printf '* %s, %s\n' "$first" "$second"
  git ls-files | grep "\b\($first/$second.lean\|$second/$first.lean\)"
done < <(
  comm -12 <(
    git ls-files '*.lean' |
      awk -F'/' '{ gsub(/\.lean$/, ""); print $(NF-1), $NF }' | sort) <(
    git ls-files '*.lean' |
      awk -F'/' '{ gsub(/\.lean$/, ""); print $NF, $(NF-1) }' | sort))

[Johan Commelin]

Hah! I don't know why my script failed to find them...

[Johan Commelin]

Anyway, I think all three of them are probably good targets for merging.

[Damiano Testa]

I think that your directories contains A/B, but not C.lean? As in, I think that they really are directories and I cannot see if you then list the content of each one of them later on...

[Johan Commelin]

aah, of course :man_facepalming: