tydeu / lean4-alloy

Write C shims from within Lean code.
Apache License 2.0
42 stars 11 forks source link

lake build does not rebuild alloy #4

Closed nomeata closed 9 months ago

nomeata commented 9 months ago

It seems that if I change my .lean file (Seccomp.lean), it does not rebuild the .alloy.c. file. I can make it do so by deleting it explicitly.

Here, loogle is an executable using Seccomp, and Seccomp.lean has been changed:

~/build/lean/mathlib4 $ lake build loogle
[258/374] Building Seccomp
[372/374] Building Loogle.Main
~/build/lean/mathlib4 $ lake build +Seccomp:alloy.c
~/build/lean/mathlib4 $ rm ./build/ir/Seccomp.alloy.c
~/build/lean/mathlib4 $ lake build +Seccomp:alloy.c
Generating Seccomp alloy
~/build/lean/mathlib4 $ lake build loogle
[370/374] Compiling Seccomp alloy
[371/374] Linking Seccomp
[372/374] Building Loogle.Main
[374/374] Linking loogle
nomeata commented 9 months ago

That was quick ❤️