Feature/notebook#32
Open
junjihashimoto wants to merge 2 commits intomainfrom
Open
Conversation
Tutorial (docs/tutorial/):
- 12 markdown master chapters (Ch00–Ch10 + Ch01b + Ch08b) under
docs/tutorial/md/, generated to docs/tutorial/Notebooks/Gen/
(Lean for `lake build`, .ipynb for JupyterLab) via xlean-convert.
- Display.lean shim: portable replacement for xeus-lean's Display.*
helpers (waveform, boolWave, blockDiagram, verilog, writeWdb,
#mermaid, #help_x, #findDecl, #listNs, #sig, #bash) so chapters
build under headless `lake build` as well as inside the kernel.
- Reference solutions for Ch02/Ch03/Ch04/Ch06/Ch07.
- Docker image (docker/tutorial/) bundling Lean + Lake + xeus-lean +
yosys + nextpnr-{ice40,ecp5} + icestorm + GTKWave; CI workflow
builds & publishes to GHCR on tag.
- .dockerignore drops `.lake/` (~8 GB) from the build context so
iterative `docker build` runs in seconds rather than minutes.
Unified simulation interface (Sparkle/Core/Sim*.lean):
- New `Sparkle.Core.Sim.Sim` typeclass with reset/step/read/destroy
+ a `run`/`trace` helper for the per-cycle loop.
- Three backends:
- PureLean (Sparkle.Core.Sim.PureLean.of) over Signal.val
- JIT (auto-emitted by `#sim` against the existing JITHandle FFI)
- Verilator (Sparkle.Core.Sim.Verilator.of writes a tb.cpp that
exposes the JIT C ABI; reuses JIT.load / JIT.evalTick FFI).
- `#sim counter` now also writes `.lake/build/gen/sim/<n>.sv` and
emits `loadVerilator` next to `load` — switching backends is one
word at the call site.
ResetKind plumbed end-to-end (Sparkle/IR + Verilog backend):
- `ResetKind` moved from Sparkle.Core.Domain to Sparkle.IR.Type
(re-exported under the old name for back-compat).
- `Stmt.register`'s reset is now `String × ResetKind`; the
Verilog emitter switches the sensitivity list per register
(`@(posedge clk)` vs `@(posedge clk or posedge rst)`).
- Compiler.Elab reads the ResetKind from the underlying `Reset
dom`'s domain and stamps it onto the IR.
- `defaultDomain`, `domain50MHz`, `domain200MHz` now genuinely
emit synchronous reset (matches their `.synchronous` value).
Signal.circuit do — `;` is now optional:
- circuitStmt syntax accepts an optional trailing `;` and uses
withPosition/colGe so statements can also be separated by a
newline at matching indent. All tutorial chapters drop the
`;` and read like ordinary Lean `do` blocks.
Docs reorg (move-only, history preserved by git rename detection):
- docs/{architecture,ip-catalog,known-issues,reference}/ folders
with per-folder README indices + top-level docs/README.md.
- docs/tutorial/README.md lists every chapter; old docs/Tutorial*.md
carry deprecation banners pointing into docs/tutorial/.
CI:
- New tutorial-notebooks job runs (a) `lake build TutorialNotebooks`
with the Display shim and (b) builds + executes the .ipynbs under
the real xeus-lean kernel (continue-on-error so kernel breakage
doesn't gate the bedrock shim path).
Tests/Hesper:
- Vendored Hesper float-bridge fixtures + equivalence tests.
Verified:
- `lake build` (70 jobs) green
- `lake exe test` (full suite) green; CoSim mismatch report is
the bit-accuracy negative-test (expected ✗ on a deliberately
corrupted vector).
- `lake build TutorialNotebooks` (52 jobs) green for both old
and new circuit-do syntax.
Previously every Lean function called from a Signal graph was
inlined into the caller, producing a single flat Verilog module.
That works for `lake build` correctness but breaks downstream
flows: place-and-route region constraints, OOC synthesis,
hierarchical timing, and floorplanning all need user-authored
module boundaries to survive into the netlist.
New policy:
- User-defined `def`s become a sub-module instance in the
generated Verilog by default.
- Tag a definition `@[inline_hardware]` to force the old
inline-into-caller behaviour (for primitive combinators and
small helpers where a module boundary would just bloat the
netlist).
- `Sparkle.Compiler.Elab.handleDefinitionUnfold` checks the
attribute and dispatches accordingly. Sub-module synthesis
failures (typeclass dictionaries, polymorphic combinators
that return through dictionary dispatch) silently fall back
to inlining so existing Sparkle code keeps building.
Codegen tweaks for the sub-module path:
- Each sub-module call gets a fresh, unique `inst_<name>_<n>`
identifier — two calls to the same sub-module produce two
distinct Verilog instances (you can't CSE a hardware
instantiation).
- The parent module auto-imports clk/rst input ports if any
child needs them, and auto-routes them to each child's
`clk` / `rst`.
- The same sub-module called multiple times is added to the
Design exactly once (one `module foo` definition + N
`foo inst_foo_<n> (…);` instantiations).
Files:
- Sparkle/Compiler/InlineAttr.lean — `@[inline_hardware]`
attribute registration.
- Sparkle/Compiler/Elab.lean — flipped dispatch + auto-wired
clk/rst + freshName-based instance naming + duplicate-
module-add guard.
- Tests/Tutorial/HierarchyTest.lean — focused test that
asserts:
`latch8x2` → SV contains `module latch8 (` + 2 `inst_latch8_*`
`latch8x2_inl` → SV contains *no* `module latch8inl (` def
- docs/tutorial/md/Ch04_Modules.md §4.6b — new section
showing the multi-module output and explaining
`@[inline_hardware]` opt-out.
- docs/tutorial/md/Ch05_Verilog.md §5.5 — corrected stale
claim ("emits an instance") to point at Ch04 §4.6b.
- lakefile.lean — `tutorial-hierarchy` exe target.
Verified:
- `lake build` (full repo): green.
- `lake exe test`: exit 0, 0 failures.
- `lake exe tutorial-hierarchy`: PASS.
- `lake build TutorialNotebooks`: 53 jobs green.
junjihashimoto
force-pushed
the
feature/notebook
branch
from
ee8a7e9 to
f614785
Compare
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.
No description provided.