@iHiD I would be interested, but I need to look into the current state of the repo, the CI/CD infrastructure and so on. I also think the track need to be for Idris2 for me to be interested.
@iHiD I looked into:
- GitHub - exercism/idris: Exercism exercises in Idris.
- Building Tracks | Exercism's Docs
- GitHub - exercism/generic-track
- Workflow runs · exercism/idris · GitHub
Considering that I have never contributed to a track, only used Idris2 (in a Docker container), never used GitHub actions (and see failing workflow for main) and that I am unsure if it is possible to test the track through the web interface before it becomes active, makes me quite concerned. It would also be interesting to know what would be the minimum changes required after cloning the generic track to get something showing on the website (preferably in some kind of development mode).
Thanks for looking at stuff!
There are generally three things that need community help to get a track live:
- Create a test runner (a piece of software that runs a provided student solution against a test suite, and returns a JSON file of the results).
- 20+ exercises.
- Put together the basic docs (e.g. Pyret’s)
Things like GitHub actions can generally be solved by the Exercism community, and with the help of @ErikSchierboom .
My suggestion would be to:
- Look at the existing exercises (idris/exercises/practice at main · exercism/idris · GitHub) and put together a PR that updates them to be Idris2 (or tell us that they’re all ok
)
- Add/update the docs to get them right.
- Choose and start porting other exercises from problem-specifications. If you’re unsure what would be good, then I’d suggest looking at other new tracks (e.g. pyret) to see what they chose (although obviously different exercises might suit Idris better). The “Building Tracks” docs you linked to should help you with this, but if it’s not clear, let me know, and I’ll ask some of the community to weigh in with help (they’re very friendly
) Stick to one PR per exercise please.
- Wait until @ErikSchierboom is back off holiday, and he’ll create you a test-runner repository that you can use to get a working Idris test runner (he can help with this), which means the Idris track can then be used via the online editor.
@iHiD an initial investigation of the existing exercises shows that I need to replace the test library, which leads me to thinking about how the tests will run. Am I right that GitHub actions is involved and that docker images are involved and also that there is freedom to decide which base image?
The docker image (the idris-test-runner
repo) is what’s used to run the tests in production on the server. You can then also reuse that for GitHub actions if you want, or not - it depends what’s easiest.
You can choose whatever image you want for the idris-test-runner
- the main criteria is that it’s fast and the second one is that it’s lightweight (we pay per GB for storage, so there’s a real cost to the images)
Tests can run in two different ways:
- Locally, which happens when people download exercises via the CLI
- Online, via our online editor. This is powered by the aforementioned test runner. These are implemented as Docker images. See the docs for more information.
@ErikSchierboom am I right that the steps to a working test runner would be suitable updates to the Dockerfile and run.sh as well as provide “complete” solution trees in the subfolders to tests?
That is correct
This PR with initial tooling for the test runner seems to work with rudementary golden tests. However there is an issue when running in docker that the command to run a test wants to write to a subfolder to /root/.pack
, which contains the tooling for Idris. If the docker container is run with --read-only
, this leads to an issue which I am not sure how to handle.
Disclaimer: I am not a Docker user.
- Is the
.pack
data part of the setup? If so, should that be prepopulated in the image? - If it is test-run-related data, can you use a
--tmpfs
path for the test data?
See also The container's root filesystem should be set to read-only
I’m actually having a similar-sounding issue with the D track runner image needing to write to /root/.dub
at Bump DMD to 2.109.0 by BNAndras · Pull Request #66 · exercism/d-test-runner · GitHub. Erik mentioned looking at permissions and the user running the image so I was going to take a look at that this weekend.
The .pack folder contains the Idris2 tooling, some comes with the base image and the test library that is installed by the Dockerfile in the test runner repo. My guess is that the command that runs the test also locally installs the solution and feels a need to use a tmp folder under the .pack directory.
It seems like the exact same symptom. Thanks for the link. But if I understand it correctly, perhaps me ignoring the problem will work, if the --read-only flag is not passes in production.
We don’t currently use read-only
in production, but we may do in future. We’ll give warning if we do. Our aim is to have things ready for that time (ie they work with the flag) but it’s not a show-stopper.
It seems like the link to the PR is utterly broken, will find a better one when at a computer.
The workflow failure is hopefully fixed, thanks @BNAndras! It seems someone has to approve the workflow to re-run though. Thanks for all help.
I’ve hit approve on the workflow run
I very cleverly did not remove the --read-only
flag yesterday. Now it is removed however and the workflow needs approval again.