Closed AdrienChampion closed 5 months ago
@AdrienChampion I've just removed Std
from lean-auto
's dependencies. It seems that enough definitions/theorems have been moved to leanprover/lean4
such that lean-auto
no longer needs to depend on Std
. So, the renaming part is no longer necessary.
It still makes sense to wait for the stable release.
@PratherConid See #27
I'm starting to use lean-auto, and noticed it does not require
std
'sstable
branch butmain
instead, which does not build as it's now in 4.8.0-rc1.I have a version of lean-auto that builds on 4.8.0-rc1 here. I don't think you'd want to merge it as is, but hopefully it can be useful as a blueprint for you.
The main things I had to accomodate are:
std
is nowbatteries
(and moved from leanprover to leanprover-community on github);simp
and other tactics behave slightly differently causing a few proofs to fail, solved by removing/adding minor things;theorem
-s now have to have typeProp
, causing some of your theorems to become (sometimesnoncomputable
)def
-s.I think that's most of it.
Also, it seems some definitions are still under the
Std
namespace such asStd.Queue
. So it might be a good idea to wait until 4.8.0 releases before updating, and probably requirestd
batteries
from its stable branch.