Hi everyone,
I’m interested in volunteering to create a Lean 4 track (https://lean-lang.org/). I’ve built a testing framework for Lean 4 that could be adapted for Exercism’s test runner.
I’m learning and it could be a fun project.
Is there existing interest or effort towards this?
Thanks!
I would also be happy to contribute towards a Lean 4 track.
I’m unable to help for a few months, but this is the next language I intend to learn. If you need help with, say, adding exercises, I’ll be around by May or June.
Generally, I think we ask for a Hello, World! exercise and test suite as well.
I have a hello world example here.
If a copy of the test framework was included with each exercise, like in the Standard ML and ARM64 Assembly tracks, perhaps
lake update
lake build
./.lake/build/bin/HelloWorldTest
could be reduced to
lake test
(The ARM64 Assembly track uses CI / pre-commit to verify the test framework is consistent across exercises.)
Updated to include a copy of the test framework. Now it is simplified to lake test.
Have you looked at how various tracks generates their tests? Any preferences?
For examples:
Is the language Lean or Lean 4? It seems Lean 4 wasn’t backwards compatible with Lean 3, but what happens if there’s a Lean 5? Will the track need to update its slug? That might cause some work on the backend so I think perhaps the slug should just be lean without a version number.
good idea.
Regarding test generation, I’ll point out it’s not strictly necessary for launching a track. You need a test runner Docker image for the Exercism infrastructure end of story, but the other tooling is all optional but beneficial.
If you do decide to generate your tests, it’s generally better to work on your approach sooner rather than later so you don’t have to redo as much work on the test suites that may have already been added. If you decide to do that, I think it’s simpler to do it in the same language if practical because that means other contributors don’t also need to know languages X or Y to troubleshoot. However, that’s not always an option, but Python tends to be a fairly safe bet as a backup. Whatever works for you though.
Given test generation is purely optional, I don’t use it on the handful of the tracks I maintain. Vim Script is the exception where I inherited a very nice setup that works consistently well with very minor tweaks. Otherwise, that’s a whole other system I have to manage on top of the track repo to get stuff done.
I added the darts exercise.
And I used the assembly tracks approach to ensure the test package is the same across all exercises.
Seems to be working well so far.
The quickest way to implement a test runner from the generic repo would be to start with the leanprovercommunity/lean4 image, but that is 720MB. If we can achieve something smaller, that saves Exercism money every month. (Many of the smaller test runner images use Alpine Linux, but I don’t know if that is feasible here.)
Good point… but wouldn’t any custom image also require lean. Making it just as big?
Definitely interested in saving costs of course.
EDIT: I think the pragmatic approach would be start with official image , validate it works and then optimize once the track is launched.
Not necessarily. If the official imagine is built on, say, the Ubuntu base OS, it may have a lot of stuff that isn’t actually needed.
Yup I see there are slim images for custom builds.
Alpine might be tricky but maybe slim Ubuntu would cut down the build size significantly.
I think the docker image might be unmaintained leanprovercommunity/lean - Docker Image
Best might might be to build out own images with debian:slim not sure if lean is alpine compatible.
Probably work on this tomorrow.
Make sure you have linked your Exercism and GitHub accounts in Integrations, so tim-br GitHub contributions to https://github.com/exercism/ repos will show up in your Contributions