Skip to content

Commit

Permalink
update dependencies
Browse files Browse the repository at this point in the history
  • Loading branch information
digama0 committed Jul 16, 2024
1 parent f841650 commit 7fe2435
Show file tree
Hide file tree
Showing 24 changed files with 667 additions and 765 deletions.
1,114 changes: 525 additions & 589 deletions mm0-rs/Cargo.lock

Large diffs are not rendered by default.

32 changes: 17 additions & 15 deletions mm0-rs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ server = [
"lsp-types", "mm0_deepsize/lsp-types",
"lsp-server", "crossbeam", "simplelog", "log",
"mm0_util/server", "mm1_parser/server"]
doc = ["lsp-types", "pulldown-cmark", "webbrowser"]
doc = ["lsp-types", "url", "pulldown-cmark", "pulldown-cmark-escape", "webbrowser"]
memory = [
"mm0_deepsize", "mm0_deepsize_derive",
"mm0_util/memory", "mm1_parser/memory", "mmcc/memory"]
Expand All @@ -32,25 +32,25 @@ debug = true
opt-level = 2

[dependencies]
bitflags = "1.3"
byteorder = "1.4"
bitflags = "2.6"
byteorder = "1.5"
once_cell = "1.12"
if_chain = "1.0"
itertools = "0.10"
itertools = "0.13"
pathdiff = "0.2"
arrayvec = "0.7"
num = "0.4"
pretty = "0.11"
clap = { version = "3.1", features = ["derive", "unstable-v4"] }
pretty = "0.12"
clap = { version = "4.5", features = ["derive"] }
futures = { version = "0.3", features = ["thread-pool"] }
serde = "1.0"
serde_json = "1.0"
serde_repr = "0.1"
annotate-snippets = { version = "0.9", features = ["color"] }
annotate-snippets = "0.11"
libc = "0.2"
zerocopy = "0.6"
memchr = "2.5"
bit-set = "0.5"
zerocopy = "0.7"
memchr = "2.7"
bit-set = "0.6"
typed-arena = "2.0"
mm0_deepsize_derive = { path = "components/mm0_deepsize_derive", optional = true }
debug_derive = { path = "components/debug_derive" }
Expand All @@ -64,12 +64,14 @@ mm1_parser = { path = "components/mm1_parser" }
log = { version = "0.4", optional = true }
simplelog = { version = "0.12", optional = true }
crossbeam = { version = "0.8", optional = true }
lsp-types = { version = "0.93", optional = true }
lsp-server = { version = "0.6", optional = true }
lsp-types = { version = "0.97", optional = true }
lsp-server = { version = "0.7", optional = true }

# For "doc" feature
pulldown-cmark = { version = "0.9", optional = true }
webbrowser = { version = "0.8", optional = true }
url = { version = "2.5", optional = true }
pulldown-cmark = { version = "0.11", optional = true }
pulldown-cmark-escape = { version = "0.11", optional = true }
webbrowser = { version = "1.0", optional = true }

# For "wasm" feature
console_error_panic_hook = { version = "0.1", optional = true }
Expand All @@ -82,7 +84,7 @@ mmcc = { path = "components/mmcc", optional = true }
im = { version = "15.1", optional = true }

[target.'cfg(target_os = "linux")'.dependencies]
procfs = "0.14"
procfs = "0.16"

[target.'cfg(not(target_arch = "wasm32"))'.dependencies]
memmap = "0.7"
Expand Down
2 changes: 1 addition & 1 deletion mm0-rs/components/debug_derive/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,4 +11,4 @@ proc-macro = true

[dependencies]
quote = "1.0"
syn = { version = "1.0", features = ["full"] }
syn = { version = "2.0", features = ["full"] }
6 changes: 3 additions & 3 deletions mm0-rs/components/mm0_deepsize/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,9 @@ mm0_deepsize_derive = { version = "0.1.1", path = "../mm0_deepsize_derive" }
num = { version = "0.4", optional = true }
typed-arena = { version = "2.0", optional = true }
smallvec = { version = "1.8", optional = true }
bit-vec = { version = "0.6", optional = true }
bit-set = { version = "0.5", optional = true }
lsp-types = { version = "0.93", optional = true }
bit-vec = { version = "0.7", optional = true }
bit-set = { version = "0.6", optional = true }
lsp-types = { version = "0.97", optional = true }
futures = { version = "0.3", optional = true }
hybrid-rc = { version = "0.6", optional = true }

