PR reviews

Stream: PhysLean

[Joseph Tooby-Smith]

This is a thread similar to the #**PR reviews> channel for Mathlib, where one can discuss PR reviews for PhysLean or ping people for reviews.

[Joseph Tooby-Smith]

From my side, I have this PR open PhysLean#952 on integrals and measures on Space d, which needs a review.

[Gregory Loges]

I have opened PhysLean#957 (SpaceDHilbertSpace and UnboundedOperator) for review since I won't be able to continue with this until next week or so and I am at a point where everything is currently sorry-free. I am still a lean beginner, so please let me know if there's anything I can do to improve "meta" lean things like naming conventions for lemmas, use of namespaces and introduction of global variables.

[Daniel Morrison]

I'll try to take a look at these in the next couple days.

[Joseph Tooby-Smith]

Thanks for posting this here @Gregory Loges ! I got busy so didn't get time to look over your PR again.

[Joseph Tooby-Smith]

This documentation-only PR needs reviewing PhysLean#959

[Daniel Morrison]

Reviewed PhysLean#952 @Joseph Tooby-Smith and PhysLean#957 @Gregory Loges

[Joseph Tooby-Smith]

Vibe coded a PR tracker for the PhysLean website: https://physlean.com/PRTracker.html

[Shlok Vaibhav]

Joseph Tooby-Smith said:

Vibe coded a PR tracker for the PhysLean website: https://physlean.com/PRTracker.html

Just wondering, will it be good to have a claude.md file for the project that can help everyone using assistants to use as a guideline and guardrails to be followed for PhysLean codes and actions? Also, curious about what recommended review plugins are run on llm generated code for PhysLean?

[Joseph Tooby-Smith]

Just wondering, will it be good to have a claude.md file for the project that can help everyone using assistants to use as a guideline and guardrails to be followed for PhysLean codes and actions?

Maybe, but I think I personally would prefer it to be housed not in the main PhysLean repo but either on the website or in its own repo.

Also, curious about what recommended review plugins are run on llm generated code for PhysLean?

I don't think I understand your question properly: But let me state, LLM generated code for the main PhysLean repo goes through the same human review as any other code. The PhysLean website repo is not currently held to the same standard (but maybe it should be).

Are review plugins some specific tool on GitHub?

[Shlok Vaibhav]

Joseph Tooby-Smith said:

Just wondering, will it be good to have a claude.md file for the project that can help everyone using assistants to use as a guideline and guardrails to be followed for PhysLean codes and actions?

Maybe, but I think I personally would prefer it to be housed not in the main PhysLean repo but either on the website or in its own repo.

Also, curious about what recommended review plugins are run on llm generated code for PhysLean?

I don't think I understand your question properly: But let me state, LLM generated code for the main PhysLean repo goes through the same human review as any other code. The PhysLean website repo is not currently held to the same standard (but maybe it should be).

Are review plugins some specific tool on GitHub?

Yes, I was referring to the website code, in particular features like dashboard. By plugins, I meant various tools that are used by devs to verify the vulnerabilities and corner cases in llm generated code. Because more and more of it will go into building backend infrastructure of the physlean repo, it will be better to have some kind of feedback loop because llm generates verbose code with flavor of an independent coder and it's time-consuming for anyone to debug it later if issues escape notice

Also, making llm generated code part of a public repo also means the user needs to check if it has not accidentally mentioned private details of the user's laptop or files anywhere in the code or hard-coded some private info available to it. For static things like dashboard, claude shouldn't make mistakes and the mistakes should at worst just cause dashboard to be incorrect but it's better to have such guardrails. I use llm for private repos and for me "/review" command from claude and bandit python package suffices but I'm also trying to learn more sophisticated methods being developed to give feedback on PRs, that's why asked out of curiosity.

[Joseph Tooby-Smith]

Ok, I think this was be a very good idea and this will be very important. I think maintainability here is something we should worry about.

Also, making llm generated code part of a public repo also means the user needs to check if it has not accidentally mentioned private details of the user's laptop or files anywhere in the code or hard-coded some private info available to it.

Indeed I know of at least one cyber-security incident at a major firm where the attackers got in due to a private info being stored where it shouldn't.

In terms of actionable points:

• We should at least put the PR criteria for the website up to the standards as the PhysLean repo

Do you think there is anything else we could do now?

[Shlok Vaibhav]

I will try to read more about what standard practices are used to incorporate ai generated PRs, I only use it for personal private repos where it's not a critical issue for me so I would be curious to hear about such practices.

Yes, I think the website infrastructure should be always reviewed since that's the landing point for PhysLean and technical debt may pile up.