Skip to content

Adjust docs #164

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
oxe-i merged 3 commits into from
Mar 26, 2026
Merged

Adjust docs #164

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
605b511
adjust usage of generator script, adjust CONTRIBUTING.md
Mar 26, 2026
1710b08
correct generator doc title
Mar 26, 2026
28dbc39
add reference to bin/sort-exercises in CONTRIBUTING.md
Mar 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Please read this [community blog post][guidelines] for details.
2. Discuss the proposal with the maintainers
3. After receiving the go-ahead, submit a pull request

Pull requests are automatically closed and will **remain closed until approved by a maintainer**.

Pull requests must follow [Exercism's style guide][style].

Before submitting, please read:
Expand All @@ -27,9 +29,17 @@ When opening a PR:

If the PR touches an existing exercise, please also consider [this warning][unnecessary-test-runs].

### Using LLMs

Exercism is both an educational platform and an open-source project.
As such, open issues in this track are not only about solving problems or adding content, but also about _involving the community_ and _providing opportunities for students to learn_.

Although the use of LLMs is not forbidden, they should be treated as an **auxiliary educational tool**.
Pull requests with reduced code quality or that fail to conform to our guidelines may be closed.

### Adding an exercise

Practice exercises should follow the [Add a Practice Exercise docs][add-exercise].
Practice exercises must follow the [Add a Practice Exercise docs][add-exercise].

All exercises must include a test generator located in:

Expand All @@ -44,9 +54,12 @@ The generator must:
- register them in the `dispatch` table

The Lean track provides a generator script to help with this process.

See the [generator documentation][generator-doc].

**The test file must be generated from its test generator using the generator script.**

After adding an exercise, run the `bin/sort-exercises` script to ensure the correct order in `config.json`.

[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
Expand Down
0 bin/reorder-exercises → bin/sort-exercises
View file
Open in desktop
File renamed without changes.
8 changes: 4 additions & 4 deletions generators/GenerateTestFile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ This script implements utilities for generating test files for exercises in the

## Running the generator

Run the generator from this folder using the following command:
Run the generator from the root folder using the following command:

```lean
lake exe generator [Options] <exercise-slug> [Extra-Parameters]
bin/run-generator [Options] <exercise-slug> [Extra-Parameters]
```

The following options are available:
Expand All @@ -34,7 +34,7 @@ The slug must be in kebab-case, for example: `two-fer`.

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:
This test 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`
Expand Down Expand Up @@ -257,7 +257,7 @@ def getIncludes (toml : String) : TreeMap String String :=

def showUsage : IO Unit :=
let usageMsg := s!"Usage is:
lake exe generator [Options] <exercise-slug> [Extra-Parameters]
bin/run-generator [Options] <exercise-slug> [Extra-Parameters]

Options:
-s / --stub :
Expand Down
6 changes: 3 additions & 3 deletions generators/GenerateTestFile.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ This script implements utilities for generating test files for exercises in the

## Running the generator

Run the generator from this folder using the following command:
Run the generator from the root folder using the following command:

```lean
lake exe generator [Options] <exercise-slug> [Extra-Parameters]
bin/run-generator [Options] <exercise-slug> [Extra-Parameters]
```

The following options are available:
Expand All @@ -26,7 +26,7 @@ The slug must be in kebab-case, for example: `two-fer`.

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:
This test 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`
Expand Down
Loading