Lean error

[arademaker]

After cloning to run the Lean code of SHA1.lean

% lake build
error: base: configuration file not found: ./././../../aeneas/backends/lean/lakefile.lean

In the Infoview, I got the error below

`/Users/ar/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/bin/lake setup-file /Users/ar/r/verified-fips-in-rust/lean/VerifiedFipsCryptography/Specs/SHA1.lean Init Init.Data.ByteArray Init.Data.Repr Mathlib.Data.UInt Mathlib.Data.Vector.Defs Init.Data.Nat.Basic VerifiedFipsCryptography.Util.HexString --no-build` failed:

stderr:
error: base: configuration file not found: ./././../../aeneas/backends/lean/lakefile.lean
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

I guess there may be reasons to depend on the https://github.com/AeneasVerif/aeneas. But do the Specs also need to depend on Aeneas?

[arademaker]

OK, I have missed the README file, but after following it:

% lake update
info: toolchain not updated; already up-to-date
error: base: no configuration file with a supported extension:
./././../../aeneas/backends/lean/lakefile.lean
./././../../aeneas/backends/lean/lakefile.toml

[arademaker]

The lake build finished with error

error: Lean exited with code 1
Some required builds logged failures:
- VerifiedFipsCryptography.Specs.SHA1
- VerifiedFipsCryptography.Specs.AES.AES
- VerifiedFipsCryptography.ForBatteries
- VerifiedFipsCryptography.RustTranslations.FipsImplementations
error: build failed