Tutorial Equations: well-founded recursion

CONTRIBUTING.md

@@ -13,6 +13,10 @@ There are different possible ways to contribute depending on your time and techn
 - There is technical work to be done on the (interactive) web interface side
 
 
+> [!TIP]
+> Before starting to work on something and invest time into it, check if it is not already existing,
+> or if someone hasn't already started working on it, either by creating a discussion on the [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) or a draft pull request about it.
+
 ### Writing Tutorials and How-tos
 If you have an idea for a tutorial or how-to, you can create a discussion on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs)
 to get feedback on your idea, through the writing and to reach others that may be interested.
@@ -23,10 +27,6 @@ Equation, you can create a discussion in the associated stream.
 Once you have a plan and some content, you can create a draft pull request to make your code accessible
 and get feedback on it while you (and others) progress on it.
 
-> [!WARNING]
-> Before starting to work on a tutorial or a how-to and invest time into it, check if it is not already existing,
-> or if someone hasn't already started working on it, either by creating a discussion on the [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs) or a draft pull request about it.
-
 > [!WARNING]
 > Lots of stuff have already be written about Coq, it can make sense to reuse some of the content.
 > If you wish to do so, be careful that you are indeed allowed by the copyright owners or the content licenses.
@@ -82,7 +82,7 @@ As examples, we have been working on new tutorials for the package Equations.
 The first one is complete and can be checked out [here](src/Tutorial_Equations_basics.v).
 
 
-### Horizontality
+### Writing Horizontal Tutorials
 
 Tutorials do not necessarily need to be long, nor should aim to present
 all the aspects of a feature in one unique tutorial.
@@ -104,8 +104,33 @@ Doing so only takes a bit more time when writing a tutorial but saves a lot of t
 that will not have to chase information in different other tutorials, tutorials which could in turn refer to other tutorials.
 It also eases maintenance as one does not need to worry about potential modifications to other tutorials.
 
+### Discussing Recurring Issues
+
+When writing a tutorial, it often happens to be confronted to something that
+does not work as easily as expected due to limitations of a feature or genuine bugs.
+In this case, often people decide not to mention the problem as they plan /
+it is planned to fix the problem.
+The issue is that most times, it turns out that it is actually not that easy to fix
+nor that fast, and meanwhile users are left with a solution.
+Worse, not only they are not told how to go around the problem,
+but they are not even warned that a problem may rise up.
+This can be particularly limiting for non expert users, that may not be able
+to identify the problem and manage to go around it on their own.
+
+This issue is particularly relevant in our case, as the documentation is aimed
+at the general public, and is indexed on the versions of Coq platform
+that do not change everyday.
+
+> [!NOTE]
+> Consequently, it is really important to mention in tutorials issues that
+> often come up with a feature, and to provide as reasonable solution as possible.
+> The tutorials can always be modified once the fix are effective, but meanwhile
+> users have solutions.
+
+
 ### Adding Exercises
-As tutorials are meant for studying, do not hesitate to add some exercises for the users to try, e.g. functions or properties to prove or finish.
+As tutorials are meant for studying, do not hesitate to add some exercises
+for the users to try, e.g. functions or properties to prove or finish.
 In general, we recommend to provide at least definitions prefilled with typing information like:
 
 ```
@@ -115,13 +140,11 @@ Lemma map_app {A B} (f : A -> B) (l l' : list A) : map f (l ++ l') = map f l + m
 Proof. Admitted.
 ```
 
-To do so, you can add the following code at the beginning of the tutorial.
-It creates an axiom `to_fill` and hides it so that it is does not appear in the body of the tutorial.
+To do so, you can add the following code at the beginning of the tutorial,
+that creates an axiom that can fill any goal.
 ```
-(* begin hide *)
 Axiom to_fill : forall A, A.
 Arguments to_fill {_}.
-(* end hide *)
 ```
 
 You can also provides tests for the users to be able to check if their definition works.

README.md

@@ -76,9 +76,14 @@ of tutorials and how-tos it could be interesting to have.
 This list is not fixed and will necessarily evolve through discussions with the community and experience,
 but it should already give an idea of the potential of this project.
 
-The project can already been discussed on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs).
 We will also soon submit a Coq Enhancement Proposal.
 
+> [!NOTE]
+> For more information about project and to participate in disccusions, please checkout on the dedicated [Zulip stream](https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs).
+> Among others, you can find there information about [new tutorials and how-tos](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/New.20Tutorials.20and.20How-to.20to.20check.20out), and a [wishlist](https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs/topic/Wishlist.20Tutorials) to tell us what you need
+
+
+
 
 
 ### How to contribute to the documentation
@@ -91,7 +96,8 @@ There are different possible ways to contribute depending on your time and techn
 - There is a lot of tutorials and how-tos to write, both about Coq and plugins in its Platform
 - There is technical work to be done on the (interactive) web interface side
 
-For more information on how to contribute, please check the [Contribution Guidelines](CONTRIBUTING.md).
+> [!IMPORTANT]
+> For more information on how to contribute, please check the [Contribution Guidelines](CONTRIBUTING.md).