hacspec
regression around `Inconsistent implicit qualifiers (did not expect argument aquals)`
Hi,
our CI just broke on unchanged code:
/home/runner/.nix-profile/bin/fstar.exe
fstar.exe --cmi --warn_error -331-321-274 --cache_checked_modules --cache_dir .cache --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" --include "/nix/store/18l7w674px4kwazy5ip88yxqskwlcwxc-source"/lib --include "/nix/store/1hnjzj74rsk1g80pkq3jhvs7qg6mkfy2-fstar"/rust_primitives --include "/nix/store/1hnjzj74rsk1g80pkq3jhvs7qg6mkfy2-fstar"/core --include "/nix/store/vss9b7rkwgv7wxk4xxzh3q481iq5vimf-hax-lib"/proofs/fstar/extraction --admit_smt_queries true Riot_rs_runqueue.Runqueue.fst --hint_file .hints/Riot_rs_runqueue.Runqueue.fst.hints
* Error 92 at Riot_rs_runqueue.Runqueue.fst(17,33-17,38):
- Inconsistent implicit qualifiers (did not expect argument aquals)
We're using the hax action from "master", so I'm assuming some of the just merged changes here are the cause. Let me know if I can provide more info!
I can confirm that pinning hax_reference to d10f891a19f96bcafa9e31b1d78763e4f3cf30b4 makes our CI work again, we'll be temporary doing that.
Hi, thanks for the report!
I will try to look at before the end of the day, I suspect that it is something easy to fix. We changed a convention and our F* core library may be not entirely updated yet, hence the problem you have here.
This issue is related to https://github.com/hacspec/hax/issues/719. One patch we merged for solving #719 yielded this issue, but was not fixing entirely #719. Thus, fixing this issue now would just make it re-appear differently when #719 is fixed. I'm thus waiting for #719 to be fixed before fixing this one.
Hi @kaspar030, sorry for the delay. I just checked, and I believe this regression is fixed in latest hax, can you confirm it is fixed on your end?
