Disable comments by default

[franziskuskiefer]

adds option to enable them

[msprotz]

confused as to why it's failing, maybe it's something that got fixed upstream, I remember @mtzguido pointing out that he broke some builds and revert some change... mind pushing a dummy commit see if it helps? thanks!

[mtzguido]

I see it still failed.. the change that broke the F* nix build was fixed over a week ago so I think you should have been fine originally. This

2024-10-14T06:47:37.5456736Z        > cd out/test-symcrust && clang -Wall -Werror -Wno-unused-variable  -I/nix/store/rls42j9rdf5izgv9rjsh5n6yac7701sw-karamel-8c3612018c25889288da6857771be3ad03b75bcd/include -I. -I../../include  symcrust.c main.c && ./a.out
2024-10-14T06:47:37.5462286Z        > grep -q XXX1 out/test-array/array.c && \
2024-10-14T06:47:37.5464581Z        > grep -q XXX2 out/test-array/array.c && \
2024-10-14T06:47:37.5466443Z        > grep -q XXX3 out/test-array/array.c && \
2024-10-14T06:47:37.5467964Z        > true
2024-10-14T06:47:37.5469530Z        > make: *** [Makefile:40: custom-test-array] Error 1
2024-10-14T06:47:37.5479254Z        > rm out/test-where_clauses_closures/main.c out/test-const_generics/main.c out/test-array2d/main.c out/test-where_clauses_simple/main.c out/test-mismatch/main.c out/test-symcrust/main.c out/test-array/main.c out/test-where_clauses_fncg/main.c out/test-traits/main.c out/test-nested_arrays2/main.c out/test-slice_array/main.c out/test-int_switch/main.c out/test-partial_eq/main.c out/test-nested_arrays/main.c out/test-inline_attributes/main.c

seems like either the C compilation or the program are failing?

[msprotz]

Oh didn't realize that was the error. I saw something about a path not found and assumed that was the error. Thanks

       > F* library not found in ulib; falling back to lib/fstar

[msprotz]

@franziskuskiefer will take a look later

[franziskuskiefer]

What is being tested here? Maybe the test is expecting the comments?

[msprotz]

Oh you changed my patch to drop comments by default -- didn't realize that. Yeah, adding test-comments: EXTRA=-fcomments in Makefile at line 33 would probably fix it. The option should probably be a feature option (- f) since it controls the shape of the generated code, too.

Thanks!