Expand Down
4 changes: 2 additions & 2 deletions mm0-rs/components/mm0_deepsize/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -408,9 +408,9 @@ impl DeepSizeOf for num::BigInt {
}

#[cfg(feature = "lsp-types")]
impl DeepSizeOf for lsp_types::Url {
impl DeepSizeOf for lsp_types::Uri {
fn deep_size_of_children(&self, _: &mut Context) -> usize {
// this is an underestimate, but Url doesn't expose its capacity
// this is an underestimate, but Uri doesn't expose its capacity
self.as_str().len()
}
}
Expand Down
2 changes: 1 addition & 1 deletion mm0-rs/components/mm0_deepsize_derive/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -32,4 +32,4 @@ version = "^1.0"
version = "^1.0"

[dependencies.syn]
version = "^1.0"
version = "^2.0"
8 changes: 4 additions & 4 deletions mm0-rs/components/mm0_util/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,18 +15,18 @@ categories = ["command-line-utilities", "development-tools", "mathematics"]
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
bitflags = "1.3"
bitflags = "2.6"

# optional dependencies
mm0_deepsize = { version = "0.1.0", path = "../mm0_deepsize", optional = true }
mm0_deepsize_derive = { version = "0.1.1", path = "../mm0_deepsize_derive", optional = true }
once_cell = { version = "1.12", optional = true }
once_cell = { version = "1.19", optional = true }
pathdiff = { version = "0.2", optional = true }
libc = { version = "0.2", optional = true }
lsp-types = { version = "0.93", optional = true }
lsp-types = { version = "0.97", optional = true }

[target.'cfg(target_os = "linux")'.dependencies]
procfs = { version = "0.14", optional = true }
procfs = { version = "0.16", optional = true }

[features]
default = ["lined_string"]
Expand Down
5 changes: 3 additions & 2 deletions mm0-rs/components/mm0_util/src/ids.rs
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,7 @@ id_wrapper!(AtomId: u32, AtomVec);

bitflags::bitflags! {
/// Visibility and sort modifiers for Sort statements and Declarations.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Modifiers: u8 {
// Note: These particular values are important because they are used in the MMB format.

Expand Down Expand Up @@ -153,7 +154,7 @@ impl Modifiers {

/// Construct a [`Modifiers`] from a byte.
#[must_use]
pub fn new(bits: u8) -> Self { Self { bits } }
pub fn new(bits: u8) -> Self { Self::from_bits_retain(bits) }

/// The set of all valid sort modifiers. One can check if a modifier set is valid for a sort
/// using `sort_data().contains(m)`.
Expand All @@ -164,7 +165,7 @@ impl Modifiers {

/// Parses a string into a singleton [`Modifiers`], or [`NONE`](Self::NONE) if the string is not valid.
#[must_use]
pub fn from_name(s: &[u8]) -> Modifiers {
pub fn from_keyword(s: &[u8]) -> Modifiers {
match s {
b"pure" => Modifiers::PURE,
b"strict" => Modifiers::STRICT,
Expand Down
32 changes: 20 additions & 12 deletions mm0-rs/components/mm0_util/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ use std::mem::{self, MaybeUninit};
use std::ops::{Deref, DerefMut};
use std::path::PathBuf;
use std::rc::Rc;
use std::str::FromStr;
use std::sync::Arc;

mod atoms;
Expand Down Expand Up @@ -487,14 +488,14 @@ struct FileRefInner {
path: PathBuf,
rel: String,
#[cfg(feature = "server")]
url: Option<lsp_types::Url>,
uri: Option<lsp_types::Uri>,
}

/// A reference to a file. It wraps an [`Arc`] so it can be cloned thread-safely.
/// A [`FileRef`] can be constructed either from a [`PathBuf`] or a
/// (`file://`) [`Url`](lsp_types::Url),
/// (`file://`) [`Uri`](lsp_types::Uri),
/// and provides (precomputed) access to these views using
/// [`path()`](FileRef::path) and [`url()`](FileRef::url), as well as
/// [`path()`](FileRef::path) and [`uri()`](FileRef::uri), as well as
/// [`rel()`](FileRef::rel) to get the relative path from [`struct@CURRENT_DIR`].
#[cfg_attr(feature = "memory", derive(DeepSizeOf))]
#[derive(Clone, Default)]
Expand All @@ -503,27 +504,34 @@ pub struct FileRef(Arc<FileRefInner>);
#[cfg(any(target_arch = "wasm32", feature = "lined_string"))]
impl From<PathBuf> for FileRef {
fn from(path: PathBuf) -> FileRef {
fn from_file_path(path: &std::path::Path) -> Option<lsp_types::Uri> {
lsp_types::Uri::from_str(&format!("file://{}", path.to_str()?)).ok()
}
let rel = make_relative(&path);
FileRef(Arc::new(FileRefInner {
#[cfg(all(not(target_arch = "wasm32"), feature = "server"))]
url: lsp_types::Url::from_file_path(&path).ok(),
uri: from_file_path(&path),
#[cfg(all(target_arch = "wasm32", feature = "server"))]
url: lsp_types::Url::parse(&format!("wasm:/{rel}")).ok(),
uri: lsp_types::Uri::from_str(&format!("wasm:/{rel}")).ok(),
rel,
path,
}))
}
}

#[cfg(feature = "server")]
impl From<lsp_types::Url> for FileRef {
fn from(url: lsp_types::Url) -> FileRef {
impl From<lsp_types::Uri> for FileRef {
fn from(uri: lsp_types::Uri) -> FileRef {
fn to_file_path(uri: &lsp_types::Uri) -> Option<PathBuf> {
if uri.scheme()?.as_str() != "file" || uri.authority().is_some() { return None }
Some(PathBuf::from(uri.path().as_str()))
}
#[cfg(not(target_arch = "wasm32"))]
let path = url.to_file_path().expect("bad URL");
let path = to_file_path(&uri).expect("bad URI");
#[cfg(target_arch = "wasm32")]
let path = PathBuf::from(url.path());
let path = PathBuf::from(uri.path().as_str());
let rel = make_relative(&path);
FileRef(Arc::new(FileRefInner { path, rel, url: Some(url) }))
FileRef(Arc::new(FileRefInner { path, rel, uri: Some(uri) }))
}
}

Expand All @@ -536,10 +544,10 @@ impl FileRef {
#[must_use]
pub fn rel(&self) -> &str { &self.0.rel }

/// Convert this [`FileRef`] to a `file://` URL, for use with LSP.
/// Convert this [`FileRef`] to a `file://` URI, for use with LSP.
#[cfg(feature = "server")]
#[must_use]
pub fn url(&self) -> &lsp_types::Url { self.0.url.as_ref().expect("bad file location") }
pub fn url(&self) -> &lsp_types::Uri { self.0.uri.as_ref().expect("bad file location") }

/// Get a pointer to this allocation, for use in hashing.
#[must_use]
Expand Down
6 changes: 3 additions & 3 deletions mm0-rs/components/mm0b_parser/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ categories = ["command-line-utilities", "development-tools", "mathematics"]

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
byteorder = "1.4"
zerocopy = "0.6"
memchr = "2.5"
byteorder = "1.5"
zerocopy = { version = "0.7", features = ["derive"] }
memchr = "2.7"
mm0_util = { version = "0.1.4", path = "../mm0_util", default-features = false }
14 changes: 7 additions & 7 deletions mm0-rs/components/mm0b_parser/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ use std::mem::size_of;

use byteorder::LE;
use mm0_util::{Modifiers, SortId, TermId, ThmId};
use zerocopy::{AsBytes, FromBytes, Unaligned, U16, U32, U64};
use zerocopy::{AsBytes, FromZeroes, FromBytes, Unaligned, U16, U32, U64};

pub use mm0_util::u32_as_usize;
pub use {parser::*, ty::*, write::*};
Expand Down Expand Up @@ -514,7 +514,7 @@ impl TryFrom<(u8, u32)> for UnifyCmd {
/// It is followed by a `sorts: [`[`SortData`]`; num_sorts]` array
/// (which we keep separate because of the dependency).
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, Default, FromBytes, AsBytes)]
#[derive(Debug, Clone, Copy, Default, FromZeroes, FromBytes, AsBytes)]
pub struct Header {
/// The magic number, which is used to identify this as an mmb file. Must be
/// equal to [`MM0B_MAGIC`](cmd::MM0B_MAGIC) = `"MM0B"`.
Expand Down Expand Up @@ -584,7 +584,7 @@ impl Header {
/// of the modifiers in [`Modifiers::sort_data`]: [`PURE`](Modifiers::PURE),
/// [`STRICT`](Modifiers::STRICT), [`PROVABLE`](Modifiers::PROVABLE), [`FREE`](Modifiers::FREE).
#[repr(C)]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes, Unaligned)]
#[derive(Debug, Clone, Copy, FromZeroes, FromBytes, AsBytes, Unaligned)]
pub struct SortData(pub u8);

impl TryFrom<SortData> for Modifiers {
Expand All @@ -603,7 +603,7 @@ impl TryFrom<SortData> for Modifiers {
/// An entry in the term table, which describes the "signature" of the term/def,
/// the information needed to apply the term and use it in theorems.
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
#[derive(Debug, Clone, Copy, FromZeroes, FromBytes, AsBytes)]
pub struct TermEntry {
/// The number of arguments to the term.
pub num_args: U16<LE>,
Expand All @@ -621,7 +621,7 @@ pub struct TermEntry {
/// An entry in the theorem table, which describes the "signature" of the axiom/theorem,
/// the information needed to apply the theorem to use it in other theorems.
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
#[derive(Debug, Clone, Copy, FromZeroes, FromBytes, AsBytes)]
pub struct ThmEntry {
/// The number of arguments to the theorem (exprs, not hyps).
pub num_args: U16<LE>,
Expand All @@ -635,7 +635,7 @@ pub struct ThmEntry {
/// An index table entry, which is essentially an ID describing the table format, and some
/// additional data to find the actual table.
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
#[derive(Debug, Clone, Copy, FromZeroes, FromBytes, AsBytes)]
pub struct TableEntry {
/// A magic number that identifies this table entry, and determines the interpretation of the
/// rest of the data.
Expand All @@ -649,7 +649,7 @@ pub struct TableEntry {

/// An individual symbol name entry in the index.
#[repr(C, align(8))]
#[derive(Debug, Clone, Copy, FromBytes, AsBytes)]
#[derive(Debug, Clone, Copy, FromZeroes, FromBytes, AsBytes)]
pub struct NameEntry {
/// A pointer to the location in the proof stream which introduced this entity.
pub p_proof: U64<LE>,
Expand Down
16 changes: 8 additions & 8 deletions mm0-rs/components/mm0b_parser/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use mm0_util::{SortId, TermId, ThmId};
use std::borrow::Cow;
use std::ops::Range;
use std::{io, mem, mem::size_of};
use zerocopy::{FromBytes, LayoutVerified, U16, U32, U64};
use zerocopy::{FromBytes, Ref, U16, U32, U64};

/// A parsed `MMB` file, as a borrowed type. This does only shallow parsing;
/// additional parsing is done on demand via functions on this type.
Expand Down Expand Up @@ -256,10 +256,10 @@ pub fn parse_cmd(mmb: &[u8], starts_at: usize) -> Result<(u8, u32, usize), Parse
.first()
.map(|&n| (val, n.into(), starts_at + size_of::<u8>() + size_of::<u8>()))
.ok_or_else(|| exhausted!()),
DATA_16 => LayoutVerified::<_, U16<LE>>::new_from_prefix(tl)
DATA_16 => Ref::<_, U16<LE>>::new_from_prefix(tl)
.map(|(n, _)| (val, n.get().into(), starts_at + size_of::<u8>() + size_of::<u16>()))
.ok_or_else(|| exhausted!()),
DATA_32 => LayoutVerified::<_, U32<LE>>::new_from_prefix(tl)
DATA_32 => Ref::<_, U32<LE>>::new_from_prefix(tl)
.map(|(n, _)| (val, n.get(), starts_at + size_of::<u8>() + size_of::<u32>()))
.ok_or_else(|| exhausted!()),
_ => unreachable!(),
Expand Down Expand Up @@ -591,7 +591,7 @@ fn new_slice_prefix<T: FromBytes>(bytes: &[u8], n: usize) -> Option<(&[T], &[u8]
let mid = mem::size_of::<T>().checked_mul(n)?;
if mid <= bytes.len() {
let (left, right) = bytes.split_at(mid);
Some((LayoutVerified::new_slice(left)?.into_slice(), right))
Some((Ref::new_slice(left)?.into_slice(), right))
} else {
None
}
Expand Down Expand Up @@ -628,7 +628,7 @@ impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X> {
pub fn parse(buf: &'a [u8]) -> Result<Self, ParseError> {
use ParseError::{BadIndexParse, BadSorts, BadTerms, BadThms};
let (zc_header, sorts) =
LayoutVerified::<_, Header>::new_from_prefix(buf).ok_or_else(|| find_header_error(buf))?;
Ref::<_, Header>::new_from_prefix(buf).ok_or_else(|| find_header_error(buf))?;
// For potential error reporting
let p_sorts = zc_header.bytes().len();
let header = zc_header.into_ref();
Expand All @@ -638,7 +638,7 @@ impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X> {
// so if this fails, it's a size issue.
let sorts = sorts
.get(..header.num_sorts.into())
.and_then(LayoutVerified::new_slice_unaligned)
.and_then(Ref::new_slice_unaligned)
.ok_or_else(|| BadSorts(p_sorts..u32_as_usize(header.p_terms.get())))?
.into_slice();
let terms = buf
Expand All @@ -660,7 +660,7 @@ impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X> {
if n != 0 {
let (entries, _) = (|| -> Option<_> {
let (num_entries, rest) =
LayoutVerified::<_, U64<LE>>::new_unaligned_from_prefix(buf.get(n..)?)?;
Ref::<_, U64<LE>>::new_unaligned_from_prefix(buf.get(n..)?)?;
new_slice_prefix(rest, num_entries.get().try_into().ok()?)
})()
.ok_or_else(|| BadIndexParse { p_index: u64_as_usize(header.p_index) })?;
Expand Down Expand Up @@ -954,7 +954,7 @@ str_list_wrapper! {

impl<'a, X> MmbFile<'a, X> {
fn str_list_ref(&self, p_vars: U64<LE>) -> Option<StrListRef<'a>> {
let (num_vars, rest) = LayoutVerified::<_, U64<LE>>::new_unaligned_from_prefix(
let (num_vars, rest) = Ref::<_, U64<LE>>::new_unaligned_from_prefix(
self.buf.get(u64_as_usize(p_vars)..)?,
)?;
Some(StrListRef {
Expand Down
4 changes: 2 additions & 2 deletions mm0-rs/components/mm0b_parser/src/ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
use byteorder::LE;
use mm0_util::SortId;
use zerocopy::{AsBytes, FromBytes, Unaligned, U64};
use zerocopy::{AsBytes, FromZeroes, FromBytes, Unaligned, U64};

/// bound mask: `10000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000`
pub const TYPE_BOUND_MASK: u64 = 1 << 63;
Expand All @@ -22,7 +22,7 @@ pub const TYPE_DEPS_MASK: u64 = (1 << 55) - 1;
/// * Bits 0-55 (the low 7 bytes) are a bitset giving the set of bound variables
/// earlier in the list that this variable is allowed to depend on.
#[repr(C)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, FromBytes, AsBytes, Unaligned)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, FromZeroes, FromBytes, AsBytes, Unaligned)]
pub struct Type(U64<LE>);

/// Newtype for `Type` that makes some situations easier to read.
Expand Down
Loading

0 comments on commit 7fe2435

Please sign in to comment.