why does `skip <;> [skip <;> fail]` not fail?

Stream: lean4

[Jacob Prinz]

in my actual code, i have a tactic that produces two goals, and i want to sequence and fail if the second goal is not solved, like

tactic1 <;> [skip; (try_something <;> fail)]

but fail doesn't seem to work with sequencing in the way that i expect.

[Damiano Testa]

Do you have an #mwe to show? Without one, it is hard to know what could be happening.

[Jacob Prinz]

example : True := by
  skip <;> [skip <;> fail]
  trivial

i would expect this proof to fail, but instead it succeeds. what am i misunderstanding about either <;> or fail?

[Damiano Testa]

The tactics inside the square brackets have some form of partial recovery, using a try/catch block. In the catch part there is a logException that is supposed to let you know what happened. Except that the exception is internal of type abortTactic and logException specifically does not report those!

[Damiano Testa]

In conclusion, the tactic effectively recovers from the fail, although this seems like an unintended behaviour.

[Jacob Prinz]

thanks for the help

[Jakub Nowak]

I still don't understand why first one doesn't fail but second does.

import Batteries

set_option linter.unnecessarySeqFocus false

example : True := by
  skip <;> [skip <;> fail]
  skip <;> [fail]
  trivial