Does this mean that it is safe/suitable to enable it, or should something else happen first. What will happen when it gets enabled? Will that make the track show up on the exercism website?
It’s safe to enable the test runner in the track config. This will allow maintainers to use the online editor when testing the track at https://exercism.org/tracks/idris/
The track will only show up for regular (non-maintainer) users once the active field is set to true in the track config.
1 Like
Thanks to @keiraville there are 20 exercises on the Idris track. I will try to make the documentation less wrong during this week.
2 Likes
I am trying out the idris track using exercism cli and have found some things I am not clear on how to fix. Some pointers would be greatly appreaciated:
exercism test → Error: the "idris" track does not yet support running tests using the Exercism CLI.
It is also interesting that "test_runner": false in config.json does not seem to have any effect. The documentation suggests that this has to do with running submitted solutions and letting students run tests when using the online editor. Both of these seems to work even when the value is set to false.
|It seems there isn’t a config for Idris at cli/workspace/test_configurations.go at main · exercism/cli (github.com).
I think that is expected.
1 Like
test_runner is set to true in the config. Enable test runner (#144) · exercism/idris@4f9b9be · GitHub
I’m not sure what you mean.
That is correct. We’ve only recently added instructions to the new track docs mentioning this: Exercism CLI | Exercism's Docs
1 Like
My bad, I hadn’t synced between repos properly. test_runner seems to do its job. 
1 Like
Add idris test configuration by isberg · Pull Request #1152 · exercism/cli · GitHub I will fix the formatting issue later today… and now it has been fixed. 
2 Likes
PR for test runner as well as CLI waiting for review.
The following documentation files need to be rewritten, now that the track uses Idris 2.
docs/INSTALLATION.md
docs/TESTS.md
exercises/shared/.docs/help.md
exercises/shared/.docs/tests.md
1 Like
The documentation has been updated, and we have a good range of exercises. @isberg - after an update to pack, the test runner and CLI, we should be ready to launch.
4 Likes
Exciting! Thanks @keiraville for picking up the slack! As far as I understand it seems ready to go. Can’t wait to send a few colleagues to try once it is live. 
3 Likes
We now have 77 languages.
2 Likes
Hi, I have a suggestion for the Idris track. I found out that the Exercism environment does not allow for access to linear collections such as Data.Linear.Array that enable mutable level efficiency, a huge selling point actually of Idris, relevant to some of the problems that naturally do dynamic programming using mutating a table. I suggest adding “contrib” to enable such access. What do people think? It would require changing both the exercism/idris and exercism/idris-test-runner:
idris-test-runner: add
RUN pack install contrib
idris: add to the ipkg generation
depends = contrib
I realize that there is a general Exercism goal of minimizing the Docker image, but showcasing Idris linear types seems an important thing to do.
Lots of thanks for your interest.
What is the size of the Docker image, before and after the change?
Is is possible to lock to a specific version of contrib? For example, the test runner currently has
ghcr.io/stefan-hoeck/idris2-pack:nightly-250523-jammy
and in GitHub workflows we Pin actions to SHAs
If not, would it feasible to make more use of linear types (the language feature) without contrib ?
How large is “contrib”? Can existing exercises easily be done without it? Racket is in a similar situation where the full distribution would definitely make sense but the minimal one is sufficient for the existing concept exercises.
Also this might be more appropriately done for concept exercises if/when Idris gets a syllabus. A practice exercise by design can be solved multiple ways so we could include “contrib”, but a student isn’t necessarily going to use the package. In a concept exercise, we can structure the exercise to use a particular approach so then you could highlight linear types there.