search

leanprover-contrib / lean-build-action

3 stars 3 forks source link

lean4 support #1

Open Julian opened 3 years ago

Julian commented 3 years ago

It seems at least leanpkg test doesn't exist on lean4 (yet?), so running this on a lean4 repository just fails immediately.

I had no expectations it'd work, but perhaps a first way to fix things presuming that this repo would support both lean3 and lean4 (perhaps a poor assumption?) is to fallback to just running leanpkg build on lean4?

Julian commented 3 years ago

I put a branch which does that 1 word change, though whilst not maintaining the lean3 behavior here and yeah that at least passes my build