fix: S example segfault

tydeu · May 7, 2024 · d2c496f · d2c496f
1 parent 2c6dea2
commit d2c496f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/examples/S/S.lean b/examples/S/S.lean
@@ -26,7 +26,7 @@ static S g_s = {0, 0, NULL};
 end
 
 alloy c opaque_extern_type S => S where
-  foreach(s, f) := lean_apply_1(f, s->m_s)
+  foreach(s, f) := lean_inc(f); lean_apply_1(f, s->m_s)
   finalize(s) := lean_dec(s->m_s); free(s)
 
 --------------------------------------------------------------------------------

diff --git a/examples/S/lakefile.lean b/examples/S/lakefile.lean
@@ -1,9 +1,8 @@
 import Lake
 open Lake DSL
 
-package s {
+package s where
   buildType := .debug
-}
 
 require alloy from ".."/".."
 

diff --git a/examples/S/test.sh b/examples/S/test.sh
@@ -3,4 +3,4 @@ rm -rf .lake
 LAKE=${LAKE:-lake}
 $LAKE build -U
 $LAKE build Test -v
-#.lake/build/bin/s # TODO: Segfaults for some reason
+.lake/build/bin/s