TEST: Gather feedback on level 1

[lnay]

Test the level on target undergraduates on Thursday session, work feedback into plan of action.

[grhkm21]

Fun! Nice to see harder and less trivial problems in games. A tip like "try to prove it on paper first" might help?

[lnay]

@grhkm21 nice to see some interest! We're still learning/deciding how to design levels. I've touched on something related in issue #4. I'm currently on the side of injecting specific theorems to use in rewrites and push the users down one of a few very specific path with many hints. At least for the "unavoidable" worlds/levels. Still open to thoughts.

On another note, if you are interested in being involved in this project, keep a look out on this repo. I'm hoping that we can organise a plan and specify a list of well defined tasks at some point in the future to make it feasible to handle external contributions. I see this happening after we fully understand how to design a good game level.

[codrutiftode]

I tried the game on Thursday's session, I think allowing "nth_rw" would be quite useful, as well as maybe "calc" (to allow those who don't know how to extend linarith with a hypothesis).

Other than that, it looks really promising and cool! Great work people :))

[grhkm21]

I think repeat would be useful too. Also, a hint for sub_sub_sub_comm would be nice, or just replace it with more intuitive ones? (I don't have a strong opinion.) Since from experience, it seems not many people look at right panel :joy: Here's my proofs for level 1 btw:

constructor
/- part 1 -/
intro h x y
specialize h x y 0
rw [sub_zero, sub_zero] at h
linarith
/- part 2 -/
intro h x y z
specialize h (x - z) (y - z)
rw [sub_sub_sub_comm, sub_self, sub_zero] at h
linarith

[lnay]

The game incorrectly says "intermediate goal solved", when in reality we just used the dot to concentrate on the first goal.

Indentation in the webapp is not visually clear to the user with the lines so far apart (unlike in a text editor), so there's little use to having dots in the model solutions.

It's also very hard to trigger the hints, I'm trying to work out how to make the hints trigger.

[lnay]

Actually the hints do trigger reliably, I forgot to rebuild the game. The hints seem to trigger when the state of the proof reaches a certain stage, not if the user writes exactly the same lines as the model solution (no need to choose same names for instance). The source can also use the dot to concentrate on the current goal without any drawbacks to the usability of the game.