From f9a940da9e0bd0fd185881017c908e319c0d2b06 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 30 Jul 2024 22:31:21 +0200 Subject: [PATCH] update dependencies fixes #165 --- Cargo.lock | 555 +++++++++++++++++++++------------ metamath-knife/Cargo.toml | 10 +- metamath-knife/src/main.rs | 284 +++++++++-------- metamath-rs/Cargo.toml | 10 +- metamath-rs/src/database.rs | 4 +- metamath-rs/src/diag.rs | 362 ++++++++++----------- metamath-rs/src/scopeck.rs | 18 +- metamath-rs/src/segment_set.rs | 11 +- 8 files changed, 710 insertions(+), 544 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index af4978d..edc216c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -17,54 +17,83 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.0.1" +version = "1.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67fc08ce920c31afb70f013dcce1bfc3a3195de6a228474e45e1f145b36f8d04" +checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916" dependencies = [ "memchr", ] [[package]] name = "annotate-snippets" -version = "0.9.1" +version = "0.11.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3b9d411ecbaf79885c6df4d75fff75858d5995ff25385657a28af47e82f9c36" +checksum = "24e35ed54e5ea7997c14ed4c70ba043478db1112e98263b3b035907aa197d991" dependencies = [ + "anstyle", "unicode-width", - "yansi-term", ] [[package]] -name = "ansi_term" -version = "0.12.1" +name = "anstream" +version = "0.6.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" dependencies = [ - "winapi", + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", ] [[package]] -name = "assert_matches" -version = "1.5.0" +name = "anstyle" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b34d609dfbaf33d6889b2b7106d3ca345eacad44200913df5ba02bfd31d2ba9" +checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" [[package]] -name = "atty" -version = "0.2.14" +name = "anstyle-parse" +version = "0.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" dependencies = [ - "hermit-abi", - "libc", - "winapi", + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" +dependencies = [ + "windows-sys 0.52.0", ] +[[package]] +name = "anstyle-wincon" +version = "3.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" +dependencies = [ + "anstyle", + "windows-sys 0.52.0", +] + +[[package]] +name = "assert_matches" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b34d609dfbaf33d6889b2b7106d3ca345eacad44200913df5ba02bfd31d2ba9" + [[package]] name = "autocfg" -version = "1.2.0" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1fdabc7756949593fe60f30ec81974b613357de856987752631dea1e3394c80" +checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" [[package]] name = "bitflags" @@ -74,9 +103,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" +checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "byteorder" @@ -92,28 +121,58 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "2.34.0" +version = "4.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" +checksum = "35723e6a11662c2afb578bcf0b88bf6ea8e21282a953428f240574fcc3a2b5b3" dependencies = [ - "ansi_term", - "atty", - "bitflags 1.3.2", + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.5.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49eb96cbfa7cfa35017b7cd548c75b14c3118c98b423041d70562665e07fb0fa" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", "strsim", - "textwrap", - "unicode-width", - "vec_map", ] +[[package]] +name = "clap_derive" +version = "4.5.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d029b67f89d30bbb547c89fd5161293c0aec155fc691d7924b64550662db93e" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "0.7.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" + +[[package]] +name = "colorchoice" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" + [[package]] name = "colored" -version = "1.9.3" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f4ffc801dacf156c5854b9df4f425a626539c3a6ef7893cc0c5084a23f0b6c59" +checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" dependencies = [ - "atty", "lazy_static", - "winapi", + "windows-sys 0.48.0", ] [[package]] @@ -136,18 +195,27 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13b588ba4ac1a99f7f2964d24b3d896ddc6bf847ee3855dbd4366f058cfcd331" dependencies = [ "quote", - "syn 2.0.60", + "syn", +] + +[[package]] +name = "deranged" +version = "0.3.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4" +dependencies = [ + "powerfmt", ] [[package]] name = "derive_more" -version = "0.99.17" +version = "0.99.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fb810d30a7c1953f91334de7244731fc3f3c10d7fe163338a35b9f640960321" +checksum = "5f33878137e4dafd7fa914ad4e259e18a4e8e532b9617a2d0150262bf53abfce" dependencies = [ "proc-macro2", "quote", - "syn 1.0.109", + "syn", ] [[package]] @@ -164,9 +232,9 @@ checksum = "dcbb2bf8e87535c23f7a8a321e364ce21462d0ff10cb6407820e8e96dfff6653" [[package]] name = "dtoa-short" -version = "0.3.4" +version = "0.3.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dbaceec3c6e4211c79e7b1800fb9680527106beb2f9c51904a3210c03a448c74" +checksum = "cd1511a7b6a56299bd043a9c167a6d2bfb37bf84a6dfceaba651168adfb43c87" dependencies = [ "dtoa", ] @@ -179,20 +247,20 @@ checksum = "3a68a4904193147e0a8dec3314640e6db742afd5f6e634f428a6af230d9b3591" [[package]] name = "either" -version = "1.8.1" +version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" +checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" [[package]] name = "filetime" -version = "0.2.21" +version = "0.2.23" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5cbc844cecaee9d4443931972e1289c8ff485cb4cc2767cb03ca139ed6885153" +checksum = "1ee447700ac8aa0b2f2bd7bc4462ad686ba06baa6727ac149a2d6277f0d240fd" dependencies = [ "cfg-if", "libc", - "redox_syscall 0.2.16", - "windows-sys", + "redox_syscall 0.4.1", + "windows-sys 0.52.0", ] [[package]] @@ -231,9 +299,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.14" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94b22e06ecb0110981051723910cbf0b5f5e09a2062dd7663334ee79a9d1286c" +checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" dependencies = [ "cfg-if", "libc", @@ -241,60 +309,63 @@ dependencies = [ ] [[package]] -name = "hermit-abi" -version = "0.1.19" +name = "heck" +version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" -dependencies = [ - "libc", -] +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "html5ever" -version = "0.26.0" +version = "0.27.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bea68cab48b8459f17cf1c944c67ddc572d272d9f2b274140f223ecb1da4a3b7" +checksum = "c13771afe0e6e846f1e67d038d4cb29998a6779f93c809212e4e9c32efd244d4" dependencies = [ "log", "mac", "markup5ever", "proc-macro2", "quote", - "syn 1.0.109", + "syn", ] +[[package]] +name = "is_terminal_polyfill" +version = "1.70.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" + [[package]] name = "itertools" -version = "0.12.0" +version = "0.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25db6b064527c5d482d0423354fcd07a89a2dfe07b67892e62411946db7f07b0" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" dependencies = [ "either", ] [[package]] name = "itoa" -version = "1.0.6" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" +checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "lazy_static" -version = "1.4.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" +checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.153" +version = "0.2.155" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" +checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" [[package]] name = "lock_api" -version = "0.4.11" +version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" +checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17" dependencies = [ "autocfg", "scopeguard", @@ -302,9 +373,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.18" +version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "518ef76f2f87365916b142844c16d8fefd85039bc5699050210a7778ee1cd1de" +checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" [[package]] name = "mac" @@ -314,13 +385,13 @@ checksum = "c41e0c4fef86961ac6d6f8a82609f55f31b05e4fce149ac5710e439df7619ba4" [[package]] name = "markup5ever" -version = "0.11.0" +version = "0.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a2629bb1404f3d34c2e921f21fd34ba00b206124c81f65c50b43b6aaefeb016" +checksum = "16ce3abbeba692c8b8441d036ef91aea6df8da2c6b6e21c7e14d3c18e526be45" dependencies = [ "log", - "phf 0.10.1", - "phf_codegen", + "phf 0.11.2", + "phf_codegen 0.11.2", "string_cache", "string_cache_codegen", "tendril", @@ -328,13 +399,13 @@ dependencies = [ [[package]] name = "memchr" -version = "2.5.0" +version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" [[package]] name = "metamath-knife" -version = "0.3.8" +version = "0.3.9" dependencies = [ "annotate-snippets", "clap", @@ -344,7 +415,7 @@ dependencies = [ [[package]] name = "metamath-rs" -version = "0.3.8" +version = "0.3.9" dependencies = [ "annotate-snippets", "assert_matches", @@ -367,11 +438,17 @@ version = "1.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "650eef8c711430f1a879fdd01d4745a7deea475becfb90269c06775983bbf086" +[[package]] +name = "num-conv" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9" + [[package]] name = "num_threads" -version = "0.1.6" +version = "0.1.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2819ce041d2ee131036f4fc9d6ae7ae125a3a40e97ba64d04fe799ad9dabbb44" +checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9" dependencies = [ "libc", ] @@ -384,9 +461,9 @@ checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "parking_lot" -version = "0.12.1" +version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +checksum = "f1bf18183cf54e8d6059647fc3063646a1801cf30896933ec2311622cc4b9a27" dependencies = [ "lock_api", "parking_lot_core", @@ -394,15 +471,15 @@ dependencies = [ [[package]] name = "parking_lot_core" -version = "0.9.9" +version = "0.9.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e" +checksum = "1e401f977ab385c9e4e3ab30627d6f26d00e2c73eef317493c4ec6d468726cf8" dependencies = [ "cfg-if", "libc", - "redox_syscall 0.4.1", + "redox_syscall 0.5.3", "smallvec", - "windows-targets", + "windows-targets 0.52.6", ] [[package]] @@ -434,6 +511,16 @@ dependencies = [ "phf_shared 0.10.0", ] +[[package]] +name = "phf_codegen" +version = "0.11.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e8d39688d359e6b34654d328e262234662d16cc0f60ec8dcbe5e718709342a5a" +dependencies = [ + "phf_generator 0.11.2", + "phf_shared 0.11.2", +] + [[package]] name = "phf_generator" version = "0.10.0" @@ -464,7 +551,7 @@ dependencies = [ "phf_shared 0.11.2", "proc-macro2", "quote", - "syn 2.0.60", + "syn", ] [[package]] @@ -485,11 +572,21 @@ dependencies = [ "siphasher", ] +[[package]] +name = "powerfmt" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" + [[package]] name = "ppv-lite86" -version = "0.2.17" +version = "0.2.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" +checksum = "2288c0e17cc8d342c712bb43a257a80ebffce59cdb33d5000d8348f3ec02528b" +dependencies = [ + "zerocopy", + "zerocopy-derive", +] [[package]] name = "precomputed-hash" @@ -499,9 +596,9 @@ checksum = "925383efa346730478fb4838dbe9137d2a47675ad789c546d150a6e1dd4ab31c" [[package]] name = "proc-macro2" -version = "1.0.81" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d1597b0c024618f09a9c3b8655b7e430397a36d23fdafec26d6965e9eec3eba" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" dependencies = [ "unicode-ident", ] @@ -547,27 +644,39 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.2.16" +version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a" +checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" dependencies = [ "bitflags 1.3.2", ] [[package]] name = "redox_syscall" -version = "0.4.1" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" +checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4" dependencies = [ - "bitflags 1.3.2", + "bitflags 2.6.0", ] [[package]] name = "regex" -version = "1.8.3" +version = "1.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81ca098a9821bd52d6b24fd8b10bd081f47d39c22778cafaa75a2857a62c6390" +checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df" dependencies = [ "aho-corasick", "memchr", @@ -576,9 +685,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.7.2" +version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "436b050e76ed2903236f032a59761c1eb99e1b0aead2c257922771dab1fc8c78" +checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b" [[package]] name = "scopeguard" @@ -588,9 +697,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "scraper" -version = "0.19.0" +version = "0.19.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b80b33679ff7a0ea53d37f3b39de77ea0c75b12c5805ac43ec0c33b3051af1b" +checksum = "761fb705fdf625482d2ed91d3f0559dcfeab2798fe2771c69560a774865d0802" dependencies = [ "ahash", "cssparser", @@ -608,14 +717,14 @@ version = "0.25.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4eb30575f3638fc8f6815f448d50cb1a2e255b0897985c8c59f4d37b72a07b06" dependencies = [ - "bitflags 2.5.0", + "bitflags 2.6.0", "cssparser", "derive_more", "fxhash", "log", "new_debug_unreachable", "phf 0.10.1", - "phf_codegen", + "phf_codegen 0.10.0", "precomputed-hash", "servo_arc", "smallvec", @@ -623,9 +732,23 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.163" +version = "1.0.204" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2113ab51b87a539ae008b5c6c02dc020ffa39afd2d83cffcb3f4eb2722cebec2" +checksum = "bc76f558e0cbb2a839d37354c575f1dc3fdc6546b5be373ba43d95f231bf7c12" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.204" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] [[package]] name = "servo_arc" @@ -638,15 +761,14 @@ dependencies = [ [[package]] name = "simple_logger" -version = "1.16.0" +version = "5.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45b60258a35dc3cb8a16890b8fd6723349bfa458d7960e25e633f1b1c19d7b5e" +checksum = "e8c5dfa5e08767553704aa0ffd9d9794d527103c736aba9854773851fd7497eb" dependencies = [ - "atty", "colored", "log", "time", - "winapi", + "windows-sys 0.48.0", ] [[package]] @@ -695,26 +817,15 @@ dependencies = [ [[package]] name = "strsim" -version = "0.8.0" +version = "0.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "syn" -version = "1.0.109" +version = "2.0.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.60" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "909518bc7b1c9b779f1bbf07f2929d35af9f0f37e47c6e9ef7f9dddc1e1821f3" +checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af" dependencies = [ "proc-macro2", "quote", @@ -732,24 +843,18 @@ dependencies = [ "utf-8", ] -[[package]] -name = "textwrap" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" -dependencies = [ - "unicode-width", -] - [[package]] name = "time" -version = "0.3.21" +version = "0.3.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f3403384eaacbca9923fa06940178ac13e4edb725486d70e8e15881d0c836cc" +checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885" dependencies = [ + "deranged", "itoa", "libc", + "num-conv", "num_threads", + "powerfmt", "serde", "time-core", "time-macros", @@ -757,24 +862,25 @@ dependencies = [ [[package]] name = "time-core" -version = "0.1.1" +version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7300fbefb4dadc1af235a9cef3737cea692a9d97e1b9cbcd4ebdae6f8868e6fb" +checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3" [[package]] name = "time-macros" -version = "0.2.9" +version = "0.2.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "372950940a5f07bf38dbe211d7283c9e6d7327df53794992d293e534c733d09b" +checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf" dependencies = [ + "num-conv", "time-core", ] [[package]] name = "tinyvec" -version = "1.6.0" +version = "1.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "87cc5ceb3875bb20c2890005a4e226a4651264a5c75edb2421b52861a0a0cb50" +checksum = "445e881f4f6d382d5f27c034e25eb92edd7c784ceab92a0937db7f2e9471b938" [[package]] name = "typed-arena" @@ -790,9 +896,9 @@ checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" [[package]] name = "unicode-width" -version = "0.1.10" +version = "0.1.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" +checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d" [[package]] name = "utf-8" @@ -801,16 +907,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09cc8ee72d2a9becf2f2febe0205bbed8fc6615b7cb429ad062dc7b7ddd036a9" [[package]] -name = "vec_map" -version = "0.8.2" +name = "utf8parse" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" [[package]] name = "version_check" -version = "0.9.4" +version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "wasi" @@ -819,124 +925,167 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] -name = "winapi" -version = "0.3.9" +name = "windows-sys" +version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "winapi-i686-pc-windows-gnu", - "winapi-x86_64-pc-windows-gnu", + "windows-targets 0.48.5", ] [[package]] -name = "winapi-i686-pc-windows-gnu" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" - -[[package]] -name = "winapi-x86_64-pc-windows-gnu" -version = "0.4.0" +name = "windows-sys" +version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets 0.52.6", +] [[package]] -name = "windows-sys" -version = "0.48.0" +name = "windows-targets" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" dependencies = [ - "windows-targets", + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", ] [[package]] name = "windows-targets" -version = "0.48.0" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_aarch64_gnullvm 0.52.6", + "windows_aarch64_msvc 0.52.6", + "windows_i686_gnu 0.52.6", + "windows_i686_gnullvm", + "windows_i686_msvc 0.52.6", + "windows_x86_64_gnu 0.52.6", + "windows_x86_64_gnullvm 0.52.6", + "windows_x86_64_msvc 0.52.6", ] [[package]] name = "windows_aarch64_gnullvm" -version = "0.48.0" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" [[package]] name = "windows_aarch64_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" [[package]] name = "windows_i686_gnu" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" [[package]] name = "windows_i686_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" [[package]] name = "windows_x86_64_gnu" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" [[package]] name = "windows_x86_64_gnullvm" -version = "0.48.0" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" [[package]] name = "windows_x86_64_msvc" -version = "0.48.0" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] -name = "xml-rs" -version = "0.8.14" +name = "windows_x86_64_msvc" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52839dc911083a8ef63efa4d039d1f58b5e409f923e44c80828f206f66e5541c" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] -name = "yansi-term" -version = "0.1.2" +name = "xml-rs" +version = "0.8.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe5c30ade05e61656247b2e334a031dfd0cc466fadef865bdcdea8d537951bf1" -dependencies = [ - "winapi", -] +checksum = "791978798f0597cfc70478424c2b4fdc2b7a8024aaff78497ef00f24ef674193" [[package]] name = "zerocopy" -version = "0.7.32" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be" +checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" dependencies = [ + "byteorder", "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.32" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" +checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.60", + "syn", ] diff --git a/metamath-knife/Cargo.toml b/metamath-knife/Cargo.toml index d563bc8..f3ace8f 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 = "0.3.8" +version = "0.3.9" authors.workspace = true license.workspace = true repository.workspace = true @@ -11,9 +11,9 @@ categories.workspace = true edition = "2021" [dependencies] -clap = "2.33" -simple_logger = "1.13" -annotate-snippets = "0.9" +clap = { version = "4.5", features = ["derive"] } +simple_logger = "5.0" +annotate-snippets = "0.11" metamath-rs = { path = "../metamath-rs" } [[bin]] @@ -22,7 +22,7 @@ path = "src/main.rs" doc = false [features] -default = ["annotate-snippets/color", "verify_markup"] +default = ["verify_markup"] dot = ["metamath-rs/dot"] xml = ["metamath-rs/xml"] verify_markup = ["metamath-rs/verify_markup"] diff --git a/metamath-knife/src/main.rs b/metamath-knife/src/main.rs index 1274b1c..9084c29 100644 --- a/metamath-knife/src/main.rs +++ b/metamath-knife/src/main.rs @@ -4,8 +4,9 @@ mod list_stmt; -use annotate_snippets::display_list::DisplayList; -use clap::{clap_app, crate_version}; +use annotate_snippets::Renderer; +use clap::error::ErrorKind; +use clap::{CommandFactory, Parser}; use list_stmt::list_statements; use metamath_rs::database::{Database, DbOptions}; use metamath_rs::parser::is_valid_label; @@ -14,160 +15,192 @@ use simple_logger::SimpleLogger; use std::fs::File; use std::io::{self, stdout, BufWriter}; use std::mem; -use std::str::FromStr; - -fn positive_integer(val: String) -> Result<(), String> { - u32::from_str(&val).map(|_| ()).map_err(|e| format!("{e}")) -} - -fn main() { - let app = clap_app!(("smetamath-knife") => - (version: crate_version!()) - (about: "A Metamath database verifier and processing tool") - (@arg DATABASE: required_unless("TEXT") "Database file to load") - (@arg TEXT: --text value_names(&["NAME", "TEXT"]) ... - "Provides raw database content on the command line") - (@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 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") - (@arg verify_usage: -u --("verify-usage") "Checks axiom usage") - (@arg outline: -O --outline "Shows database outline") - (@arg dump_typesetting: -T --("dump-typesetting") "Dumps typesetting information") - (@arg parse_typesetting: -t --("parse-typesetting") "Parses typesetting information") - (@arg grammar: -g --grammar "Checks grammar") - (@arg parse_stmt: -p --("parse-stmt") - "Parses all statements according to the database's grammar") - (@arg verify_parse_stmt: --("verify-parse-stmt") - "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") - (@arg free: --free "Explicitly deallocates working memory before exit") - (@arg repeat: --repeat "Demonstrates incremental verifier") - (@arg jobs: -j --jobs +takes_value validator(positive_integer) - "Number of threads to use for verification") - (@arg export: -e --export [LABEL] ... "Outputs a proof file") - (@arg biblio: --biblio [FILE] ... "Supplies a bibliography file for verify-markup\n\ - Can be used one or two times; the second is for exthtml processing") - ); +/// A Metamath database verifier and processing tool +#[derive(Debug, clap::Parser)] +#[command(version, about, verbatim_doc_comment)] +struct Cli { + /// Database file to load + #[arg(id("DATABASE"), required_unless_present("text"))] + db: Option, + /// Provides raw database content on the command line + #[arg(long, value_names(&["NAME", "TEXT"]))] + text: Vec, + /// Processes files > 1 MiB in multiple segments + #[arg(long)] + split: bool, + /// Prints milliseconds after each stage + #[arg(long = "time")] + timing: bool, + /// Checks proof validity + #[arg(short, long)] + verify: bool, + /// Regenerates `discouraged` file + #[arg(short = 'D', long, value_name("FILE"))] + discouraged: Option, + /// Generate `axiom-use` file + #[arg(short = 'X', long, value_name("FILE"))] + axiom_use: Option, + /// Outputs statements directly or indirectly using the given list of statements + #[arg(long, value_names(&["FILE", "LABELS"]))] + stmt_use: Vec, + /// Checks axiom usage + #[arg(short = 'u', long)] + verify_usage: bool, + /// Shows database outline + #[arg(short = 'O', long)] + outline: bool, + /// Dumps typesetting information + #[arg(short = 'T', long)] + dump_typesetting: bool, + /// Parses typesetting information + #[arg(short = 't', long)] + parse_typesetting: bool, + /// Checks grammar + #[arg(short, long)] + grammar: bool, + /// Parses all statements according to the database's grammar + #[arg(short, long)] + parse_stmt: bool, + /// Checks that printing parsed statements gives back the original formulas + #[arg(long)] + verify_parse_stmt: bool, + /// Dumps the database's grammar + #[arg(short = 'G', long)] + dump_grammar: bool, + /// Dumps the formulas of this database + #[arg(short = 'F', long)] + dump_formula: bool, + /// List all statements of this database + #[arg(short = 'S', long)] + list_statements: bool, + /// Activates debug logs, including for the grammar building and statement parsing + #[arg(long)] + debug: bool, + /// Prints segments as they are recalculated + #[arg(long)] + trace_recalc: bool, + /// Explicitly deallocates working memory before exit + #[arg(long)] + free: bool, + /// Demonstrates incremental verifier + #[arg(long)] + repeat: bool, + /// Number of threads to use for verification + #[arg(short, long, value_parser = clap::value_parser!(u32).range(1..))] + jobs: Option, + /// Outputs a proof file + #[arg(short, long, value_name("LABEL"))] + export: Vec, + /// Supplies a bibliography file for verify-markup + /// Can be used one or two times; the second is for exthtml processing + #[arg(long, value_name("FILE"))] + biblio: Vec, #[cfg(feature = "dot")] - let app = clap_app!(@app (app) - (@arg export_grammar_dot: -E --("export-grammar-dot") - "Export the database's grammar in Graphviz DOT format for visualization") - ); - + /// Export the database's grammar in Graphviz DOT format for visualization + #[arg(short = 'E', long)] + export_grammar_dot: bool, #[cfg(feature = "xml")] - let app = clap_app!(@app (app) - (@arg export_graphml_deps: --("export-graphml-deps") [FILE] - "Exports all theorem dependencies in the GraphML file format") - ); - + /// Exports all theorem dependencies in the GraphML file format + #[arg(long, value_name("FILE"))] + export_graphml_deps: Option, #[cfg(feature = "verify_markup")] - let app = clap_app!(@app (app) - (@arg verify_markup: -m --("verify-markup") "Checks comment markup") - ); - - let matches = app.get_matches(); + /// Checks comment markup + #[arg(short = 'm', long)] + verify_markup: bool, +} +fn main() { + let cli = Cli::parse(); + let mut cmd = Cli::command(); + + let incremental = cli.repeat + || cli.grammar + || cli.parse_stmt + || cli.verify_parse_stmt + || cli.dump_grammar + || cli.dump_formula; + #[cfg(feature = "dot")] + let incremental = incremental || cli.export_grammar_dot; let options = DbOptions { - autosplit: matches.is_present("split"), - timing: matches.is_present("timing"), - trace_recalc: matches.is_present("trace_recalc"), - incremental: matches.is_present("repeat") - || matches.is_present("grammar") - || matches.is_present("parse_stmt") - || matches.is_present("verify_parse_stmt") - || matches.is_present("export_grammar_dot") - || matches.is_present("dump_grammar") - || matches.is_present("dump_formula"), - jobs: usize::from_str(matches.value_of("jobs").unwrap_or("1")) - .expect("validator should check this"), + autosplit: cli.split, + timing: cli.timing, + trace_recalc: cli.trace_recalc, + incremental, + jobs: cli.jobs.unwrap_or(1) as usize, }; - if matches.is_present("debug") { + if cli.debug { SimpleLogger::new().init().unwrap(); } let mut db = Database::new(options); let mut data = Vec::new(); - if let Some(tvals) = matches.values_of_lossy("TEXT") { - for kv in tvals.chunks(2) { - data.push((kv[0].clone(), kv[1].clone().into_bytes())); - } + for kv in cli.text.chunks(2) { + data.push((kv[0].clone(), kv[1].clone().into_bytes())); } - let start = matches - .value_of("DATABASE") - .map(|x| x.to_owned()) - .unwrap_or_else(|| data[0].0.clone()); + let start = cli.db.unwrap_or_else(|| data[0].0.clone()); loop { db.parse(start.clone(), data.clone()); - if matches.is_present("verify") { + if cli.verify { db.verify_pass(); } - if matches.is_present("grammar") { + if cli.grammar { db.grammar_pass(); } - if matches.is_present("parse_stmt") { + if cli.parse_stmt { db.stmt_parse_pass(); } - if matches.is_present("parse_typesetting") { + if cli.parse_typesetting { db.typesetting_pass(); } - if matches.is_present("verify_parse_stmt") { + if cli.verify_parse_stmt { db.stmt_parse_pass(); db.verify_parse_stmt(); } - if matches.is_present("verify_usage") { + if cli.verify_usage { db.verify_usage_pass(); } let mut diags = db.diag_notations(); - if matches.is_present("discouraged") { - File::create(matches.value_of("discouraged").unwrap()) + if let Some(discouraged) = &cli.discouraged { + File::create(discouraged) .and_then(|file| db.write_discouraged(&mut BufWriter::new(file))) .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into()))); } #[cfg(feature = "xml")] - if matches.is_present("export_graphml_deps") { - File::create(matches.value_of("export_graphml_deps").unwrap()) + if let Some(file) = cli.export_graphml_deps { + File::create(file) .map_err(|err| err.into()) .and_then(|file| db.export_graphml_deps(&mut BufWriter::new(file))) .unwrap_or_else(|diag| diags.push((StatementAddress::default(), diag))); } - if matches.is_present("axiom_use") { - File::create(matches.value_of("axiom_use").unwrap()) + if let Some(file) = &cli.axiom_use { + File::create(file) .and_then(|file| { db.write_stmt_use(|label| label.starts_with(b"ax-"), &mut BufWriter::new(file)) }) .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into()))); } - if matches.is_present("stmt_use") { - let vals: Vec<_> = matches.values_of("stmt_use").unwrap().collect(); - let output_file_path = vals[0]; - let stmt_list: Vec<_> = vals[1].split(',').map(str::as_bytes).collect(); + if !cli.stmt_use.is_empty() { + let output_file_path = &cli.stmt_use[0]; + let stmt_list: Vec<_> = cli.stmt_use[1].split(',').map(str::as_bytes).collect(); if !stmt_list.iter().copied().all(is_valid_label) { - clap::Error::with_description( + cmd.error( + ErrorKind::InvalidValue, "Expected list of labels as second argument to --stmt-use", - clap::ErrorKind::InvalidValue, ) .exit(); } @@ -181,34 +214,40 @@ fn main() { .unwrap_or_else(|err| diags.push((StatementAddress::default(), err.into()))); } - if matches.is_present("list_statements") { + if cli.list_statements { db.scope_pass(); _ = list_statements(&db, |_label| true, &mut stdout()); } + let r = Renderer::styled(); #[allow(unused_mut)] let mut count = db - .render_diags(diags, |snippet| { - println!("{}", DisplayList::from(snippet)); - }) + .render_diags(diags, |msg| println!("{}", r.render(msg))) .len(); #[cfg(feature = "verify_markup")] - if matches.is_present("verify_markup") { + if cli.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| { + if cli.biblio.len() > 2 { + cmd.error( + ErrorKind::TooManyValues, + "expected at most 2 bibliography files", + ) + .exit() + } + let sources: Vec<_> = cli + .biblio + .iter() + .map(|val| { let file = std::fs::read(val).unwrap(); metamath_rs::SourceInfo::new(val.to_owned(), std::sync::Arc::new(file)) }) - .collect() - }); + .collect(); let mut bib_diags = vec![]; let mut bibs = sources .iter() @@ -218,61 +257,56 @@ fn main() { ext: bibs.next(), }); - count += BibError::render_list(&bib_diags, |snippet| { - println!("{}", DisplayList::from(snippet)); - }) - .len(); + count += BibError::render_list(&bib_diags, |msg| println!("{}", r.render(msg))).len(); let diags = db.verify_markup(bib.as_ref()); count += db - .render_diags(diags, |snippet| { - println!("{}", DisplayList::from(snippet)); - }) + .render_diags(diags, |msg| println!("{}", r.render(msg))) .len(); } println!("{count} diagnostics issued."); - if matches.is_present("dump_grammar") { + if cli.dump_grammar { db.grammar_pass(); db.dump_grammar(); } #[cfg(feature = "dot")] - if matches.is_present("export_grammar_dot") { + if cli.export_grammar_dot { db.grammar_pass(); db.export_grammar_dot(); } - if matches.is_present("dump_formula") { + if cli.dump_formula { db.stmt_parse_pass(); db.dump_formula(); } - if matches.is_present("outline") { + if cli.outline { db.outline_pass(); db.print_outline(); } - if matches.is_present("print_typesetting") { + if cli.dump_typesetting { db.typesetting_pass(); db.print_typesetting(); } - if let Some(exps) = matches.values_of_lossy("export") { + if !cli.export.is_empty() { db.scope_pass(); - for file in exps { - db.export(&file); + for file in &cli.export { + db.export(file); } } - if matches.is_present("repeat") { + if cli.repeat { let mut input = String::new(); if io::stdin().read_line(&mut input).unwrap() == 0 { break; } } else { - if !matches.is_present("free") { + if !cli.free { mem::forget(db); } diff --git a/metamath-rs/Cargo.toml b/metamath-rs/Cargo.toml index 3d751fb..08e1e2c 100644 --- a/metamath-rs/Cargo.toml +++ b/metamath-rs/Cargo.toml @@ -2,7 +2,7 @@ name = "metamath-rs" readme = "README.md" description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases" -version = "0.3.8" +version = "0.3.9" authors.workspace = true license.workspace = true repository.workspace = true @@ -11,26 +11,26 @@ categories.workspace = true edition = "2021" [dependencies] -itertools = "0.12" +itertools = "0.13" 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" +annotate-snippets = "0.11" 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 } +html5ever = { version = "0.27.0", optional = true } scraper = { version = "0.19.0", optional = true } [dev-dependencies] assert_matches = "1.5" [features] -default = ["annotate-snippets/color", "verify_markup"] +default = ["verify_markup"] dot = ["dot-writer"] xml = ["xml-rs"] verify_markup = ["scraper", "html5ever"] diff --git a/metamath-rs/src/database.rs b/metamath-rs/src/database.rs index 97f2222..f8f7998 100644 --- a/metamath-rs/src/database.rs +++ b/metamath-rs/src/database.rs @@ -122,7 +122,7 @@ use crate::typesetting::TypesettingData; use crate::verify; use crate::verify::VerifyResult; use crate::StatementRef; -use annotate_snippets::snippet::Snippet; +use annotate_snippets::Message; use std::cmp::Ordering; use std::collections::BinaryHeap; use std::fmt; @@ -1024,7 +1024,7 @@ impl Database { pub fn render_diags( &self, diags: Vec<(StatementAddress, Diagnostic)>, - f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy, + f: impl for<'a> FnOnce(Message<'a>) -> T + Copy, ) -> Vec { let mut lc = LineCache::default(); time(&self.options.clone(), "diag", move || { diff --git a/metamath-rs/src/diag.rs b/metamath-rs/src/diag.rs index e8e242e..7bab1e1 100644 --- a/metamath-rs/src/diag.rs +++ b/metamath-rs/src/diag.rs @@ -20,8 +20,7 @@ use crate::statement::NO_STATEMENT; use crate::Span; use crate::StatementRef; use crate::StatementType; -use annotate_snippets::display_list::FormatOptions; -use annotate_snippets::snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation}; +use annotate_snippets::{Level, Message, Snippet}; use itertools::Itertools; use std::borrow::Borrow; use std::borrow::Cow; @@ -218,7 +217,7 @@ pub(crate) fn to_annotations( sset: &SegmentSet, lc: &mut LineCache, mut diags: Vec<(StatementAddress, Diagnostic)>, - f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy, + f: impl for<'a> FnOnce(Message<'a>) -> T + Copy, ) -> Vec { diags.sort_by(|x, y| sset.order.cmp(&x.0, &y.0)); diags @@ -233,14 +232,14 @@ pub(crate) fn to_annotations( /// Annotation info /// /// * `label` - A global error message for the diagnostic -/// For each annotation: -/// * `label` - The diagnostic message -/// * `annotation_type` - Severity level of the message -/// * `span` - The location of the error (byte offset within the segment; _this is -/// not the same as the byte offset in the file_). +/// * For each annotation: +/// * `label` - The diagnostic message +/// * `annotation_type` - Severity level of the message +/// * `span` - The location of the error (byte offset within the segment; +/// _this is not the same as the byte offset in the file_). type AnnInfo<'a> = ( Cow<'a, str>, - Vec<(AnnotationType, Cow<'a, str>, StatementRef<'a>, Span)>, + Vec<(Level, Cow<'a, str>, StatementRef<'a>, Span)>, ); /// Creates a `Snippet` containing a diagnostic annotation. @@ -253,51 +252,37 @@ type AnnInfo<'a> = ( #[must_use] fn make_snippet_from<'b, T>( label: &str, - infos: impl Iterator, Span, &'b SourceInfo)>, + infos: impl Iterator, Span, &'b SourceInfo)>, footer: &[&str], lc: &mut LineCache, - f: impl for<'a> FnOnce(Snippet<'a>) -> T, + f: impl for<'a> FnOnce(Message<'a>) -> T, ) -> T { - let mut slices = vec![]; + let mut snippets = vec![]; let arena: Arena = Arena::new(); - for (annotation_type, label, span, source) in infos { + let mut level = None; + for (level2, label, span, source) in infos { + level.get_or_insert(level2); let offs = (span.start + source.span.start) as usize; let (line_start, col) = lc.from_offset(&source.text, offs); let end_offs = (span.end + source.span.start) as usize; let source_start = offs + 1 - col as usize; let source_end = LineCache::line_end(&source.text, end_offs); - slices.push(Slice { - source: as_str(&source.text[source_start..source_end]), - line_start: line_start as usize, - origin: Some(source.name.as_str()), - annotations: vec![SourceAnnotation { - label: arena.alloc(label.to_string()), - annotation_type, - range: (offs - source_start, end_offs - source_start), - }], - fold: true, - }); + let annotation = level2 + .span(offs - source_start..end_offs - source_start) + .label(arena.alloc(label.to_string())); + let snippet = Snippet::source(as_str(&source.text[source_start..source_end])) + .line_start(line_start as usize) + .origin(source.name.as_str()) + .fold(true) + .annotation(annotation); + snippets.push(snippet); } - f(Snippet { - title: Some(Annotation { - label: Some(label), - id: None, - annotation_type: slices[0].annotations[0].annotation_type, - }), - footer: footer - .iter() - .map(|msg| Annotation { - id: None, - label: Some(msg), - annotation_type: AnnotationType::Note, - }) - .collect(), - slices, - opt: FormatOptions { - color: true, - ..FormatOptions::default() - }, - }) + + f(level + .unwrap() + .title(label) + .snippets(snippets) + .footers(footer.iter().map(|msg| Level::Note.title(msg)))) } /// Creates a `Snippet` containing a diagnostic annotation. @@ -314,7 +299,7 @@ fn make_snippet( (label, infos): AnnInfo<'_>, footer: &[&str], lc: &mut LineCache, - f: impl for<'a> FnOnce(Snippet<'a>) -> T, + f: impl for<'a> FnOnce(Message<'a>) -> T, ) -> T { let iter = (infos.into_iter()).map(|(annotation_type, label, stmt, span)| { let source = sset.source_info(stmt.segment().id).borrow(); @@ -329,7 +314,7 @@ impl Diagnostic { sset: &SegmentSet, stmt: StatementRef<'_>, lc: &mut LineCache, - f: impl for<'a> FnOnce(Snippet<'a>) -> T, + f: impl for<'a> FnOnce(Message<'a>) -> T, ) -> T { fn t(v: &Token) -> String { as_str(v).to_owned() @@ -337,43 +322,43 @@ impl Diagnostic { let mut notes: &[&str] = &[]; let infos = match self { BadCharacter(pos, byte) => ("Invalid character".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Invalid character (byte value {byte}); Metamath source files are limited to \ US-ASCII with controls TAB, CR, LF, FF)").into(), stmt, Span::new(*pos, *pos + 1), )]), BadCommand(span) => ("Invalid command".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Commands must start with a keyword".into(), stmt, *span, )]), BadCommentEnd(tok, opener) => ("Bad comment end".into(), vec![( - AnnotationType::Warning, + Level::Warning, "$) sequence must be surrounded by whitespace to end a comment".into(), stmt, *tok, ), ( - AnnotationType::Note, + Level::Note, "Comment started here".into(), stmt, *opener, )]), BadExplicitLabel(ref tok) => ("Bad explicit label".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Explicit label {label} does not refer to a hypothesis of the parent step", label = t(tok)).into(), stmt, stmt.span(), )]), BadFloating => ("Bad floating".into(), vec![( - AnnotationType::Error, + Level::Error, "A $f statement must have exactly two math tokens".into(), stmt, stmt.span(), )]), BadLabel(lbl) => ("Bad label".into(), vec![( - AnnotationType::Error, + Level::Error, "Statement labels may contain only alphanumeric characters and - _ .".into(), stmt, *lbl, @@ -382,72 +367,72 @@ impl Diagnostic { notes = &["Avoid uses of escape characters in bibliography tags \ since they break regex-based implementations"]; ("Invalid escape character".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Use of ~ or ` in a bibliography tag".into(), stmt, Span::new2(index, index + 1), ), ( - AnnotationType::Note, + Level::Note, "computed bibliography span".into(), stmt, span, )]) } ChainBackref(span) => ("Chain backref".into(), vec![( - AnnotationType::Error, + Level::Error, "Backreference steps are not permitted to have local labels".into(), stmt, *span, )]), CommandExpectedAs(span) => ("Expected 'as'".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Expected the keyword 'as' here".into(), stmt, *span, )]), CommandExpectedString(span) => ("Expected string, got keyword argument".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Expected a string here".into(), stmt, *span, )]), CommandIncomplete(span) => ("Incomplete command".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This command ended early, it was expecting more arguments".into(), stmt, *span, )]), CommentMarkerNotStart(marker) => ("Wrong comment marker".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This comment marker must be the first token in the comment to be effective".into(), stmt, *marker, )]), ConstantNotTopLevel => ("Constant is not at top level".into(), vec![( - AnnotationType::Error, + Level::Error, "$c statements are not allowed in nested groups".into(), stmt, stmt.span(), )]), DisjointSingle => ("Disjoint statement with single variable".into(), vec![( - AnnotationType::Warning, + Level::Warning, "A $d statement which lists only one variable is meaningless".into(), stmt, stmt.span(), )]), DjNotVariable(index) => ("Disjoint constraints are not applicable to constants".into(), vec![( - AnnotationType::Error, + Level::Error, "$d constraints are not applicable to constants".into(), stmt, stmt.math_span(*index), )]), DjRepeatedVariable(index1, index2) => ("Variable repeated in disjoint statement".into(), vec![( - AnnotationType::Error, + Level::Error, "A variable may not be used twice in the same $d constraint".into(), stmt, stmt.math_span(*index1), ), ( - AnnotationType::Note, + Level::Note, "Previous appearance was here".into(), stmt, stmt.math_span(*index2), @@ -455,25 +440,25 @@ impl Diagnostic { &DateOrderError(contrib, later) => { notes = &["It is easiest to read the contribution comments when they come in order"]; (format!("at {}: Parentheticals should come in chronological order", as_str(stmt.label())).into(), vec![( - AnnotationType::Warning, + Level::Warning, "this date...".into(), stmt, contrib, ), ( - AnnotationType::Warning, + Level::Warning, "comes after this one".into(), stmt, later, )]) } &DateParseError(span) => ("Failed to parse date".into(), vec![( - AnnotationType::Error, + Level::Error, "Expected DD-MMM-YYYY format".into(), stmt, span, )]), &DefaultAuthor(span) => ("Use of default author".into(), vec![( - AnnotationType::Warning, + Level::Warning, "There should be a person's name here".into(), stmt, span, @@ -482,53 +467,53 @@ impl Diagnostic { notes = &["The 'Contributed by' field indicates the first author of a theorem.\n\ Use 'Revised by' for subsequent contributions to the same theorem."]; ("Statement has multiple contributors".into(), vec![( - AnnotationType::Note, + Level::Note, "First contributor here".into(), stmt, fst, ), ( - AnnotationType::Warning, + Level::Warning, "Second contributor here".into(), stmt, snd, )]) }, DuplicateExplicitLabel(ref tok) => ("Duplicate explicit label".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Explicit label {label} is used twice in the same step", label = t(tok)).into(), stmt, stmt.span(), )]), DuplicateLabel(prevstmt) => ("Duplicate label".into(), vec![( - AnnotationType::Error, + Level::Error, "Statement labels must be unique".into(), stmt, stmt.span(), ), ( - AnnotationType::Note, + Level::Note, "Label was previously used here".into(), sset.statement(*prevstmt), sset.statement(*prevstmt).span(), )]), &DuplicateMarkupDef(kind, fst, snd) => (format!("Duplicate {}", kind.def_name()).into(), vec![( - AnnotationType::Warning, + Level::Warning, "This token has already been defined".into(), stmt, snd, ), ( - AnnotationType::Note, + Level::Note, "Token was previously defined here".into(), sset.statement_or_dummy(StatementAddress::new(fst.0, NO_STATEMENT)), fst.1, )]), EmptyFilename => ("Empty filename".into(), vec![( - AnnotationType::Error, + Level::Error, "Filename included by a $[ directive must not be empty".into(), stmt, stmt.span(), )]), EmptyMathString => ("Empty math string".into(), vec![( - AnnotationType::Error, + Level::Error, "A math string must have at least one token".into(), stmt, stmt.span(), @@ -538,92 +523,92 @@ impl Diagnostic { was used at the end of a comment,", "or before , a math string, or a bibliography tag"]; ("Empty label reference".into(), vec![( - AnnotationType::Error, + Level::Error, "This references nothing".into(), stmt, Span::new2(index, index + 1), )]) }, EssentialAtTopLevel => ("Essential at top level".into(), vec![( - AnnotationType::Error, + Level::Error, "$e statements must be inside scope brackets, not at the top level".into(), stmt, stmt.span(), )]), ExprNotConstantPrefix(index) => ("Expression does not have a constant prefix".into(), vec![( - AnnotationType::Error, + Level::Error, "The math string of an $a, $e, or $p assertion must start with a constant, \ not a variable".into(), stmt, stmt.math_span(*index), )]), FilenameDollar => ("Dollar in filename".into(), vec![( - AnnotationType::Error, + Level::Error, "Filenames included by $[ are not allowed to contain the $ character".into(), stmt, stmt.span(), )]), FilenameSpaces => ("Spaces in filename".into(), vec![( - AnnotationType::Error, + Level::Error, "Filenames included by $[ are not allowed to contain whitespace".into(), stmt, stmt.span(), )]), FloatNotConstant(index) => ("Typecode was not declared".into(), vec![( - AnnotationType::Error, + Level::Error, "The first token of a $f statement must be a declared constant (typecode)".into(), stmt, stmt.math_span(*index), )]), FloatNotVariable(index) => ("Variable not declared".into(), vec![( - AnnotationType::Error, + Level::Error, "The second token of a $f statement must be a declared variable (to \ associate the type)".into(), stmt, stmt.math_span(*index), )]), FloatRedeclared(saddr) => ("Float redeclared".into(), vec![( - AnnotationType::Error, + Level::Error, "There is already an active $f for this variable".into(), stmt, stmt.span(), ), ( - AnnotationType::Note, + Level::Note, "Previous $f was here".into(), sset.statement(*saddr), sset.statement(*saddr).span(), )]), FormulaVerificationFailed => ("Formula verification failed".into(), vec![( - AnnotationType::Error, + Level::Error, "Formula verification failed at this symbol".into(), stmt, stmt.span(), )]), GrammarAmbiguous(prevstmt) => ("Grammar ambiguous".into(), vec![( - AnnotationType::Error, + Level::Error, "Grammar is ambiguous; ".into(), stmt, stmt.span(), ), ( - AnnotationType::Note, + Level::Note, "Collision with this statement:".into(), sset.statement(*prevstmt), sset.statement(*prevstmt).span(), )]), GrammarCantBuild(message) => ("Can't build the grammar".into(), vec![( - AnnotationType::Error, + Level::Error, (*message).into(), stmt, stmt.span(), )]), GrammarProvableFloat => ("Floating declaration of provable type".into(), vec![( - AnnotationType::Error, + Level::Error, "Floating declaration of provable type".into(), stmt, stmt.span(), )]), HtmlParseError(span, msg) => (format!("HTML parse error(s): {}", msg.iter().format(", ")).into(), vec![( - AnnotationType::Warning, + Level::Warning, "in this HTML block".into(), stmt, *span, @@ -631,25 +616,25 @@ impl Diagnostic { HeaderCommentParseError(lvl) => { notes = lvl.diagnostic_note(); ("Invalid header comment".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Could not parse this as a header".into(), stmt, stmt.span(), )]) }, InvalidAxiomRestatement(ax_span, th_span) => ("Invalid axiom restatement".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This ax* theorem does not match the corresponding ax-*".into(), stmt, *th_span, ), ( - AnnotationType::Note, + Level::Note, "Axiom ax-* here".into(), stmt, *ax_span, )]), IoError(ref err) => (format!("I/O error: {error}", error = err.clone()).into(), vec![( - AnnotationType::Error, + Level::Error, "Source file could not be read".into(), stmt, stmt.span(), @@ -657,32 +642,32 @@ impl Diagnostic { LabelContainsUnderscore(span) => { notes = &["Prefer '-' over '_' in labels"]; ("Label contains underscore".into(), vec![( - AnnotationType::Warning, + Level::Warning, "this statement has an underscore".into(), stmt, *span, )]) }, LineLengthExceeded(span) => ("Line is too long".into(), vec![( - AnnotationType::Warning, + Level::Warning, "These characters go over the line limit".into(), stmt, *span, )]), LocalLabelAmbiguous(span) => ("Local label is ambiguous".into(), vec![( - AnnotationType::Error, + Level::Error, "Local label conflicts with the name of an existing statement".into(), stmt, *span, )]), LocalLabelDuplicate(span) => ("Duplicate local Label".into(), vec![( - AnnotationType::Error, + Level::Error, "Local label duplicates another label in the same proof".into(), stmt, *span, )]), &MarkupNeedsWhitespace(index) => ("Markup character requires surrounding whitespace".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Put spaces around this character".into(), stmt, Span::new2(index, index + 1), @@ -696,37 +681,37 @@ impl Diagnostic { if that_name.is_empty() { "defined in a different mathbox".into() } else { format!("defined in {}'s mathbox", as_str(that_name)).into() }; ("Mathbox uses a theorem from another mathbox".into(), vec![ - (AnnotationType::Warning, ann1, stmt, this), - (AnnotationType::Note, "it refers to a theorem here...".into(), stmt, span), - (AnnotationType::Note, ann2, stmt, that) + (Level::Warning, ann1, stmt, this), + (Level::Note, "it refers to a theorem here...".into(), stmt, span), + (Level::Note, ann2, stmt, that) ]) } MathboxHeaderFormat(span) => ("Malformed mathbox header".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Expected 'Mathbox for '".into(), stmt, *span, )]), MalformedAdditionalInfo(span) => ("Malformed additional info".into(), vec![( - AnnotationType::Error, + Level::Error, "Malformed additional information".into(), stmt, *span, )]), MidStatementCommentMarker(marker) => ("Mid-statement comment".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Marked comments are only effective between statements, not inside them".into(), stmt, *marker, )]), MissingContributor => ("Missing or malformed contribution comment".into(), vec![( - AnnotationType::Warning, + Level::Warning, "No (Contributed by...) provided for this statement".into(), stmt, stmt.label_span(), )]), MissingLabel => ("Missing label".into(), vec![( - AnnotationType::Error, + Level::Error, "This statement type requires a label".into(), stmt, stmt.span(), @@ -736,44 +721,44 @@ impl Diagnostic { .chain(alt_html.then_some("althtmldef")) .chain(latex.then_some("latexdef")); (format!("Missing {} for token", msg.format(", ")).into(), vec![( - AnnotationType::Warning, + Level::Warning, "This token has not been declared in the $t comment".into(), stmt, span, )]) }, MissingProof(math_end) => ("Missing proof".into(), vec![( - AnnotationType::Error, + Level::Error, "Provable assertion requires a proof introduced with $= here; use $= ? $. \ if you do not have a proof yet".into(), stmt, *math_end, )]), MMReservedLabel(span) => ("Reserved label".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Labels beginning with 'mm' are reserved for Metamath file names".into(), stmt, *span, )]), NestedComment(tok, opener) => ("Nested comment".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Nested comments are not supported - comment will end at the first $)".into(), stmt, *tok, ), ( - AnnotationType::Note, + Level::Note, "Comment started here".into(), stmt, *opener, )]), NotActiveSymbol(index) => ("Inactive symbol".into(), vec![( - AnnotationType::Error, + Level::Error, "Token used here must be active in the current scope".into(), stmt, stmt.math_span(*index), )]), NotAProvableStatement => ("Not a provable statement".into(), vec![( - AnnotationType::Error, + Level::Error, "Statement does not start with the provable constant type".into(), stmt, stmt.span(), @@ -781,7 +766,7 @@ impl Diagnostic { OldAltNotDiscouraged if stmt.statement_type() == StatementType::Axiom => { notes = &["Add (New usage is discouraged.) to the comment"]; ("OLD/ALT axiom not discouraged".into(), vec![( - AnnotationType::Warning, + Level::Warning, "OLD and ALT axioms should be discouraged".into(), stmt, stmt.label_span(), @@ -791,7 +776,7 @@ impl Diagnostic { notes = &["Add (Proof modification is discouraged.) \ and (New usage is discouraged.) to the comment"]; ("OLD/ALT theorem not discouraged".into(), vec![( - AnnotationType::Warning, + Level::Warning, "OLD and ALT theorems should be discouraged".into(), stmt, stmt.label_span(), @@ -800,43 +785,43 @@ impl Diagnostic { &ParenOrderError(contrib, later) => { notes = &["The contribution comment should come before any revisions"]; ("(Revised by...) precedes (Contributed by...)".into(), vec![( - AnnotationType::Warning, + Level::Warning, "contribution comment here".into(), stmt, contrib, ), ( - AnnotationType::Warning, + Level::Warning, "earlier revision comment".into(), stmt, later, )]) } ProofDvViolation => ("Distinct variable violation".into(), vec![( - AnnotationType::Error, + Level::Error, "Disjoint variable constraint violated".into(), stmt, stmt.span(), )]), ProofExcessEnd => ("Proof does not end with a single statement".into(), vec![( - AnnotationType::Error, + Level::Error, "Must be exactly one statement on stack at end of proof".into(), stmt, stmt.span(), )]), ProofIncomplete => ("Proof incomplete".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Proof is incomplete".into(), stmt, stmt.span(), )]), ProofInvalidSave => ("Invalid save".into(), vec![( - AnnotationType::Error, + Level::Error, "Z must appear immediately after a complete step integer".into(), stmt, stmt.span(), )]), ProofMalformedVarint => ("Proof too long".into(), vec![( - AnnotationType::Error, + Level::Error, "Proof step number too long or missing terminator".into(), stmt, stmt.span(), @@ -845,49 +830,49 @@ impl Diagnostic { notes = &["it doesn't make sense to put this marker on an axiom,\n\ because axioms don't have proofs"]; ("Axiom contains (Proof modification is discouraged.)".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This doesn't make sense".into(), stmt, span, )]) }, ProofNoSteps => ("Empty proof".into(), vec![( - AnnotationType::Error, + Level::Error, "Proof must have at least one step (use ? if deliberately incomplete)".into(), stmt, stmt.span(), )]), ProofUnderflow => ("Proof underflow".into(), vec![( - AnnotationType::Error, + Level::Error, "Too few statements on stack to satisfy step's mandatory hypotheses".into(), stmt, stmt.span(), )]), ProofUnterminatedRoster => ("Unterminated roster".into(), vec![( - AnnotationType::Error, + Level::Error, "List of referenced assertions in a compressed proof must be terminated by )".into(), stmt, stmt.span(), )]), ProofWrongExprEnd => ("Proven statement does not match assertion".into(), vec![( - AnnotationType::Error, + Level::Error, "Final step statement does not match assertion".into(), stmt, stmt.span(), )]), ProofWrongTypeEnd => ("Proven statement has wrong typecode".into(), vec![( - AnnotationType::Error, + Level::Error, "Final step typecode does not match assertion".into(), stmt, stmt.span(), )]), RepeatedLabel(l_span, f_span) => ("Repeated label".into(), vec![( - AnnotationType::Error, + Level::Error, "A statement may have only one label".into(), stmt, *l_span, ), ( - AnnotationType::Note, + Level::Note, "First label was here".into(), stmt, *f_span, @@ -896,7 +881,7 @@ impl Diagnostic { notes = &["The '@' character is discouraged in tokens because it is\n\ traditionally used to replace '$' in commented out database source code."]; ("Token contains '@'".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Used '@' character here".into(), stmt, *span, @@ -906,204 +891,204 @@ impl Diagnostic { notes = &["The '?' character is discouraged in tokens because it is\n\ sometimes used as a math token search wildcard."]; ("Token contains '?'".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Used '?' character here".into(), stmt, *span, )]) } SpuriousLabel(lspan) => ("Spurious label".into(), vec![( - AnnotationType::Error, + Level::Error, "Labels are only permitted for statements of type $a, $e, $f, or $p".into(), stmt, *lspan, )]), SpuriousProof(math_end) => ("Spurious proof".into(), vec![( - AnnotationType::Error, + Level::Error, "Proofs are only allowed on $p assertions".into(), stmt, *math_end, )]), StepEssenWrong => ("Wrong essential statement".into(), vec![( - AnnotationType::Error, + Level::Error, "Step used for $e hypothesis does not match statement".into(), stmt, stmt.span(), )]), StepEssenWrongType => ("Wrong essential typecode".into(), vec![( - AnnotationType::Error, + Level::Error, "Step used for $e hypothesis does not match typecode".into(), stmt, stmt.span(), )]), StepFloatWrongType => ("Wrong floating typecode".into(), vec![( - AnnotationType::Error, + Level::Error, "Step used for $f hypothesis does not match typecode".into(), stmt, stmt.span(), )]), StepMissing(ref tok) => ("Missing step".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Step {step} referenced by proof does not correspond to a $p statement (or \ is malformed)", step = t(tok)).into(), stmt, stmt.span(), )]), StepOutOfRange => ("Step out of range".into(), vec![( - AnnotationType::Error, + Level::Error, "Step in compressed proof is out of range of defined steps".into(), stmt, stmt.span(), )]), StepUsedAfterScope(ref tok) => ("Step used after scope".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Step {step} referenced by proof is a hypothesis not active in this scope", step = t(tok)).into(), stmt, stmt.span(), )]), StepUsedBeforeDefinition(ref tok) => ("Step used before definition".into(), vec![( - AnnotationType::Error, + Level::Error, format!("Step {step} referenced by proof has not yet been proved", step = t(tok)).into(), stmt, stmt.span(), )]), StmtParseError(err) => err.build_info(stmt), SymbolDuplicatesLabel(index, saddr) => ("Symbol duplicates label".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Metamath spec forbids symbols which are the same as labels in the same \ database".into(), stmt, stmt.math_span(*index), ), ( - AnnotationType::Note, + Level::Note, "Symbol was used as a label here".into(), sset.statement(*saddr), sset.statement(*saddr).span(), )]), SymbolRedeclared(index, taddr) => ("Symbol redeclared".into(), vec![( - AnnotationType::Error, + Level::Error, "This symbol is already active in this scope".into(), stmt, stmt.math_span(*index), ), ( - AnnotationType::Note, + Level::Note, "Symbol was previously declared here".into(), stmt, sset.statement(taddr.statement).math_span(taddr.token_index), )]), TabUsed(span) => ("Tab character used".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Use spaces instead".into(), stmt, *span, )]), TrailingWhitespace(span) => ("Trailing whitespace".into(), vec![( - AnnotationType::Warning, + Level::Warning, "whitespace here".into(), stmt, *span, )]), UnclosedBeforeEof => ("Unclosed before eof".into(), vec![( - AnnotationType::Error, + Level::Error, "${ group must be closed with a $} before end of file".into(), stmt, stmt.span(), )]), UnclosedBeforeInclude(index) => ("Include not at top level".into(), vec![( - AnnotationType::Error, + Level::Error, "${ group must be closed with a $} before another file can be included".into(), stmt, stmt.span(), ), ( - AnnotationType::Note, + Level::Note, "Include statement is here".into(), stmt.segment().statement(*index), stmt.segment().statement(*index).span(), )]), UnclosedCommandComment(span) => ("Unclosed comment".into(), vec![( - AnnotationType::Error, + Level::Error, "$t/$j comment requires closing */ before end of statement".into(), stmt, *span, )]), UnclosedCommandString(span) => ("Unclosed string".into(), vec![( - AnnotationType::Error, + Level::Error, "A string must be closed with ' or \"".into(), stmt, *span, )]), UnclosedComment(comment) => ("Unclosed comment".into(), vec![( - AnnotationType::Error, + Level::Error, "Comment requires closing $) before end of file".into(), stmt, *comment, )]), &UnclosedHtml(start, end) => ("Unclosed ".into(), vec![( - AnnotationType::Error, + Level::Error, "HTML blocks must be closed".into(), stmt, Span::new2(end, end + 2), // the $) ), ( - AnnotationType::Note, + Level::Note, "HTML block started here".into(), stmt, Span::new2(start, start + 6), // the )]), UnclosedInclude => ("Unclosed include".into(), vec![( - AnnotationType::Error, + Level::Error, "$[ requires a matching $]".into(), stmt, stmt.span(), )]), UnclosedMath => ("Unclosed math".into(), vec![( - AnnotationType::Error, + Level::Error, "A math string must be closed with $= or $.".into(), stmt, stmt.span(), )]), &UnclosedMathMarkup(start, end) => ("Unclosed math".into(), vec![( - AnnotationType::Error, + Level::Error, "A math string must be closed with `".into(), stmt, Span::new2(end, end + 2), // the $) ), ( - AnnotationType::Note, + Level::Note, "Math string started here".into(), stmt, Span::new2(start, start + 1), // the ` )]), UnclosedProof => ("Unclosed proof".into(), vec![( - AnnotationType::Error, + Level::Error, "A proof must be closed with $.".into(), stmt, stmt.span(), )]), UnconventionalAxiomLabel(span) => ("Unconventional axiom label".into(), vec![( - AnnotationType::Warning, + Level::Warning, "Axioms should start with 'ax-' or 'df-'".into(), stmt, *span, )]), UndefinedBibTag(span) => ("Missing bibliography tag".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This tag was not found in the bibliography file".into(), stmt, *span, )]), UndefinedToken(span, tk) => (format!("Undeclared token '{}'", as_str(tk)).into(), vec![( - AnnotationType::Warning, + Level::Warning, "This token was not declared in any $v or $c statement".into(), stmt, *span, )]), UnknownKeyword(kwspan) => ("Unknown keyword".into(), vec![( - AnnotationType::Error, + Level::Error, "Statement-starting keyword must be one of $a $c $d $e $f $p $v".into(), stmt, *kwspan, )]), UnknownTypesettingCommand(kwspan) => ("Unknown $t command".into(), vec![( - AnnotationType::Error, + Level::Error, "Typesetting command must be one of:\n\ latexdef, htmldef, althtmldef, htmlvarcolor, htmltitle, htmlhome,\n\ exthtmltitle, exthtmlhome, exthtmllabel, htmldir, althtmldir,\n\ @@ -1119,49 +1104,49 @@ impl Diagnostic { "Use ~~ or [[ or `` or _\u{200B}_ if you mean to include the character literally" ]; ("Invalid escape character".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This escape character should be doubled".into(), stmt, Span::new2(index, index + 1), )]) } UninterpretedHtml(tok) => ("incorrect use of ".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This was not interpreted".into(), stmt, *tok, )]), UnknownLabel(span) => ("Unknown label".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This is not the label of any statement".into(), stmt, *span, )]), UnmatchedCloseGroup => ("Unmatched close group".into(), vec![( - AnnotationType::Error, + Level::Error, "This $} does not match any open ${".into(), stmt, stmt.span(), )]), UsageViolation(span, label, axiom) => ("Usage violation".into(), vec![( - AnnotationType::Warning, + Level::Warning, format!("Statement {label} uses axiom {axiom} despite $j declaring it avoids its usage.", label=as_str(label), axiom=as_str(axiom)).into(), stmt, *span, )]), VariableMissingFloat(index) => ("Variable missing float".into(), vec![( - AnnotationType::Error, + Level::Error, "Variable token used in statement must have an active $f".into(), stmt, stmt.math_span(*index), )]), VariableRedeclaredAsConstant(index, taddr) => ("Variable redeclared as a constant".into(), vec![( - AnnotationType::Error, + Level::Error, "Symbol cannot be used as a variable here and as a constant later".into(), stmt, stmt.math_span(*index), ), ( - AnnotationType::Note, + Level::Note, "Symbol will be used as a constant here".into(), sset.statement(taddr.statement), sset.statement(taddr.statement).math_span(taddr.token_index), @@ -1170,7 +1155,7 @@ impl Diagnostic { notes = &["On windows, it is not legal to name a file any of:\n\ CON, PRN, AUX, CLOCK$, NUL, COM[1-9], LPT[1-9]."]; ("Windows reserved label".into(), vec![( - AnnotationType::Warning, + Level::Warning, "This label cannot be used as the name of a file on windows".into(), stmt, *span, @@ -1212,8 +1197,8 @@ impl StmtParseError { /// The diagnostic's severity #[must_use] #[allow(clippy::unused_self)] - pub const fn severity(&self) -> AnnotationType { - AnnotationType::Error + pub const fn severity(&self) -> Level { + Level::Error } fn build_info<'a>(&self, stmt: StatementRef<'a>) -> AnnInfo<'a> { @@ -1259,12 +1244,9 @@ impl StmtParseError { stmt, *span, ), - StmtParseError::ParsedStatementNoTypeCode => ( - AnnotationType::Error, - "Empty statement".into(), - stmt, - stmt.span(), - ), + StmtParseError::ParsedStatementNoTypeCode => { + (Level::Error, "Empty statement".into(), stmt, stmt.span()) + } }; (self.label(), vec![info]) } @@ -1301,18 +1283,18 @@ impl BibError { &self, source: &SourceInfo, lc: &mut LineCache, - f: impl for<'a> FnOnce(Snippet<'a>) -> T, + f: impl for<'a> FnOnce(Message<'a>) -> T, ) -> T { let (label, infos): (Cow<'_, str>, Vec<_>) = match self { &BibError::DuplicateBib(span, other) => ( "duplicate bibliography anchor".into(), vec![ ( - AnnotationType::Warning, + Level::Warning, "this anchor has already appeared".into(), span, ), - (AnnotationType::Note, "previous occurrence".into(), other), + (Level::Note, "previous occurrence".into(), other), ], ), }; @@ -1324,7 +1306,7 @@ impl BibError { /// Convert a list of diagnostics collected by `diag_notations` to a list of snippets. pub fn render_list( diags: &[(&SourceInfo, BibError)], - f: impl for<'a> FnOnce(Snippet<'a>) -> T + Copy, + f: impl for<'a> FnOnce(Message<'a>) -> T + Copy, ) -> Vec { let mut lc = LineCache::default(); diags diff --git a/metamath-rs/src/scopeck.rs b/metamath-rs/src/scopeck.rs index 24d77b1..10adb82 100644 --- a/metamath-rs/src/scopeck.rs +++ b/metamath-rs/src/scopeck.rs @@ -2,23 +2,23 @@ //! can be done at the same time: //! //! 1. For `$c $v $f` and labelled statements (`$e $f $a $p`): Check for -//! duplication +//! duplication //! -//! 1. For `$e $d $f $a $p`: Check that all used math symbols are active in -//! scope +//! 2. For `$e $d $f $a $p`: Check that all used math symbols are active in +//! scope //! -//! 1. For `$a $p`: Compute the frame +//! 3. For `$a $p`: Compute the frame //! //! Rules of precedence for error detection and recovery: //! //! 1. Math symbols and labels are actually in separate namespaces. We warn -//! about collisions but otherwise do nothing. Variables have responsibility -//! for the warning. +//! about collisions but otherwise do nothing. Variables have responsibility +//! for the warning. //! -//! 1. When two definitions have overlapping live ranges, the earlier one wins. +//! 2. When two definitions have overlapping live ranges, the earlier one wins. //! -//! 1. Constant/nested variable collisions are special because they don't -//! involve scope overlaps. The constant wins, the variable must notify. +//! 3. Constant/nested variable collisions are special because they don't +//! involve scope overlaps. The constant wins, the variable must notify. //! //! Since this is always run before the verifier, it focuses on supporting the //! verifier; things that the verifier won't use mostly aren't done. This diff --git a/metamath-rs/src/segment_set.rs b/metamath-rs/src/segment_set.rs index 82f9538..c148d78 100644 --- a/metamath-rs/src/segment_set.rs +++ b/metamath-rs/src/segment_set.rs @@ -19,12 +19,13 @@ //! `segment_set` implements two levels of caching: //! //! 1. When a file is loaded from disk, its pathname and modification time are -//! saved, along with all of the segments which it generated. If the file -//! hasn't changed at all, we can reuse the segments after a single `stat`. +//! saved, along with all of the segments which it generated. If the file +//! hasn't changed at all, we can reuse the segments after a single `stat`. //! -//! 1. After a file is loaded and split, slices are cached by content. This -//! speeds up operation when local changes are made to large files, or when -//! modification times cannot be used (such as some language server scenarios). +//! 2. After a file is loaded and split, slices are cached by content. This +//! speeds up operation when local changes are made to large files, or when +//! modification times cannot be used (such as some language server +//! scenarios). //! //! In either case, some care is needed to retain only data which is relevant in //! the cache. The caches are discarded on every read, but any data obtained