From 090ec130e7b58402dd05f11cf0ce57b15e162c1b Mon Sep 17 00:00:00 2001 From: oxe-i Date: Sun, 8 Mar 2026 15:01:39 -0300 Subject: [PATCH 1/2] update CONTRIBUTING.md, add doc for the generator --- CONTRIBUTING.md | 60 ++++++++++++++++--------- generators/GenerateTestFile.lean | 77 ++++++++++++++++++++++++++++---- generators/GenerateTestFile.md | 57 +++++++++++++++++++++++ 3 files changed, 165 insertions(+), 29 deletions(-) create mode 100644 generators/GenerateTestFile.md diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 0e0a9e0..6b0e159 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index 9b51b5a..e21f6bb 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -5,6 +5,66 @@ import Generator open Lean open Std +/-! +# GenerateTestFile + +This script implements utilities for generating test files for exercises in the track. + +## Running the generator + +The generator should be run from this folder using the following command: + +```lean +lake exe generator [Options] [Extra-Parameters] +``` + +The following options are available: + +* `-s` or `--stub` - Generates a stub test generator for the exercise in `./generators/Generator/Generator/` +* `-a` or `--add` - 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` or `--generate` - Generates a test file for the exercise in `./exercises/practice//` +* `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data. + This option does not take any parameters. + +The `` is a required parameter for every option except `--regenerate`. +This slug should be passed in kebab-case, for example: `two-fer`. + +## Test generators + +Generating test files requires a test generator in `./generators/Generator/Generator/`. + +This test generator must be imported by `./generators/Generator/Generator.lean` and must define at least three functions with the following type signatures: + +1. `introGenerator : String → String` +2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String` +3. `endBodyGenerator : String → String` + +These functions must 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 test generator files are built by Lean every time this script runs. +Please keep dependencies to the minimum necessary. + +In particular, *do not* import the entire `Lean` package. +-/ + structure OrderedMap where order : Array String map : TreeMap.Raw String Json @@ -189,21 +249,22 @@ def getIncludes (toml : String) : TreeMap String String := def showUsage : IO Unit := let usageMsg := s!"Usage is: - lake exe generator [Options] [Extra-Options] + lake exe generator [Options] [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// + 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//` -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 diff --git a/generators/GenerateTestFile.md b/generators/GenerateTestFile.md new file mode 100644 index 0000000..d7003b1 --- /dev/null +++ b/generators/GenerateTestFile.md @@ -0,0 +1,57 @@ +# GenerateTestFile + +This script implements utilities for generating test files for exercises in the track. + +## Running the generator + +The generator should be run from this folder using the following command: + +```lean +lake exe generator [Options] [Extra-Parameters] +``` + +The following options are available: + +* `-s` or `--stub` - Generates a stub test generator for the exercise in `./generators/Generator/Generator/` +* `-a` or `--add` - 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` or `--generate` - Generates a test file for the exercise in `./exercises/practice//` +* `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data. + This option does not take any parameters. + +The `` is a required parameter for every option except `--regenerate`. +This slug should be passed in kebab-case, for example: `two-fer`. + +## Test generators + +Generating test files requires a test generator in `./generators/Generator/Generator/`. + +This test generator must be imported by `./generators/Generator/Generator.lean` and must define at least three functions with the following type signatures: + +1. `introGenerator : String → String` +2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String` +3. `endBodyGenerator : String → String` + +These functions must 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 test generator files are built by Lean every time this script runs. +Please keep dependencies to the minimum necessary. + +In particular, *do not* import the entire `Lean` package. From d06c610c67e425bf4aec3a5ca84a33300f1d41eb Mon Sep 17 00:00:00 2001 From: oxe-i Date: Mon, 9 Mar 2026 05:55:41 -0300 Subject: [PATCH 2/2] improve style and add info about extra cases --- generators/GenerateTestFile.lean | 32 ++++++++++++++++++++------------ generators/GenerateTestFile.md | 32 ++++++++++++++++++++------------ 2 files changed, 40 insertions(+), 24 deletions(-) diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index e21f6bb..2a7afdd 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -12,7 +12,7 @@ This script implements utilities for generating test files for exercises in the ## Running the generator -The generator should be run from this folder using the following command: +Run the generator from this folder using the following command: ```lean lake exe generator [Options] [Extra-Parameters] @@ -20,27 +20,27 @@ lake exe generator [Options] [Extra-Parameters] The following options are available: -* `-s` or `--stub` - Generates a stub test generator for the exercise in `./generators/Generator/Generator/` -* `-a` or `--add` - 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` or `--generate` - Generates a test file for the exercise in `./exercises/practice//` +* `-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//` * `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data. This option does not take any parameters. -The `` is a required parameter for every option except `--regenerate`. -This slug should be passed in kebab-case, for example: `two-fer`. +`` 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 test generator must be imported by `./generators/Generator/Generator.lean` and must define at least three functions with the following type signatures: +This generator must be imported in `./generators/Generator/Generator.lean` and must define the following three functions: -1. `introGenerator : String → String` +1. `introGenerator : String → String` 2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String` -3. `endBodyGenerator : String → String` +3. `endBodyGenerator : String → String` -These functions must be added to the `dispatch` table in `./generators/Generator/Generator.lean`, using the exercise name in `PascalCase` as the key. +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 @@ -59,10 +59,18 @@ It also adds an import for it in `./generators/Generator/Generator.lean` and an The test generator may `import Helper` in order to use helper functions defined in `./generators/Generator/Helper.lean`. -Note that all test generator files are built by Lean every time this script runs. +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//.meta` folder. + +The `testCaseGenerator` function is called for each case from `problem-specifications` and for any extra cases. -/ structure OrderedMap where diff --git a/generators/GenerateTestFile.md b/generators/GenerateTestFile.md index d7003b1..0aa914f 100644 --- a/generators/GenerateTestFile.md +++ b/generators/GenerateTestFile.md @@ -4,7 +4,7 @@ This script implements utilities for generating test files for exercises in the ## Running the generator -The generator should be run from this folder using the following command: +Run the generator from this folder using the following command: ```lean lake exe generator [Options] [Extra-Parameters] @@ -12,27 +12,27 @@ lake exe generator [Options] [Extra-Parameters] The following options are available: -* `-s` or `--stub` - Generates a stub test generator for the exercise in `./generators/Generator/Generator/` -* `-a` or `--add` - 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` or `--generate` - Generates a test file for the exercise in `./exercises/practice//` +* `-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//` * `-r` or `--regenerate` - Regenerates all test files with a test generator, syncing all docs and test data. This option does not take any parameters. -The `` is a required parameter for every option except `--regenerate`. -This slug should be passed in kebab-case, for example: `two-fer`. +`` 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 test generator must be imported by `./generators/Generator/Generator.lean` and must define at least three functions with the following type signatures: +This generator must be imported in `./generators/Generator/Generator.lean` and must define the following three functions: -1. `introGenerator : String → String` +1. `introGenerator : String → String` 2. `testCaseGenerator : String → Std.TreeMap.Raw String Lean.Json → String` -3. `endBodyGenerator : String → String` +3. `endBodyGenerator : String → String` -These functions must be added to the `dispatch` table in `./generators/Generator/Generator.lean`, using the exercise name in `PascalCase` as the key. +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 @@ -51,7 +51,15 @@ It also adds an import for it in `./generators/Generator/Generator.lean` and an The test generator may `import Helper` in order to use helper functions defined in `./generators/Generator/Helper.lean`. -Note that all test generator files are built by Lean every time this script runs. +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//.meta` folder. + +The `testCaseGenerator` function is called for each case from `problem-specifications` and for any extra cases.