From a15f6c96f999848c620b221aa8d690a5aae6f1b5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 12 May 2026 20:43:08 -0400 Subject: [PATCH] Update versions and add top-level CI --- .github/workflows/lean.yml | 42 ++++++++ .github/workflows/rust.yml | 75 ++++++++++++++ lean/.github/workflows/lean_action_ci.yml | 3 +- lean/.github/workflows/nix.yml | 2 +- lean/flake.lock | 23 ++--- lean/flake.nix | 119 ++++++++++++---------- lean/lean-toolchain | 2 +- rust/.cargo/config.toml | 60 ----------- rust/.github/workflows/ci.yml | 24 ++--- rust/Cargo.toml | 54 ++++++++++ 10 files changed, 255 insertions(+), 149 deletions(-) create mode 100644 .github/workflows/lean.yml create mode 100644 .github/workflows/rust.yml delete mode 100644 rust/.cargo/config.toml diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml new file mode 100644 index 0000000..592f48c --- /dev/null +++ b/.github/workflows/lean.yml @@ -0,0 +1,42 @@ +name: Lean CI + +on: + push: + branches: main + paths: + - 'lean/**' + - '.github/workflows/lean.yml' + pull_request: + paths: + - 'lean/**' + - '.github/workflows/lean.yml' + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} + cancel-in-progress: true + +jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - uses: leanprover/lean-action@v1 + with: + lake-package-directory: lean + build-args: "--wfail -v" + + nix-test: + name: Nix Tests + runs-on: ubuntu-latest + defaults: + run: + working-directory: lean + steps: + - uses: actions/checkout@v6 + - uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixos-unstable + github_access_token: ${{ secrets.GITHUB_TOKEN }} + - run: nix build --print-build-logs --accept-flake-config + - run: nix run .#lean-bin --print-build-logs --accept-flake-config \ No newline at end of file diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml new file mode 100644 index 0000000..43237ca --- /dev/null +++ b/.github/workflows/rust.yml @@ -0,0 +1,75 @@ +name: Rust CI + +on: + push: + branches: main + paths: + - 'rust/**' + - '.github/workflows/rust.yml' + pull_request: + paths: + - 'rust/**' + - '.github/workflows/rust.yml' + workflow_dispatch: + +concurrency: + group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} + cancel-in-progress: true + +defaults: + run: + working-directory: rust + +jobs: + linux-test: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - name: Get Rust toolchain channel + id: rust-tc + run: echo "channel=$(awk -F '\"' '/^channel/ {print $2}' rust-toolchain.toml)" >> "$GITHUB_OUTPUT" + - uses: actions-rust-lang/setup-rust-toolchain@v1 + with: + toolchain: ${{ steps.rust-tc.outputs.channel }} + cache-workspaces: rust + - uses: taiki-e/install-action@nextest + - name: Linux Tests + run: cargo nextest run --profile ci --workspace + + lints: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - name: Get Rust toolchain channel + id: rust-tc + run: echo "channel=$(awk -F '\"' '/^channel/ {print $2}' rust-toolchain.toml)" >> "$GITHUB_OUTPUT" + - uses: actions-rust-lang/setup-rust-toolchain@v1 + with: + toolchain: ${{ steps.rust-tc.outputs.channel }} + components: rustfmt, clippy + cache-workspaces: rust + - name: Check Rustfmt code style + run: cargo fmt --all -- --check + - name: Check *everything* compiles + run: cargo check --all-targets --all-features --workspace + - name: Check clippy lints + run: cargo clippy --workspace --all-targets --all-features -- -D warnings + - name: Doctests + run: cargo test --doc --workspace + - name: Cargo-deny + uses: EmbarkStudios/cargo-deny-action@v2 + with: + manifest-path: rust/Cargo.toml + rust-version: ${{ steps.rust-tc.outputs.channel }} + + nix-test: + name: Nix Tests + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixos-unstable + github_access_token: ${{ secrets.GITHUB_TOKEN }} + - run: nix build --print-build-logs --accept-flake-config + - run: nix flake check --print-build-logs --accept-flake-config \ No newline at end of file diff --git a/lean/.github/workflows/lean_action_ci.yml b/lean/.github/workflows/lean_action_ci.yml index 1130c03..093d34b 100644 --- a/lean/.github/workflows/lean_action_ci.yml +++ b/lean/.github/workflows/lean_action_ci.yml @@ -14,8 +14,7 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v5 + - uses: actions/checkout@v6 - uses: leanprover/lean-action@v1 with: build-args: "--wfail -v" - #test: true diff --git a/lean/.github/workflows/nix.yml b/lean/.github/workflows/nix.yml index 56bbb73..34e82be 100644 --- a/lean/.github/workflows/nix.yml +++ b/lean/.github/workflows/nix.yml @@ -17,7 +17,7 @@ jobs: name: Nix Tests runs-on: ubuntu-latest steps: - - uses: actions/checkout@v5 + - uses: actions/checkout@v6 - uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixos-unstable diff --git a/lean/flake.lock b/lean/flake.lock index ad93d4e..eada8b7 100644 --- a/lean/flake.lock +++ b/lean/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1767609335, - "narHash": "sha256-feveD98mQpptwrAEggBQKJTYbvwwglSbOv53uCfH9PY=", + "lastModified": 1777988971, + "narHash": "sha256-qIoWPDs+0/8JecyYgE3gpKQxW/4bLW/gp45vow9ioCQ=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "250481aafeb741edfe23d29195671c19b36b6dca", + "rev": "0678d8986be1661af6bb555f3489f2fdfc31f6ff", "type": "github" }, "original": { @@ -42,16 +42,15 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1766533068, - "narHash": "sha256-o9AUUOBq1SKEPGiwjBIP628N9fPNwAjqSm9xXhVEDNY=", - "owner": "argumentcomputer", + "lastModified": 1777357224, + "narHash": "sha256-bNSODbOOy5tb/vNOPGBlGqMrT8yz7Ghlr8VbVcNbNzY=", + "owner": "lenianiva", "repo": "lean4-nix", - "rev": "7653ecd6d80710f42fcc2c117144698b18acdfc1", + "rev": "14326a235621e8f98526daa0974a8a2ad3682d30", "type": "github" }, "original": { - "owner": "argumentcomputer", - "ref": "7653ecd6d80710f42fcc2c117144698b18acdfc1", + "owner": "lenianiva", "repo": "lean4-nix", "type": "github" } @@ -74,11 +73,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1765674936, - "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=", + "lastModified": 1777168982, + "narHash": "sha256-GOkGPcboWE9BmGCRMLX3worL4EMnsnG8MyKmXNeYuhQ=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85", + "rev": "f5901329dade4a6ea039af1433fb087bd9c1fe14", "type": "github" }, "original": { diff --git a/lean/flake.nix b/lean/flake.nix index 3c823f8..872008c 100644 --- a/lean/flake.nix +++ b/lean/flake.nix @@ -1,33 +1,35 @@ { description = "Lean Nix flake"; - nixConfig = { - extra-substituters = [ - "https://cache.garnix.io" - ]; - extra-trusted-public-keys = [ - "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g=" - ]; - }; + # First enable Garnix GH App for the repo + # nixConfig = { + # extra-substituters = [ + # "https://cache.garnix.io" + # ]; + # extra-trusted-public-keys = [ + # "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g=" + # ]; + # }; inputs = { # System packages nixpkgs.follows = "lean4-nix/nixpkgs"; # Lean 4 & Lake - lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=7653ecd6d80710f42fcc2c117144698b18acdfc1"; + lean4-nix.url = "github:lenianiva/lean4-nix"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; }; - outputs = inputs @ { - nixpkgs, - flake-parts, - lean4-nix, - ... - }: - flake-parts.lib.mkFlake {inherit inputs;} { + outputs = + inputs@{ + nixpkgs, + flake-parts, + lean4-nix, + ... + }: + flake-parts.lib.mkFlake { inherit inputs; } { # Systems we want to build for systems = [ "aarch64-darwin" @@ -36,50 +38,55 @@ "x86_64-linux" ]; - perSystem = { - system, - pkgs, - ... - }: let - lake2nix = pkgs.callPackage lean4-nix.lake {}; - lakeArgs = { - src = ./.; - }; - lakeDeps = lake2nix.buildDeps lakeArgs; - lakeBuildArgs = - lakeArgs - // { + perSystem = + { + system, + pkgs, + ... + }: + let + lake2nix = pkgs.callPackage lean4-nix.lake { }; + lakeArgs = { + src = ./.; + }; + lakeDeps = lake2nix.buildDeps lakeArgs; + lakeBuildArgs = lakeArgs // { inherit lakeDeps; }; - leanLib = lake2nix.mkPackage (lakeBuildArgs - // { - name = "Template"; - buildLibrary = true; - }); - leanBin = lake2nix.mkPackage (lakeBuildArgs - // { - lakeArtifacts = leanLib; - installArtifacts = false; - name = "template"; - }); - in { - # Lean overlay - _module.args.pkgs = import nixpkgs { - inherit system; - overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; - }; + leanLib = lake2nix.mkPackage ( + lakeBuildArgs + // { + name = "Template"; + buildLibrary = true; + } + ); + leanBin = lake2nix.mkPackage ( + lakeBuildArgs + // { + lakeArtifacts = leanLib; + installArtifacts = false; + name = "template"; + } + ); + in + { + # Lean overlay + _module.args.pkgs = import nixpkgs { + inherit system; + overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ]; + }; - packages = { - default = leanLib; - lean-bin = leanBin; - }; + packages = { + default = leanLib; + lean-bin = leanBin; + }; - # Provide a unified dev shell with Lean + Rust - devShells.default = pkgs.mkShell { - packages = with pkgs; [ - lean.lean-all # Includes Lean compiler, lake, stdlib, etc. - ]; + # Provide a unified dev shell with Lean + Rust + devShells.default = pkgs.mkShell { + packages = with pkgs; [ + lean.lean-all # Includes Lean compiler, lake, stdlib, etc. + ]; + }; }; - }; }; } diff --git a/lean/lean-toolchain b/lean/lean-toolchain index e59446d..14791d7 100644 --- a/lean/lean-toolchain +++ b/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.29.0 diff --git a/rust/.cargo/config.toml b/rust/.cargo/config.toml deleted file mode 100644 index 5b5c014..0000000 --- a/rust/.cargo/config.toml +++ /dev/null @@ -1,60 +0,0 @@ -[alias] -# Collection of project wide clippy lints. This is done via an alias because -# clippy doesn't currently allow for specifying project-wide lints in a -# configuration file. This is a similar workaround to the ones presented here: -# -xclippy = [ - "clippy", "--workspace", "--all-targets", "--all-features", "--", - "-Wclippy::all", - "-Wclippy::cast_lossless", - "-Wclippy::cast_possible_truncation", - "-Wclippy::cast_precision_loss", - "-Wclippy::cast_sign_loss", - "-Wclippy::cast_possible_wrap", - "-Wclippy::cast_sign_loss", - "-Wclippy::char_lit_as_u8", - "-Wclippy::fn_to_numeric_cast", - "-Wclippy::fn_to_numeric_cast_with_truncation", - "-Wclippy::ptr_as_ptr", - "-Wclippy::unnecessary_cast", - "-Winvalid_reference_casting", - "-Wclippy::checked_conversions", - "-Wclippy::dbg_macro", - "-Wclippy::disallowed_methods", - "-Wclippy::derive_partial_eq_without_eq", - "-Wclippy::enum_glob_use", - "-Wclippy::explicit_into_iter_loop", - "-Wclippy::fallible_impl_from", - "-Wclippy::filter_map_next", - "-Wclippy::flat_map_option", - "-Wclippy::from_iter_instead_of_collect", - "-Wclippy::implicit_clone", - "-Wclippy::inefficient_to_string", - "-Wclippy::invalid_upcast_comparisons", - "-Wclippy::large_stack_arrays", - "-Wclippy::large_types_passed_by_value", - "-Wclippy::macro_use_imports", - "-Wclippy::manual_assert", - "-Wclippy::manual_ok_or", - "-Wclippy::map_err_ignore", - "-Wclippy::map_flatten", - "-Wclippy::map_unwrap_or", - "-Wclippy::match_same_arms", - "-Wclippy::match_wild_err_arm", - "-Wclippy::needless_borrow", - "-Wclippy::needless_continue", - "-Wclippy::needless_for_each", - "-Wclippy::needless_pass_by_value", - "-Wclippy::option_option", - "-Wclippy::same_functions_in_if_condition", - "-Wclippy::trait_duplication_in_bounds", - "-Wclippy::unnecessary_wraps", - "-Wclippy::unnested_or_patterns", - "-Wnonstandard_style", - "-Wrust_2018_idioms", - "-Wtrivial_numeric_casts", - "-Wunused_lifetimes", - "-Wunreachable_pub", - "-Wtrivial_numeric_casts", - "-Wunused_qualifications", -] diff --git a/rust/.github/workflows/ci.yml b/rust/.github/workflows/ci.yml index 823aa40..0ad1e96 100644 --- a/rust/.github/workflows/ci.yml +++ b/rust/.github/workflows/ci.yml @@ -17,34 +17,24 @@ jobs: # Change to warp-ubuntu-latest-x64-16x for a more powerful runner (GitHub App must be enabled for this repo) runs-on: ubuntu-latest steps: - - uses: actions/checkout@v5 - with: - repository: argumentcomputer/ci-workflows - - uses: ./.github/actions/ci-env - - uses: actions/checkout@v5 - - uses: dtolnay/rust-toolchain@stable + - uses: actions/checkout@v6 + - uses: actions-rust-lang/setup-rust-toolchain@v1 - uses: taiki-e/install-action@nextest - - uses: Swatinem/rust-cache@v2 - name: Linux Tests run: | - cargo nextest run --profile ci --cargo-profile dev-ci --workspace + cargo nextest run --profile ci --workspace lints: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v5 - with: - repository: argumentcomputer/ci-workflows - - uses: ./.github/actions/ci-env - - uses: actions/checkout@v5 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@v6 + - uses: actions-rust-lang/setup-rust-toolchain@v1 - name: Check Rustfmt code style - run: cargo fmt --all --check + uses: actions-rust-lang/rustfmt@v1 - name: Check *everything* compiles run: cargo check --all-targets --all-features --workspace - name: Check clippy lints - run: cargo clippy --workspace --all-targets -- -D warnings + run: cargo clippy --workspace --all-targets --all-features -- -D warnings - name: Doctests run: cargo test --doc --workspace - name: Get Rust version diff --git a/rust/Cargo.toml b/rust/Cargo.toml index 79047f9..8e57519 100644 --- a/rust/Cargo.toml +++ b/rust/Cargo.toml @@ -21,3 +21,57 @@ opt-level = 3 lto = "thin" incremental = false codegen-units = 16 + +[lints.rust] +invalid_reference_casting = "warn" +nonstandard_style = "warn" +rust_2018_idioms = { level = "warn", priority = -1 } +trivial_numeric_casts = "warn" +unreachable_pub = "warn" +unused_lifetimes = "warn" +unused_qualifications = "warn" + +[lints.clippy] +all = { level = "warn", priority = -1 } +cast_lossless = "warn" +cast_possible_truncation = "warn" +cast_possible_wrap = "warn" +cast_precision_loss = "warn" +cast_sign_loss = "warn" +char_lit_as_u8 = "warn" +checked_conversions = "warn" +dbg_macro = "warn" +derive_partial_eq_without_eq = "warn" +disallowed_methods = "warn" +enum_glob_use = "warn" +explicit_into_iter_loop = "warn" +fallible_impl_from = "warn" +filter_map_next = "warn" +flat_map_option = "warn" +fn_to_numeric_cast = "warn" +fn_to_numeric_cast_with_truncation = "warn" +from_iter_instead_of_collect = "warn" +implicit_clone = "warn" +inefficient_to_string = "warn" +invalid_upcast_comparisons = "warn" +large_stack_arrays = "warn" +large_types_passed_by_value = "warn" +macro_use_imports = "warn" +manual_assert = "warn" +manual_ok_or = "warn" +map_err_ignore = "warn" +map_flatten = "warn" +map_unwrap_or = "warn" +match_same_arms = "warn" +match_wild_err_arm = "warn" +needless_borrow = "warn" +needless_continue = "warn" +needless_for_each = "warn" +needless_pass_by_value = "warn" +option_option = "warn" +ptr_as_ptr = "warn" +same_functions_in_if_condition = "warn" +trait_duplication_in_bounds = "warn" +unnecessary_cast = "warn" +unnecessary_wraps = "warn" +unnested_or_patterns = "warn" \ No newline at end of file