From f0b7f558c2fecd5a18dff69e84ced3b0ef11d368 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sat, 25 Nov 2023 18:30:32 +0100 Subject: [PATCH 1/2] Split into library and binary --- Cargo.lock | 12 ++++- Cargo.toml | 44 ++++--------------- metamath-knife/Cargo.toml | 22 ++++++++++ {src => metamath-knife/src}/main.rs | 12 ++--- metamath-rs/Cargo.toml | 34 ++++++++++++++ {src => metamath-rs/src}/axiom_use.rs | 0 {src => metamath-rs/src}/bit_set.rs | 0 {src => metamath-rs/src}/comment_parser.rs | 0 .../src}/comment_parser_tests.rs | 0 {src => metamath-rs/src}/database.rs | 0 {src => metamath-rs/src}/diag.rs | 0 {src => metamath-rs/src}/discouraged.rs | 0 {src => metamath-rs/src}/export.rs | 0 {src => metamath-rs/src}/export_deps.rs | 0 {src => metamath-rs/src}/formula.rs | 0 {src => metamath-rs/src}/formula_tests.rs | 0 {src => metamath-rs/src}/grammar.rs | 4 +- {src => metamath-rs/src}/grammar_tests.rs | 0 {src => metamath-rs/src}/lib.rs | 0 {src => metamath-rs/src}/line_cache.rs | 0 {src => metamath-rs/src}/nameck.rs | 0 {src => metamath-rs/src}/outline.rs | 0 {src => metamath-rs/src}/parser.rs | 0 {src => metamath-rs/src}/parser_tests.rs | 0 {src => metamath-rs/src}/proof.rs | 0 {src => metamath-rs/src}/scopeck.rs | 0 {src => metamath-rs/src}/segment.rs | 0 {src => metamath-rs/src}/segment_set.rs | 0 {src => metamath-rs/src}/statement.rs | 0 {src => metamath-rs/src}/tree.rs | 0 {src => metamath-rs/src}/typesetting.rs | 2 +- {src => metamath-rs/src}/usage_tests.rs | 0 {src => metamath-rs/src}/util.rs | 0 {src => metamath-rs/src}/util_tests.rs | 0 {src => metamath-rs/src}/verify.rs | 0 {src => metamath-rs/src}/verify_markup.rs | 0 36 files changed, 84 insertions(+), 46 deletions(-) create mode 100644 metamath-knife/Cargo.toml rename {src => metamath-knife/src}/main.rs (97%) create mode 100644 metamath-rs/Cargo.toml rename {src => metamath-rs/src}/axiom_use.rs (100%) rename {src => metamath-rs/src}/bit_set.rs (100%) rename {src => metamath-rs/src}/comment_parser.rs (100%) rename {src => metamath-rs/src}/comment_parser_tests.rs (100%) rename {src => metamath-rs/src}/database.rs (100%) rename {src => metamath-rs/src}/diag.rs (100%) rename {src => metamath-rs/src}/discouraged.rs (100%) rename {src => metamath-rs/src}/export.rs (100%) rename {src => metamath-rs/src}/export_deps.rs (100%) rename {src => metamath-rs/src}/formula.rs (100%) rename {src => metamath-rs/src}/formula_tests.rs (100%) rename {src => metamath-rs/src}/grammar.rs (99%) rename {src => metamath-rs/src}/grammar_tests.rs (100%) rename {src => metamath-rs/src}/lib.rs (100%) rename {src => metamath-rs/src}/line_cache.rs (100%) rename {src => metamath-rs/src}/nameck.rs (100%) rename {src => metamath-rs/src}/outline.rs (100%) rename {src => metamath-rs/src}/parser.rs (100%) rename {src => metamath-rs/src}/parser_tests.rs (100%) rename {src => metamath-rs/src}/proof.rs (100%) rename {src => metamath-rs/src}/scopeck.rs (100%) rename {src => metamath-rs/src}/segment.rs (100%) rename {src => metamath-rs/src}/segment_set.rs (100%) rename {src => metamath-rs/src}/statement.rs (100%) rename {src => metamath-rs/src}/tree.rs (100%) rename {src => metamath-rs/src}/typesetting.rs (99%) rename {src => metamath-rs/src}/usage_tests.rs (100%) rename {src => metamath-rs/src}/util.rs (100%) rename {src => metamath-rs/src}/util_tests.rs (100%) rename {src => metamath-rs/src}/verify.rs (100%) rename {src => metamath-rs/src}/verify_markup.rs (100%) diff --git a/Cargo.lock b/Cargo.lock index 6be8934..063c718 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -168,8 +168,17 @@ name = "metamath-knife" version = "0.3.6" dependencies = [ "annotate-snippets", - "assert_matches", "clap", + "metamath-rs", + "simple_logger", +] + +[[package]] +name = "metamath-rs" +version = "0.3.6" +dependencies = [ + "annotate-snippets", + "assert_matches", "dot-writer", "filetime", "fnv", @@ -177,7 +186,6 @@ dependencies = [ "lazy_static", "log", "regex", - "simple_logger", "tinyvec", "typed-arena", "xml-rs", diff --git a/Cargo.toml b/Cargo.toml index 92713c2..b2d3348 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,42 +1,21 @@ -[package] +[workspace] +members = [ + "metamath-rs", + "metamath-knife", +] +resolver = "2" + +[workspace.package] authors = ["David A. Wheeler ", "Stefan O'Rear "] 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 +28,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 new file mode 100644 index 0000000..26ab9e8 --- /dev/null +++ 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.workspace = true +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 b/metamath-knife/src/main.rs similarity index 97% rename from src/main.rs rename to metamath-knife/src/main.rs index 44404fb..920aba1 100644 --- a/src/main.rs +++ b/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 new file mode 100644 index 0000000..72ba013 --- /dev/null +++ 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.workspace = true +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 b/metamath-rs/src/axiom_use.rs similarity index 100% rename from src/axiom_use.rs rename to metamath-rs/src/axiom_use.rs diff --git a/src/bit_set.rs b/metamath-rs/src/bit_set.rs similarity index 100% rename from src/bit_set.rs rename to metamath-rs/src/bit_set.rs diff --git a/src/comment_parser.rs b/metamath-rs/src/comment_parser.rs similarity index 100% rename from src/comment_parser.rs rename to metamath-rs/src/comment_parser.rs diff --git a/src/comment_parser_tests.rs b/metamath-rs/src/comment_parser_tests.rs similarity index 100% rename from src/comment_parser_tests.rs rename to metamath-rs/src/comment_parser_tests.rs diff --git a/src/database.rs b/metamath-rs/src/database.rs similarity index 100% rename from src/database.rs rename to metamath-rs/src/database.rs diff --git a/src/diag.rs b/metamath-rs/src/diag.rs similarity index 100% rename from src/diag.rs rename to metamath-rs/src/diag.rs diff --git a/src/discouraged.rs b/metamath-rs/src/discouraged.rs similarity index 100% rename from src/discouraged.rs rename to metamath-rs/src/discouraged.rs diff --git a/src/export.rs b/metamath-rs/src/export.rs similarity index 100% rename from src/export.rs rename to metamath-rs/src/export.rs diff --git a/src/export_deps.rs b/metamath-rs/src/export_deps.rs similarity index 100% rename from src/export_deps.rs rename to metamath-rs/src/export_deps.rs diff --git a/src/formula.rs b/metamath-rs/src/formula.rs similarity index 100% rename from src/formula.rs rename to metamath-rs/src/formula.rs diff --git a/src/formula_tests.rs b/metamath-rs/src/formula_tests.rs similarity index 100% rename from src/formula_tests.rs rename to metamath-rs/src/formula_tests.rs diff --git a/src/grammar.rs b/metamath-rs/src/grammar.rs similarity index 99% rename from src/grammar.rs rename to metamath-rs/src/grammar.rs index cb6f901..5aa03a0 100644 --- a/src/grammar.rs +++ b/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 b/metamath-rs/src/grammar_tests.rs similarity index 100% rename from src/grammar_tests.rs rename to metamath-rs/src/grammar_tests.rs diff --git a/src/lib.rs b/metamath-rs/src/lib.rs similarity index 100% rename from src/lib.rs rename to metamath-rs/src/lib.rs diff --git a/src/line_cache.rs b/metamath-rs/src/line_cache.rs similarity index 100% rename from src/line_cache.rs rename to metamath-rs/src/line_cache.rs diff --git a/src/nameck.rs b/metamath-rs/src/nameck.rs similarity index 100% rename from src/nameck.rs rename to metamath-rs/src/nameck.rs diff --git a/src/outline.rs b/metamath-rs/src/outline.rs similarity index 100% rename from src/outline.rs rename to metamath-rs/src/outline.rs diff --git a/src/parser.rs b/metamath-rs/src/parser.rs similarity index 100% rename from src/parser.rs rename to metamath-rs/src/parser.rs diff --git a/src/parser_tests.rs b/metamath-rs/src/parser_tests.rs similarity index 100% rename from src/parser_tests.rs rename to metamath-rs/src/parser_tests.rs diff --git a/src/proof.rs b/metamath-rs/src/proof.rs similarity index 100% rename from src/proof.rs rename to metamath-rs/src/proof.rs diff --git a/src/scopeck.rs b/metamath-rs/src/scopeck.rs similarity index 100% rename from src/scopeck.rs rename to metamath-rs/src/scopeck.rs diff --git a/src/segment.rs b/metamath-rs/src/segment.rs similarity index 100% rename from src/segment.rs rename to metamath-rs/src/segment.rs diff --git a/src/segment_set.rs b/metamath-rs/src/segment_set.rs similarity index 100% rename from src/segment_set.rs rename to metamath-rs/src/segment_set.rs diff --git a/src/statement.rs b/metamath-rs/src/statement.rs similarity index 100% rename from src/statement.rs rename to metamath-rs/src/statement.rs diff --git a/src/tree.rs b/metamath-rs/src/tree.rs similarity index 100% rename from src/tree.rs rename to metamath-rs/src/tree.rs diff --git a/src/typesetting.rs b/metamath-rs/src/typesetting.rs similarity index 99% rename from src/typesetting.rs rename to metamath-rs/src/typesetting.rs index 799c106..4e3b7e9 100644 --- a/src/typesetting.rs +++ b/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 b/metamath-rs/src/usage_tests.rs similarity index 100% rename from src/usage_tests.rs rename to metamath-rs/src/usage_tests.rs diff --git a/src/util.rs b/metamath-rs/src/util.rs similarity index 100% rename from src/util.rs rename to metamath-rs/src/util.rs diff --git a/src/util_tests.rs b/metamath-rs/src/util_tests.rs similarity index 100% rename from src/util_tests.rs rename to metamath-rs/src/util_tests.rs diff --git a/src/verify.rs b/metamath-rs/src/verify.rs similarity index 100% rename from src/verify.rs rename to metamath-rs/src/verify.rs diff --git a/src/verify_markup.rs b/metamath-rs/src/verify_markup.rs similarity index 100% rename from src/verify_markup.rs rename to metamath-rs/src/verify_markup.rs From 476fd5be21722664bc3554eb93684b796c6cf4d0 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Mon, 27 Nov 2023 00:08:56 +0100 Subject: [PATCH 2/2] Different versions for library and binary --- Cargo.toml | 1 - metamath-knife/Cargo.toml | 2 +- metamath-rs/Cargo.toml | 2 +- 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index b2d3348..4e1682e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,6 @@ resolver = "2" authors = ["David A. Wheeler ", "Stefan O'Rear "] license = "MIT OR Apache-2.0" readme = "README.md" -version = "0.3.6" description = "A parallel and incremental verifier for Metamath databases" repository = "https://github.com/metamath/metamath-knife" keywords = ["theorem", "proving", "verifier", "proof", "assistant"] diff --git a/metamath-knife/Cargo.toml b/metamath-knife/Cargo.toml index 26ab9e8..ae205ba 100644 --- a/metamath-knife/Cargo.toml +++ b/metamath-knife/Cargo.toml @@ -2,7 +2,7 @@ name = "metamath-knife" readme = "metamath-knife/README.md" description = "A command-line tool for Metamath, including parallel and incremental verifier for Metamath databases" -version.workspace = true +version = "0.3.6" authors.workspace = true license.workspace = true repository.workspace = true diff --git a/metamath-rs/Cargo.toml b/metamath-rs/Cargo.toml index 72ba013..7d4a4fa 100644 --- a/metamath-rs/Cargo.toml +++ b/metamath-rs/Cargo.toml @@ -2,7 +2,7 @@ name = "metamath-rs" readme = "metamath-rs/README.md" description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases" -version.workspace = true +version = "0.3.6" authors.workspace = true license.workspace = true repository.workspace = true