Crash related to revert

[bryangingechen]

Reported by @Vtec234 on Zulip. The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"):

lemma segfault {α: Type u} {a a': α} (H : a = a') : a = a' := begin
  revert a a,
end

This does not crash when run in the web editor.

[bryangingechen]

The crash occurs because m_user_name2idxs.find returns a null pointer here: https://github.com/leanprover-community/lean/blob/master/src/library/local_context.cpp#L189

Would it make sense to just have erase_user_name return immediately if m_user_name2idxs.find is null?

(This code was removed in Lean 4 in this commit: leanprover/lean4@69070f4#diff-8e1b5fb692d035eb36593afedf77385f)

[cipher1024]

I wouldn't go this deep. I think revert_lst should check that the variables exist when reverting them

[cipher1024]

(I have recent commit that does similar things: 06ff399)

[bryangingechen]

Sounds good; I think I see something reasonable to PR when I’m back with my Lean computer.

[bryangingechen]

(Namely, I want to skip over duplicates in this loop:

lean/src/library/tactic/revert_tactic.cpp

Line 36 in ec1613a

for (expr const & l : ls) {

)

[cipher1024]

I'm not sure if it's worth getting through the trouble of skipping duplicates. I think reporting an error is better. It has the nice property that revert_lst (xs ++ ys) = revert_lst xs >> revert_lst ys (if you ignore the return value, otherwise, the rhs is (+) <$> revert_lst xs <*> revert_lst ys, which is also nice, albeit a bit more complicated)

[bryangingechen]

OK, we can certainly throw an error, but I think we still have to do duplicate detection, right? Otherwise we’ll have to make deeper changes. I might be missing an easier way to test for this though.

[cipher1024]

We still have to do duplicate detection. I was just saying that throwing an error will probably be simpler than removing duplicates.