Tracking issue for converting the top-level checking code from regular Rust functions (that manually construct proof trees) into judgment functions.
How it works today
a-mir-formality begins today by calling check_all_crates. This in turn checks every combination of crates (they are expected to appear in dependency order) with check_crate, which calls check_crate_item, which dispatches on CrateItem variants.
Each of these Rust functions returns an Fallible<T> which is a type alias for anyhow::Result. They manually construct proof trees in the case of a successful run. They are written in a functional style that avoids mutating data that is not local to the function.
How we want it to work
We want to move away from Rust functions towards judgment functions. This is a great issue to practice writing judgment functions. Using a judgment function means that we'll automatically construct proof trees via the macro, but it also means we'll have better support for instrumentation, coverage checking, reference text generation, and other things we plan to do in the future.
See the formality-core book for documentation on how judgment functions work.
Example: check_crate_item
As a simple example, see PR #287 which converted some of the "top-level Rust functions" into judgments.
How to help out
Find a subissue that is not claimed.
Add a comment @rustbot claim.
To leave room for others, please just claim one sub-issue so others can pick up the rest.
Things we don't need to convert
These functions can stay as Rust, they're more like little helper functions or tests or plumbing. You may wish to extract similar helper functions in some cases.
check_for_duplicate_items / check_trait_items_have_unique_names — structural validation, not proof logicmerge_binders — utilityprove_goal / prove_judgment / prove_not_goal — wrappers around judgment functionsprove_where_clauses_well_formed — thin wrapper
Sub-issues
Tracking issue for converting the top-level checking code from regular Rust functions (that manually construct proof trees) into judgment functions.
How it works today
a-mir-formality begins today by calling
check_all_crates. This in turn checks every combination of crates (they are expected to appear in dependency order) withcheck_crate, which callscheck_crate_item, which dispatches onCrateItemvariants.Each of these Rust functions returns an
Fallible<T>which is a type alias foranyhow::Result. They manually construct proof trees in the case of a successful run. They are written in a functional style that avoids mutating data that is not local to the function.How we want it to work
We want to move away from Rust functions towards judgment functions. This is a great issue to practice writing judgment functions. Using a judgment function means that we'll automatically construct proof trees via the macro, but it also means we'll have better support for instrumentation, coverage checking, reference text generation, and other things we plan to do in the future.
See the formality-core book for documentation on how judgment functions work.
Example:
check_crate_itemAs a simple example, see PR #287 which converted some of the "top-level Rust functions" into judgments.
How to help out
Find a subissue that is not claimed.
Add a comment
@rustbot claim.To leave room for others, please just claim one sub-issue so others can pick up the rest.
Things we don't need to convert
These functions can stay as Rust, they're more like little helper functions or tests or plumbing. You may wish to extract similar helper functions in some cases.
check_for_duplicate_items/check_trait_items_have_unique_names— structural validation, not proof logicmerge_binders— utilityprove_goal/prove_judgment/prove_not_goal— wrappers around judgment functionsprove_where_clauses_well_formed— thin wrapperSub-issues
check_traitto a judgment function #289 — Convertcheck_traitto a judgment functioncheck_trait_implto a judgment function #290 — Convertcheck_trait_implto a judgment functioncheck_neg_trait_implto a judgment function #291 — Convertcheck_neg_trait_implto a judgment functioncheck_adtto a judgment function #292 — Convertcheck_adtto a judgment functioncheck_fn/check_free_fnto judgment functions #293 — Convertcheck_fn/check_free_fnto judgment functionscheck_coherenceto a judgment function #294 — Convertcheck_coherenceto a judgment function