Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Add flag-sensitive build job helper for FFI code #126

Closed
arthurpaulino opened this issue Sep 21, 2022 · 2 comments
Closed

Add flag-sensitive build job helper for FFI code #126

arthurpaulino opened this issue Sep 21, 2022 · 2 comments
Labels
enhancement New feature or request
Milestone

Comments

@arthurpaulino
Copy link
Contributor

I was trying to build a project that uses the FFI and there was a compilation error telling me to add -fPIC as a parameter. I tried to add it in many ways, including the right one: in the array of flags. Either way didn't work.

Turns out I just had to do lake clean before trying lake build again, which is a bit strange because I was expecting lake build to notice that I had a different build setup.

For more context: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/C.20FFI.20usage/near/299865961

@tydeu
Copy link
Member

tydeu commented Sep 21, 2022

This is because your ffi.o is a custom target. In order to make it rebuild upon the changing of compile flags you need to include those flags in the trace of that build (e.g., via extraDepTrace on buildAfterDep). The builtin targets for module compilation already do this (see buildLeanO).

@Kha
Copy link
Member

Kha commented Sep 22, 2022

Reinterpreting this issue as a feature request, I suppose a generic buildO job capturing this common pattern would be a nice addition

@tydeu tydeu changed the title lake build doesn't pick new build setup Add flag-sensitive build job helper for FFI code Sep 23, 2022
@tydeu tydeu added the enhancement New feature or request label Sep 23, 2022
@tydeu tydeu added this to the v4.1.0 milestone Oct 1, 2022
tydeu added a commit that referenced this issue Oct 1, 2022
@tydeu tydeu closed this as completed in 53a89f9 Nov 24, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants