Creating an Idris Track

Exercism Building Exercism
21

@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.

1 Like
22

@iHiD I looked into:

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).

3 Likes
23

Thanks for looking at stuff!

There are generally three things that need community help to get a track live:

  1. 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).
  2. 20+ exercises.
  3. 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:

  1. 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 :slight_smile:)
  2. Add/update the docs to get them right.
  3. 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 :slight_smile:) Stick to one PR per exercise please.
  4. 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.
2 Likes
24

@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?

25

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)

1 Like
26

Tests can run in two different ways:

  1. Locally, which happens when people download exercises via the CLI
  2. 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.
1 Like
27

I’ve created the test runner repo: GitHub - exercism/idris-test-runner

3 Likes
28

@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?

1 Like
29

That is correct

1 Like
30

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.

1 Like
31

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

1 Like
32

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.

1 Like
33

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.

34

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.

35

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.

1 Like
36

It seems like the link to the PR is utterly broken, will find a better one when at a computer.

37
38

The workflow failure is hopefully fixed, thanks @BNAndras! It seems someone has to approve the workflow to re-run though. Thanks for all help. :slight_smile:

1 Like
39

I’ve hit approve on the workflow run :slight_smile:

1 Like
40

I very cleverly did not remove the --read-only flag yesterday. Now it is removed however and the workflow needs approval again. :blush:

1 Like