is the environment mutable in practice?

Stream: general

[Jason Rute]

The tactic state contains a few types of information. It contains information about local declarations and it also contains information about the environment. The environment contains lots of information about previous definitions and other things. It can be changed by a tactic. The most obvious example is the set_env. My question is do any of the interactive tactics which are used in begin...end blocks actually change the environment? (Also if they do, does it have any effect on anything outside the begin...end block?)

[Mario Carneiro]

The environment is a "persistent" data structure. That means that everything that appears to change it is really making a modified copy. When you undo a tactic it reverts any changes to the environment

[Mario Carneiro]

Most interactive tactics don't change the environment because they cannot effect permanent changes

[Mario Carneiro]

The determination is not whether it is in a begin end block but rather whether it is a def or theorem. A theorem is elaborated asynchronously, and any changes to the environment are discarded once the proof is obtained, while a def operates synchronously with the processing of the file, meaning that any tactics here hold up the processing of everything else, but they can change the environment, for example by adding auxiliary definitions or theorems. The abstract {} tactic is an interactive tactic that does this

[Jason Rute]

I knew the persistence thing already. (For example a tactic never "changes" the goals, just makes new goals.) But thanks for the clarification on the rest. I think this example illustrates what you told me well:

def foo (n : nat) : n=n := begin
induction n,
abstract abc123 {simp},
try {rw [foo.abc123]}, -- can be called internally
simp,
end

#check foo.abc123 -- 0 = 0

theorem bar (n : nat) : n=n := begin
induction n,
abstract abc123 {simp},
try {rw [bar.abc123]}, -- can be called internally
simp,
end

#check bar.abc123 -- fails

[Mario Carneiro]

Lean actually has to inline the proofs of lemmas that were added to the environment in the middle of a theorem. If you #print foo and bar you will see that foo actually references foo.abc123 but bar doesn't, and the proof is right there in the middle of the theorem