Lean.Replay

Stream: lean4

[Kim Morrison]

Mario Carneiro said:

Kim Morrison Why is Lean.Replay in lean instead of lean4checker now? It would be easier to fix this from lean4checker?

From memory it has been split that way since the beginning of lean4checker. I'd be pretty happy to move this code down to lean4checker, though, if you or anyone else thinks there's a good reason to. (In particular, I'd merge PRs making this happen, or add P-medium to an issue asking for this to happen, and if there's an urgent reason do it myself. :-)

[Kim Morrison]

Ah -- I just remembered that Replay is also used by the REPL, so I'd prefer that it is not in lean4checker.

[Notification Bot]

2 messages were moved here from #Equational > Mathlib Bump by Mario Carneiro.

[Mario Carneiro]

what's the context of the use of replay in the REPL?

[Mario Carneiro]

why does it not just import environments the normal way?

[Jannis Limperg]

Aesop also uses replay. This is because when we construct the final proof, we effectively merge different environments stored at nodes of the proof tree. It seems safer to do this with replay than to just copy the constants over.