fix(library/module): do not implicitly cast bool to int (#249)

src/library/module.cpp

@@ -89,7 +89,7 @@ struct module_ext : public environment_extension {
     /** Top-level doc strings for modules which have them. Lean doesn't have a notion
      * of module different from that of a source file, so we use file names to index
      * the docstring map. */
-    rb_map<std::string, list<std::pair<pos_info, std::string>>, string_lt> m_module_docs;
+    rb_map<std::string, list<std::pair<pos_info, std::string>>, string_cmp> m_module_docs;
     // Map from declaration name to olean file where it was defined
     name_map<std::string>     m_decl2olean;
     name_map<pos_info>        m_decl2pos_info;
@@ -541,7 +541,7 @@ environment add_doc_string(environment const & env, std::string const & doc, pos
     return add(env, std::make_shared<mod_doc_modification>(doc, pos));
 }
 
-rb_map<std::string, list<std::pair<pos_info, std::string>>, string_lt> const & get_doc_strings(environment const & env) {
+rb_map<std::string, list<std::pair<pos_info, std::string>>, string_cmp> const & get_doc_strings(environment const & env) {
     return get_extension(env).m_module_docs;
 }
 

src/library/module.h

@@ -155,7 +155,7 @@ environment add(environment const & env, certified_declaration const & d);
 environment add_doc_string(environment const & env, std::string const & doc, pos_info pos);
 
 /** \brief Returns the map of module-level docs indexed by source file name. */
-rb_map<std::string, list<std::pair<pos_info, std::string>>, string_lt> const & get_doc_strings(environment const & env);
+rb_map<std::string, list<std::pair<pos_info, std::string>>, string_cmp> const & get_doc_strings(environment const & env);
 
 /** \brief Return true iff \c n is a definition added to the current module using #module::add */
 bool is_definition(environment const & env, name const & n);

src/library/string.h

@@ -33,9 +33,9 @@ std::string quote_string_literal(std::string const & s);
 format pp_string_literal(std::string const & s);
 format pp_char_literal(unsigned c);
 
-struct string_lt {
-    bool operator()(std::string const & a, std::string const & b) const {
-        return a < b;
+struct string_cmp {
+    int operator()(std::string const & a, std::string const & b) const {
+        return a.compare(b);
     }
 };
 

tests/lean/run/doc_string7a.lean

@@ -0,0 +1,2 @@
+/-!a-/
+/-!b-/

tests/lean/run/doc_string7b.lean

@@ -0,0 +1,11 @@
+import .doc_string7a
+open tactic
+
+#eval do
+ds ← olean_doc_strings,
+let ds := (do
+    ⟨some fn, d⟩ ← ds | [],
+    guard $ fn.backn 17 = "doc_string7a.lean",
+    d),
+trace ds,
+guard $ ds = [(⟨1, 0⟩, "a"), (⟨2,0⟩, "b")]