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

Dump a list of tutorials and commands they first introduce #1186

Merged
merged 8 commits into from Apr 3, 2023

Conversation

kostmo
Copy link
Member

@kostmo kostmo commented Mar 29, 2023

May be able to reduce likelihood of #1086 by having a autogenerated table of the commands and the tutorials they are introduced in.

This work is related to #1106 in that robot commands should be given distinct markup (backticks).

Demo

scripts/play.sh generate pedagogy

Updated: See rendered output.

New tests

scripts/run-tests.sh --test-arguments '--pattern "Pedagogical soundness"'

Note that the test for crash.yaml is currently failing because the Give command (and some others) are utilized in this tutorial without having been mentioned in the description or in earlier tutorials.

Additionally, the "bug" described in this comment should be caught by these tests (i.e. fail the tests) since the embedded solution code in the YAML file utilizes the give command. That is, if it currently weren't for this issue.

@kostmo kostmo changed the title [WIP] Dump a list of tutorials and commands they first introduce Dump a list of tutorials and commands they first introduce Mar 30, 2023
src/Swarm/Docs/Pedagogy.hs Outdated Show resolved Hide resolved
@kostmo kostmo requested a review from byorgey March 30, 2023 06:32
@kostmo
Copy link
Member Author

kostmo commented Mar 30, 2023

This isn't finished yet, but wanted to give a heads-up @byorgey on the work in progress, and I had one question.

src/Swarm/Docs/Util.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/Util.hs Outdated Show resolved Hide resolved
src/Swarm/Game/ScenarioInfo.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/DocGen.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/Pedagogy.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/Pedagogy.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/Pedagogy.hs Outdated Show resolved Hide resolved
src/Swarm/Docs/Pedagogy.hs Outdated Show resolved Hide resolved
test/unit/TestPedagogy.hs Outdated Show resolved Hide resolved
mergify bot pushed a commit that referenced this pull request Apr 1, 2023
Simplify #1186 by offloading some refactoring.

See [this comment](#1186 (comment)).
@kostmo kostmo force-pushed the tutorial-commands branch 2 times, most recently from a72b519 to 71444bc Compare April 1, 2023 20:36
@byorgey
Copy link
Member

byorgey commented Apr 1, 2023

@kostmo , apropos of nothing, I am wondering why you often force-push completely new commits to PRs instead of just pushing additional commits on top of the existing ones. In my experience it makes PRs somewhat harder to review, because (a) I cannot easily see what has been updated, e.g. when there are additional changes after I reviewed the initial PR, and (b) it is slightly annoying if I pulled the branch locally to test it; when I go to update it to test a later version of the PR I cannot just pull, I have to delete the local branch and re-pull the entire thing.

One good reason might be to make a nicer, more logical commit history; but since we squash PRs into a single commit when merging anyway, this doesn't make much difference. But there might be other benefits I am not thinking of.

@kostmo
Copy link
Member Author

kostmo commented Apr 2, 2023

why you often force-push completely new commits to PRs instead of just pushing additional commits on top of the existing ones

Thanks for bringing this up; I hadn't sufficiently considered the review difficulties. For what it's worth, have you tried the "Compare" button next to the "force-pushed" GitHub log entries?

There are a couple of situations where I might want to force push:

  1. A rebase, e.g. for Pedagogy separate refactoring #1194. In addition to the rebase itself requiring a force push, sometimes I have squashed the commits to make the rebase process simpler. However, then the output of the "Compare" button may conflate changes specific to the PR with the changes since made to the main branch and be less useful. It might then be helpful to have left commits un-squashed.
  2. While grouping related changes into a single commit, e.g. a specific bit of reviewer feedback, I may later notice an oversight that semantically belongs to that same commit. It might then make sense to amend the commit for the sake of the reviewer.

But in general, I will try to avoid gratuitously squashing after the point a reviewer has taken the first look at a PR.

Even though merging a PR will squash the commits, I sometimes like to preserve individual commits for historical interest that one can go back to the PR to view. I can wait to do that until reviewers are done.

Also, preserve SrcLoc just in case
@byorgey
Copy link
Member

byorgey commented Apr 2, 2023

For what it's worth, have you tried the "Compare" button next to the "force-pushed" GitHub log entries?

I... hadn't noticed that before! Thanks, that definitely helps.

There are a couple of situations where I might want to force push: ...

Yes, those all make sense.

Even though merging a PR will squash the commits, I sometimes like to preserve individual commits for historical interest that one can go back to the PR to view.

Agreed, I have sometimes gone back to look at individual commits in a PR, e.g. when tracking down the specific change that introduced a bug via git bisect.

Copy link
Member

@byorgey byorgey left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is looking good, I think. What do you still have in mind before it is ready?

data/scenarios/Tutorials/crash.yaml Show resolved Hide resolved
src/Swarm/Doc/Pedagogy.hs Show resolved Hide resolved
src/Swarm/Language/Syntax.hs Show resolved Hide resolved
@kostmo kostmo marked this pull request as ready for review April 2, 2023 19:16
@kostmo
Copy link
Member Author

kostmo commented Apr 2, 2023

This is looking good, I think. What do you still have in mind before it is ready?

I think it's ready for now, @byorgey. In the future maybe we could augment the output to measure "tutorial coverage" of all of the extant commands.

@byorgey
Copy link
Member

byorgey commented Apr 3, 2023

In the future maybe we could augment the output to measure "tutorial coverage" of all of the extant commands.

Perhaps, though (in my mind at least) the goal is not to cover all commands in the tutorial; some commands you should just learn about by playing the game --- crafting new devices, reading their descriptions, and so on.

@kostmo kostmo added the merge me Trigger the merge process of the Pull request. label Apr 3, 2023
@mergify mergify bot merged commit 65e3f2b into main Apr 3, 2023
8 checks passed
@mergify mergify bot deleted the tutorial-commands branch April 3, 2023 14:49
@kostmo kostmo added the T-Tutorial Involves the tutorial experience for new players. label Apr 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Trigger the merge process of the Pull request. T-Tutorial Involves the tutorial experience for new players.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants