search

coq / platform-docs

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.
https://coq.inria.fr/platform-docs/
Other
19 stars 11 forks source link

Adding a Search tutorial #11

Closed Villetaneuse closed 5 months ago

Villetaneuse commented 5 months ago

There are no exercises yet, but this can be for a later version.

thomas-lamiaux commented 5 months ago

There are no exercises yet, but this can be for a later version.

Exercises can definitely be added in future version. Though, if there is no particular rush to merge the PR, I suggest adding a few exercises to section 1 before merging. Exercises for section 2 seems more optional to me as it is a section about more advanced features.

Villetaneuse commented 5 months ago

I've taken into account your most easy criticisms. I will get back to it tomorrow, if I have some time, to include your other remarks and @MSoegtropIMC's remark about scopes.

Villetaneuse commented 5 months ago

Here is my latest iteration. I have added exercises and a discussion about scopes. It's not totally finished.

Villetaneuse commented 5 months ago

Again an iteration, where I have taken most of your remarks into account except:

However, I think we should move on. There can be modifications later and more following users' feedbacks.

thomas-lamiaux commented 5 months ago

Ok, that sounds good enough, but we should be careful not to forget and never come back to it.

Zimmi48 commented 5 months ago

If you want to, you can open issues to track things that need to be taken care of in the future.

Villetaneuse commented 5 months ago

To make my previous thoughts clearer: I am very grateful for your many remarks, but, from my experience, working on pedagogical content is literally infinite. We can always make a new version which is better by an epsilon margin. At some point, though, one needs to fix a "good enough" limit (I would rate my own limit as already pretty high). Does this tutorial effectively teaches how to use Search? I'd say probably. Most of its defects cannot be foretold at this point and will be revealed by users anyway.

thomas-lamiaux commented 5 months ago

I agree and I think it is a good point. Though, we should be careful to stuffs like sum up and toc as it what users are going to see first and checkout to decide if they will read the tutorial or not