Add Copilot instructions and automated environment setup for repository

.github/copilot-instructions.md

@@ -0,0 +1,137 @@
+# Flux Repository - Copilot Coding Agent Instructions
+
+## Overview
+
+Flux is a refinement type checker for Rust. This is a Rust workspace with multiple crates, requiring specific dependencies (Z3, fixpoint) and custom build tooling through `cargo xtask`.
+
+**Languages & Frameworks:** Rust (edition 2024), custom rustc integration  
+**Repository Size:** ~15 crates in workspace + 4 library packages + test suites
+
+**Note:** Required dependencies (fixpoint and Z3 4.12.1) are automatically installed in the Copilot coding agent environment via `.github/workflows/copilot-setup-steps.yml`. For local development, developers need to install these dependencies manually (see CI workflow for installation steps).
+
+## Build & Test Instructions
+
+### Test Commands
+
+1. **Run all regression tests**:
+   ```bash
+   cargo xtask test
+   ```
+   This runs tests from `tests/pos/` (should pass) and `tests/neg/` (should fail with specific errors)
+
+2. **Run specific tests** (filtered by substring):
+   ```bash
+   cargo xtask test <filter>
+   # Example: cargo xtask test impl_trait
+   ```
+
+3. **Test on a single file**:
+   ```bash
+   cargo xtask run <file.rs>
+   # Example: cargo xtask run tests/pos/surface/impl_trait00.rs
+   ```
+   This automatically sets up proper flags for Flux attributes and debugging
+
+### Linting & Formatting
+
+1. **Format code**:
+   ```bash
+   cargo fmt --check  # Check only
+   cargo fmt          # Auto-format
+   ```
+   Uses `rustfmt.toml` configuration
+
+2. **Run clippy**:
+   ```bash
+   cargo clippy
+   ```
+   Uses `clippy.toml` with custom lints defined in `Cargo.toml` workspace section
+
+## Project Layout
+
+### Directory Structure
+
+```
+/
+├── crates/           - Main Flux implementation crates
+│   ├── flux-bin/     - CLI binary (flux, cargo-flux)
+│   ├── flux-driver/  - Rustc driver integration
+│   ├── flux-middle/  - Core type system and refinement types
+│   ├── flux-refineck/ - Refinement type checker
+│   ├── flux-syntax/  - Parsing Flux surface syntax
+│   ├── flux-errors/  - Error reporting
+│   └── ...          - Other supporting crates
+├── lib/             - User-facing Flux libraries
+│   ├── flux-rs/     - Main library with macros (#[flux::sig], etc.)
+│   ├── flux-core/   - Extern specs for std library
+│   ├── flux-attrs/  - Attribute proc macros
+│   └── flux-alloc/  - Extern specs for alloc
+├── tests/           - Regression test suite
+│   ├── pos/         - Tests that should type check
+│   └── neg/         - Tests that should fail with errors
+├── xtask/           - Build system implementation
+├── book/            - User documentation (mdBook).
+├── .github/
+│   └── workflows/
+│       ├── ci.yml   - Main CI: tests, vtock, lean-demo, rustfmt, clippy
+│       └── ...
+└── Configuration files (see below)
+```
+
+### Key Files
+
+- **Cargo.toml**: Workspace configuration with all crates, dependencies, and lints
+- **rust-toolchain.toml**: Specifies Rust toolchain (edition 2024, nightly features)
+- **clippy.toml**: Clippy configuration (allowed/denied lints)
+- **rustfmt.toml**: Code formatting rules
+- **typos.toml**: Spell checking configuration
+- **book/src/guide/develop.md**: Detailed developer guide
+
+### Architecture Notes
+
+- **Flux is a rustc driver**: It integrates with the Rust compiler as a custom driver
+- **Two-stage execution**: 
+  1. Build flux-driver and cargo-flux binaries
+  2. Use cargo-flux to build libraries with refinement types
+- **Custom test framework**: Uses `cargo xtask test` which invokes the test harness in `tests/` package
+
+## CI Pipeline
+
+The `.github/workflows/ci.yml` runs on push/PR to main:
+
+1. **tests job**: Runs `cargo xtask test` on ubuntu/macos/windows
+2. **vtock job**: Tests Flux on the Tock OS kernel (verification use case)
+3. **lean-demo job**: Tests Flux-to-Lean translation feature
+4. **rustfmt job**: Checks code formatting
+5. **clippy job**: Runs `cargo check` and `cargo clippy`
+
+All jobs (except formatting/clippy) require fixpoint and Z3 to be installed first. In the Copilot coding agent environment, these dependencies are automatically installed via `.github/workflows/copilot-setup-steps.yml`.
+
+## Validation Steps
+
+Before submitting changes:
+
+1. **Format code**: `cargo fmt`
+2. **Run regression tests**: `cargo xtask test`
+
+## Important Conventions
+
+- **Error reporting**: Use `bug!`, `span_bug!`, `tracked_span_bug!`, or `QueryErr::bug` for unreachable code paths
+- **Debugging flags**: `-Ztrack-diagnostics=y` to show where errors are emitted (enabled by `cargo xtask run`)
+- **Backtraces**: Set `RUST_BACKTRACE=1`; dev profile gives better traces
+
+## Development Workflow
+
+1. Make changes to relevant crates in `crates/` or `lib/`
+2. Test specific functionality: `cargo xtask test <filter>`
+3. Or test single file: `cargo xtask run <file.rs>`
+4. Run formatter: `cargo fmt`
+5. Run full test suite: `cargo xtask test`
+
+## Trust These Instructions
+
+The information above has been validated against the repository structure, CI configuration, and developer documentation. When you need to build, test, or understand Flux:
+
+- **ALWAYS use `cargo xtask`** for building and testing
+- **NEVER run `cargo test`** directly on the workspace
+- Refer to these instructions first before searching the codebase for build/test commands

.github/workflows/copilot-setup-steps.yml

@@ -0,0 +1,41 @@
+name: "Copilot Setup Steps"
+
+# Automatically run the setup steps when they are changed to allow for easy validation, and
+# allow manual testing through the repository's "Actions" tab
+on:
+  workflow_dispatch:
+  push:
+    paths:
+      - .github/workflows/copilot-setup-steps.yml
+  pull_request:
+    paths:
+      - .github/workflows/copilot-setup-steps.yml
+
+jobs:
+  # The job MUST be called `copilot-setup-steps` or it will not be picked up by Copilot.
+  copilot-setup-steps:
+    runs-on: ubuntu-latest
+
+    # Set the permissions to the lowest permissions possible needed for your steps.
+    # Copilot will be given its own token for its operations.
+    permissions:
+      # If you want to clone the repository as part of your setup steps, for example to install dependencies, you'll need the `contents: read` permission. If you don't clone the repository in your setup steps, Copilot will do this for you automatically after the steps complete.
+      contents: read
+
+    # You can define any steps you want, and they will run before the agent starts.
+    # If you do not check out your code, Copilot will do this for you.
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Install fixpoint
+        uses: ./.github/actions/install-fixpoint
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Install Z3
+        uses: cda-tum/setup-z3@v1.6.6
+        with:
+          # Note: Using 4.12.1 for standard tests. vtock and lean-demo tests use 4.15.3
+          # to avoid hanging issues, but those run in separate CI jobs.
+          version: 4.12.1