All workflows lean_action_ci.yml

Actor

All actors max

Status

All status success failure waiting running

Layer 3.3a: substantive unit/counit + typed-correctness for adjoint triple

#43 -Commit 391a048dcf pushed by max

Dev_REL2

2026-05-07 08:41:25 -05:00

0s

Axiom debt cleanup: discharge or convert all 99 engine axioms

#42 -Commit 0a7228a8e5 pushed by max

Dev_REL2

2026-05-06 07:32:42 -05:00

0s

Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification)

#41 -Commit 567d8722d5 pushed by max

Dev_REL2

2026-05-06 06:07:52 -05:00

0s

Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification

#40 -Commit cfabca3404 pushed by max

Dev_REL2

2026-05-06 03:25:12 -05:00

0s

Refactor Phase 2: modal unification — Lean engine cascade

#39 -Commit 6e4936d6ee pushed by max

Dev_REL2

2026-05-06 03:13:17 -05:00

0s

Remove Test/Reify.lean — Phase 1 macro-debugging scratch

#38 -Commit c334bf9784 pushed by max

Dev_REL2

2026-05-06 03:01:54 -05:00

0s

Refactor Phase 1: derive_reflect_reify macro — Reflect.lean elegance pass

#37 -Commit 2417ec667b pushed by max

Dev_REL2

2026-05-06 02:43:02 -05:00

0s

Modal cascade Phase 3: Modal.lean module proper — Layer 0 complete

#36 -Commit c7f91fa933 pushed by max

Dev_REL2

2026-05-06 02:42:35 -05:00

0s

Modal cascade Phase 2: Rust ABI v5 → v6 (modal constructors)

#35 -Commit c6bc0aa68f pushed by max

Dev_REL2

2026-05-06 00:28:03 -05:00

0s

Modal cascade Phase 1: Syntax + Lean engine cascade

#34 -Commit b9ca1d8875 pushed by max

Dev_REL2

2026-05-06 00:18:35 -05:00

0s

Layer 0 substrate round 6: contract auto-registration

#33 -Commit 825d8af68d pushed by max

Dev_REL2

2026-05-05 23:22:05 -05:00

0s

Layer 0 substrate round 5: Tactic/EqContract.lean + barrel + Ω-call fixes

#32 -Commit 294e96633d pushed by max

Dev_REL2

2026-05-05 16:56:05 -05:00

0s

Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr

#31 -Commit 2f343b0980 pushed by max

Dev_REL2

2026-05-05 16:19:43 -05:00

0s

Omega.lean: upgrade operators to use CTerm.code (engine universe-code)

#30 -Commit 7ca4ac8d6a pushed by max

Dev_REL2

2026-05-05 15:51:32 -05:00

0s

Layer 0 substrate round 3: Contract.lean — topos-internal contract framework

#29 -Commit 5de7d9e7d0 pushed by max

Dev_REL2

2026-05-05 15:05:02 -05:00

0s

Layer 0 substrate round 2: Subobject + SIP + Modality + Bridge/Set

#28 -Commit 7934275f68 pushed by max

Dev_REL2

2026-05-05 10:45:18 -05:00

0s

Layer 0 substrate (Truncation, Decidable, Omega, Category, Reify)

#27 -Commit f6231f3e64 pushed by max

Dev_REL2

2026-05-05 10:26:59 -05:00

0s

REL2 universe stratification + topolei naming cleanup + Rust ABI v4

#26 -Commit 19928d040a pushed by max

Dev_REL2

2026-05-05 02:41:25 -05:00

0s

Drop Infoductor dependency; cubical-transport is now pure cubical engine

#25 -Commit d03746497b pushed by max

Dev_REL2

2026-05-02 12:58:20 -05:00

0s

Extract Algebra/ foundation to Infoductor; require it from forgejo

#24 -Commit e26ada2fbc pushed by max

Dev_REL2

2026-05-01 08:53:01 -05:00

0s

Drop algebra-restructure exe — source code IS the CLI

#23 -Commit de56626059 pushed by max

Dev_REL2

2026-05-01 08:22:22 -05:00

0s

Abstract the four ⚠️ tools into well-defined primitives

#22 -Commit 48b7326523 pushed by max

Dev_REL2

2026-05-01 07:23:38 -05:00

0s

algebra-restructure CLI + asyncMode .sync on registries

#21 -Commit b88f6e6f62 pushed by max

Dev_REL2

2026-05-01 03:57:49 -05:00

0s

EngineMethodologies + cubical_close: ALGEBRA §9 closer set

#20 -Commit 333f31d4bc pushed by max

Dev_REL2

2026-05-01 02:17:09 -05:00

0s

@[metaPath] + structured failure + engine-bound methodologies

#19 -Commit 60f7ecdf54 pushed by max

Dev_REL2

2026-05-01 02:06:10 -05:00

0s

ALGEBRA Phases A+B+C+D' + cubical_search tactic + doc state-of-play

#18 -Commit 7ccebb606d pushed by max

Dev_REL2

2026-05-01 02:03:35 -05:00

0s

QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing

#17 -Commit 271b47102e pushed by max

Dev_REL2

2026-05-01 01:59:12 -05:00

0s

QUESTIONS Level 1: CompQ reified + classifier-conditioned axioms

#16 -Commit 6adbce0c1b pushed by max

Dev_REL2

2026-05-01 01:34:16 -05:00

0s

Document the question-form algebra + Dev_Algebra plan + Eulerian record

#15 -Commit 95f11020d7 pushed by max

Dev_REL2

2026-05-01 01:22:27 -05:00

0s

REL2 Phase 2: Bridge.lean — Eq ↔ Path interop

#14 -Commit 7152807b66 pushed by max

Dev_REL2

2026-05-01 01:04:48 -05:00

0s