search

JamesGallicchio / LeanColls

WIP collections library for Lean 4
https://jamesgallicchio.github.io/LeanColls/docs/
Apache License 2.0
30 stars 7 forks source link

bump to leanprover/lean4:v4.7.0 #28

Closed digama0 closed 7 months ago

JamesGallicchio commented 7 months ago

did lake CLI change again? CI is failing because -Kdocs=on isn't getting lake to pull the doc-gen conditional dependency :frowning_face:

digama0 commented 7 months ago

try adding -R

JamesGallicchio commented 7 months ago

The CI already has -R. I think previously the manifest included doc-gen, and now doesn't, which is probably the issue.

I'll push the full manifest, but LMK if there is another recommended solution!

JamesGallicchio commented 7 months ago

that seems to have worked. merging!