hax
hax copied to clipboard
Makefile error: Identifier not found: [Core.Iter.Traits.Iterator.f_position]
Thank you for your great work on this Project!
We ran into an error due to some missing identifier. We are using Iterator::position
in our code.
Error is
* Error 72 at Riot_rs_runqueue.Runqueue.Clist.fst(83,40-83,50):
- Identifier not found: [Core.Iter.Traits.Iterator.f_position]
- Module Core.Iter.Traits.Iterator resolved into Core.Iter.Traits.Iterator,
definition f_position not found
1 error was reported (see above)
make[1]: *** [Makefile:86: .cache/Riot_rs_runqueue.Runqueue.Clist.fst.checked] Error 1
make[1]: Leaving directory '/home/runner/work/RIOT-rs/RIOT-rs/src/riot-rs-runqueue/proofs/fstar/extraction'
make: *** [Makefile:48: all] Error 2
See https://github.com/future-proof-iot/RIOT-rs/actions/runs/8662006305/job/23753096732?pr=248.
Can this be fixed somehow on your side or do we have to change our code?