feat: add Nix flake for reproducible builds

[paolino]

Add a Nix flake for reproducible builds, testing, and development.

What it provides

• nix build — compiles the Blaster library with -O3
• nix build .#z3check — builds the z3check executable with Z3 4.15.2 in PATH
• nix develop — dev shell with Lean 4.24.0, Lake, elan, and Z3 4.15.2 (works with VS Code Lean 4 extension on NixOS via direnv)
• nix flake check — builds library, z3check, and the full test suite

Key details

• Lean version derived automatically from lean-toolchain via lean4-nix
• Z3 pinned to exactly 4.15.2 (built from source via nixpkgs overlay) to match the project requirement
• Full test suite runs in the Nix sandbox with Z3 injected into each module build via overrideBuildModAttrs
• .envrc included for direnv integration
• ci-nix workflow (manual dispatch) runs nix flake check on ubuntu-latest
• Supports x86_64-linux and aarch64-darwin

Files

File	Change
flake.nix	new — flake definition
flake.lock	new — pinned inputs
.envrc	new — direnv support
.gitignore	updated — result, .direnv/
README.md	updated — Nix section
.github/workflows/ci-nix.yaml	new — manual Nix CI workflow
tests/nix/TestBlaster.lean	new — tactic smoke test

[RSoulatIOHK]

Hi @paolino 👋
Thank you for willing to contribute to Lean-blaster!

Let us know when this is ready by moving this PR to "Ready", we'll assign a reviewer to it.

[RSoulatIOHK]

Thanks! I'll have a look

[Copilot]

Pull request overview

Adds first-class Nix support to make Blaster builds, checks, and development reproducible across supported systems, including a CI workflow to run nix flake check.

Changes:

• Introduces a flake.nix/flake.lock defining build outputs, checks (including a smoke test), and a dev shell with pinned Lean/Z3.
• Adds direnv integration (.envrc) and updates .gitignore for common Nix/direnv artifacts.
• Documents Nix usage in README.md and adds a GitHub Actions workflow to run nix flake check.

Reviewed changes

Copilot reviewed 5 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
flake.nix	Defines Nix flake outputs: library build, wrapped z3check, test builds, smoke-check, and dev shell.
flake.lock	Pins nixpkgs, flake-parts, and lean4-nix inputs for reproducibility.
.envrc	Enables direnv to load the flake dev shell.
.gitignore	Ignores Nix build outputs and direnv artifacts.
README.md	Adds documentation for Nix-based development/build/check workflows.
.github/workflows/ci-nix.yaml	Adds manual CI job running nix flake check.
tests/nix/TestBlaster.lean	Adds a small Lean smoke test to ensure blaster works under Nix.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

src = pkgs.lib.cleanSource ./.; does not respect .gitignore, so local build artifacts (e.g. .lake/, result*, .direnv/) can get captured into the Nix source, breaking reproducibility and potentially slowing builds. Consider switching to cleanSourceWith (or a fileset) with an explicit filter that excludes these directories/files.

Suggested change

	src = pkgs.lib.cleanSource ./.;
	src = pkgs.lib.cleanSourceWith {
	src = ./.;
	filter = path: type:
	pkgs.lib.cleanSourceFilter path type
	&& let
	baseName = builtins.baseNameOf (toString path);
	in
	baseName != ".lake"
	&& baseName != ".direnv"
	&& !(pkgs.lib.hasPrefix "result" baseName);
	};

[paolino]

Fixed in 2009c2b — switched to cleanSourceWith filtering out .lake, .direnv, and result*.

[mpetruska]

Works perfectly. (Tested on Arch, kernel: 6.19.12, nix: 2.34.6)
Only a minor request.

[mpetruska]

I think this should not be added in .gitignore . (I mean the WIP.md file.)

[mpetruska]

@paolino I'd like to humbly request to put local work-files (WIP.md) in the local gitignore (.git/info/exclude).