Merge branch 'metamath:main' into main

README.md

@@ -70,14 +70,17 @@ FLAGS:
     -v, --verify               Checks proof validity
     -m, --verify-markup        Checks comment markup
         --verify-parse-stmt    Checks that printing parsed statements gives back the original formulas
+    -u, --verify-usage         Checks axiom usage
 
 OPTIONS:
-        --text <NAME> <TEXT>    Provides raw database content on the command line
-        --biblio <FILE>...      Supplies a bibliography file for verify-markup
-                                Can be used one or two times; the second is for exthtml processing
-    -D, --discouraged <FILE>    Regenerates `discouraged` file
-    -e, --export <LABEL>...     Outputs a proof file
-    -j, --jobs <jobs>           Number of threads to use for verification
+        --text <NAME> <TEXT>          Provides raw database content on the command line
+    -X, --axiom-use <FILE>            Generate `axiom-use` file
+        --biblio <FILE>...            Supplies a bibliography file for verify-markup
+                                      Can be used one or two times; the second is for exthtml processing
+    -D, --discouraged <FILE>          Regenerates `discouraged` file
+    -e, --export <LABEL>...           Outputs a proof file
+    -j, --jobs <jobs>                 Number of threads to use for verification
+        --stmt-use <FILE> <LABELS>    Outputs statements directly or indirectly using the given list of statements
 
 ARGS:
     <DATABASE>    Database file to load

metamath-knife/Cargo.toml

@@ -20,3 +20,9 @@ metamath-rs = { path = "../metamath-rs" }
 name = "metamath-knife"
 path = "src/main.rs"
 doc = false
+
+[features]
+default = ["annotate-snippets/color", "verify_markup"]
+dot = ["metamath-rs/dot"]
+xml = ["metamath-rs/xml"]
+verify_markup = ["metamath-rs/verify_markup"]

metamath-knife/src/list_stmt.rs

@@ -0,0 +1,56 @@
+use metamath_rs::{as_str, Database, StatementRef, StatementType};
+
+pub fn list_statements(
+    db: &Database,
+    label_test: impl Fn(&[u8]) -> bool,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    let separator = "-".repeat(79);
+    let scope = db.scope_result();
+    let name = db.name_result();
+    for stmt in db.statements() {
+        if let StatementType::Axiom | StatementType::Provable = stmt.statement_type() {
+            let label = stmt.label();
+            if label_test(label) {
+                if let Some(frame) = scope.get(label) {
+                    for (ix1, ix2) in &*frame.mandatory_dv {
+                        writeln!(
+                            out,
+                            "$d {} {} $.",
+                            as_str(name.atom_name(frame.var_list[*ix1])),
+                            as_str(name.atom_name(frame.var_list[*ix2]))
+                        )?;
+                    }
+                    for hyp in frame.hypotheses.iter().skip(frame.mandatory_count) {
+                        write_statement(db.statement_by_address(hyp.address()), out)?;
+                    }
+                    write_statement(stmt, out)?;
+                    writeln!(out, "{}", separator)?;
+                }
+            }
+        }
+    }
+    Ok(())
+}
+
+pub fn write_statement(
+    stmt: StatementRef,
+    out: &mut impl std::io::Write,
+) -> Result<(), std::io::Error> {
+    write!(
+        out,
+        "{} ${}",
+        as_str(stmt.label()),
+        match stmt.statement_type() {
+            StatementType::Axiom => "a",
+            StatementType::Essential => "e",
+            StatementType::Provable => "p",
+            _ => "x",
+        }
+    )?;
+    for token in stmt.math_iter() {
+        write!(out, " {}", as_str(&token))?;
+    }
+    writeln!(out)?;
+    Ok(())
+}

metamath-knife/src/main.rs

@@ -2,20 +2,19 @@
 //! databases.  The entry point for all API operations is in the `database`
 //! module, as is a discussion of the data representation.
 
+mod list_stmt;
+
 use annotate_snippets::display_list::DisplayList;
 use clap::{clap_app, crate_version};
+use list_stmt::list_statements;
 use metamath_rs::database::{Database, DbOptions};
-use metamath_rs::diag::BibError;
 use metamath_rs::parser::is_valid_label;
 use metamath_rs::statement::StatementAddress;
-use metamath_rs::verify_markup::{Bibliography, Bibliography2};
-use metamath_rs::SourceInfo;
 use simple_logger::SimpleLogger;
 use std::fs::File;
-use std::io::{self, BufWriter};
+use std::io::{self, stdout, BufWriter};
 use std::mem;
 use std::str::FromStr;
