feat(blueprint.yml): run shake in CI

[grunweg]

@pitmonticone I'm interested if you have any comments here. (No worries, this is not urgent.)

[grunweg]

This doesn't work yet: the workflow step needs to install lake first.

[kbuzzard]

Yeah I've been running shake manually every week or two -- this would be welcome, if you can figure out how to make it work! At my end it is also not urgent :-)

[azide0x37]

claim 😉

https://github.com/azide0x37/FLT/pull/1/files

with.run doesn't use the shell, invoking specifically works.

Could also add step ahead of lake invocations:

- name: Make lake available on PATH
  run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

Which allows lake syntax below when using env:

- name: check for unused imports
  id: shake
  uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845
  env:
    LEAN_ABORT_ON_PANIC: "1"
  with:
    linters: gcc
    run: lake exe shake --gh-style