search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
54 stars 13 forks source link

REPL does not enable initialization #1

Closed gebner closed 1 year ago

gebner commented 1 year ago

When importing modules, you need to enable initializer execution (using enableInitializersExecution) otherwise attributes, etc. won't work.

Input:

{"cmd": "import Lake open Lake DSL\npackage REPL"}

Output:

{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 12},
   "data": "unknown attribute [package]"}],
 "env": 0}
semorrison commented 1 year ago

Fixed in https://github.com/leanprover-community/repl/commit/11daea2ee742b512cc94b4a280849485254e592a