feat(library/init/meta/interactive): give sorry tactic ignored itac…

…tic block (#689)

This supports being able to "comment out" parts of a tactic proof, which is useful during proof development when there are slow subproofs.

For example, to skip over the first subproof:
```
example (p : Prop) : p ↔ p :=
begin
  split,
  sorry { intro h, assumption, },
  { intro h, assumption, },
end
```

library/init/meta/interactive.lean

@@ -854,14 +854,32 @@ meta def trivial : tactic unit :=
 tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed"
 
 /--
-Closes the main goal using `sorry`.
+Closes the main goal using `sorry`. Takes an optional ignored tactic block.
+
+The ignored tactic block is useful for "commenting out" part of a proof during development:
+```lean
+begin
+  split,
+  admit { expensive_tactic },
+
+end
+```
 -/
-meta def admit : tactic unit := tactic.admit
+meta def admit (t : parse (with_desc "{...}" parser.itactic)?) : tactic unit := tactic.admit
 
 /--
-Closes the main goal using `sorry`.
+Closes the main goal using `sorry`. Takes an optional ignored tactic block.
+
+The ignored tactic block is useful for "commenting out" part of a proof during development:
+```lean
+begin
+  split,
+  sorry { expensive_tactic },
+
+end
+```
 -/
-meta def «sorry» : tactic unit := tactic.admit
+meta def «sorry» (t : parse (with_desc "{...}" parser.itactic)?) : tactic unit := tactic.admit
 
 /--
 The contradiction tactic attempts to find in the current local context a hypothesis that is equivalent to an empty inductive type (e.g. `false`), a hypothesis of the form `c_1 ... = c_2 ...` where `c_1` and `c_2` are distinct constructors, or two contradictory hypotheses.

library/init/meta/interactive_base.lean

@@ -49,6 +49,9 @@ do hs ← l.get_locals,
 /-- Use `desc` as the interactive description of `p`. -/
 meta def with_desc {α : Type} (desc : format) (p : parser α) : parser α := p
 
+meta instance with_desc.reflectable {α : Type} (p : parser α) [h : lean.parser.reflectable p]
+  (f : format) : reflectable (with_desc f p) := h
+
 namespace types
 variables {α β : Type}
 

tests/lean/sorry_itactic.lean

@@ -0,0 +1,29 @@
+example (p : Prop) : p ↔ p :=
+begin
+  split,
+  sorry { intro h, assumption, },
+  { intro h, assumption, },
+end
+
+example (p : Prop) : p ↔ p :=
+begin
+  split,
+  sorry,
+  { intro h, assumption, },
+end
+
+-- Make sure other ways to comment out blocks still work:
+
+example (p : Prop) : p ↔ p :=
+begin
+  split,
+  sorry; { intro h, assumption, },
+  { intro h, assumption, },
+end
+
+example (p : Prop) : p ↔ p :=
+begin
+  split,
+  sorry <|> { intro h, assumption, },
+  { intro h, assumption, },
+end

tests/lean/sorry_itactic.lean.expected.out

@@ -0,0 +1,4 @@
+sorry_itactic.lean:1:0: warning: declaration '[anonymous]' uses sorry
+sorry_itactic.lean:8:0: warning: declaration '[anonymous]' uses sorry
+sorry_itactic.lean:17:0: warning: declaration '[anonymous]' uses sorry
+sorry_itactic.lean:24:0: warning: declaration '[anonymous]' uses sorry