Add SearchDependRecursive command for transitive dependency analysis

[JasonGross]

This commit adds a new SearchDependRecursive command that extends the existing SearchDepend functionality by recursively collecting all transitive dependencies of a given definition, rather than just the immediate dependencies.

Changes:

• Add collect_dependance_recursive function with cycle detection
• Add display_dependance_recursive to display recursive dependencies
• Refactor common display logic into display_data function
• Add SearchDependRecursive Vernac command
• Add test cases in tests/search_recursive.cmd and tests/search_comparison.cmd

🤖 Generated with Claude Code

[ybertot]

Thanks, this is a nice extension to the SearchDepend command. But I am puzzled, what is the use case?
The SearchDepend command itself is not documented. It was included only as a way to test quickly that dependency search works correctly.

The intended usage was to produce direct dependencies in a dpd file, and then to analyse this dependency file with independent Ocaml code. so why should we add yet another undocumented command in the package?

[JasonGross]

Oh, I was missing Print DependGraph (I'd only ever used FileDependGraph), I guess I can get the information I need from the .dpd file; the weight is the count of how many times the lemma is used?

[ybertot]

If you use Print DependGraph the symbols listed with the N: header in the generated file are all the symbols your code depends on recursively. For the weight, I just reverse engineered the code and it seems to be the number of occurrences of the target symbol in the type and body of the source symbol. I don't find it very meaningful.