Yicheng Tao

lug: elan update

1

The original lean-package `std4` was renamed to `batteries`. There are still some lean projects using the old name. I wonder if I should delete the old script. For now, I...

Unicode in data

1

I noticed that all the unicode characters in the dataset are ascii-encoded Seems like you didn't set `ensure_ascii=False`. I wonder if this will affect the performance of premise selection. After...

leanOption in lakefile doesn't work

5

I want to set the option `autoImplicit` to false in a project on my self host server. My `mathlib-demo/lakefile.lean` is as follows: ``` import Lake open Lake DSL package "MathlibLatest"...