add .gitpod.yml #42
add .gitpod.yml #42
Conversation
.gitpod.yml
Outdated
| - jroesch.lean | ||
|
|
||
| tasks: | ||
| - command: . /home/gitpod/.profile && scripts/get-cache.sh |
There was a problem hiding this comment.
This is a lean-liquid script, isn't it?
There was a problem hiding this comment.
aah, that's a good point, I guess. I'll copy it over for now.
There was a problem hiding this comment.
Actually, I removed the call to that script. I don't think we have olean caches for the tutorials project, and maybe we don't need them either.
|
Do you want to add a link/banner/whatever to the readme so it's easier to find? Otherwise looks good, we can test it live. |
|
Good idea. Done. |
.gitpod.yml
Outdated
| - jroesch.lean | ||
|
|
||
| tasks: | ||
| - command: . /home/gitpod/.profile |
There was a problem hiding this comment.
Shouldn't this have a leanpkg configure and leanpkg get-mathlib-cache? (Or maybe just one of them)
There was a problem hiding this comment.
I don't know! I have no idea how gitpod works.
There was a problem hiding this comment.
Ah, yeah. The call to the script you deleted would have done this in lean-liquid. https://github.com/leanprover-community/lean-liquid/blob/master/scripts/get-cache.sh
You need at least leanproject get-mathlib-cache. I don't know what directory this runs in, you might need the cd too.
|
As I clearly have no idea what I'm doing, I would love to hand this over to someone who has experience with setting up repos for gitpod. |
Please make sure you modified the files in
src/solutionsand used themk_exercises.pyscript to recreate the files insrc/exercises. Otherwise your modifications will soon be automatically overwritten.