Skip to content

Commit 621b2bd

Browse files
bsdinismkovaxx
andauthored
workspace: update dependencies (#2650)
Co-authored-by: Máté Kovács <481354+mkovaxx@users.noreply.github.com> Co-authored-by: Mate Kovacs <mkovaxx@gmail.com>
1 parent a79e8e2 commit 621b2bd

30 files changed

Lines changed: 916 additions & 811 deletions

File tree

source/Cargo.lock

Lines changed: 760 additions & 662 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

source/Cargo.toml

Lines changed: 35 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -28,51 +28,59 @@ exclude = [
2828
tag = "workspace"
2929

3030
[workspace.dependencies]
31-
anyhow = "1.0"
32-
bincode = "1.0.1"
31+
anyhow = "1.0.103"
32+
bincode-next = { version = "3.1", features = ["serde"] }
3333
cargo_metadata = "0.23.1"
3434
chrono = "0.4.41"
3535
clap-cargo = { version = "0.18.3", features = ["clap", "cargo_metadata"] }
36-
clap = { version = "4.5.53", features = ["derive"] }
37-
colored = "3.0.0"
38-
console = { version = "0.15", default-features = false, features = ["ansi-parsing"] }
36+
clap = { version = "4.6.1", features = ["derive"] }
37+
colored = "3.1"
38+
console = { version = "0.16", default-features = false, features = ["ansi-parsing"] }
3939
convert_case = "0.4"
4040
crates_io_api = "0.12.0"
4141
getopts = { git = "https://github.com/utaal/getopts.git", branch = "parse-partial" }
42-
git2 = { version = "0.18", default-features = false, features = [] }
42+
git2 = { version = "0.21", default-features = false, features = [] }
4343
hex = "0.4.3"
44-
html5ever = "0.25.2"
44+
html5ever = "0.26" # TODO: kuchikiki depends on 0.26
4545
im = "15.1.0"
46-
indexmap = "1"
47-
indicatif = "0.17.7"
46+
indexmap = "2"
47+
indicatif = "0.18"
4848
indoc = "2.0.7"
49-
is-terminal = { version = "0.4.9" }
50-
itertools = "0.14.0"
51-
kuchiki = "0.8.1"
52-
num-bigint = { version = "0.4.4", features = ["serde"] }
53-
num-format = "0.4.0"
49+
is-terminal = "0.4.17"
50+
itertools = "0.15.0"
51+
# kuchikiki has a shakey maintainability story, would be great to remove
52+
# it is transitively using an old version of html5ever and of rand (which has as security advisory)
53+
kuchikiki = "0.8.2"
54+
num-bigint = { version = "0.5.1", features = ["serde"] }
55+
num-format = "0.4.4"
5456
num-traits= "0.2.16"
5557
petgraph = "0.6"
56-
proc-macro2 = "1.0.39"
58+
proc-macro2 = "1.0.106"
5759
quote = "1.0"
58-
rand = { version = "0.8.0" }
59-
regex = "1.11"
60-
rustc_tools_util = "0.3.0"
61-
serde_json = { version = "1.0.145", features = ["preserve_order"] }
60+
rand = "0.10"
61+
regex = "1.13"
62+
rustc_tools_util = "0.4"
63+
serde_json = { version = "1.0.150", features = ["preserve_order"] }
6264
serde = { version = "1", features = ["std", "derive", "rc"] }
63-
sha2 = "0.10.2"
64-
sise = "0.6.0"
65+
sha2 = "0.11"
66+
sise = "0.8.0"
67+
# smt-scope is using very outdated dependencies and seems unmaintained
68+
# it is using:
69+
# - petgraph 0.6
70+
# - instant (unmaintained) -- transitive
71+
# - fxhash (unmaintained)
72+
# - bincode (unmaintained)
73+
# - proc-macro-error (unmaintained) -- transitive
6574
smt-scope = { version = "0.1.7", features = ["analysis"] }
6675
synstructure = "0.13.2"
6776
syn = { version = "2.0", features = ["full", "visit", "visit-mut", "extra-traits"] }
68-
tabled = "0.14.0"
69-
tempfile = "3.23"
77+
tabled = "0.21.0"
78+
tempfile = "3.27"
7079
toml = "1.1.2"
7180
toml_edit = { version = "0.23.3", features = ["serde"] }
72-
tracing = "0.1"
73-
walkdir = "2.3.2"
74-
yansi = "0.5"
75-
zip = "0.6.6"
81+
walkdir = "2.5"
82+
yansi = "1"
83+
zip = "8.6"
7684

7785
# internal dependencies
7886
air = { path = "air" }

source/air/src/context.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use crate::scope_map::ScopeMap;
1212
use crate::smt_process::SmtProcess;
1313
use crate::smt_verify::ReportLongRunning;
1414
use crate::typecheck::Typing;
15-
use sise::Node;
15+
use sise::TreeNode as Node;
1616
use std::any::Any;
1717
use std::collections::HashSet;
1818
use std::sync::Arc;
@@ -527,7 +527,7 @@ impl Context {
527527
}
528528
}
529529

530-
pub fn eval_expr(&mut self, expr: sise::Node) -> String {
530+
pub fn eval_expr(&mut self, expr: sise::TreeNode) -> String {
531531
self.smt_log.log_eval(expr);
532532
let smt_data = self.smt_log.take_pipe_data();
533533
let smt_output = self.get_smt_process().send_commands(smt_data);

source/air/src/emitter.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ use crate::ast::{Decl, Expr, Ident, Query};
22
use crate::context::SmtSolver;
33
use crate::printer::{NodeWriter, Printer, macro_push_node};
44
use crate::{node, nodes};
5-
use sise::Node;
5+
use sise::TreeNode as Node;
66
use std::io::Write;
77

88
pub(crate) struct Emitter {

source/air/src/main.rs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use air::context::{Context, SmtSolver, ValidityResult};
44
use air::messages::{AirMessage, AirMessageLabel, Reporter};
55
use air::profiler::{PROVER_LOG_FILE, Profiler};
66
use getopts::Options;
7-
use sise::Node;
7+
use sise::TreeNode as Node;
88
use std::fs::File;
99
use std::io::Read;
1010

@@ -82,18 +82,18 @@ pub fn main() {
8282

8383
// Open input file
8484
let in_filename = &matches.free[0];
85-
let mut in_bytes: Vec<u8> = Vec::new();
86-
in_bytes.push('(' as u8);
85+
let mut in_string = String::new();
86+
in_string.push('(');
8787
{
8888
File::open(in_filename)
89-
.and_then(|mut file| file.read_to_end(&mut in_bytes))
89+
.and_then(|mut file| file.read_to_string(&mut in_string))
9090
.unwrap_or_else(|e| panic!("could not read file {}: {:?}", in_filename, e));
9191
}
92-
in_bytes.push(')' as u8);
92+
in_string.push(')');
9393

9494
// Parse input file to vector of Node
95-
let mut parser = sise::Parser::new(&in_bytes);
96-
let node = sise::read_into_tree(&mut parser).unwrap();
95+
let mut parser = sise::Parser::new(in_string.as_str());
96+
let node = sise::parse_tree(&mut parser).unwrap();
9797
let nodes = match node {
9898
Node::Atom(_) => panic!("internal error: nodes"),
9999
Node::List(nodes) => nodes,

source/air/src/parser.rs

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ use crate::def::mk_skolem_id;
77
use crate::messages::ArcDynMessageLabel;
88
use crate::model::{ModelDef, ModelDefX, ModelDefs};
99
use crate::printer::node_to_string;
10-
use sise::Node;
11-
use std::io::Write;
10+
use sise::TreeNode as Node;
1211
use std::sync::Arc;
1312

1413
// Following SMT-LIB syntax specification
@@ -577,19 +576,21 @@ impl Parser {
577576
}
578577
match (qid.clone(), skolemid) {
579578
(Some(q), Some(skolem)) => {
580-
let expected_skolemid = mk_skolem_id(&q);
579+
let expected_skolemid = mk_skolem_id(q.as_str());
581580
if skolem == expected_skolemid {
582581
Ok((Arc::new(triggers), qid))
583582
} else {
584583
Err(format!(
585584
"for qid {}, expected skolemid {}; found {}",
586-
q, expected_skolemid, skolem
585+
q.as_str(),
586+
expected_skolemid,
587+
skolem
587588
))
588589
}
589590
}
590591
(Some(q), None) => Err(format!(
591592
"for qid {}, expected skolemid {} but found no skolemid at all",
592-
q,
593+
q.as_str(),
593594
mk_skolem_id(&q)
594595
)),
595596
(None, Some(_)) => Err(format!("skolemid must be accompanied by a qid")),
@@ -882,11 +883,8 @@ impl Parser {
882883
}
883884

884885
pub(crate) fn parse_sexpression(lines: &Vec<String>) -> Node {
885-
let mut model_bytes: Vec<u8> = Vec::new();
886-
for line in lines {
887-
writeln!(model_bytes, "{}", line).expect("model_bytes");
888-
}
889-
let mut parser = sise::Parser::new(&model_bytes[..]);
890-
let node = sise::read_into_tree(&mut parser).unwrap();
886+
let expr = lines.join("\n");
887+
let mut parser = sise::Parser::new(expr.as_str());
888+
let node = sise::parse_tree(&mut parser).unwrap();
891889
node
892890
}

source/air/src/printer.rs

Lines changed: 12 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use crate::ast::{
66
use crate::context::SmtSolver;
77
use crate::def::mk_skolem_id;
88
use crate::util::vec_map;
9-
use sise::{Node, Writer};
9+
use sise::TreeNode as Node;
1010
use std::sync::Arc;
1111

1212
pub fn str_to_node(s: &str) -> Node {
@@ -580,23 +580,22 @@ impl NodeWriter {
580580

581581
pub fn write_node(
582582
&mut self,
583-
writer: &mut sise::SpacedStringWriter,
583+
serializer: &mut sise::Serializer,
584584
node: &Node,
585585
break_len: usize,
586586
brk: bool,
587587
) {
588-
let opts =
589-
sise::SpacedStringWriterNodeOptions { break_line_len: if brk { 0 } else { break_len } };
588+
let break_line_at = if brk { 0 } else { break_len };
590589
match node {
591590
Node::Atom(a) => {
592-
writer.write_atom(a, opts).unwrap();
591+
serializer.put_atom(a, break_line_at);
593592
}
594593
Node::List(l) => {
595-
writer.begin_list(opts).unwrap();
594+
serializer.begin_list(break_line_at);
596595
let mut brk = false;
597596
let mut was_pattern = false;
598597
for n in l {
599-
self.write_node(writer, n, break_len + 1, brk && !was_pattern);
598+
self.write_node(serializer, n, break_len + 1, brk && !was_pattern);
600599
was_pattern = false;
601600
match n {
602601
Node::Atom(a)
@@ -621,21 +620,19 @@ impl NodeWriter {
621620
_ => {}
622621
}
623622
}
624-
writer.end_list(()).unwrap();
623+
serializer.end_list();
625624
}
626625
}
627626
}
628627

629628
pub fn node_to_string_indent(&mut self, indent: &String, node: &Node) -> String {
630629
let indentation = " ";
631-
let style = sise::SpacedStringWriterStyle {
632-
line_break: &("\n".to_string() + &indent),
633-
indentation,
634-
};
630+
let style =
631+
sise::SerializerStyle { line_break: &("\n".to_string() + &indent), indentation };
635632
let mut result = String::new();
636-
let mut string_writer = sise::SpacedStringWriter::new(style, &mut result);
637-
self.write_node(&mut string_writer, &node, 80, false);
638-
string_writer.finish(()).unwrap();
633+
let mut serializer = sise::Serializer::new(style, &mut result);
634+
self.write_node(&mut serializer, &node, 80, false);
635+
serializer.finish(false);
639636
// Clean up result:
640637
clean_up_lines(result, indentation)
641638
}

source/air/src/smt_process.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
use yansi::Paint;
2+
13
use crate::context::SmtSolver;
24
use std::io::{BufRead, BufReader, Write};
35
use std::process::{Child, ChildStdin, ChildStdout};
@@ -121,10 +123,11 @@ impl SmtProcess {
121123
Err(err) => {
122124
eprintln!(
123125
"{}",
124-
yansi::Paint::red(format!(
126+
format!(
125127
"error: could not execute {} process ({})",
126128
solver_info.executable_name, err
127-
))
129+
)
130+
.red()
128131
);
129132
eprintln!(
130133
"help: {name} needs to be in the PATH, or the environment variable {var} must be set to the path of the {name} executable",

source/air/src/tests.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ use crate::parser::Parser;
66
#[allow(unused_imports)]
77
use crate::printer::{macro_push_node, str_to_node};
88
#[allow(unused_imports)]
9-
use sise::Node;
9+
use sise::TreeNode as Node;
1010

1111
#[allow(dead_code)]
12-
fn run_nodes_as_test(should_typecheck: bool, should_be_valid: bool, nodes: &[Node]) {
12+
fn run_nodes_as_test(should_typecheck: bool, should_be_valid: bool, nodes: &[sise::TreeNode]) {
1313
let message_interface = std::sync::Arc::new(crate::messages::AirMessageInterface {});
1414
let reporter = Reporter {};
1515
// TODO: Support testing with cvc5 too

source/rust_verify/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ edition = "2024"
77

88
[dependencies]
99
air = { workspace = true }
10-
bincode = { workspace = true }
10+
bincode-next = { workspace = true }
1111
console = { workspace = true }
1212
getopts = { git = "https://github.com/utaal/getopts.git", branch = "parse-partial" }
1313
hex = { workspace = true }

0 commit comments

Comments
 (0)