about summary refs log tree commit diff
path: root/compiler/rustc_mir_transform/src/coverage/mod.rs
diff options
context:
space:
mode:
authorMichael Goulet <michael@errs.io>2023-08-10 21:17:09 -0700
committerGitHub <noreply@github.com>2023-08-10 21:17:09 -0700
commita04dfc32e61a0a4b46260045f007ab9448ce4e01 (patch)
tree7a267948155baa9bb7b7429f10b1f45eb6f9ebb9 /compiler/rustc_mir_transform/src/coverage/mod.rs
parent2845baddb34df21358dbcacbc25d5067540ba17b (diff)
parent02529d2cbecfd4edb6f481c8f0aaad9ad1fadfbb (diff)
downloadrust-a04dfc32e61a0a4b46260045f007ab9448ce4e01.tar.gz
rust-a04dfc32e61a0a4b46260045f007ab9448ce4e01.zip
Rollup merge of #114694 - lcnr:provisional-cache, r=compiler-errors
make the provisional cache slightly less broken

It is still broken for the following cycles:
```mermaid
graph LR
   R["R: coinductive"] --> A["A: inductive"]
   R --> B["B: coinductive"]
   A --> B
   B --> R
```
the `R -> A -> B -> R` cycle should be considered to not hold, as it is mixed, but because we first put `B` into the cache from the `R -> B -> R` cycle which is coinductive, it does hold.

This issue will also affect our new coinduction approach. Longterm cycles are coinductive as long as one step goes through an impl where-clause, see https://github.com/rust-lang/a-mir-formality/blob/f4fc5bae36ab1a9fefddd54e5ccffc5f671467ec/crates/formality-prove/src/prove/prove_wc.rs#L51-L62. Here we would first have a fully inductive cycle `R -> B -> R` which is then entered by a cycle with a coinductive step `R -> A -coinductive-> B -> R`.

I don't know how to soundly implement a provisional cache for goals not on the stack without tracking all cycles the goal was involved in and whether they were inductive or not. We could then only use goals from the cache if the *inductivity?* of every cycle remained the same. This is a mess to implement. I therefore want to rip out the provisional cache entirely, but will wait with this until I talked about it with `@nikomatsakis.`

r? `@compiler-errors`
Diffstat (limited to 'compiler/rustc_mir_transform/src/coverage/mod.rs')
0 files changed, 0 insertions, 0 deletions