metamath · digama0 · Nov 27, 2023 · Nov 25, 2023 · Nov 26, 2023
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,42 +1,20 @@
-[package]
+[workspace]
+members = [
+    "metamath-rs",
+    "metamath-knife",
+]
+resolver = "2"
+
+[workspace.package]
 authors = ["David A. Wheeler <[email protected]>", "Stefan O'Rear <[email protected]>"]
 license = "MIT OR Apache-2.0"
-name = "metamath-knife"
 readme = "README.md"
-version = "0.3.6"
 description = "A parallel and incremental verifier for Metamath databases"
-repository = "https://github.com/david-a-wheeler/metamath-knife"
+repository = "https://github.com/metamath/metamath-knife"
 keywords = ["theorem", "proving", "verifier", "proof", "assistant"]
 categories = ["command-line-utilities", "development-tools", "mathematics"]
 edition = "2021"
 
-[dependencies]
-lazy_static = "1.4"
-itertools = "0.10"
-filetime = "0.2"
-fnv = "1.0"
-regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
-tinyvec = "1.5"
-log = "0.4"
-annotate-snippets = "0.9"
-typed-arena = "2.0"
-
-# Dependencies for standalone executable, not needed for a library
-clap = "2.33"
-simple_logger = "1.13"
-
-# Optional dependencies
-dot-writer = { version = "0.1.2", optional = true }
-xml-rs = { version = "0.8.14", optional = true }
-
-[dev-dependencies]
-assert_matches = "1.5"
-
-[features]
-default = ["annotate-snippets/color"]
-dot = ["dot-writer"]
-xml = ["xml-rs"]
-
 [profile]
 
 [profile.release]
@@ -49,8 +27,3 @@ codegen-units = 4
 
 [profile.test]
 codegen-units = 4
-
-[[bin]]
-name = "metamath-knife"
-path = "src/main.rs"
-doc = false
diff --git a/metamath-knife/Cargo.toml b/metamath-knife/Cargo.toml
@@ -0,0 +1,22 @@
+[package]
+name = "metamath-knife"
+readme = "metamath-knife/README.md"
+description = "A command-line tool for Metamath, including parallel and incremental verifier for Metamath databases"
+version = "0.3.6"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+clap = "2.33"
+simple_logger = "1.13"
+annotate-snippets = "0.9"
+metamath-rs = { path = "../metamath-rs" }
+
+[[bin]]
+name = "metamath-knife"
+path = "src/main.rs"
+doc = false
diff --git a/src/main.rs → metamath-knife/src/main.rs b/src/main.rs → metamath-knife/src/main.rs
@@ -4,12 +4,12 @@
 
 use annotate_snippets::display_list::DisplayList;
 use clap::{clap_app, crate_version};
-use metamath_knife::database::{Database, DbOptions};
-use metamath_knife::diag::BibError;
-use metamath_knife::parser::is_valid_label;
-use metamath_knife::statement::StatementAddress;
-use metamath_knife::verify_markup::{Bibliography, Bibliography2};
-use metamath_knife::SourceInfo;
+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};

