Skip to content

Commit

Permalink
feat: build ITree in CI (#47)
Browse files Browse the repository at this point in the history
Thus ensuring we don't break ITree when making changes to the framework.

In the process, we've cleaned up the CI workflows, by running lake exe cache get only once, in its own step.
  • Loading branch information
alexkeizer authored Oct 11, 2024
1 parent 68a7dc4 commit fc4fe05
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 8 deletions.
18 changes: 10 additions & 8 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,14 @@ jobs:
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Compile Library 🧐
run: |
lake -R exe cache get
lake -R build
- name: Fetch cached dependencies 🕑
run : lake -R exe cache get

- name: Compile Tests
run: |
lake -R exe cache get
lake -R build +Test
- name: Compile QpfTypes library 🧐
run: lake -R build

- name: Compile tests 🧐
run: lake -R build +Test

- name: Compile ITree library 🧐
run: lake -R build +ITree
1 change: 1 addition & 0 deletions ITree.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
import ITree.Basic

0 comments on commit fc4fe05

Please sign in to comment.