Cannot extract tests because of the macro `#[test]`

[paracetamolo]

Using the command cargo hax --cargo-args --tests \; into fstar

error[HAX0001]: (AST import) something is not implemented yet.
                Pointer, with [cast] being (Types.ClosureFnPointer Types.Normal)
  --> tests/main.rs:22:1
   |
21 |   #[test]
   |   ------- in this procedural macro expansion
22 | / fn t1() {
23 | |     println!("hello");
24 | | }
   | |_^
   |

this is not a blocking problem, moving the same tests under src/ as a binary w/o the macro extracts fine.

[W95Psp]

Thanks for the bug report, it's probably due to the test driver being generated which contains some hax unsupported chunks of code. I will look into that.

This is related to https://github.com/hacspec/hax/issues/500

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[W95Psp]

This is still relevant

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Still relevant