diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..13aeca1 --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,146 @@ +# AGENTS.md + +This file provides guidance to coding agents collaborating on this repository. + +## Mission + +Geolog is a Rust codebase for geometric logic: + +- a parser and pretty-printer for the Geolog language, +- an elaboration layer that turns syntax into core structures, +- a REPL and workspace/persistence layer, +- a chase/query/solver runtime, +- and an optional egui GUI behind the `gui` Cargo feature. + +Priorities, in order: + +1. Semantic correctness of theories, instances, queries, and chase behavior. +2. Clear boundaries between parsing, elaboration, core structures, REPL/workspace, and GUI code. +3. Focused, maintainable changes with good regression coverage. +4. Performance only after correctness and testability are preserved. + +## Core Rules + +- Use English for code, comments, docs, tests, and commit-facing text. +- Prefer small, targeted changes over broad rewrites. +- Fix root causes rather than layering on ad hoc workarounds. +- Keep modules decoupled: parsing in parser/lexer, semantics in `core`/`elaborate`, runtime behavior in `repl`/`query`/`solver`, presentation in `gui`. +- Do not introduce unnecessary global mutable state. +- Preserve feature gating: GUI code must remain behind the `gui` feature. +- Avoid adding dependencies unless clearly justified. +- Add comments only when they clarify non-obvious invariants, algorithms, or semantic constraints. + +Quick examples: + +- Good: add a targeted regression test for a chase bug in an existing GUI or unit test module. +- Good: fix a REPL/workspace bug in `src/repl.rs` or `src/store/` without refactoring unrelated parser code. +- Bad: rewrite the AST/core boundary during a small GUI task. +- Bad: mix GUI presentation logic into core semantic modules. + +## Repository Layout + +- `src/lib.rs`: crate entrypoint and module exports. +- `src/ast.rs`, `src/lexer.rs`, `src/parser.rs`, `src/pretty.rs`: syntax pipeline and round-tripping. +- `src/core.rs`: core semantic data structures such as signatures, theories, and structures. +- `src/elaborate/`: elaboration from AST into core representations. +- `src/repl.rs`: REPL state, command handling, and top-level execution flow. +- `src/store/`: persistence/workspace and storage-related logic. +- `src/query/`: chase, query compilation, optimization, backend execution. +- `src/solver/`: solver and tactic logic. +- `src/tensor/`: tensor-based checking/evaluation support. +- `src/gui/`: egui GUI state, panels, and visualizations. +- `src/bin/geolog.rs`: CLI/REPL binary. +- `src/bin/geolog-gui.rs`: GUI binary (requires `--features gui`). +- `examples/geolog/`: sample Geolog programs. +- `tests/`: integration, regression, unit-style cross-module, and property tests. +- `docs/`: architecture and syntax documentation. +- `proofs/`: Lean proofs and formal artifacts. +- `fuzz/`: fuzzing targets. + +## Architecture Constraints + +- Keep the syntax pipeline clean: text → lexer → parser → AST. +- Keep elaboration separate from parsing and separate from UI code. +- `core` types should remain usable without the GUI. +- GUI code should orchestrate and present existing behavior, not reimplement semantic logic. +- Workspace/persistence behavior belongs in `repl`/`store`, not inside GUI widgets. +- Query/chase behavior changes must preserve observable semantics and existing tests. +- If a change affects persistence or serialization, consider compatibility with existing workspace behavior. + +## GUI Rules + +- The GUI is optional and must compile cleanly only when the `gui` feature is enabled. +- Prefer fixing GUI bugs in `src/gui/state.rs`, `src/gui/panels/`, or `src/gui/visualizations/` before touching core logic. +- Keep GUI state transitions explicit and centralized when possible. +- Avoid hard-coding theme assumptions; UI should remain readable in the intended visual style. +- File dialog, editor, browser, inspector, console, and visualization behavior should stay consistent with REPL/workspace state. + +## Testing Layout Rules + +- Prefer unit tests near the code they exercise when there is already a local test module. +- Put broader cross-module coverage in `tests/`. +- Keep regression tests close to the bug they reproduce when that is the clearest fit. +- Do not add a new testing framework if existing `cargo test`, property tests, or fuzz targets are sufficient. +- If you move behavior across modules, move or rewrite the relevant tests with it. + +## Workflow + +Before coding: + +1. Identify whether the task is parser, elaboration, runtime, persistence, solver/query, or GUI work. +2. Read the touched module and nearby tests first. +3. Check whether the change should live in `core`/`repl`/`store` rather than the GUI. + +Implement and validate: + +1. Make the smallest change that solves the problem. +2. Add or update tests when behavior changes or a bug is fixed. +3. Run the narrowest relevant command while iterating. +4. Run broader validation once the change is stable. +5. Update docs if user-facing behavior or workflow changed. + +## Validation Commands + +Use the narrowest relevant command first: + +- General compile check: `cargo check` +- Full test suite: `cargo test` +- GUI compile check: `cargo check --features gui --bin geolog-gui` +- GUI-related tests: `cargo test --features gui` +- Single test/module during iteration: `cargo test ` + +Formatting: + +- Prefer formatting only touched Rust files when the repository is not already fully formatted. +- Avoid reformatting unrelated files as part of a focused bugfix. + +## Testing Expectations + +- No semantic bugfix is complete without appropriate validation. +- Parser/elaboration changes should preserve round-trip and error-reporting behavior where relevant. +- Query/chase/solver changes need explicit coverage because regressions can be subtle. +- GUI bugfixes should get a focused test when practical, especially for state transitions or regressions. +- Keep tests deterministic and focused on observable behavior. + +## Documentation Expectations + +- Update `README.md` when user workflow, CLI behavior, or GUI usage changes. +- Update `docs/ARCHITECTURE.md` or `docs/SYNTAX.md` when architectural or language behavior changes materially. +- If you find stale docs directly related to your change, fix them in the same patch. + +## Review Guidelines + +Review output should be concise and focus on real defects. + +- `P0`: broken build, broken tests, data loss, or incorrect core semantics. +- `P1`: likely semantic regression, unsafe state transition, missing validation on risky changes. + +Use this review format: + +1. `Severity` (`P0`/`P1`) +2. `File:line` +3. `Issue` +4. `Why it matters` +5. `Minimal fix direction` + +Do not include style-only feedback or broad praise. diff --git a/src/gui/app.rs b/src/gui/app.rs index f006587..db0e0f6 100644 --- a/src/gui/app.rs +++ b/src/gui/app.rs @@ -146,7 +146,7 @@ impl GeologApp { /// Handle opening a file fn handle_open_file(&mut self) { - if let Some(path) = rfd::FileDialog::new() + if let Some(path) = Self::new_file_dialog() .add_filter("Geolog", &["geolog"]) .add_filter("All Files", &["*"]) .pick_file() @@ -168,7 +168,7 @@ impl GeologApp { } } else { // Save As - if let Some(path) = rfd::FileDialog::new() + if let Some(path) = Self::new_file_dialog() .add_filter("Geolog", &["geolog"]) .save_file() { @@ -185,6 +185,14 @@ impl GeologApp { } } + fn new_file_dialog() -> rfd::FileDialog { + let dialog = rfd::FileDialog::new(); + match std::env::current_dir() { + Ok(dir) => dialog.set_directory(dir), + Err(_) => dialog, + } + } + /// Run chase on an instance fn handle_run_chase(&mut self, instance_name: &str) { use crate::core::RelationStorage;