diff --git a/metamath-rs/Cargo.toml b/metamath-rs/Cargo.toml
@@ -0,0 +1,34 @@
+[package]
+name = "metamath-rs"
+readme = "metamath-rs/README.md"
+description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases"
+version = "0.3.6"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+lazy_static = "1.4"
+itertools = "0.10"
+filetime = "0.2"
+fnv = "1.0"
+regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
+tinyvec = "1.5"
+log = "0.4"
+annotate-snippets = "0.9"
+typed-arena = "2.0"
+
+# Optional dependencies
+dot-writer = { version = "0.1.2", optional = true }
+xml-rs = { version = "0.8.14", optional = true }
+
+[dev-dependencies]
+assert_matches = "1.5"
+
+[features]
+default = ["annotate-snippets/color"]
+dot = ["dot-writer"]
+xml = ["xml-rs"]
diff --git a/src/axiom_use.rs → metamath-rs/src/axiom_use.rs b/src/axiom_use.rs → metamath-rs/src/axiom_use.rs
diff --git a/src/bit_set.rs → metamath-rs/src/bit_set.rs b/src/bit_set.rs → metamath-rs/src/bit_set.rs
diff --git a/src/comment_parser.rs → metamath-rs/src/comment_parser.rs b/src/comment_parser.rs → metamath-rs/src/comment_parser.rs
diff --git a/src/comment_parser_tests.rs → metamath-rs/src/comment_parser_tests.rs b/src/comment_parser_tests.rs → metamath-rs/src/comment_parser_tests.rs
diff --git a/src/database.rs → metamath-rs/src/database.rs b/src/database.rs → metamath-rs/src/database.rs
diff --git a/src/diag.rs → metamath-rs/src/diag.rs b/src/diag.rs → metamath-rs/src/diag.rs
diff --git a/src/discouraged.rs → metamath-rs/src/discouraged.rs b/src/discouraged.rs → metamath-rs/src/discouraged.rs
diff --git a/src/export.rs → metamath-rs/src/export.rs b/src/export.rs → metamath-rs/src/export.rs
diff --git a/src/export_deps.rs → metamath-rs/src/export_deps.rs b/src/export_deps.rs → metamath-rs/src/export_deps.rs
diff --git a/src/formula.rs → metamath-rs/src/formula.rs b/src/formula.rs → metamath-rs/src/formula.rs
diff --git a/src/formula_tests.rs → metamath-rs/src/formula_tests.rs b/src/formula_tests.rs → metamath-rs/src/formula_tests.rs
diff --git a/src/grammar.rs → metamath-rs/src/grammar.rs b/src/grammar.rs → metamath-rs/src/grammar.rs
@@ -139,7 +139,7 @@ impl GrammarTree {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
@@ -1675,7 +1675,7 @@ impl Grammar {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();

diff --git a/src/grammar_tests.rs → metamath-rs/src/grammar_tests.rs b/src/grammar_tests.rs → metamath-rs/src/grammar_tests.rs
diff --git a/src/lib.rs → metamath-rs/src/lib.rs b/src/lib.rs → metamath-rs/src/lib.rs
diff --git a/src/line_cache.rs → metamath-rs/src/line_cache.rs b/src/line_cache.rs → metamath-rs/src/line_cache.rs
diff --git a/src/nameck.rs → metamath-rs/src/nameck.rs b/src/nameck.rs → metamath-rs/src/nameck.rs
diff --git a/src/outline.rs → metamath-rs/src/outline.rs b/src/outline.rs → metamath-rs/src/outline.rs
diff --git a/src/parser.rs → metamath-rs/src/parser.rs b/src/parser.rs → metamath-rs/src/parser.rs
diff --git a/src/parser_tests.rs → metamath-rs/src/parser_tests.rs b/src/parser_tests.rs → metamath-rs/src/parser_tests.rs
diff --git a/src/proof.rs → metamath-rs/src/proof.rs b/src/proof.rs → metamath-rs/src/proof.rs
diff --git a/src/scopeck.rs → metamath-rs/src/scopeck.rs b/src/scopeck.rs → metamath-rs/src/scopeck.rs
diff --git a/src/segment.rs → metamath-rs/src/segment.rs b/src/segment.rs → metamath-rs/src/segment.rs
diff --git a/src/segment_set.rs → metamath-rs/src/segment_set.rs b/src/segment_set.rs → metamath-rs/src/segment_set.rs
diff --git a/src/statement.rs → metamath-rs/src/statement.rs b/src/statement.rs → metamath-rs/src/statement.rs
diff --git a/src/tree.rs → metamath-rs/src/tree.rs b/src/tree.rs → metamath-rs/src/tree.rs
diff --git a/src/typesetting.rs → metamath-rs/src/typesetting.rs b/src/typesetting.rs → metamath-rs/src/typesetting.rs
@@ -1,7 +1,7 @@
 //! The typesetting data.
 //!
 //! This is the result of parsing a `$t` metamath comment, which contains information
-//! used by the metamath website generator. Although `metamath-knife` tries to be
+//! used by the metamath website generator. Although `metamath-rs` tries to be
 //! generic and so it does not itself contain a website generator, this pass can be
 //! used to collect information for generating HTML in the style of
 //! [`metamath.exe`](https://github.com/metamath/metamath-exe).

diff --git a/src/usage_tests.rs → metamath-rs/src/usage_tests.rs b/src/usage_tests.rs → metamath-rs/src/usage_tests.rs
diff --git a/src/util.rs → metamath-rs/src/util.rs b/src/util.rs → metamath-rs/src/util.rs
diff --git a/src/util_tests.rs → metamath-rs/src/util_tests.rs b/src/util_tests.rs → metamath-rs/src/util_tests.rs
diff --git a/src/verify.rs → metamath-rs/src/verify.rs b/src/verify.rs → metamath-rs/src/verify.rs
diff --git a/src/verify_markup.rs → metamath-rs/src/verify_markup.rs b/src/verify_markup.rs → metamath-rs/src/verify_markup.rs