Skip to content

Commit

Permalink
fix: disable unsafe closed term extraction (#3509)
Browse files Browse the repository at this point in the history
The compiler extracts the closed term `Option.get none ◾` here, which causes a segfault in compiled code depending on mathlib, like e.g. mathport.
  • Loading branch information
gebner committed Apr 19, 2023
1 parent 15adff0 commit c0a6fe8
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib/ModelTheory/Encoding.lean
Expand Up @@ -59,6 +59,7 @@ def listEncode : L.Term α → List (Sum α (Σi, L.Functions i))
Sum.inr (⟨_, f⟩ : Σi, L.Functions i)::(List.finRange _).bind fun i => (ts i).listEncode
#align first_order.language.term.list_encode FirstOrder.Language.Term.listEncode

set_option compiler.extract_closed false in -- https://github.com/leanprover/lean4/issues/1965
/-- Decodes a list of variables and function symbols as a list of terms. -/
def listDecode : List (Sum α (Σi, L.Functions i)) → List (Option (L.Term α))
| [] => []
Expand Down

0 comments on commit c0a6fe8

Please sign in to comment.