lean-training-data
lean-training-data copied to clipboard
semorrison
Being able to run `tactic_benchmark` on decls that use `sorry` is rather useful. For example, when benchmarking tactics on evaluations such as MiniF2F which don't come with proofs for every...
Is there an easy way to change the version of mathlib4 in lean-training-data to a fork or different commit for mathlib? Right now the library automatically installs the particular commit...
I tried `lake exe goal_comments Mathlib.Logic.Hydra` and `lake exe goal_comments Mathlib.Logic.Hydra --edit`, but the `-- ⊢ x = y` aren't inserted at all.
When I run `lake exe declaration_types Mathlib` ,I got error: "uncaught exception: Could not find native implementation of external declaration 'IO.getRandomBytes' (symbols 'l_IO_getRandomBytes___boxed' or 'l_IO_getRandomBytes'). For declarations from `Init`, `Std`,...
when i run `lake exe get cache` i get the following error message: ``` info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake/packages\mathlib' info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries' info: Qq: cloning https://github.com/leanprover-community/quote4...
The originally provided commit hashes were no longer found, as the original projects removed them. For me the program only works with this hashes. Testplan: on the master branch: ```...
