Currently, aeneas is expected to be in a sibling directory and pinned to d71d2e3f.
|
require aeneas from "../../../aeneas/backends/lean" |
However, aeneas can be explicitly pinned in the lakefile.lean by doing
require aeneas from git
"https://github.com/AeneasVerif/aeneas" @ "d71d2e3f2cb763f7faf15ab606ac9cf32da8dead" / "backends/lean"
Disclosure: I am interested in using this repository to mine Lean4 proving challenges for evaluating and training LLMs, which I would like to publish to HuggingFace as open source. This change will make running these evaluations a little more turnkey.
Currently,
aeneasis expected to be in a sibling directory and pinned to d71d2e3f.SymCrypt/SymCRust/lean/lakefile.lean
Line 4 in c2e575a
However,
aeneascan be explicitly pinned in thelakefile.leanby doingDisclosure: I am interested in using this repository to mine Lean4 proving challenges for evaluating and training LLMs, which I would like to publish to HuggingFace as open source. This change will make running these evaluations a little more turnkey.