update CONTRIBUTING.md, add doc for the generator

CONTRIBUTING.md

@@ -1,39 +1,57 @@
 # How to contribute to the Exercism Lean track
 
-#### **Do you want to add an exercise?**
+## Contributing
 
-- **Ensure that someone else isn't already adding it** by searching the [forum](https://forum.exercism.org/c/programming/lean) and the repository's [issues](https://github.com/exercism/lean/issues) and [pull requests](https://github.com/exercism/lean/pulls).
+We 💙 our community, but **this repository does not accept unsolicited pull requests at this time**.
 
-- If nobody is yet adding the exercise, [open a conversation](https://forum.exercism.org/c/programming/lean) and indicate you'd like to add the exercise.
+Please read this [community blog post][guidelines] for details.
 
-- Follow the [Add a Practice Exercise docs](https://exercism.org/docs/building/tracks/practice-exercises/add).
+### How to contribute
 
-#### **Do you want to report a bug?**
+1. Open a topic on the [Lean forum][lean-forum]
+2. Discuss the proposal with the maintainers
+3. After receiving the go-ahead, submit a pull request
 
-- **Ensure the bug was not already reported** by searching the [forum](https://forum.exercism.org/c/programming/lean).
+Pull requests must follow [Exercism's style guide][style].
 
-- If you're unable to find an open conversation addressing the problem, [open a new one](https://forum.exercism.org/new-topic?category=lean). Be sure to include a **title and clear description**, as much relevant information as possible, and (when possible) a **code sample**.
+Before submitting, please read:
 
-#### **Do you want to fix a bug?**
+- [Contributors Pull Request Guide][contributors-pr-guide]
+- [Pull Request Guide][pr-guide]
 
-- **Ensure that the bug is [reported](#do-you-want-to-report-a-bug)**.
-  Only start fixing the bug when there is agreement on whether (and how) it should be fixed.
+When opening a PR:
 
-- Fix the bug and [submit a Pull Request](https://exercism.org/docs/building/github/contributors-pull-request-guide) to this repository.
+- Clearly describe the problem and the solution
+- Link to the corresponding forum discussion
+- Add a link to the PR in that same discussion
 
-- Ensure the PR description clearly describes the problem and solution.
-  Include a link to the bug's corresponding forum conversation.
+If the PR touches an existing exercise, please also consider [this warning][unnecessary-test-runs].
 
-- Before submitting, please read the [Contributors Pull Request Guide](https://exercism.org/docs/building/github/contributors-pull-request-guide) and [Pull Request Guide](https://exercism.org/docs/community/being-a-good-community-member/pull-requests).
+### Adding an exercise
 
-#### **Do you intend to add a new feature or change an existing one?**
+Practice exercises should follow the [Add a Practice Exercise docs][add-exercise].
 
-- **Ensure that the feature or change is discussed on the [forum](https://forum.exercism.org/c/programming/lean).**
-  Only start adding the feature or change when there is agreement on whether (and how) it should be added or changed.
+All exercises must include a test generator located in:
 
-- Add the feature or change and [submit a Pull Request](https://exercism.org/docs/building/github/contributors-pull-request-guide) to this repository.
+```text
+generator/Generator/Generator
+```
 
-- Ensure the PR description clearly describes the problem and solution.
-  Include a link to the bug's corresponding forum conversation.
+The generator must:
 
-- Before submitting, please read the [Contributors Pull Request Guide](https://exercism.org/docs/building/github/contributors-pull-request-guide) and [Pull Request Guide](https://exercism.org/docs/community/being-a-good-community-member/pull-requests).
+- be imported by `generator/Generator/Generator.lean`
+- define the required generator functions
+- register them in the `dispatch` table
+
+The Lean track provides a generator script to help with this process.
+
+See the [generator documentation][generator-doc].
+
+[guidelines]: https://exercism.org/blog/contribution-guidelines-nov-2023
+[lean-forum]: https://forum.exercism.org/c/programming/lean/761
+[style]: https://exercism.org/docs/building/markdown/style-guide
+[contributors-pr-guide]: https://exercism.org/docs/building/github/contributors-pull-request-guide
+[pr-guide]: https://exercism.org/docs/community/being-a-good-community-member/pull-requests
+[unnecessary-test-runs]: https://exercism.org/docs/building/tracks#h-avoiding-triggering-unnecessary-test-runs
+[add-exercise]: https://exercism.org/docs/building/tracks/practice-exercises/add
+[generator-doc]: generators/GenerateTestFile.md

generators/GenerateTestFile.lean

@@ -5,6 +5,74 @@ import Generator
 open Lean
 open Std
 
+/-!
+# GenerateTestFile
+
+This script implements utilities for generating test files for exercises in the track.
+
+## Running the generator
+
+Run the generator from this folder using the following command:
+
+```lean
+lake exe generator [Options] <exercise-slug> [Extra-Parameters]
+```
+
+The following options are available:
+
+* `-s` or `--stub`       - Generates a stub test generator in `./generators/Generator/Generator/`
+* `-a` or `--add`        - Adds a practice exercise to `./exercises/practice` and generates a test file if a test generator exists.
+                           The author and the difficulty of the new exercise may be passed as extra parameters.
+* `-g` or `--generate`   - Generates a test file in `./exercises/practice/<exercise-slug>/`
+* `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data.
+                           This option does not take any parameters.
+
+`<exercise-slug>` is a required parameter for all options except `--regenerate`.
+The slug must be in kebab-case, for example: `two-fer`.
+
+## Test generators
+
+Generating test files requires a test generator in `./generators/Generator/Generator/`.
+
+This generator must be imported in `./generators/Generator/Generator.lean` and must define the following three functions:
+
+1. `introGenerator    : String → String`
+2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String`
+3. `endBodyGenerator  : String → String`
+
+These functions must also be added to the `dispatch` table in `./generators/Generator/Generator.lean`, using the exercise name in `PascalCase` as the key.
+For example:
+
+```lean
+def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
+  Std.HashMap.ofList [
+    ...
+    ("TwoFer", (TwoFerGenerator.genIntro, TwoFerGenerator.genTestCase, TwoFerGenerator.genEnd))
+    ...
+  ]
+```
+
+Running the generator with `-s` or `--stub` automatically creates a stub test generator in the correct folder.
+It also adds an import for it in `./generators/Generator/Generator.lean` and an entry for its functions in the `dispatch` table.
+
+## Importing files
+
+The test generator may `import Helper` in order to use helper functions defined in `./generators/Generator/Helper.lean`.
+
+Note that all generator files are built by Lean each time this script runs.
+Please keep dependencies to the minimum necessary.
+
+In particular, *do not* import the entire `Lean` package.
+
+## Adding test cases
+
+Practice exercises get their test cases from `https://github.com/exercism/problem-specifications/`.
+
+Additional test cases may be defined by the author in JSON format in an `extra.json` file in `exercises/practice/<exercise-slug>/.meta` folder.
+
+The `testCaseGenerator` function is called for each case from `problem-specifications` and for any extra cases.
+-/
+
 structure OrderedMap where
   order : Array String
   map : TreeMap.Raw String Json
@@ -189,21 +257,22 @@ def getIncludes (toml : String) : TreeMap String String :=
 
 def showUsage : IO Unit :=
   let usageMsg := s!"Usage is:
-    lake exe generator [Options] <exercise-slug> [Extra-Options]
+    lake exe generator [Options] <exercise-slug> [Extra-Parameters]
 
     Options:
       -s / --stub :
-        Generates a stub Generator for the exercise in ./generators/Generator/Generator/
-
-      -g / --generate :
-        Generates a test file for the exercise in ./exercises/practice/<exercise-slug>/
+        Generates a stub test generator for the exercise in `./generators/Generator/Generator/`
 
       -a / --add :
-        Adds a practice exercise and then generates a test file, if there is a Generator for it.
-        Other than the exercise slug, the author and the difficulty of the new exercise may be passed as extra options.
+        Adds a practice exercise to `./exercises/practice` and then generates a test file if a test generator exists.
+        The author and the difficulty of the new exercise may be passed as extra parameters.
+
+      -g / --generate :
+        Generates a test file for the exercise in `./exercises/practice/<exercise-slug>/`
 
       -r / --regenerate :
-        Regenerates all test files with a Generator, syncing all docs and test data with canonical-data."
+        Regenerates all test files with a test generator, syncing all docs and test data.
+        This option does not take any parameters."
   IO.println usageMsg
 
 def generateTestFile (exercise : String) : IO Unit := do

generators/GenerateTestFile.md

@@ -0,0 +1,65 @@
+# GenerateTestFile
+
+This script implements utilities for generating test files for exercises in the track.
+
+## Running the generator
+
+Run the generator from this folder using the following command:
+
+```lean
+lake exe generator [Options] <exercise-slug> [Extra-Parameters]
+```
+
+The following options are available:
+
+* `-s` or `--stub`       - Generates a stub test generator in `./generators/Generator/Generator/`
+* `-a` or `--add`        - Adds a practice exercise to `./exercises/practice` and generates a test file if a test generator exists.
+                           The author and the difficulty of the new exercise may be passed as extra parameters.
+* `-g` or `--generate`   - Generates a test file in `./exercises/practice/<exercise-slug>/`
+* `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data.
+                           This option does not take any parameters.
+
+`<exercise-slug>` is a required parameter for all options except `--regenerate`.
+The slug must be in kebab-case, for example: `two-fer`.
+
+## Test generators
+
+Generating test files requires a test generator in `./generators/Generator/Generator/`.
+
+This generator must be imported in `./generators/Generator/Generator.lean` and must define the following three functions:
+
+1. `introGenerator    : String → String`
+2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String`
+3. `endBodyGenerator  : String → String`
+
+These functions must also be added to the `dispatch` table in `./generators/Generator/Generator.lean`, using the exercise name in `PascalCase` as the key.
+For example:
+
+```lean
+def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
+  Std.HashMap.ofList [
+    ...
+    ("TwoFer", (TwoFerGenerator.genIntro, TwoFerGenerator.genTestCase, TwoFerGenerator.genEnd))
+    ...
+  ]
+```
+
+Running the generator with `-s` or `--stub` automatically creates a stub test generator in the correct folder.
+It also adds an import for it in `./generators/Generator/Generator.lean` and an entry for its functions in the `dispatch` table.
+
+## Importing files
+
+The test generator may `import Helper` in order to use helper functions defined in `./generators/Generator/Helper.lean`.
+
+Note that all generator files are built by Lean each time this script runs.
+Please keep dependencies to the minimum necessary.
+
+In particular, *do not* import the entire `Lean` package.
+
+## Adding test cases
+
+Practice exercises get their test cases from `https://github.com/exercism/problem-specifications/`.
+
+Additional test cases may be defined by the author in JSON format in an `extra.json` file in `exercises/practice/<exercise-slug>/.meta` folder.
+
+The `testCaseGenerator` function is called for each case from `problem-specifications` and for any extra cases.