-use std::sync::Arc;
 
 fn positive_integer(val: String) -> Result<(), String> {
     u32::from_str(&val).map(|_| ()).map_err(|e| format!("{e}"))
@@ -31,7 +30,6 @@ fn main() {
         (@arg split: --split "Processes files > 1 MiB in multiple segments")
         (@arg timing: --time "Prints milliseconds after each stage")
         (@arg verify: -v --verify "Checks proof validity")
-        (@arg verify_markup: -m --("verify-markup") "Checks comment markup")
         (@arg discouraged: -D --discouraged [FILE] "Regenerates `discouraged` file")
         (@arg axiom_use: -X --("axiom-use") [FILE] "Generate `axiom-use` file")
         (@arg stmt_use: --("stmt-use") value_names(&["FILE", "LABELS"]) "Outputs statements directly or indirectly using the given list of statements")
@@ -46,6 +44,7 @@ fn main() {
             "Checks that printing parsed statements gives back the original formulas")
         (@arg dump_grammar: -G --("dump-grammar") "Dumps the database's grammar")
         (@arg dump_formula: -F --("dump-formula") "Dumps the formulas of this database")
+        (@arg list_statements: -S --("list-statements") "List all statements of this database")
         (@arg debug: --debug
             "Activates debug logs, including for the grammar building and statement parsing")
         (@arg trace_recalc: --("trace-recalc") "Prints segments as they are recalculated")
@@ -70,6 +69,11 @@ fn main() {
         "Exports all theorem dependencies in the GraphML file format")
     );
 
+    #[cfg(feature = "verify_markup")]
+    let app = clap_app!(@app (app)
+        (@arg verify_markup: -m --("verify-markup") "Checks comment markup")
+    );
+
     let matches = app.get_matches();
 
     let options = DbOptions {
@@ -177,21 +181,31 @@ fn main() {
                 .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into())));
         }
 
+        if matches.is_present("list_statements") {
+            db.scope_pass();
+            _ = list_statements(&db, |_label| true, &mut stdout());
+        }
+
+        #[allow(unused_mut)]
         let mut count = db
             .render_diags(diags, |snippet| {
                 println!("{}", DisplayList::from(snippet));
             })
             .len();
 
