Skip to content

Update Pulse Tutorial#569

Draft
gebner wants to merge 6 commits into
mainfrom
gebner_update_tutorial
Draft

Update Pulse Tutorial#569
gebner wants to merge 6 commits into
mainfrom
gebner_update_tutorial

Conversation

@gebner
Copy link
Copy Markdown
Contributor

@gebner gebner commented Feb 21, 2026

The Pulse tutorial is slowly bitrotting away. We need to change that.

  • The tutorial is not being updated nearly as much as it should since it's in a separate repository.
  • The tutorial code is not being updated since that requires coordination with the other repo.
  • The tutorial contains automatically generated code that is not being updated at all (and is out of date by now, as expected).
  • Some examples in the tutorial are not checked at all and completely rotten away by now, as expected.

I propose the following changes in workflow:

  1. We move the tutorial in the Pulse repo next to the accompanying code, to reduce coordination effort and widen the net of potential contributors.
  2. Major PRs include updates to the tutorial.

Additionally, we need to do some one time work to get the tutorial up to date with the current state of the Pulse:

  1. Examples need to be reviewed for current idiomatic style.
  2. Recent additions to the language should be documented.
    • ANF
    • |-> syntax
    • preserves/multiple requires
    • new-style while loops
    • Impure specs
    • Gotos
    • Automatic lemmas
    • Located resources
    • Uninitialized memory

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants