Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Test pack and lsp during CI #3067

Merged
merged 22 commits into from
Sep 13, 2023
+99 −8
Merged

Test pack and lsp during CI #3067

Changes from 20 commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
9515c12
[ ci ] Move external libs outside of Idris2 job
CodingCellist Aug 28, 2023
f9873b7
[ ci ] Run extern-libs after Idris2
CodingCellist Aug 28, 2023
cde9fe5
[ ci ] Copy setup-jobs from ci-idris2 to extern-libs
CodingCellist Aug 28, 2023
8ec3d40
[ ci ] rm the ci-idris2 dependency from extern-libs
CodingCellist Aug 28, 2023
63ab414
[ ci ] All extern libs depend on self-host
CodingCellist Aug 28, 2023
6f54787
[ ci ] Add extern libs concurrency group
CodingCellist Aug 29, 2023
4c27d3c
[ ci ] Build pack and the LSP as part of ext-libs
CodingCellist Aug 29, 2023
814ecb4
[ ci ] Fix pack URL? RM lsp test for now
CodingCellist Aug 30, 2023
cd6226c
[ ci ] Add GH_REF_NAME to pack idris2.commit
CodingCellist Aug 30, 2023
6909bec
[ ci ] Fetch the PR before attempting pack install
CodingCellist Aug 30, 2023
af4bd1b
[ ci ] Mark CWD as safe for git-fetch reasons
CodingCellist Aug 30, 2023
ddf9d1f
[ ci ] Restore the REF to the commit pack param
CodingCellist Aug 30, 2023
d39a52b
[ ci ] Use 'latest' syntax to fix things
CodingCellist Aug 31, 2023
01f83c4
[ ci ] Make linter happy
CodingCellist Sep 1, 2023
f9f3eab
[ ci ] Enable the pack-lsp test
CodingCellist Sep 1, 2023
526847d
[ ci ] Don't prompt before building lsp
CodingCellist Sep 1, 2023
d739f3e
[ admin ] Merge branch 'main' into ci-pack-lsp
CodingCellist Sep 1, 2023
1f97374
[ ci ] Avoid work duplication in idris2 vs ext-libs
CodingCellist Sep 8, 2023
4d27adc
[ ci ] Rename idris2 CI job to reflect lib building
CodingCellist Sep 8, 2023
e827708
[ admin ] Merge branch 'main' into ci-pack-lsp
CodingCellist Sep 8, 2023
8364769
[ ci ] Depend on 'initialise' to make linter happy
CodingCellist Sep 11, 2023
2a96c36
[ ci ] Group pack toml file-writing commands
CodingCellist Sep 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 100 additions & 11 deletions .github/workflows/ci-idris2.yml → .github/workflows/ci-idris2-and-libs.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
name: Idris2
name: Idris2 and External Libs

on:
push:
Expand Down Expand Up @@ -487,14 +487,19 @@ jobs:
shell: bash

######################################################################
# Ubuntu testing some libraries.
# Testing some libraries on Ubuntu and pack.
#
# We are particularly interested in libraries that are heavily using
# dependent types, that are prone to find bugs and regressions in the
# compiler.
######################################################################

ubuntu-test-collie:
needs: [initialise, ubuntu-self-host-previous-version]
######################################################################
# Test that we can build Collie
######################################################################

ub-test-collie:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
Expand All @@ -521,8 +526,12 @@ jobs:
run: |
make

ubuntu-test-frex:
needs: [initialise, ubuntu-self-host-previous-version]
########################################################################
# Test that we can build Frex
########################################################################

ub-test-frex:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
Expand Down Expand Up @@ -550,8 +559,14 @@ jobs:
make
make test

ubuntu-test-elab:
needs: [initialise, ubuntu-self-host-previous-version]
######################################################################
# Test that we can build Stefan Höck's elab-util and pack
######################################################################

# ELAB-UTIL

ub-test-elab-util:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
Expand All @@ -578,12 +593,86 @@ jobs:
run: |
make all

# PACK
#
# N.B. instead of bootstrapping pack, we use the dockerimage where it is
# already, and then use pack to rebuild pack with this job's idris2 sources

ub-pack-test-pack:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
|| contains(needs.initialise.outputs.commit_message, '[ci: libs]')
env:
IDRIS2_CG: chez
PACK_DIR: /root/.pack
strategy:
fail-fast: false
# N.B.:
container: ghcr.io/stefan-hoeck/idris2-pack:latest
steps:
- name: Checkout
uses: actions/checkout@v3
with:
repository: 'stefan-hoeck/idris2-pack'
# by default, pack uses the main idris2 head, not the current job's one
- name: Toml setup
run: |
echo "[idris2]" > pack.toml
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
run: |
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

git config --global --add safe.directory "${PWD}"
git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
pack install pack

######################################################################
# Test that we can build the LSP
######################################################################

ub-pack-test-lsp:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
|| contains(needs.initialise.outputs.commit_message, '[ci: libs]')
env:
IDRIS2_CG: chez
PACK_DIR: /root/.pack
# LSP is vastly easier to build using pack, so do that
container: ghcr.io/stefan-hoeck/idris2-pack:latest
strategy:
fail-fast: false
steps:
- name: Checkout
uses: actions/checkout@v3
with:
repository: 'idris-community/idris2-lsp'
- name: Toml setup
run: |
echo "[idris2]" > pack.toml
echo "url = \"https://github.com/${GITHUB_REPOSITORY}\"" >> pack.toml
echo "commit = \"latest:${GITHUB_REF_NAME}\"" >> pack.toml
echo "bootstrap = true" >> pack.toml
# make sure pack is running the PR's Idris2 before building LSP
- name: Build pack with PR-Idris
run: |
git config --global --add safe.directory "${PWD}"
git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
pack install pack
- name: Build+install idris2-lsp
run: |
pack --no-prompt install-app idris2-lsp

######################################################################
# Ubuntu using katla to build html doc of the libs
# Test that we can use Katla to build html doc of the libs
######################################################################

ubuntu-katla:
needs: [initialise, ubuntu-test-collie]
ub-test-katla-and-html:
needs: ubuntu-self-host-previous-version
runs-on: ubuntu-latest
if: |
!contains(needs.initialise.outputs.commit_message, '[ci:')
Expand Down
Loading