+        #[cfg(feature = "verify_markup")]
         if matches.is_present("verify_markup") {
+            use metamath_rs::diag::BibError;
+            use metamath_rs::verify_markup::{Bibliography, Bibliography2};
+
             db.scope_pass();
             db.typesetting_pass();
 
             let sources = matches.values_of("biblio").map_or_else(Vec::new, |vals| {
                 assert!(vals.len() <= 2, "expected at most 2 bibliography files");
                 vals.map(|val| {
                     let file = std::fs::read(val).unwrap();
-                    SourceInfo::new(val.to_owned(), Arc::new(file))
+                    metamath_rs::SourceInfo::new(val.to_owned(), std::sync::Arc::new(file))
                 })
                 .collect()
             });

metamath-rs/Cargo.toml

@@ -23,11 +23,14 @@ typed-arena = "2.0"
 # Optional dependencies
 dot-writer = { version = "0.1.2", optional = true }
 xml-rs = { version = "0.8.14", optional = true }
+html5ever = { version = "0.26.0", optional = true }
+scraper = { version = "0.19.0", optional = true }
 
 [dev-dependencies]
 assert_matches = "1.5"
 
 [features]
-default = ["annotate-snippets/color"]
+default = ["annotate-snippets/color", "verify_markup"]
 dot = ["dot-writer"]
 xml = ["xml-rs"]
+verify_markup = ["scraper", "html5ever"]

metamath-rs/src/axiom_use.rs

@@ -34,7 +34,7 @@ struct UsagePass<'a> {
 impl<'a> UsagePass<'a> {
     // Parses the 'usage' commmands in the database,
     fn parse_command(
-        &mut self,
+        &self,
         sref: SegmentRef<'_>,
         args: &[CommandToken],
     ) -> Result<(), Vec<Diagnostic>> {

metamath-rs/src/bit_set.rs

@@ -60,6 +60,7 @@ impl Bitset {
     }
 
     fn tail(&self) -> &[usize] {
+        #[allow(clippy::manual_unwrap_or_default)] // clippy#12928
         match self.tail {
             None => Default::default(),
             Some(ref bx) => bx,

metamath-rs/src/database.rs

@@ -996,7 +996,8 @@ impl Database {
     ///
     /// Currently there is no way to incrementally fetch diagnostics, so this
     /// will be a bit slow if there are thousands of errors.
-    pub fn diag_notations(&mut self) -> Vec<(StatementAddress, Diagnostic)> {
+    #[must_use]
+    pub fn diag_notations(&self) -> Vec<(StatementAddress, Diagnostic)> {
         let mut diags = self.parse_result().parse_diagnostics();
         if let Some(pass) = self.try_scope_result() {
             diags.extend(pass.diagnostics())

metamath-rs/src/diag.rs

@@ -129,6 +129,7 @@ pub enum Diagnostic {
     GrammarAmbiguous(StatementAddress),
     GrammarCantBuild(&'static str),
     GrammarProvableFloat,
+    HtmlParseError(Span, Vec<Cow<'static, str>>),
     HeaderCommentParseError(HeadingLevel),
     InvalidAxiomRestatement(Span, Span),
     IoError(String),
@@ -621,6 +622,12 @@ impl Diagnostic {
                 stmt,
                 stmt.span(),
             )]),
+            HtmlParseError(span, msg) => (format!("HTML parse error(s): {}", msg.iter().format(", ")).into(), vec![(
+                AnnotationType::Warning,
+                "in this HTML block".into(),
+                stmt,
+                *span,
+            )]),
             HeaderCommentParseError(lvl) => {
                 notes = lvl.diagnostic_note();
                 ("Invalid header comment".into(), vec![(

metamath-rs/src/lib.rs

@@ -37,6 +37,7 @@
     clippy::let_underscore_untyped,
     clippy::missing_errors_doc,
     clippy::module_name_repetitions,
+    clippy::multiple_crate_versions,
     clippy::needless_range_loop,
     clippy::option_if_let_else,
     clippy::redundant_pub_crate,
@@ -73,6 +74,8 @@ pub mod scopeck;
 pub mod statement;
 pub mod typesetting;
 pub mod verify;
+
+#[cfg(feature = "verify_markup")]
 pub mod verify_markup;
 
 #[cfg(feature = "xml")]

metamath-rs/src/util.rs

@@ -33,11 +33,7 @@ pub(crate) fn fast_extend<T: Copy>(vec: &mut Vec<T>, other: &[T]) {
     vec.reserve(other.len());
     unsafe {
         let len = vec.len();
-        short_copy(
-            other.get_unchecked(0),
-            vec.get_unchecked_mut(len),
-            other.len(),
-        );
+        short_copy(other.as_ptr(), vec.as_mut_ptr().add(len), other.len());
         vec.set_len(len + other.len());
     }
 }

metamath-rs/src/verify_markup.rs

@@ -20,6 +20,7 @@ use crate::segment_set::SourceInfo;
 use crate::statement::{StatementAddress, NO_STATEMENT};
 use crate::util::{HashMap, HashSet};
 use crate::{Database, Span, StatementRef, StatementType};
+use html5ever::tendril::{stream::Utf8LossyDecoder, Tendril, TendrilSink as _};
 use regex::bytes::Regex;
 use std::ops::Range;
 use std::sync::OnceLock;
@@ -438,7 +439,7 @@ fn verify_markup_comment(
 
     let mut temp_buffer = vec![];
     let mut in_math = None;
-    let mut in_html = None;
+    let mut in_html = None::<HtmlParser>;
     for item in CommentParser::new(buf, span) {
         match item {
             CommentItem::Text(sp) => {
@@ -450,6 +451,9 @@ fn verify_markup_comment(
                     }
                 });
                 check_uninterpreted_html(buf, sp, &mut diag);
+                if let Some(parser) = &mut in_html {
+                    parser.feed(sp.as_ref(buf))
+                }
             }
             CommentItem::StartMathMode(i) => {
                 in_math = Some(i);
@@ -481,8 +485,8 @@ fn verify_markup_comment(
                     }
                 }
             }
-            CommentItem::StartHtml(i) => in_html = Some(i),
-            CommentItem::EndHtml(_) => in_html = None,
+            CommentItem::StartHtml(i) => in_html = Some(HtmlParser::new(i)),
+            CommentItem::EndHtml(i) => in_html.take().unwrap().validate(i + 7, &mut diag),
             CommentItem::LineBreak(_)
             | CommentItem::StartSubscript(_)
             | CommentItem::EndSubscript(_)
@@ -507,8 +511,8 @@ fn verify_markup_comment(
     if let Some(i) = in_math {
         diag(Diagnostic::UnclosedMathMarkup(i as u32, span.end))
     }
-    if let Some(i) = in_html {
-        diag(Diagnostic::UnclosedHtml(i as u32, span.end))
+    if let Some(parser) = in_html {
+        diag(Diagnostic::UnclosedHtml(parser.start as u32, span.end))
     }
 }
 
@@ -565,3 +569,46 @@ impl Bibliography {
         self.0.contains(tag)
     }
 }
+
+struct HtmlParser {
+    start: usize,
+    parser: Utf8LossyDecoder<html5ever::Parser<scraper::Html>>,
+    string: String,
+}
+
+impl HtmlParser {
+    fn new(start: usize) -> Self {
+        use html5ever::{local_name, namespace_url, ns};
+        let parser = html5ever::driver::parse_fragment(
+            scraper::Html::new_fragment(),
+            html5ever::ParseOpts::default(),
+            html5ever::QualName::new(None, ns!(html), local_name!("div")),
+            vec![],
+        );
+        Self {
+            start,
+            parser: parser.from_utf8(),
+            string: String::new(),
+        }
+    }
+
+    fn feed(&mut self, text: &[u8]) {
+        self.parser.process(Tendril::from_slice(text));
+        self.string += crate::as_str(text);
+    }
+
+    fn validate(self, end: usize, diag: &mut impl FnMut(Diagnostic)) {
+        let mut errors = self.parser.finish().errors;
+        if !errors.is_empty() {
+            // html5ever has garbage error messages (https://github.com/servo/html5ever/issues/492)
+            // but apparently there aren't any other HTML validators and I'm not going to write one
+            // myself
+            errors.sort();
+            errors.dedup();
+            diag(Diagnostic::HtmlParseError(
+                Span::new(self.start, end),
+                errors,
+            ))
+        }
+    }
+}