Repository navigation
Conversation
meta-cla
Bot
added
the
CLA Signed
✅ Deploy Preview for fb-oss-glean ready!
To edit notification comments on pull requests, go to your Netlify project configuration. |
simonmar
reviewed
Oct 2, 2026
simonmar
left a comment
simonmar
left a comment
Collaborator
There was a problem hiding this comment.
Disallowing recursive stored predicates is fine for now, but long term we should enable it: recursive stored predicates are particularly useful as a caching mechanism, and they're also much easier to implement than non-stored because you can just use semi-naive evaluation directly. In fact I considered doing this but never got around to it.
The first problem you mention is easily fixable, for ownership we probably have to record the derivation dependencies and propagate the ownership later.
Collaborator
|
Otherwise, LGTM! |
Contributor
Author
|
Good point. Using semi-naive directly would also be more efficient. Switching evaluation strategies should be easy enough. I will do it in a PR at the end of the of the stack. |
Contributor
|
@CatherineGasnier has imported this pull request. If you are a Meta employee, you can view this in D123391743. |
- rename `TcQueryGen` to `TcWhere` - change `TcAll` and `TcNegation` to contain `TcPat` instead of `TcQuery` / `[TcStatement]` respectively (this is more uniform and consistent, and simplifies some things) - refactoring in the type checker to unify how we handle locality. `oneBranch` is renamed `encloseLocal` and used consistently when typechecking `|`, `all`, `!`, and `if`, which all need locality. Probably fixes some bugs. - update a few out-of-date comments
When working on the compiler it's easy to accidentally break something that results in a segfault. Most of these errors can be detected by checks on the Codegen IR, in particular correct type-safety and variable-scoping. - Add Glean.Query.Lint to implement query consistency checks - Turn on query linting with `GLEAN_DEBUG=lint` or `--debug-query-lint` - Linting is automatically enabled for all tests via `withTestEnv`
Summary: `glean/test/tests/Angle/RecursionTest.hs` exercises the experimental support for recursive derived predicates (enabled with `--experimental-recursion`), but it was never listed in `glean.cabal.in`, so it wasn't built or run by the open-source build. Add a `test-suite` stanza for it, following `angle-test-derived`. It also needs `Schema.Lib` and the libraries that module depends on, like the `schematest` suites. Both existing test cases pass.
Summary:
On read-only databases `pruneDerivations` removes branches of derivation
queries that search predicates with no facts. It visited derivations in
topological order, treating a predicate as having facts if it has stored
facts, if its derivation was already visited and kept, or if it is the
predicate being pruned (so direct self-recursion worked).
With mutual recursion there is no topological order. For
predicate Q : nat
A where P A
derive P
A where Base A | Q A
whichever of P and Q was visited first saw the other as empty. Here Q was
visited first and its only branch was removed, so `Q _` returned nothing,
and P silently lost its recursive `Q A` branch. The result depended on the
visiting order.
Now we prune one strongly connected component of the dependency graph at
a time, in dependency order. For a recursive component we find which
members may have facts by iterating to a least fixed point: start by
assuming none of them has facts and add the members whose derivation
survives pruning until nothing changes. Pruning only ever keeps more when
more predicates are assumed to have facts (negation is never pruned), so
this terminates. Acyclic components are pruned exactly as before.
This also covers the `child == predId` special case for self-recursion,
with one difference: a derivation whose only branches depend on itself
(`X where P X`) is now pruned, since it can never produce facts.
This mostly matters for the experimental recursion support, but
pre-existing cycles are affected too: pairs of `default` derivations used
for schema migration (`derive P.1 default ... P.2`, `derive P.2 default
... P.1`) form a cycle when pruning runs, and are now pruned
deterministically.
Test: a new case in `angle-test-recursion`, where the cycle is closed by a
`derive` declaration in a later schema, fails without this change.
`angle-test-derived`, `angle-test-angle` and `schematest` pass.
Summary:
Add two cases to `angle-test-recursion` checking that schemas with
recursive derivations are accepted:
* non-linear recursion, where a derivation refers to itself twice
(`Path { A, X }; Path { X, B }`)
* mutual recursion between two derived predicates (R and S)
Both already pass: all predicates of a schema are in scope before any
derivation is typechecked, and predicate types are declared, so a
derivation can refer to itself or to predicates that refer back to it
without any typechecker changes. These tests guard that property as
recursion support is developed.
Summary: Add two cases to `angle-test-recursion`: * A recursive derivation that uses a derived predicate which is not itself recursive (`Path` built from `Step`, `Step` from `Edge`). The non-recursive predicate is inlined into each expansion of the recursive one, and pruning has to handle an acyclic dependency of a recursive component. * A derived predicate whose type refers to itself (`Chain`, which copies a linked list of `Node` facts), so the key of each derived fact refers to another derived fact. Both check query results, not just that the schema is accepted. Both already pass.
Summary:
With recursive derivations a predicate could be defined in terms of its
own negation:
predicate P : nat
A where Base A; !(Q A)
predicate Q : nat
A where P A
Such a schema has no sensible meaning: P 1 exists only if Q 1 doesn't,
and Q 1 exists only if P 1 does. Require schemas to be stratified: no
predicate may depend negatively on itself, directly or through other
predicates. Negating a recursive predicate is still allowed when the
negation isn't part of the recursion, e.g. a recursive `NeedsFlying`
that negates a recursive `LandRoute` which doesn't depend on it.
A dependency is negative when the predicate is searched inside `!(...)`,
in the condition of an `if` (the else branch runs when the condition has
no results), or inside `all (...)` (the set it builds changes as facts
are added). `tcQueryNegativeDeps` collects these.
`checkStratification` finds the recursive components of the derivation
graph and reports every negative dependency between two predicates of
the same component, with the cycle it closes:
recursion through negation is not allowed. These predicates depend
on their own negation:
x.P.1 -> !x.Q.1 -> x.P.1
It runs in `mkDbSchema`, next to the check that stored predicates don't
use negation, so it applies when opening a DB and in `validateSchema`,
independently of `--experimental-recursion`. A schema without recursive
derivations is trivially stratified, and the check only inspects the
queries of predicates in recursive components. Unlike
`checkRecursiveDefinitions` it includes `default` derivations; see
Note [Stratification].
Test: new `stratification` group in `angle-test-recursion` with four
rejected schemas (negation, self-negation, if condition, all), which are
accepted without this change, and the NeedsFlying/LandRoute schema, which
is accepted. Also a recursion test where a recursive `Path` negates a
stored predicate, checking the results. `angle-test-derived`,
`angle-test-angle` (which loads all of `glean/schema/source`) and
`schematest` pass.
Summary: Stored predicates may not use negation, directly or through the derived predicates they depend on (Note [Negation in stored predicates]). `usesOfNegation` finds those uses by visiting derivations in topological order and marking a predicate if it uses negation itself or if one of its already-visited dependencies does. With a recursive pair P <-> Q where only Q uses negation, whichever of the two is visited first doesn't see Q marked yet. When P comes first it is left unmarked, so a stored predicate that depends on P is accepted even though it depends on negation through Q. Now we visit one strongly connected component at a time, in dependency order. Since the members of a recursive component depend on each other, they all use negation if any of them does, directly or through a dependency outside the component. Acyclic predicates are handled as before. This also drops the branch that deleted a predicate from the map when it didn't use negation: each predicate is visited once, starting from an empty map, so there was never anything to delete. Test: "negation - stored dependency on recursion" in `schematest` checks a stored predicate depending on a recursive pair, both ways round so the result can't depend on the visiting order. One of the two was accepted before this change. `angle-test-recursion`, `angle-test-derived` and `angle-test-angle` pass.
Summary:
Stored predicates can't be recursive, or depend on recursive
predicates, for now. There are two problems with them:
* A recursive stored predicate depends on itself, and `checkConstraints`
in `Glean.Query.Derive` only starts a derivation once all dependencies
are complete. So `glean derive` would refuse it with an unhelpful
"incomplete dependencies" error naming the predicate itself, and two
stored predicates in the same cycle would each wait for the other.
* Ownership would be wrong. A derived fact's owners are taken from the
facts being searched when it is created. A recursive derivation
searches facts derived earlier in the same query, which live in the
query's FactSet, and `FactSet::getOwner` returns `INVALID_USET`. So the
owners of the facts they came from are dropped, and an incremental DB
could keep derived facts it should exclude. This affects any stored
predicate whose derivation involves recursion, not only recursive ones.
`checkStoredRecursion` runs in `mkDbSchema` next to the other schema
checks and reports each stored predicate that is recursive or depends on
a recursive predicate:
recursion is not supported in stored predicates yet:
x.Reachable.1 depends on the recursive predicate x.Path.1
Default derivations are left out of the graph: a pair of default
derivations that refer to each other (the schema migration pattern) is
never enabled at the same time, so a stored predicate reading such a
predicate doesn't depend on recursion. See
Note [Recursion in stored predicates].
Supporting this later needs ownership for facts derived within a query
(the "Incrementality" part of the recursion design).
Test: new `stored predicates` group in `angle-test-recursion`: a
recursive stored predicate, a stored predicate in a cycle through an
on-demand one, and a stored predicate using a recursive one are rejected
(all accepted without this change); a stored predicate reading a
predicate with a default derivation pair is accepted. `angle-test-derived`,
`angle-test-stored`, `angle-test-angle` (all of `glean/schema/source`) and
`schematest` pass.
Contributor
Author
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the first of a series of PRs adding support for recursive predicates in Angle (#736), following the design in Glean - Evaluating recursive queries. Glean already has some naive support for recursion behind
--experimental-recursion. This PR makes the passes that process schemas and derivations work when derivations form cycles. How recursive queries are evaluated comes in the PRs stacked on top of this one.Each commit can be reviewed on its own.
checkRecursiveDefinitionskeeps recursive derivations out of published schemas until recursion is ready in the PR about caching completed demandsCommits
Register the angle-test-recursion test suite.
glean/test/tests/Angle/RecursionTest.hsexisted but wasn't listed inglean.cabal.in, so it never ran. Its two tests pass.Prune mutually recursive derivations together.
On read-only DBs,
pruneDerivationsremoves derivation branches that search predicates with no facts. It visited derivations in topological order, which doesn't exist for mutual recursion, so whichever predicate of a cycle was visited first saw the others as empty and lost the branches that depend on them. WithQ _returned nothing andPsilently lost its recursive branch. Pruning now works one strongly connected component at a time, and for a recursive component it finds the members that may have facts with a least fixpoint. Acyclic predicates are pruned as before.Two things behave differently, both described in the commit message:
X where P X) is now pruned.defaultderivations used for schema migration, which are cycles when pruning runs, are now pruned in a deterministic order.Test that recursive derivations typecheck.
Non-linear recursion (
Path { A, X }; Path { X, B }) and mutual recursion between two derived predicates. Both already pass, because all of a schema's predicates are in scope before any derivation is typechecked. The tests make sure it stays that way.Test more shapes of recursive derivations.
A recursive derivation that uses a non-recursive derived predicate (
Pathbuilt fromStep), and a derived predicate whose type refers to itself (Chain, where each derived fact's key refers to another derived fact). Both already pass.Reject recursion through negation.
Schemas now have to be stratified: no predicate can depend on its own negation, directly or through other predicates. A dependency is negative when the predicate is searched inside
!(...), in the condition of anif, or insideall (...). Negating a recursive predicate is still fine as long as the negation isn't part of the recursion, as in the NeedsFlying/LandRoute example in the design's Negation section. The error shows the cycle:The check runs in
mkDbSchema, next to the one that stops stored predicates from using negation, so it applies when a DB is opened and invalidateSchema, with or without the flag. A schema without recursion always passes, and only the queries of predicates in recursive components are looked at.defaultderivations are included, andNote [Stratification]explains why.Find uses of negation through recursive derivations.
usesOfNegationmakes sure stored predicates don't depend on negation, and it visited derivations in topological order. With a recursive pair P <-> Q where only Q uses negation, P could be visited first and left unmarked, so a stored predicate depending on P was accepted. It now works one strongly connected component at a time: if any member of a component uses negation, they all do.Reject stored predicates that involve recursion.
For now a stored predicate can't be recursive, or depend on a recursive predicate. There are two reasons:
glean deriveneeds a stored predicate's dependencies to be complete first, and a recursive one never is.FactSet::getOwnerreturnsINVALID_USETfor them. Their owners would be dropped, and incremental DBs could keep facts they should exclude.defaultderivation pairs don't count as recursion, as only one side is ever enabled.Note [Recursion in stored predicates]has the details. Lifting this restriction needs ownership for facts derived within a query.Testing
All the query-related suites pass (GHC 9.6.7, GCC 15), including
angle-test-recursion(17),angle-test-angle(48, which loads all ofglean/schema/source),schematest(23) andangle-test-stored(12).gen-schema --update-indexstill validatesglean/schema/source.Every test that expects a schema to be rejected, or a result to change, fails without the change it comes with. The tests that expect a schema to be accepted (the
defaultpairs, NeedsFlying/LandRoute) are there to check that the new checks don't reject too much.