Skip to content

feat: upgrade AlgoLib to Lean 4.35.0 and document installation #27

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sorrachai merged 2 commits into from
Nov 9, 2026
Merged

feat: upgrade AlgoLib to Lean 4.35.0 and document installation #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8341621
docs: explain installing and importing AlgoLib
sorrachai Nov 9, 2026
fee4f48
feat: upgrade AlgoLib to Lean 4.35.0
sorrachai Nov 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 7 additions & 2 deletions .github/workflows/push.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ jobs:
- name: Don't 'import Mathlib', use precise imports
if: always()
run: |
! (find AlgoLib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
! (find AlgoLib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^(public )?(meta )?import Mathlib$')

build:
name: Build project
Expand All @@ -40,6 +40,11 @@ jobs:
id: build-lean
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0

- name: Check public imports and declaration checker
run: |
lake env lean tests/Import.lean
lake build checkdecls

- name: File dependencies
if: github.ref == 'refs/heads/main'
run: |
Expand All @@ -56,4 +61,4 @@ jobs:
homepage: "website"
# website/ is plain static HTML, not a Jekyll site. The action still copies
# the API docs and blueprint into website/, then uploads that folder directly.
build-page: false
build-page: false
164 changes: 83 additions & 81 deletions AlgoLib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,88 +1,90 @@
module

-- Theory
import AlgoLib.Theory.Graph.Adjacency
import AlgoLib.Theory.Graph.Basic
import AlgoLib.Theory.Graph.Basic'
import AlgoLib.Theory.Graph.Coloring.Basic
import AlgoLib.Theory.Graph.Connectivity.Basic
import AlgoLib.Theory.Graph.Connectivity.Components
import AlgoLib.Theory.Graph.Connectivity.Connectivity
import AlgoLib.Theory.Graph.Connectivity.Cuts
import AlgoLib.Theory.Graph.Connectivity.Directed
import AlgoLib.Theory.Graph.Connectivity.Reachable
import AlgoLib.Theory.Graph.Decidable
import AlgoLib.Theory.Graph.Degree
import AlgoLib.Theory.Graph.Delete
import AlgoLib.Theory.Graph.Embeddings.Basic
import AlgoLib.Theory.Graph.Finite
import AlgoLib.Theory.Graph.Graphs
import AlgoLib.Theory.Graph.Matching.Basic
import AlgoLib.Theory.Graph.Minors.Basic
import AlgoLib.Theory.Graph.Spectral.Basic
import AlgoLib.Theory.Graph.Spectral.Cheeger_LB
import AlgoLib.Theory.Graph.Spectral.Cuts
import AlgoLib.Theory.Graph.Spectral.Expansion
import AlgoLib.Theory.Graph.Spectral.Helper
import AlgoLib.Theory.Graph.Structures.Basic
import AlgoLib.Theory.Graph.Structures.Cycle
import AlgoLib.Theory.Graph.Structures.Eulerian
import AlgoLib.Theory.Graph.Structures.Forest
import AlgoLib.Theory.Graph.Structures.Hamiltonian
import AlgoLib.Theory.Graph.Structures.InGraph
import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph
import AlgoLib.Theory.Graph.Structures.InSimpleGraph
import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle
import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path
import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq
import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk
import AlgoLib.Theory.Graph.Structures.Path
import AlgoLib.Theory.Graph.Structures.SimpleCycle
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers
import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers
import AlgoLib.Theory.Graph.Structures.SimplePath
import AlgoLib.Theory.Graph.Structures.SimpleWalk
import AlgoLib.Theory.Graph.Structures.Trail
import AlgoLib.Theory.Graph.Structures.Tree
import AlgoLib.Theory.Graph.Structures.Trees.Basic
import AlgoLib.Theory.Graph.Structures.VertexSeq
import AlgoLib.Theory.Graph.Structures.VertexSeq.Append
import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic
import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix
import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges
import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase
import AlgoLib.Theory.Graph.Structures.VertexSeq.Index
import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip
import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates
import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq
import AlgoLib.Theory.Graph.Structures.Walk
import AlgoLib.Theory.Graph.Subgraph
public import AlgoLib.Theory.Graph.Adjacency
public import AlgoLib.Theory.Graph.Basic
public import AlgoLib.Theory.Graph.Basic'
public import AlgoLib.Theory.Graph.Coloring.Basic
public import AlgoLib.Theory.Graph.Connectivity.Basic
public import AlgoLib.Theory.Graph.Connectivity.Components
public import AlgoLib.Theory.Graph.Connectivity.Connectivity
public import AlgoLib.Theory.Graph.Connectivity.Cuts
public import AlgoLib.Theory.Graph.Connectivity.Directed
public import AlgoLib.Theory.Graph.Connectivity.Reachable
public import AlgoLib.Theory.Graph.Decidable
public import AlgoLib.Theory.Graph.Degree
public import AlgoLib.Theory.Graph.Delete
public import AlgoLib.Theory.Graph.Embeddings.Basic
public import AlgoLib.Theory.Graph.Finite
public import AlgoLib.Theory.Graph.Graphs
public import AlgoLib.Theory.Graph.Matching.Basic
public import AlgoLib.Theory.Graph.Minors.Basic
public import AlgoLib.Theory.Graph.Spectral.Basic
public import AlgoLib.Theory.Graph.Spectral.Cheeger_LB
public import AlgoLib.Theory.Graph.Spectral.Cuts
public import AlgoLib.Theory.Graph.Spectral.Expansion
public import AlgoLib.Theory.Graph.Spectral.Helper
public import AlgoLib.Theory.Graph.Structures.Basic
public import AlgoLib.Theory.Graph.Structures.Cycle
public import AlgoLib.Theory.Graph.Structures.Eulerian
public import AlgoLib.Theory.Graph.Structures.Forest
public import AlgoLib.Theory.Graph.Structures.Hamiltonian
public import AlgoLib.Theory.Graph.Structures.InGraph
public import AlgoLib.Theory.Graph.Structures.InSimpleDiGraph
public import AlgoLib.Theory.Graph.Structures.InSimpleGraph
public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Cycle
public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Path
public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.VertexSeq
public import AlgoLib.Theory.Graph.Structures.InSimpleGraph.Walk
public import AlgoLib.Theory.Graph.Structures.Path
public import AlgoLib.Theory.Graph.Structures.SimpleCycle
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Bipartite
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.Girth
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Bounds
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Core
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.Counting
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.HalfLayers
public import AlgoLib.Theory.Graph.Structures.SimpleGraph_only.MooreBound.RootedLayers
public import AlgoLib.Theory.Graph.Structures.SimplePath
public import AlgoLib.Theory.Graph.Structures.SimpleWalk
public import AlgoLib.Theory.Graph.Structures.Trail
public import AlgoLib.Theory.Graph.Structures.Tree
public import AlgoLib.Theory.Graph.Structures.Trees.Basic
public import AlgoLib.Theory.Graph.Structures.VertexSeq
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Append
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Basic
public import AlgoLib.Theory.Graph.Structures.VertexSeq.CommonPrefix
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Edges
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Erase
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Index
public import AlgoLib.Theory.Graph.Structures.VertexSeq.MapZip
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Predicates
public import AlgoLib.Theory.Graph.Structures.VertexSeq.Subseq
public import AlgoLib.Theory.Graph.Structures.Walk
public import AlgoLib.Theory.Graph.Subgraph

-- Algorithms
import AlgoLib.Algorithms.Graph.Connectivity.Basic
import AlgoLib.Algorithms.Graph.Flow.Basic
import AlgoLib.Algorithms.Graph.MST.Basic
import AlgoLib.Algorithms.Graph.SCC.Basic
import AlgoLib.Algorithms.Graph.Search.Basic
import AlgoLib.Algorithms.Graph.ShortestPath.Basic
import AlgoLib.Algorithms.Graph.Traversal.BFS
import AlgoLib.Algorithms.Graph.Traversal.Basic
public import AlgoLib.Algorithms.Graph.Connectivity.Basic
public import AlgoLib.Algorithms.Graph.Flow.Basic
public import AlgoLib.Algorithms.Graph.MST.Basic
public import AlgoLib.Algorithms.Graph.SCC.Basic
public import AlgoLib.Algorithms.Graph.Search.Basic
public import AlgoLib.Algorithms.Graph.ShortestPath.Basic
public import AlgoLib.Algorithms.Graph.Traversal.BFS
public import AlgoLib.Algorithms.Graph.Traversal.Basic

-- Data structures
import AlgoLib.DataStructures.BinaryTree.Basic
import AlgoLib.DataStructures.BinaryTree.BinaryTree
import AlgoLib.DataStructures.SplayTree.BSTAPI
import AlgoLib.DataStructures.SplayTree.Basic
import AlgoLib.DataStructures.SplayTree.Complexity
import AlgoLib.DataStructures.SplayTree.Correctness
import AlgoLib.DataStructures.SplayTree.StaticOptimality
import AlgoLib.DataStructures.SplayTree.Weighted
import AlgoLib.DataStructures.UnionFind.Basic
public import AlgoLib.DataStructures.BinaryTree.Basic
public import AlgoLib.DataStructures.BinaryTree.BinaryTree
public import AlgoLib.DataStructures.SplayTree.BSTAPI
public import AlgoLib.DataStructures.SplayTree.Basic
public import AlgoLib.DataStructures.SplayTree.Complexity
public import AlgoLib.DataStructures.SplayTree.Correctness
public import AlgoLib.DataStructures.SplayTree.StaticOptimality
public import AlgoLib.DataStructures.SplayTree.Weighted
public import AlgoLib.DataStructures.UnionFind.Basic

-- Utilities
import AlgoLib.Util.Decidable
import AlgoLib.Util.Finset
public import AlgoLib.Util.Decidable
public import AlgoLib.Util.Finset
12 changes: 8 additions & 4 deletions AlgoLib/Algorithms/Graph/Connectivity/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,12 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Huang.JiangYi (co/ Claude Opus 5)
-/
import AlgoLib.Theory.Graph.Decidable
import AlgoLib.Theory.Graph.Connectivity.Connectivity
import AlgoLib.Algorithms.Graph.Traversal.BFS
import AlgoLib.Util.Finset
module

public import AlgoLib.Theory.Graph.Decidable
public import AlgoLib.Theory.Graph.Connectivity.Connectivity
public import AlgoLib.Algorithms.Graph.Traversal.BFS
public import AlgoLib.Util.Finset

/-!
# The computable connectivity layer
Expand Down Expand Up @@ -70,6 +72,8 @@ never imports the algorithms tree.
algorithm: `decide` is realistic up to about six vertices.
-/

@[expose] public section

namespace AlgoLib

variable {α : Type*}
Expand Down
2 changes: 1 addition & 1 deletion AlgoLib/Algorithms/Graph/Flow/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@

module
2 changes: 1 addition & 1 deletion AlgoLib/Algorithms/Graph/MST/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@

module
2 changes: 1 addition & 1 deletion AlgoLib/Algorithms/Graph/SCC/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@

module
2 changes: 1 addition & 1 deletion AlgoLib/Algorithms/Graph/Search/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@

module
2 changes: 1 addition & 1 deletion AlgoLib/Algorithms/Graph/ShortestPath/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@

module
8 changes: 6 additions & 2 deletions AlgoLib/Algorithms/Graph/Traversal/BFS.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,10 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Huang.JiangYi (co/ Claude Fable 5.1)
-/
import AlgoLib.Theory.Graph.Decidable
import AlgoLib.Theory.Graph.Connectivity.Directed
module

public import AlgoLib.Theory.Graph.Decidable
public import AlgoLib.Theory.Graph.Connectivity.Directed

/-!
# Breadth-first search
Expand Down Expand Up @@ -73,6 +75,8 @@ arcs have decidable membership, and proves it correct against the specifications
`V(G)` reaches anything, and `Reachable s s ↔ s ∈ V(G)` is reproduced exactly.
-/

@[expose] public section

namespace AlgoLib

variable {α : Type*}
Expand Down
4 changes: 3 additions & 1 deletion AlgoLib/Algorithms/Graph/Traversal/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@ Copyright (c) 2026 AlgoLib working group. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Huang.JiangYi (co/ Claude Fable 5.1)
-/
import AlgoLib.Algorithms.Graph.Traversal.BFS
module

public import AlgoLib.Algorithms.Graph.Traversal.BFS

/-!
# `AlgoLib.Algorithms.Graph.Traversal`
Expand Down
1 change: 1 addition & 0 deletions AlgoLib/DataStructures/BinaryTree/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
module
Loading
Loading