- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
The compiler panics with the error:
> LEAN_PATH=././build /home/bollu/work/lean4/build/stage1/bin/lean -o build/GAP/P.olean -c build/temp/GAP/P.c ./GAP/P.lean
> LEAN_PATH=././build /home/bollu/work/lean4/build/stage1/bin/lean -o build/GAP/AST.olean -c build/temp/GAP/AST.c ./GAP/AST.lean
PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected
PANIC at Lean.Expr.bindingDomain! Lean.Expr:618:23: binding expected
...
Build failed.
The minimal test case is as follows:
/home/bollu/temp/lean-gap$ tree
.
├── GAP
│ ├── AST.lean
│ └── P.lean
├── GAP.lean
└── leanpkg.toml
with file contents:
-- GAP.lean
import GAP.P
import GAP.AST-- GAP/P.lean
namespace GAP.P
structure P (a: Type) where
runP: a
instance : Monad P := {
pure := fun a => { runP := a },
bind := fun a => fun a2mb => a2mb (a.runP)
}-- GAP/AST.lean
import GAP.P
open GAP.P
namespace GAP.AST
mutual
def parse_expr_logical : P Expr := do
let l <- parse_expr
def parse_expr : P Expr := parse_expr_logical
end# leanpkg.toml
[package]
name = "gap"
version = "0.1"
lean_version = "leanprover/lean4:master"Expected behavior: [The compiler should not panic]
Actual behavior: [the compiler panics]
Reproduces how often: [all the time]
You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.
/home/bollu/temp/lean-gap$ lean --version
Lean (version 4.0.0, commit af12c91b0a50, Release)
/home/bollu/temp/lean-gap$ uname -r
5.9.16-1-MANJARO
Any additional information, configuration or data that might be necessary to reproduce the issue.