PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none

[dwrensha]

Lean panics on the input def y := c.5� where � signifies the non-utf8 byte 0xff.

$ echo "ZGVmIHkgOj0gYy41/wo=" | base64 -d > panic.lean
$ cat panic.lean
def y := c.5�
$ ~/src/lean4/build/release/stage1/bin/lean --version
Lean (version 4.0.0, commit e3ec468e3bfe, Release)
$ ~/src/lean4/build/release/stage1/bin/lean panic.lean
PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x32f432c)[0x7ff39ccf432c]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0xc4)[0x7ff39ccf4694]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn+0x9f3)[0x7ff39be219a3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux+0x160)[0x7ff39be32440]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAtom+0x134)[0x7ff39be35fb4]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0x961)[0x7ff39cd0df81]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___lambda__1+0x174)[0x7ff39b4edaf4]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd1e)[0x7ff39cd0aa2e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoContext_x27___at_Lean_Elab_Term_withInfoContext_x27___spec__1+0x2ca)[0x7ff39b4eb04a]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux+0x377)[0x7ff39b51e057]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns+0x3f8)[0x7ff39b51f478]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__4+0x134)[0x7ff39b521da4]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__7+0xfb5)[0x7ff39b523a45]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd1e)[0x7ff39cd0aa2e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__8+0x31e)[0x7ff39b4f790e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x1248)[0x7ff39cd03928]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabTermEnsuringType+0x166)[0x7ff39b51bb56]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2___lambda__1+0x24f)[0x7ff39b8b434f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2___lambda__1___boxed+0x2e)[0x7ff39b8b4b3e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xa7d)[0x7ff39cd0e09d]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7ff39cd0aa95]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_addAutoBoundImplicits_x27___spec__2___rarg+0x8a)[0x7ff39b4a061a]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2___lambda__2+0x3b9)[0x7ff39b89be89]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7ff39cd0aa95]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withLevelNames___rarg+0x1c1)[0x7ff39b4bec61]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7ff39cd0aa95]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues___spec__2+0x3ab)[0x7ff39b8b4f5b]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabFunValues+0x38)[0x7ff39b8b5628]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_elabMutualDef_go___lambda__3+0x29f)[0x7ff39b90823f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xc39)[0x7ff39cd0c7b9]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb27)[0x7ff39cd0c6a7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0xb6a)[0x7ff39cd0c6ea]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_6+0xcc2)[0x7ff39cd08b62]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_withAuxDecl___spec__3___rarg+0x92)[0x7ff39b4c6112]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withFunLocalDecls___rarg+0x2f)[0x7ff39b89b41f]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7ff39cd0aa95]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__1___boxed+0x21)[0x7ff39b5f3971]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_9+0xae7)[0x7ff39cd0e107]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_runTermElabM___rarg___lambda__2___boxed+0x21)[0x7ff39b5f4891]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_8+0x9e4)[0x7ff39cd0c564]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xd85)[0x7ff39cd0aa95]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg+0xac)[0x7ff39b4a28ec]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0x93d)[0x7ff39cd0a64d]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg+0x143)[0x7ff39b4c6653]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_withAutoBoundImplicit___rarg+0x36f)[0x7ff39b4c7eaf]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7ff39cd0aae9]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__1___rarg+0x2c0)[0x7ff39b5ee1b0]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1+0x1b)[0x7ff39b5ef1db]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_7+0xdd9)[0x7ff39cd0aae9]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Term_TermElabM_run___rarg+0x257)[0x7ff39b4a18d7]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_liftTermElabM___rarg+0x49c)[0x7ff39b5ef94c]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabMutualDef+0x160)[0x7ff39b910610]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x110e)[0x7ff39cd037ee]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Command_withMacroExpansion___spec__1___rarg+0x1fe)[0x7ff39b5d9b9e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing+0x222)[0x7ff39b5db182]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10c6)[0x7ff39cd037a6]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_3+0x10ee)[0x7ff39cd037ce]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x57)[0x7ff39b5de717]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabCommandTopLevel___lambda__2+0x340)[0x7ff39b5e6f00]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend+0x1f5)[0x7ff39b7617b5]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed+0x16)[0x7ff39b7622a6]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x13c7)[0x7ff39ccfff67]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0x14)[0x7ff39a8f9f84]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0x11)[0x7ff39a8fa0d1]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x1268)[0x7ff39ccffe08]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_profileit+0x9f)[0x7ff39cc130af]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x59)[0x7ff39a8fa169]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommand+0xc0d)[0x7ff39b76509d]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Frontend_processCommands+0x5e)[0x7ff39b765eee]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_IO_processCommands+0xf6)[0x7ff39b766416]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_runFrontend___lambda__2+0x33)[0x7ff39b767853]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_run_frontend+0x4de)[0x7ff39b768c8e]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x31a0da3)[0x7ff39cba0da3]
/home/dwrensha/src/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_main+0x29c5)[0x7ff39cba4735]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x7ff399629d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x7ff399629e40]
/home/dwrensha/src/lean4/build/release/stage1/bin/lean(_start+0x25)[0x55a29404c095]
panic.lean:1:9: error: unknown identifier 'c'
panic.lean:1:12: error: expected command