aa18927d2e
This PR fixes a segfault when running `idbgClientLoop`. `@[extern]` expects that the function doesn't include erased arguments in the signature; however, `@[export]` exports the function with all arguments, including erased ones. This causes a function signature mismatch between `idbgClientLoopImpl` and `idbgClientLoop`, causing segfaults. However, instead of solving the deeper problem that `@[extern]` - `@[export]` pairs can cause such problems, this PR removes the erased arguments from `idbgClientLoopImpl` and replaces occurrences of `α` with `NonScalar`.
23 lines
782 B
Text
23 lines
782 B
Text
module
|
|
|
|
import Lean
|
|
|
|
/-! ## idbg syntax compiles in a do block -/
|
|
|
|
-- Verify the idbg syntax is accepted and type-checks.
|
|
-- We can't run this (the client loop would try to connect), just check elaboration.
|
|
-- Disable inServer so the elaborator doesn't block waiting for TCP connection
|
|
set_option Elab.inServer false in
|
|
set_option backward.do.legacy false in
|
|
def idbgTypeCheck (x : Nat) (s : String) : IO Unit := do
|
|
idbg x + s.length
|
|
|
|
/-! ## Running idbgClientLoop doesn't cause a segfault -/
|
|
|
|
-- Note: while running it once didn't consistently cause a segfault, running it twice did
|
|
|
|
#guard_msgs (drop error) in
|
|
#eval Lean.Idbg.idbgClientLoop "hi" #[`Nonexistent, `Nonexistent] id
|
|
|
|
#guard_msgs (drop error) in
|
|
#eval Lean.Idbg.idbgClientLoop "hi" #[`Nonexistent, `Nonexistent] id
|