refactor(kernel): move annotation to library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/sstream.h"
 #include "kernel/abstract.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "library/tactic/tactic.h"

src/frontends/lean/noinfo.h

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 
 namespace lean {
 /** \brief Annotate \c e with no-information generation.

src/frontends/lean/pp.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/flet.h"
 #include "kernel/replace_fn.h"
 #include "kernel/free_vars.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/aliases.h"
 #include "library/scoped_ext.h"
 #include "library/coercion.h"

src/kernel/CMakeLists.txt

@@ -3,6 +3,6 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
-annotation.cpp normalizer_extension.cpp)
+normalizer_extension.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/library/CMakeLists.txt

@@ -8,6 +8,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp
-  print.cpp)
+  print.cpp annotation.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/annotation.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <string>
 #include "util/sstream.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 
 namespace lean {
 name const & get_annotation_name() {

src/library/explicit.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/sstream.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/explicit.h"
 #include "library/kernel_bindings.h"
 

src/library/kernel_serializer.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
 #include "kernel/declaration.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/max_sharing.h"
 #include "library/kernel_serializer.h"
 

src/library/print.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/print.h"
 
 namespace lean {

src/library/tactic/expr_to_tactic.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
-#include "kernel/annotation.h"
+#include "library/annotation.h"
 #include "library/string.h"
 #include "library/num.h"
 #include "library/tactic/expr_to_tactic.h"