Test pack and lsp during CI #3067
Conversation
Seems like this is an independent check, which should be processed as such. (Hopefully I got the CI incantations right...)
Hopefully this solves the artifact issue?
DRY. But sometimes, it really is the easiest way to get things done (and it should be fine(TM)...)
Now that the setup-jobs have been copied over, this dependency should be unnecessary.
Should hopefully avoid interference with the Idris2 CI.
These are relied upon by many developers, so it seems only sensible to test that nothing in the current PR breaks these. If nothing else as a foreshadowing for the maintainers of them.
We need pack to check out the PR's ref somehow. Using `GITHUB_REPOSITORY` as the URL might work?
This might be the way? (I really don't want to have to fork pack...)
That might help...
It's probably fiiine...
I feel like this is so close to working, and yet so far...
Finally installed pack locally and tested it as well. So quite a bit more confident that this works (although you never know, CI could just throw us for a spin for the fun of it)...
Gods forbid we use a `.yaml` file instead of `.yml` -_-
This is going to be exciting!
We trust LSP, at least for CI-purposes
gallais
added
the
event: IDM 2023/08
As per discussion on PR idris-lang#3067
The job builds Idris2, but also several external libraries. Name accordingly.
| echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml | ||
| echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml | ||
| echo "bootstrap = true" >> pack.toml | ||
| - name: Build idris2-pack |
There was a problem hiding this comment.
I think, after setting pack.toml, one needs to call pack fetch to make sure pack has fetched the correct commit of the branch mentioned in latest:
There was a problem hiding this comment.
The local testing I did with this seemed to correctly get the commit, but I'll @stefan-hoeck just to be sure; afaiu, pack install pack is clever enough to fetch the latest/specified Idris2-commit before rebuilding and reinstalling itself : )
There was a problem hiding this comment.
My knowledge would be that in this case the latest commit at the moment of creation of the docker image would be used instead (without calling pack fetch, as I suggest), but right, let's wait for Stefan's answer
There was a problem hiding this comment.
Did some testing using the docker image rather than my local pack install; it seems pack fetch is indeed redundant:
Before, i.e. having just launched a fresh copy of the image:
# idris2 --version
Idris 2, version 0.6.0-72270962f
After creating a matching pack.toml and running pack install pack:
# idris2 --version
Idris 2, version 0.6.0-2a96c36fd
Which matches the latest commit on this branch : )
There was a problem hiding this comment.
git fetch is needed when there were some commits into the main branch between the docker image creation and running the CI. Since there were no commits into main recently, you cannot reproduce this situation
According to the linter this is better(?)
The extra CI jobs introduced in idris-lang#3067 work fine as long as 'main' is not the checked out branch. This is due to the fetch to a new branch, which git does (reasonably) not allow when you're trying to fetch 'main' into a new branch that's also called 'main'. In this case, we should just `git pull origin main`, which is what the script now (hopefully) does.
The extra CI jobs introduced in #3067 work fine as long as 'main' is not the checked out branch. This is due to the fetch to a new branch, which git does (reasonably) not allow when you're trying to fetch 'main' into a new branch that's also called 'main'. In this case, we should just `git pull origin main`, which is what the script now (hopefully) does.
Description
Occasionally, changes to
mainhave broken pack and/or the LSP. Given that these are by now widely used, and fairly critical, pieces of machinery, it seems appropriate to include them in the CI we already run.This PR also separates out the external library tests (frex, collie, katla, pack, and lsp) from the Ubuntu self-hosting test.
Should this change go in the CHANGELOG?
Nah.