search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

feat: support for custom user extensions #18

Closed hargoniX closed 2 years ago

hargoniX commented 2 years ago

Description

When running LeanInk against files that load custom user extensions which make user of initializers right now it will simply error because those initializers aren't run. This is addressed by telling the frontend to run the initializers.

Kha commented 2 years ago

Mmh, I would prefer the call to be inside main, and libraries using analyzeInput to repeat that. Otherwise analyzeInput itself should be would have to be unsafe, as a caller will have to ensure the enableInitializersExecution invariants are upheld in any case.

hargoniX commented 2 years ago

I moved it to the exec part since that's the first function where we actually know we'll be running analysis.

Kha commented 2 years ago

Did that break something D: ?

hargoniX commented 2 years ago

The tests are passing for me locally...something weird is going on.

Kha commented 2 years ago

Mmh, the message "Error: unknown constant 'sorryAx'" sounds like it wasn't able to import the stdlib. That's suspicious.