chore: sync development to main#75
Closed
Xinze-Li-Moqian wants to merge 39 commits into
Closed
Conversation
Informal math notes belong on the development branch, not in the production-grade main. Files preserved on development.
chore: remove informal/ from main
chore: sync development to main
chore: sync development to main
Delete MCMC/, RandomWalk/Spectral/, Metric/CommuteTime/, Metric/JensenShannon/, Metric/Diffusion/, Hyperbolicity/, Hypergraph/Sequence.lean, Open.lean from main. Fix imports in Metric/Default, Resistance/Resistance, Status, lakefile.toml, MetricRegistry, ProofAtlas.lean. Build: 3488 → 2661 jobs. Zero MCMC warnings. Zero sorry. 1 proven metric (resistanceDist). All commands work. All deleted code preserved on development branch.
chore: remove all non-facade code from main
Remove all code except Hypergraph/Basic.lean and Util/Linter/. Everything else lives on development and will be promoted to main one piece at a time as it reaches production quality. main: 126 build jobs, 0 sorry, 0 MCMC, 0 warnings. All deleted code preserved on development branch.
chore: strip main to Hypergraph definition + linters only
- .githooks/pre-push: runs lint.sh before every push - CONTRIBUTING.md: rewritten for main/development branch strategy, setup instructions include hook activation
chore: add pre-push hook + update CONTRIBUTING.md
Hypergraph is a general mathematical structure, not tied to any specific paper. Replace "BDF hypergraph" with "proof hypergraph" in docstrings. Remove paper references from the definition file.
refactor: remove BDF naming from Hypergraph definition
Main now contains only a design specification document for the proof hypergraph — no Lean code. The definition is being redesigned on development (vertices as first-class objects, not bare type parameters). Build: 6 jobs, 0 dependencies, 0 sorry.
refactor: replace Hypergraph code with design spec only
docs(readme): sync with spec-only main
- Remove outdated docs (architecture, how-to, tutorial, ROADMAP, STATUS, refactor proposal) — all describe old codebase - Add docs/milestones/phase-1.md — living checklist for current goals - Update CLAUDE.md: remove dead links, add milestones pointer - ADRs preserved (historical record)
chore: clean docs, add phase-1 checklist
docs(milestones): add two-layer Astrolabe architecture to phase-1
docs(spec): update Basic.lean with two-layer architecture
docs(milestones): three-layer architecture spec
Content-addressable by construction: id is derived from record via the identify function, not stored as a field. No constraints at this layer — atoms, self-reference, and hyperedge semantics are defined in upper layers.
- AstroCore/Core.lean: AstroNerve structure + AstroNet + composable axiom classes (IsInjective, IsClosed) - identify now takes record + refs (Merkle property) - refs carry abstract role tags: List (Role × Id) - Demo/ separated from source (like Mathlib/MathlibTest) - CLAUDE.md: every module must have a demo
Every module in ProofAtlas/ must have a Demo/ file, and demos must compile. Enforced in lint.sh (checks 4/7 and 5/7).
feat: Layer 0 AstroNerve + AstroNet with demos and CI checks (#58)
chore: rename AstroCore → Astrolabe
- DepthResult: .depth n / .cycle / .notFound (clear semantics) - depthOf, isAcyclic, maxDepth, cycleCount, cyclicNerves - degree, orphans, foldl, map, BEq, ToString - isEmpty, atomCount, edgeCount, toList, mapRecords, filterNerves - removeById, mergeNerves, isSubnetOf, nerveAt, ofArray - Deep net demo (4 layers) + cyclic net demo - Full test coverage for all methods
feat(astrolabe): depth filtration, cycle detection, standard methods
- canReach: DFS reachability between two ids - sccs: strongly connected components - sccCount: number of cycle groups - printCycles: all cycle groups - Remove TODOs from demo
feat(astrolabe): SCC, canReach, printCycles (#64)
Remove all old docs pages (architecture, commands, metrics, pipeline, theory, tutorial) and demo components. Landing page now honestly reflects current status.
chore: clean site to match spec-only main
- Convert all comments to /-- -/ docstrings (Nerve.lean, Net.lean) - Add lean/docbuild/ for doc-gen4 (lakefile + toolchain + gitignore) - Add scripts/build-docs.sh for one-command doc generation - Site: API link, fix mdx-components (remove deleted LeanSource/Mermaid) - .gitignore: exclude site/public/api/ and docbuild/.lake/
feat: add Verso docs prototype (#69)
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Bring development up to date with main before resuming feature work