Skip to content

docs(fluid-dynamics): add fluid API map#1450

Open
Robby955 wants to merge 2 commits into
leanprover-community:masterfrom
Robby955:api-map-fluid-dynamics
Open

docs(fluid-dynamics): add fluid API map#1450
Robby955 wants to merge 2 commits into
leanprover-community:masterfrom
Robby955:api-map-fluid-dynamics

Conversation

@Robby955

Copy link
Copy Markdown
Contributor

Motivation

Related to #1414, the tracking map for the fluid API in #887. An API map records the implemented status and source location of each requirement for an API, so the gap between a planned API and the current library stays visible in-tree.

Changes

Adds Physlib/FluidDynamics/API-map.yaml.

The completed entries cover what exists: the mass flux density momentumDensity and the equation of continuity in its conservative, residual and smooth forms with the implication between them. The fluid data structure is recorded as not done, since FluidState currently provides density and velocity but the requirement also asks for pressure. The Euler equation, ideal fluid, entropy flux, Bernoulli equation, energy flux and flow out of a volume are not implemented and carry location N/A.

References cite Landau and Lifshitz, Fluid Mechanics, vol. 6, 2nd ed., Chapter 1.

Testing

Ran the API-map linter:

python3 scripts/api_map_linter.py --repo .

Every declared source file and name resolves; no completed entry is missing a location.

@github-actions

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

@Robby955
Robby955 marked this pull request as ready for review July 20, 2026 22:33
@jstoobysmith

Copy link
Copy Markdown
Member

This will likely need an update based on Physlib#1125, which I will merge now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants