Skip to content

Commit b5977a5

Browse files
CopilotCopilot
authored
Add Copilot instructions and automated environment setup for repository (#1456)
1 parent 8256bd0 commit b5977a5

2 files changed

Lines changed: 178 additions & 0 deletions

File tree

‎.github/copilot-instructions.md‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
# Flux Repository - Copilot Coding Agent Instructions
2+
3+
## Overview
4+
5+
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`.
6+
7+
**Languages & Frameworks:** Rust (edition 2024), custom rustc integration
8+
**Repository Size:** ~15 crates in workspace + 4 library packages + test suites
9+
10+
**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).
11+
12+
## Build & Test Instructions
13+
14+
### Test Commands
15+
16+
1. **Run all regression tests**:
17+
```bash
18+
cargo xtask test
19+
```
20+
This runs tests from `tests/pos/` (should pass) and `tests/neg/` (should fail with specific errors)
21+
22+
2. **Run specific tests** (filtered by substring):
23+
```bash
24+
cargo xtask test <filter>
25+
# Example: cargo xtask test impl_trait
26+
```
27+
28+
3. **Test on a single file**:
29+
```bash
30+
cargo xtask run <file.rs>
31+
# Example: cargo xtask run tests/pos/surface/impl_trait00.rs
32+
```
33+
This automatically sets up proper flags for Flux attributes and debugging
34+
35+
### Linting & Formatting
36+
37+
1. **Format code**:
38+
```bash
39+
cargo fmt --check # Check only
40+
cargo fmt # Auto-format
41+
```
42+
Uses `rustfmt.toml` configuration
43+
44+
2. **Run clippy**:
45+
```bash
46+
cargo clippy
47+
```
48+
Uses `clippy.toml` with custom lints defined in `Cargo.toml` workspace section
49+
50+
## Project Layout
51+
52+
### Directory Structure
53+
54+
```
55+
/
56+
├── crates/ - Main Flux implementation crates
57+
│ ├── flux-bin/ - CLI binary (flux, cargo-flux)
58+
│ ├── flux-driver/ - Rustc driver integration
59+
│ ├── flux-middle/ - Core type system and refinement types
60+
│ ├── flux-refineck/ - Refinement type checker
61+
│ ├── flux-syntax/ - Parsing Flux surface syntax
62+
│ ├── flux-errors/ - Error reporting
63+
│ └── ... - Other supporting crates
64+
├── lib/ - User-facing Flux libraries
65+
│ ├── flux-rs/ - Main library with macros (#[flux::sig], etc.)
66+
│ ├── flux-core/ - Extern specs for std library
67+
│ ├── flux-attrs/ - Attribute proc macros
68+
│ └── flux-alloc/ - Extern specs for alloc
69+
├── tests/ - Regression test suite
70+
│ ├── pos/ - Tests that should type check
71+
│ └── neg/ - Tests that should fail with errors
72+
├── xtask/ - Build system implementation
73+
├── book/ - User documentation (mdBook).
74+
├── .github/
75+
│ └── workflows/
76+
│ ├── ci.yml - Main CI: tests, vtock, lean-demo, rustfmt, clippy
77+
│ └── ...
78+
└── Configuration files (see below)
79+
```
80+
81+
### Key Files
82+
83+
- **Cargo.toml**: Workspace configuration with all crates, dependencies, and lints
84+
- **rust-toolchain.toml**: Specifies Rust toolchain (edition 2024, nightly features)
85+
- **clippy.toml**: Clippy configuration (allowed/denied lints)
86+
- **rustfmt.toml**: Code formatting rules
87+
- **typos.toml**: Spell checking configuration
88+
- **book/src/guide/develop.md**: Detailed developer guide
89+
90+
### Architecture Notes
91+
92+
- **Flux is a rustc driver**: It integrates with the Rust compiler as a custom driver
93+
- **Two-stage execution**:
94+
1. Build flux-driver and cargo-flux binaries
95+
2. Use cargo-flux to build libraries with refinement types
96+
- **Custom test framework**: Uses `cargo xtask test` which invokes the test harness in `tests/` package
97+
98+
## CI Pipeline
99+
100+
The `.github/workflows/ci.yml` runs on push/PR to main:
101+
102+
1. **tests job**: Runs `cargo xtask test` on ubuntu/macos/windows
103+
2. **vtock job**: Tests Flux on the Tock OS kernel (verification use case)
104+
3. **lean-demo job**: Tests Flux-to-Lean translation feature
105+
4. **rustfmt job**: Checks code formatting
106+
5. **clippy job**: Runs `cargo check` and `cargo clippy`
107+
108+
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`.
109+
110+
## Validation Steps
111+
112+
Before submitting changes:
113+
114+
1. **Format code**: `cargo fmt`
115+
2. **Run regression tests**: `cargo xtask test`
116+
117+
## Important Conventions
118+
119+
- **Error reporting**: Use `bug!`, `span_bug!`, `tracked_span_bug!`, or `QueryErr::bug` for unreachable code paths
120+
- **Debugging flags**: `-Ztrack-diagnostics=y` to show where errors are emitted (enabled by `cargo xtask run`)
121+
- **Backtraces**: Set `RUST_BACKTRACE=1`; dev profile gives better traces
122+
123+
## Development Workflow
124+
125+
1. Make changes to relevant crates in `crates/` or `lib/`
126+
2. Test specific functionality: `cargo xtask test <filter>`
127+
3. Or test single file: `cargo xtask run <file.rs>`
128+
4. Run formatter: `cargo fmt`
129+
5. Run full test suite: `cargo xtask test`
130+
131+
## Trust These Instructions
132+
133+
The information above has been validated against the repository structure, CI configuration, and developer documentation. When you need to build, test, or understand Flux:
134+
135+
- **ALWAYS use `cargo xtask`** for building and testing
136+
- **NEVER run `cargo test`** directly on the workspace
137+
- Refer to these instructions first before searching the codebase for build/test commands

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

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
name: "Copilot Setup Steps"
2+
3+
# Automatically run the setup steps when they are changed to allow for easy validation, and
4+
# allow manual testing through the repository's "Actions" tab
5+
on:
6+
workflow_dispatch:
7+
push:
8+
paths:
9+
- .github/workflows/copilot-setup-steps.yml
10+
pull_request:
11+
paths:
12+
- .github/workflows/copilot-setup-steps.yml
13+
14+
jobs:
15+
# The job MUST be called `copilot-setup-steps` or it will not be picked up by Copilot.
16+
copilot-setup-steps:
17+
runs-on: ubuntu-latest
18+
19+
# Set the permissions to the lowest permissions possible needed for your steps.
20+
# Copilot will be given its own token for its operations.
21+
permissions:
22+
# 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.
23+
contents: read
24+
25+
# You can define any steps you want, and they will run before the agent starts.
26+
# If you do not check out your code, Copilot will do this for you.
27+
steps:
28+
- name: Checkout code
29+
uses: actions/checkout@v4
30+
31+
- name: Install fixpoint
32+
uses: ./.github/actions/install-fixpoint
33+
env:
34+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
35+
36+
- name: Install Z3
37+
uses: cda-tum/setup-z3@v1.6.6
38+
with:
39+
# Note: Using 4.12.1 for standard tests. vtock and lean-demo tests use 4.15.3
40+
# to avoid hanging issues, but those run in separate CI jobs.
41+
version: 4.12.1

0 commit comments

Comments
 (0)