diff --git a/.github/workflows/zz-diag.yml b/.github/workflows/zz-diag.yml deleted file mode 100644 index da119213..00000000 --- a/.github/workflows/zz-diag.yml +++ /dev/null @@ -1,67 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# TEMPORARY diagnostic workflow. Deliberately contains no `uses:` steps: a -# newly added workflow in this repo that references an action fails at -# startup ("This run likely failed because of a workflow file issue"), so -# this clones by hand and publishes each stage over a pollable topic, which -# is readable from environments where the job log endpoint is blocked. -# Delete once the branch is green. -name: ZZ diag - -on: - push: - branches: [arena/5b8efe75-echidna] - -permissions: - contents: read - -jobs: - diag: - runs-on: ubuntu-latest - timeout-minutes: 55 - steps: - - name: Collect diagnostics - env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - T: https://ntfy.sh - run: | - set -u - pub() { curl -sS -m 30 --data-binary @"$2" "${T}/$1" >/dev/null 2>&1 || true; } - note() { printf '%s\n' "$2" > /tmp/note; pub "$1" /tmp/note; } - chunked() { # topic file - rm -f /tmp/ck.* - split -C 3800 -a 3 "$2" /tmp/ck. - for f in /tmp/ck.*; do pub "$1" "${f}"; sleep 1; done - } - sudo apt-get update -qq >/dev/null 2>&1 - sudo apt-get install -y -qq capnproto protobuf-compiler pkg-config libssl-dev >/dev/null 2>&1 - if ! git clone -q --depth 5 --branch arena/5b8efe75-echidna \ - "https://x-access-token:${GH_TOKEN}@github.com/hyperpolymath/echidna.git" repo >/tmp/clone.log 2>&1; then - chunked echidna-status-7f3a91 /tmp/clone.log - note echidna-status-7f3a91 "clone FAILED" - exit 0 - fi - note echidna-status-7f3a91 "clone ok $(git -C repo rev-parse --short HEAD)" - cd repo - - cargo fmt --all && note echidna-status-7f3a91 "fmt applied" || note echidna-status-7f3a91 "fmt FAILED" - git diff > /tmp/fmt.patch - note echidna-status-7f3a91 "fmt patch bytes $(wc -c < /tmp/fmt.patch)" - base64 -w 200 /tmp/fmt.patch > /tmp/fmt.b64 - chunked echidna-fmt2-7f3a91 /tmp/fmt.b64 - note echidna-status-7f3a91 "fmt patch published" - - cargo test --locked -p echidna-core-creusot > /tmp/t1.log 2>&1 - note echidna-status-7f3a91 "core-creusot exit $?" - tail -n 40 /tmp/t1.log > /tmp/t1.tail; chunked echidna-test2-7f3a91 /tmp/t1.tail - - cargo test --locked --test corpus_estate_adapters --test corpus_cli_dispatch \ - --test lexicon_v2_test > /tmp/t2.log 2>&1 - note echidna-status-7f3a91 "estate adapters exit $?" - grep -E '^(test |error|failures:|---- )' /tmp/t2.log | tail -n 60 > /tmp/t2.tail - chunked echidna-test2-7f3a91 /tmp/t2.tail - - cargo clippy --locked --workspace --all-targets -- -D warnings > /tmp/cl.log 2>&1 - note echidna-status-7f3a91 "clippy exit $?" - grep -E '^(error|warning)' -A 6 /tmp/cl.log | head -n 400 > /tmp/cl.tail - chunked echidna-clippy-7f3a91 /tmp/cl.tail - note echidna-status-7f3a91 "DONE" diff --git a/.github/workflows/zz-fmt.yml b/.github/workflows/zz-fmt.yml deleted file mode 100644 index c895c5fc..00000000 --- a/.github/workflows/zz-fmt.yml +++ /dev/null @@ -1,46 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# TEMPORARY: applies `cargo fmt --all` on this branch and commits the result, -# because the branch was prepared in an environment with no Rust toolchain. -# It contains no `uses:` steps on purpose: a newly added workflow in this -# repo that references an action fails at startup ("This run likely failed -# because of a workflow file issue"). Delete once the branch is green. -name: ZZ fmt - -on: - push: - branches: [arena/5b8efe75-echidna] - -permissions: - contents: write - -jobs: - fmt: - runs-on: ubuntu-latest - timeout-minutes: 20 - steps: - - name: Format and commit - env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - T: https://ntfy.sh/echidna-push-7f3a91 - run: | - set -u - note() { printf '%s\n' "$*" | curl -sS -m 20 --data-binary @- "${T}" >/dev/null 2>&1 || true; } - git clone -q --depth 5 --branch arena/5b8efe75-echidna \ - "https://x-access-token:${GH_TOKEN}@github.com/hyperpolymath/echidna.git" repo || { - note "clone failed"; exit 0; } - cd repo - note "clone ok $(git rev-parse --short HEAD)" - cargo fmt --all || note "cargo fmt failed" - if git diff --quiet; then - note "already formatted at $(git rev-parse --short HEAD)" - exit 0 - fi - note "diff stat: $(git diff --shortstat)" - git config user.name "echidna fmt bot" - git config user.email "fmt-bot@users.noreply.github.com" - git commit -qam "style: cargo fmt" || { note "commit failed"; exit 0; } - if git push -q origin HEAD:arena/5b8efe75-echidna 2>/tmp/push.log; then - note "pushed $(git rev-parse --short HEAD)" - else - note "push failed: $(head -c 300 /tmp/push.log)" - fi diff --git a/src/rust/corpus/canonical.rs b/src/rust/corpus/canonical.rs index c441c087..d3558b5d 100644 --- a/src/rust/corpus/canonical.rs +++ b/src/rust/corpus/canonical.rs @@ -882,11 +882,23 @@ impl Parser { /// Application, including prefix operator use: `(+ x y)`. fn app(&mut self) -> Node { + // A bracketed group is already complete: `(eq a b)` must not be + // re-read as the prefix form `eq a b`, or the group's own arguments + // are swallowed by the enclosing application and the term collapses + // to a bare operator name. + let from_group = matches!(self.peek(), Some(Tk::Open(_))); let head = match self.atom() { Some(h) => h, None => return Node::Hole, }; - if let Node::Op(op, _) = head.clone() { + if let Node::Op(op, args) = head.clone() { + if from_group { + return if args.is_empty() { + Node::Name(op.to_string()) + } else { + head + }; + } let mut args: Vec = Vec::new(); loop { let stop = match self.peek() { @@ -940,14 +952,9 @@ impl Parser { fn expr(&mut self, min_prec: u8) -> Node { let mut left = self.app(); - loop { - let op = match self.op_at() { - Some(op) => op, - None => break, - }; - let prec = match precedence(op) { - Some(p) => p, - None => break, + while let Some(op) = self.op_at() { + let Some(prec) = precedence(op) else { + break; }; if prec < min_prec { break; diff --git a/src/rust/corpus/creusot.rs b/src/rust/corpus/creusot.rs index 8df3629d..618791fc 100644 --- a/src/rust/corpus/creusot.rs +++ b/src/rust/corpus/creusot.rs @@ -478,22 +478,23 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile { let clean = clean_source(src); let toks = tokenise(&clean); let attrs = collect_attrs(src, &toks); - let mut parsed = ParsedFile::default(); - - parsed.imports = collect_uses(src, &toks); + let mut parsed = ParsedFile { + imports: collect_uses(src, &toks), + ..Default::default() + }; let mut k = 0; while k < toks.len() { let t = &toks[k]; + let next_is_fn = k + 1 < toks.len() && is_kw(&toks[k + 1], "fn"); + let is_const_item = is_kw(t, "const") && !next_is_fn; let (kind, name_idx) = if is_kw(t, "fn") { (DeclKind::Function, k + 1) } else if is_kw(t, "struct") || is_kw(t, "enum") || is_kw(t, "union") { (DeclKind::Data, k + 1) } else if is_kw(t, "trait") { (DeclKind::Record, k + 1) - } else if is_kw(t, "type") || is_kw(t, "static") { - (DeclKind::Data, k + 1) - } else if is_kw(t, "const") && !(k + 1 < toks.len() && is_kw(&toks[k + 1], "fn")) { + } else if is_kw(t, "type") || is_kw(t, "static") || is_const_item { (DeclKind::Data, k + 1) } else { k += 1; @@ -565,10 +566,10 @@ pub(crate) fn parse_rust_file(src: &str) -> ParsedFile { axiom_usage, }); - if has_attr(&leading, "cfg(creusot)") { - if !parsed.options.iter().any(|o| o == "creusot-gated") { - parsed.options.push("creusot-gated".to_string()); - } + if has_attr(&leading, "cfg(creusot)") + && !parsed.options.iter().any(|o| o == "creusot-gated") + { + parsed.options.push("creusot-gated".to_string()); } k = advance.max(k + 1); diff --git a/src/rust/corpus/octad.rs b/src/rust/corpus/octad.rs index 1e6ee3cb..076f8f74 100644 --- a/src/rust/corpus/octad.rs +++ b/src/rust/corpus/octad.rs @@ -755,7 +755,7 @@ mod tests { coq.graph.cross_prover_identity_key, smtlib.graph.cross_prover_identity_key ); - assert_eq!(coq.graph.identity_scheme, super::canonical::SCHEME); + assert_eq!(coq.graph.identity_scheme, crate::corpus::canonical::SCHEME); assert_eq!( coq.graph.canonical_type, "(PI [NAT NAT] (EQ (ADD v0 v1) (ADD v1 v0)))" diff --git a/src/rust/corpus/spark_ada.rs b/src/rust/corpus/spark_ada.rs index f4b67b53..11cf01f8 100644 --- a/src/rust/corpus/spark_ada.rs +++ b/src/rust/corpus/spark_ada.rs @@ -725,10 +725,7 @@ fn collect_imports(toks: &[Tok]) -> Vec { let mut names: Vec = Vec::new(); let mut j = i + 1; let mut terminated = false; - loop { - let Some((name, next)) = dotted_name(&toks, j) else { - break; - }; + while let Some((name, next)) = dotted_name(toks, j) { names.push(name); if next < toks.len() && is_punct(&toks[next], ",") { j = next + 1; @@ -804,10 +801,11 @@ fn body_end_idx(toks: &[Tok], from: usize, name: &str) -> Option { fn find_end_name(toks: &[Tok], from: usize, name: &str) -> Option { let mut j = from; while j + 1 < toks.len() { - if is_kw(&toks[j], "end") && toks[j + 1].kind == TokKind::Ident { - if toks[j + 1].text.eq_ignore_ascii_case(name) { - return Some(j); - } + if is_kw(&toks[j], "end") + && toks[j + 1].kind == TokKind::Ident + && toks[j + 1].text.eq_ignore_ascii_case(name) + { + return Some(j); } j += 1; } diff --git a/src/rust/main.rs b/src/rust/main.rs index 56a4d4f5..60f9616d 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -279,10 +279,9 @@ enum CorpusOp { }, /// Look up entries across every synonym table by `semantic_class`. - /// Demonstrates cross-prover semantic equivalence — e.g. - /// `corpus crossquery well-foundedness` reports `WellFounded` in Agda - /// + `well_founded` in Coq + `WellFounded` in Lean + `WellFounded` in - /// Idris 2. + /// Demonstrates cross-prover semantic equivalence: `corpus crossquery + /// well-foundedness` reports `WellFounded` in Agda, `well_founded` in + /// Coq, and `WellFounded` in Lean and Idris 2. /// /// The cross-prover dictionaries are searched too, so classes that /// only exist there (`wrapping-arithmetic`, `frame-rule`,