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
Are we ready for a track and test runner repo?
I believe so!
I created an image on ghcr
tim@MacBook-Air-4 lean4 % docker run --rm -v "$(pwd)/exercises/practice/darts:/opt/test-runner" ghcr.io/tim-br/lean-docker:18e87e9 lake test
info: downloading https://releases.lean-lang.org/lean4/v4.25.2/lean-4.25.2-linux_aarch64.tar.zst
info: installing /usr/local/elan/toolchains/leanprover--lean4---v4.25.2
Darts
✓ Missed target
✓ On the outer circle
✓ On the middle circle
✓ On the inner circle
✓ Exactly on center
✓ Near the center
✓ Just within the inner circle
✓ Just outside the inner circle
✓ Just within the middle circle
✓ Just outside the middle circle
✓ Just within the outer circle
✓ Just outside the outer circle
✓ Asymmetric position between the inner and middle circles
Test Summary:
Total: 13
Passed: 13
ALL TESTS PASSED
But on each run lean downloads anew info: downloading https://releases.lean-lang.org/lean4/v4.25.2/lean-4.25.2-linux_aarch64.tar.zst
Even though the lean versions should match:
cat /Users/tim/lean/lean4/exercises/practice/darts/lean-toolchain
leanprover/lean4:v4.25.2
The docker repo is here:
EDIT:
Fixed it on latest! I have the docker image ready. However the image is massive and I’m not sure how to cut down the size. I got it down to less than 3gb from 3.5. The issue is the lean toolchain is massive. 3gb would put it at one of the largest Exercism test runner images.
docker run --rm -v "$(pwd)/exercises/practice/darts:/opt/test-runner" ghcr.io/tim-br/lean-docker:latest lake test
Darts
✓ Missed target
✓ On the outer circle
✓ On the middle circle
✓ On the inner circle
✓ Exactly on center
✓ Near the center
✓ Just within the inner circle
✓ Just outside the inner circle
✓ Just within the middle circle
✓ Just outside the middle circle
✓ Just within the outer circle
✓ Just outside the outer circle
✓ Asymmetric position between the inner and middle circles
Test Summary:
Total: 13
Passed: 13
ALL TESTS PASSED
I have upload a PR with small changes, and 3 PRs to add exercises. (I have implemented more exercises, but I’ll pause the exercise PRs, avoiding merge conflicts.)
Just to double check. Who will be the maintainers?
Exercism usernames:
tmtwd
keiraville
oxe-b
GitHub usernames:
tim-br
keiravillekode
oxe-i
The track and test runner repos have been created!
Have a pull request here Bootstrap lean by tim-br · Pull Request #4 · exercism/lean-test-runner · GitHub
and here bootstrapping lean by tim-br · Pull Request #3 · exercism/lean · GitHub
The test runner looks like it needs permissions or tokens to push the docker image.
I’ve done my part of enabling the images. Enable lean-test-runner for production by ErikSchierboom · Pull Request #139 · exercism/terraform · GitHub has been opened and requires @iHiD to do some work.
I’ve noticed that the image is very big though: 2.78GB I’d appreciate someone trying to make it (a. lot) smaller.
Does something also need to happen so maintainers can download exercises and solve them offline using
https://exercism.org/tracks/lean/exercises ?
@tmtwd mentioned not having access to the track using https://exercism.org/tracks/lean
They are listed as a maintainer on GitHub and their Exercism account also seems to be linked to GitHub, since there is some reputation for exercise contributions and reviewing here.
I’ve noticed that in both my profile and keiraville’s, there is a maintainer role that seems to be missing from tmtwd’s profile. I mean this icon here:
Perhaps some magic has to occur on your end (or maybe @iHiD’s end)?
namespace TwoFer
def twoFer (name : Option String) : String :=
"One for " ++ name.getOr "you" ++ ", one for me."
end TwoFer
passes locally but I get the following error message in the editor.
info: two-fer: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
✖ [2/12] Building TwoFer (5.9s)
trace: .> LEAN_PATH=/tmp/tmp.IIc8PwExBq/.lake/build/lib/lean /usr/local/elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /tmp/tmp.IIc8PwExBq/TwoFer.lean -o /tmp/tmp.IIc8PwExBq/.lake/build/lib/lean/TwoFer.olean -i /tmp/tmp.IIc8PwExBq/.lake/build/lib/lean/TwoFer.ilean -c /tmp/tmp.IIc8PwExBq/.lake/build/ir/TwoFer.c --setup /tmp/tmp.IIc8PwExBq/.lake/build/ir/TwoFer.setup.json --json
error: TwoFer.lean:4:16: Invalid field `getOr`: The environment does not contain `Option.getOr`
name
has type
Option String
error: Lean exited with code 1
✔ [4/12] Built LeanTest.Assertions (6.2s)
✔ [5/12] Built LeanTest.Test (825ms)
✔ [6/12] Built LeanTest.Assertions:c.o (1.3s)
✔ [7/12] Built LeanTest.Test:c.o (557ms)
✔ [8/12] Built LeanTest (356ms)
✔ [11/12] Built LeanTest:c.o (92ms)
Some required targets logged failures:
- TwoFer
error: build failed
I’m using Lake version 5.0.0-src+b86e2e5 (Lean version 4.25.2).
Thank you for your feedback! I believe the function is Option.getD. This idiom of using getD is common in different types (for example, this is the equivalent for Arrays). I couldn’t find a mention of Option.getOr in the reference, so maybe this was a typo?
Once we solve this issue with @tmtwd not having access to the track, we should request help from other maintainers to test it.
I performed the magic :)
Got in! Thanks