hacl-star / merkle-tree

A verified Merkle Tree, built as a standalone project on top of EverCrypt
6 stars 5 forks source link

merkle-tree no longer builds with latest everest #11

Closed gebner closed 10 months ago

gebner commented 10 months ago

When trying to build merkle-tree locally using the everest build script, I get the following error:

In file included from internal/EverCrypt_Hash.h:11,
                 from EverCrypt_Hash.c:8:
./internal/Merkle_Krmllib.h:18:1: error: inline declaration of ‘FStar_UInt8_eq_mask’ follows declaration with attribute ‘noinline’ [-Werror=attributes]
   18 | static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
      | ^~~~~~
In file included from internal/MerkleTree.h:11,
                 from MerkleTree.c:8:
./internal/Merkle_Krmllib.h:18:1: error: inline declaration of ‘FStar_UInt8_eq_mask’ follows declaration with attribute ‘noinline’ [-Werror=attributes]
   18 | static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
      | ^~~~~~
In file included from /home/gebner/everest/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h:27,
                 from /home/gebner/everest/karamel/include/krml/internal/types.h:99,
                 from ./internal/Merkle_Krmllib.h:12:
/home/gebner/everest/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h:179:30: note: previous definition of ‘FStar_UInt8_eq_mask’ with type ‘uint8_t(uint8_t,  uint8_t)’ {aka ‘unsigned char(unsigned char,  unsigned char)’}
  179 | static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
      |                              ^~~~~~~~~~~~~~~~~~~
In file included from /home/gebner/everest/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h:27,
                 from /home/gebner/everest/karamel/include/krml/internal/types.h:99,
                 from ./internal/Merkle_Krmllib.h:12:
/home/gebner/everest/karamel/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h:179:30: note: previous definition of ‘FStar_UInt8_eq_mask’ with type ‘uint8_t(uint8_t,  uint8_t)’ {aka ‘unsigned char(unsigned char,  unsigned char)’}
  179 | static KRML_NOINLINE uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b)
      |                              ^~~~~~~~~~~~~~~~~~~

(My GCC version is 13.2.1.) An update of the dist directory (using rm dist/Makefile.basic; make dist/Makefile.basic) fixes the issue. I can submit a PR updating that directory if you want.

gebner commented 10 months ago

It seems like this is related to https://github.com/FStarLang/FStar/commit/1630ebd965acf23765a4ec05bb3bbf3f7aea92f8, but I didn't encounter the GCC error before this week.

msprotz commented 10 months ago

yes to update, thanks!