chore: sync main with development#77
Merged
Merged
Conversation
* chore: remove informal/ from main Informal math notes belong on the development branch, not in the production-grade main. Files preserved on development. * chore: remove all non-facade code from 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: strip main to Hypergraph definition + linters only 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: add pre-push hook + update CONTRIBUTING.md - .githooks/pre-push: runs lint.sh before every push - CONTRIBUTING.md: rewritten for main/development branch strategy, setup instructions include hook activation * refactor: remove BDF naming from Hypergraph definition 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: replace Hypergraph code with design spec only 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. * docs(readme): sync with spec-only main * chore: clean docs, add phase-1 checklist - 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) * docs(milestones): add two-layer Astrolabe architecture to phase-1 * docs(spec): update Basic.lean with two-layer Astrolabe architecture * docs(milestones): three-layer architecture spec with definitions * feat: add AstroNerve Layer 0 structure (#58) 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. * feat: Layer 0 AstroNerve + AstroNet, separate Demo/ (#58) - 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 * feat(ci): add demo coverage + demo build checks to lint.sh Every module in ProofAtlas/ must have a Demo/ file, and demos must compile. Enforced in lint.sh (checks 4/7 and 5/7). * chore: rename AstroCore → Astrolabe * feat(astrolabe): depth filtration, cycle detection, standard methods - 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): add SCC, canReach, printCycles - canReach: DFS reachability between two ids - sccs: strongly connected components - sccCount: number of cycle groups - printCycles: all cycle groups - Remove TODOs from demo * chore: clean site to match spec-only main Remove all old docs pages (architecture, commands, metrics, pipeline, theory, tutorial) and demo components. Landing page now honestly reflects current status. * feat: doc-gen4 integration + docstrings (#69) - 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/ * chore: convert Nerve.lean comments to docstrings for doc-gen4 * chore: convert all comments to docstrings, add DocstringRequired linter - Net.lean: all `--` → `/-- -/` docstrings for doc-gen4 - Nerve.lean: fix remaining `--` on ToString instance, add linter import - New DocstringRequired linter: every public declaration must have docstring - Barrel import ProofAtlas.Util.Linter for transitive linter loading - Disable MathTag weak option (linter code retained, not enforced) * chore: trigger CI with updated base
chore: sync development with main
|
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 docstring changes, DocstringRequired linter, and branch strategy into main