hax icon indicating copy to clipboard operation
hax copied to clipboard

Makefile error: Identifier not found: [Core.Iter.Traits.Iterator.f_position]

Open elenaf9 opened this issue 10 months ago • 2 comments

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?

elenaf9 avatar Apr 12 '24 12:04 elenaf9