search

argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
122 stars 9 forks source link

Remove `prelude` flag from compiler options #198

Closed winston-h-zhang closed 2 years ago

winston-h-zhang commented 2 years ago

AFAIU, originally --prelude was added to avoid doing a relatively expensive delta computation. But in #195, we replaced the delta computation with Lean's internal declaration tracker. So now is --prelude still needed?

winston-h-zhang commented 2 years ago

@arthurpaulino

arthurpaulino commented 2 years ago

That flag is used to skip the call to setLibsPaths, which is needed when we are compiling Lean code that use things from Init

winston-h-zhang commented 2 years ago

Ah, I see then O_O. Thanks for explaining, sorry for the disturbance!