FStarLang/karamel

Separate compilation with -static-header -library does not honor CMacro

tahina-pro opened this issue · 1 comments

On https://github.com/FStarLang/kremlin/tree/taramana_sepcomp_cmacro/test/sepcomp

a contains a library:

  • A.Base contains definitions that are extracted to A.h with static inlines and a macro A_THIS_IS_A_CONSTANT, as expected
  • A.Combinators contains a higher-order function f that is not extracted, as expected. That function f uses A_THIS_IS_A_CONSTANT.

b contains an application that uses A.Combinators.f without extracting A.h again. Thus, b is indirectly using A.Base.this_is_a_constant declared as CMacro, but I end up with B.h declaring and B.c using A_this_is_a_constant, instead of the expected A_THIS_IS_A_CONSTANT from A.h

Thank you @msprotz for having fixed this bug! Just merged into master.