feat(library/tactic/goal): add option pp.compact_goals

src/library/tactic/goal.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/buffer.h"
 #include "util/sstream.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/replace_fn.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
@@ -15,7 +16,24 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/tactic/goal.h"
 
+#ifndef LEAN_DEFAULT_PP_COMPACT_GOALS
+#define LEAN_DEFAULT_PP_COMPACT_GOALS false
+#endif
+
 namespace lean {
+static name * g_pp_compact_goals = nullptr;
+void initialize_goal() {
+    g_pp_compact_goals = new name({"pp", "compact_goals"});
+    register_bool_option(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS,
+                         "(pretty printer) try to display goal in a single line when possible");
+}
+void finalize_goal() {
+    delete g_pp_compact_goals;
+}
+bool get_pp_compact_goals(options const & o) {
+    return o.get_bool(*g_pp_compact_goals, LEAN_DEFAULT_PP_COMPACT_GOALS);
+}
+
 format goal::pp(formatter const & fmt) const {
     return pp(fmt, substitution());
 }
@@ -25,6 +43,7 @@ format goal::pp(formatter const & fmt, substitution const & s) const {
     options const & opts = fmt.get_options();
     unsigned indent  = get_pp_indent(opts);
     bool unicode     = get_pp_unicode(opts);
+    bool compact     = get_pp_compact_goals(opts);
     format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
     expr conclusion  = m_type;
     buffer<expr> tmp;
@@ -38,9 +57,12 @@ format goal::pp(formatter const & fmt, substitution const & s) const {
         expr t     = tmp_subst.instantiate(mlocal_type(l));
         r += group(fmt(l) + space() + colon() + nest(indent, line() + fmt(t)));
     }
+    if (compact)
         r = group(r);
     r += line() + turnstile + space() + nest(indent, fmt(tmp_subst.instantiate(conclusion)));
-    return group(r);
+    if (compact)
+        r = group(r);
+    return r;
 }
 
 expr goal::abstract(expr const & v) const {

src/library/tactic/goal.h

@@ -79,4 +79,7 @@ io_state_stream const & operator<<(io_state_stream const & out, goal const & g);
 
 UDATA_DEFS(goal)
 void open_goal(lua_State * L);
+
+void initialize_goal();
+void finalize_goal();
 }

src/library/tactic/init_module.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/tactic/goal.h"
 #include "library/tactic/proof_state.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/apply_tactic.h"
@@ -16,6 +17,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 void initialize_tactic_module() {
+    initialize_goal();
     initialize_proof_state();
     initialize_expr_to_tactic();
     initialize_apply_tactic();
@@ -37,5 +39,6 @@ void finalize_tactic_module() {
     finalize_apply_tactic();
     finalize_expr_to_tactic();
     finalize_proof_state();
+    finalize_goal();
 }
 }

tests/lean/cls_err.lean.expected.out

@@ -1,2 +1,3 @@
 cls_err.lean:13:2: error: failed to synthesize placeholder
-A : Type ⊢ H A
+A : Type
+⊢ H A

tests/lean/empty.lean.expected.out

@@ -1,2 +1,3 @@
 empty.lean:6:25: error: failed to synthesize placeholder
- ⊢ nonempty Empty
+
+⊢ nonempty Empty

tests/lean/goals1.lean.expected.out

@@ -1,5 +1,11 @@
 goals1.lean:9:0: error: unsolved placeholder, unsolved subgoals
-A : Type, a : A, b : A, c : A, Hab : eq a b, Hbc : eq b c ⊢ eq b c
+A : Type,
+a : A,
+b : A,
+c : A,
+Hab : eq a b,
+Hbc : eq b c
+⊢ eq b c
 goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
   λ (A : Type) (a b c : A) (Hab : eq a b) (Hbc : eq b c),
     ?M_1

tests/lean/interactive/proof_state_info.input.expected.out

@@ -8,6 +8,11 @@ tactic
 tactic.info
 -- ACK
 -- PROOF_STATE|7|2
-a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a ∧ b
+a : Prop,
+b : Prop,
+c : Prop,
+Ha : a,
+Hb : b
+⊢ a ∧ b
 -- ACK
 -- ENDINFO

tests/lean/interactive/proof_state_info2.input.expected.out

@@ -5,7 +5,12 @@
 tactic
 -- ACK
 -- PROOF_STATE|5|17
-a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a ∧ b
+a : Prop,
+b : Prop,
+c : Prop,
+Ha : a,
+Hb : b
+⊢ a ∧ b
 -- ACK
 -- ENDINFO
 -- BEGININFO
@@ -13,8 +18,18 @@ a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a ∧ b
 tactic
 -- ACK
 -- PROOF_STATE|6|17
-a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a
-a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ b
+a : Prop,
+b : Prop,
+c : Prop,
+Ha : a,
+Hb : b
+⊢ a
+a : Prop,
+b : Prop,
+c : Prop,
+Ha : a,
+Hb : b
+⊢ b
 -- ACK
 -- ENDINFO
 -- BEGININFO
@@ -22,6 +37,11 @@ a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ b
 tactic
 -- ACK
 -- PROOF_STATE|7|10
-a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ b
+a : Prop,
+b : Prop,
+c : Prop,
+Ha : a,
+Hb : b
+⊢ b
 -- ACK
 -- ENDINFO

tests/lean/pstate.lean.expected.out

@@ -1,5 +1,11 @@
 pstate.lean:4:26: error: unsolved placeholder, don't know how to synthesize it
-A : Type, a : A, b : A, c : A, h₁ : a = b, h₂ : b = c ⊢ b = c
+A : Type,
+a : A,
+b : A,
+c : A,
+h₁ : a = b,
+h₂ : b = c
+⊢ b = c
 pstate.lean:4:7: error: failed to add declaration 'foo' to environment, value has metavariables
   λ (A : Type) (a b c : A) (h₁ : a = b) (h₂ : b = c),
     eq.trans h₁ ?M_1