Skip to content
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.

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

doc: layout algorithm #3915

Merged
merged 2 commits into from
May 3, 2024
Merged

doc: layout algorithm #3915

merged 2 commits into from
May 3, 2024

Conversation

digama0
Copy link
Collaborator

@digama0 digama0 commented Apr 15, 2024

The layout algorithm, while somewhat finicky, is (unfortunately) necessary for C code to interface with lean structures. This adds a (AFAIK) complete description of the layout algorithm, including a worked example large enough to make it possible to reconstruct the whole decision diagram.

@digama0 digama0 mentioned this pull request Apr 15, 2024
doc/dev/ffi.md Show resolved Hide resolved
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 15, 2024
@Kha
Copy link
Member

Kha commented Apr 18, 2024

If we're documenting access, shouldn't we also document construction?

@digama0
Copy link
Collaborator Author

digama0 commented Apr 18, 2024

The example with access functions was mainly for demonstration purposes, to show the way offsets are used. Hopefully pointing to the existence of setter functions and saying "these are used similarly" should be sufficient.

@Kha Kha self-assigned this Apr 30, 2024
doc/dev/ffi.md Outdated Show resolved Hide resolved
doc/dev/ffi.md Outdated Show resolved Hide resolved
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 62bb0f662b20355d2d95a08665fdb09d7be277e5 --onto 806e41151b6eb645e4ed5a40915b94b99f933564. (2024-05-02 22:22:13)

@Kha Kha added this pull request to the merge queue May 3, 2024
Merged via the queue into leanprover:master with commit 2db602c May 3, 2024
11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants