fix(library/module): ignore multiple declarations of 'sorry', fixes #59

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

src/frontends/lean/CMakeLists.txt

@@ -5,6 +5,6 @@ server.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
 dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
-structure_cmd.cpp sorry.cpp info_manager.cpp noinfo.cpp)
+structure_cmd.cpp info_manager.cpp noinfo.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/parser.cpp

@@ -29,6 +29,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/num.h"
 #include "library/string.h"
+#include "library/sorry.h"
 #include "library/error_handling/error_handling.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
@@ -37,7 +38,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp_options.h"
-#include "frontends/lean/sorry.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true

src/library/CMakeLists.txt

@@ -4,7 +4,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
   private.cpp placeholder.cpp aliases.cpp level_names.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
-  standard_kernel.cpp hott_kernel.cpp
+  standard_kernel.cpp hott_kernel.cpp sorry.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)

src/library/module.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "util/name_map.h"
 #include "kernel/type_checker.h"
 #include "library/module.h"
+#include "library/sorry.h"
 #include "library/kernel_serializer.h"
 #include "version.h"
 
@@ -300,6 +301,8 @@ struct import_modules_fn {
         declaration decl = read_declaration(d, midx);
         lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
         environment env  = m_senv.env();
+        if (decl.get_name() == get_sorry_name() && has_sorry(env))
+            return;
         if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
             if (!m_keep_proofs && decl.is_theorem())
                 m_senv.add(theorem2axiom(decl));

src/library/sorry.cpp

@@ -29,7 +29,6 @@ environment declare_sorry(environment const & env) {
     }
 }
 
-expr const & get_sorry_constant() {
+expr const & get_sorry_constant() { return g_sorry; }
-    return g_sorry;
+name const & get_sorry_name() { return g_sorry_name; }
-}
 }

src/library/sorry.h

@@ -17,4 +17,5 @@ environment declare_sorry(environment const & env);
 
 /** \brief Return the constant \c sorry */
 expr const & get_sorry_constant();
+name const & get_sorry_name();
 }