search

logsem / iris-tutorial

MIT License
25 stars 13 forks source link

Some exercises aren't actually exercises due syntax issues #4

Open meithecatte opened 2 days ago

meithecatte commented 2 days ago

See for example:

https://github.com/logsem/iris-tutorial/blob/5bfe72bdc84f807919cc24e891c9a4a0fe853f86/exercises/resource_algebra.v#L326-L330

I count four occurrences across resource_algebra.v, and no further results from a grep across exercises/.

Not sure if it makes sense to set up some kind of linting for this. I'm not sure how easy it is to define custom Vernacular aliases, but having a Solution := Proof alias used to mark the exercises would prevent this whole category of "typo silently kills exercise".

simongregersen commented 17 hours ago

Thanks for creating the issue @meithecatte!

If you'd be okay with submitting a pull request with your changes, that would be much appreciated! Just fixing the typos would be great, but I agree some kind of linting rule would be the ideal in the future.