mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
docs: update AGENTS.md with GitHub repo reference
SilverSight is the primary target for all new formal work. Research Stack is read-only.
This commit is contained in:
parent
4f7c554981
commit
730fd5f280
1 changed files with 8 additions and 2 deletions
10
AGENTS.md
10
AGENTS.md
|
|
@ -2,7 +2,13 @@
|
||||||
|
|
||||||
**SilverSight is the clean-slate rebase of the Research Stack.**
|
**SilverSight is the clean-slate rebase of the Research Stack.**
|
||||||
|
|
||||||
## Location
|
## Repository
|
||||||
|
|
||||||
|
**GitHub:** `https://github.com/allaunthefox/SilverSight`
|
||||||
|
**Local clone:** `/tmp/SilverSight` (or wherever you clone it)
|
||||||
|
**Formal modules:** `formal/SilverSight/`
|
||||||
|
|
||||||
|
## Location (in Research Stack — for lake build integration)
|
||||||
|
|
||||||
```
|
```
|
||||||
0-Core-Formalism/lean/SilverSight/
|
0-Core-Formalism/lean/SilverSight/
|
||||||
|
|
@ -18,7 +24,7 @@
|
||||||
|
|
||||||
## Rules
|
## Rules
|
||||||
|
|
||||||
1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes here.
|
1. **SilverSight is the ONLY target for new formal work.** Do NOT add new modules to `0-Core-Formalism/lean/Semantics/Semantics/`. All new Lean code goes to the SilverSight repository.
|
||||||
|
|
||||||
2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc.
|
2. **Imports from Semantics are allowed** (cross-project): `import Semantics.FixedPoint`, `import Semantics.Spectrum`, etc.
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue