chore(*): fix test and style

src/emacs/lean-info.el

@@ -45,7 +45,7 @@
 
 (defun lean-get-info-record-at-point (cont)
   "Get info-record at the current point"
-  (lean-server-sync)
+  ;; TODO(sullrich): finding the start position should go into the server
   (let ((pos (lean-find-hname-beg)))
     (lean-server-send-command
      (list :command "info"

src/frontends/lean/elaborator.h

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/tactic/tactic_state.h"
 #include "frontends/lean/elaborator_exception.h"
-#include "info_manager.h"
+#include "frontends/lean/info_manager.h"
 
 namespace lean {
 enum class elaborator_strategy {

src/frontends/lean/info_manager.cpp

@@ -7,13 +7,14 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <set>
-#include <library/tactic/tactic_state.h>
-#include <frontends/lean/json.h>
-#include <util/lean_path.h>
+#include <string>
 #include "library/choice.h"
 #include "library/scoped_ext.h"
 #include "library/pp_options.h"
-#include "info_manager.h"
+#include "library/tactic/tactic_state.h"
+#include "frontends/lean/json.h"
+#include "frontends/lean/info_manager.h"
+#include "util/lean_path.h"
 
 namespace lean {
 class type_info_data : public info_data_cell {
@@ -24,7 +25,7 @@ public:
 
     expr const & get_type() const { return m_expr; }
 
-    virtual void add_info(io_state_stream const & ios, json & record) const {
+    virtual void report(io_state_stream const & ios, json & record) const override {
         std::ostringstream ss;
         ss << flatten(ios.get_formatter()(m_expr));
         record["type"] = ss.str();
@@ -43,7 +44,7 @@ class identifier_info_data : public info_data_cell {
 public:
     identifier_info_data(name const & full_id): m_full_id(full_id) {}
 
-    virtual void add_info(io_state_stream const & ios, json & record) const {
+    virtual void report(io_state_stream const & ios, json & record) const override {
         record["full-id"] = m_full_id.to_string();
         if (auto olean = get_decl_olean(ios.get_environment(), m_full_id))
             record["source"]["file"] = olean_file_to_lean_file(*olean);
@@ -169,7 +170,7 @@ class proof_state_info_data : public info_data_cell {
 public:
     proof_state_info_data(unsigned c, tactic_state const & s):info_data_cell(c), m_state(s) {}
     virtual info_kind kind() const { return info_kind::ProofState; }
-    virtual void add_info(io_state_stream const & ios, unsigned line) const {
+    virtual void report(io_state_stream const & ios, unsigned line) const {
         ios << "-- PROOF_STATE|" << line << "|" << get_column() << "\n";
         bool first = true;
         for (expr const & g : m_state.goals()) {
@@ -216,14 +217,14 @@ line_info_data_set info_manager::get_line_info_set(unsigned l) const {
 }
 
 void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) {
-    //if (is_tactic_type(e))
-    //    return;
+    // if (is_tactic_type(e))
+    //     return;
     add_info(l, c, mk_type_info(e));
 }
 
 void info_manager::add_identifier_info(unsigned l, unsigned c, name const & full_id) {
-    //if (is_tactic_id(full_id))
-    //    return;
+    // if (is_tactic_id(full_id))
+    //     return;
     add_info(l, c, mk_identifier_info(full_id));
 }
 
@@ -262,7 +263,7 @@ static bool is_tactic_id(name const & id) {
 }
 
 void info_manager::add_proof_state_info(unsigned l, unsigned c, tactic_state const & s) {
-    add_info(l, mk_proof_state_info(c, s));
+    report(l, mk_proof_state_info(c, s));
 }
 */
 
@@ -274,7 +275,7 @@ json info_manager::get_info_record(environment const & env, options const & o, i
             for (auto const & d : ds) {
                 type_context tc(env, o);
                 io_state_stream out = regular(env, ios, tc).update_options(o);
-                d.add_info(out, record);
+                d.report(out, record);
             }
         }
     });

src/frontends/lean/info_manager.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <algorithm>
 #include <vector>
 #include "kernel/expr.h"
 #include "library/io_state_stream.h"
@@ -22,14 +23,13 @@ protected:
     friend info_data;
 public:
     virtual ~info_data_cell() {}
-    virtual void add_info(io_state_stream const & ios, json & record) const = 0;
+    virtual void report(io_state_stream const & ios, json & record) const = 0;
 };
 
 class info_data {
 private:
     info_data_cell * m_ptr;
 public:
-    //info_data();
     info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); }
     info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
@@ -37,8 +37,8 @@ public:
     friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); }
     info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); }
     info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); }
-    void add_info(io_state_stream const & ios, json & record) const {
-        return m_ptr->add_info(ios, record);
+    void report(io_state_stream const & ios, json & record) const {
+        return m_ptr->report(ios, record);
     }
     info_data_cell const * raw() const { return m_ptr; }
 };

src/frontends/lean/json.cpp

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Gabriel Ebner
 */
-#if defined(LEAN_SERVER)
-#include "json.h"
+#include "frontends/lean/json.h"
 
 namespace lean {
 
@@ -34,4 +33,3 @@ void json_message_stream::report(message const & msg) {
 }
 
 }
-#endif

src/frontends/lean/json.h

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #pragma once
-#if defined(LEAN_SERVER)
 #include "library/messages.h"
 #include "util/json.hpp"
 
@@ -26,4 +25,3 @@ public:
 };
 
 }
-#endif

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

@@ -1,3 +0,0 @@
-{"message":"new file name, reloading","response":"ok"}
-{"is_ok":true,"messages":[{"caption":"eval result","file_name":"f","pos_col":0,"pos_line":1,"severity":"information","text":"tt"}],"response":"ok"}
-{"messages":[{"column":5,"full_id":"bool.tt","kind":"full_id","line":1}],"response":"ok"}

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

@@ -0,0 +1,3 @@
+{"message":"new file name, reloading","response":"ok"}
+{"is_ok":true,"messages":[],"response":"ok"}
+{"record":{"full-id":"bool.tt","source":{"column":10,"file":"/library/init/core.lean","line":162},"type":"bool"},"response":"ok"}

tests/lean/interactive/test_single.sh

@@ -1,11 +1,14 @@
 #!/usr/bin/env bash
+REALPATH=realpath
+
 if [ $# -ne 3 -a $# -ne 2 ]; then
     echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
     exit 1
 fi
 ulimit -s unlimited
 LEAN=$1
-export LEAN_PATH=../../../library:.
+ROOT_PATH=$($REALPATH ../../..)
+export LEAN_PATH=$ROOT_PATH/library:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no
 else
@@ -13,7 +16,12 @@ else
 fi
 f=$2
 echo "-- testing $f"
-"$LEAN" -D pp.unicode=true --server < "$f" > "$f.produced.out"
+
+OUTPUT="$("$LEAN" -D pp.unicode=true --server < "$f")"
+# make paths system-independent
+OUTPUT=${OUTPUT//$ROOT_PATH/}
+echo "$OUTPUT" > "$f.produced.out"
+
 if test -f "$f.expected.out"; then
     if diff --ignore-all-space "$f.produced.out" "$f.expected.out"; then
         echo "-- checked"