ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(131,21-131,22): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(136,13-136,14): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(285) * Warning 285 at PulseTutorial.ImplicationAndForall.fst(24,5-24,7): - No modules in namespace GR and no file with that name either

(285) * Warning 285 at PulseTutorial.LinkedList.fst(222,5-222,6): - No modules in namespace I and no file with that name either

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(288) * Warning 288 at Test.ReflikeClass.fst(19,32-19,37): - Pulse.Lib.Reference.alloc is deprecated - Reference.alloc is unsound; use Box.alloc instead - See also lib/pulse/lib/Pulse.Lib.Reference.fsti(46,0-51,21)

(249) * Warning 249 at Bug166.fst(13,9-13,10): - Losing precision when encoding a function literal: fun _ -> Pulse.Lib.Core.emp - Unannotated abstraction in the compiler? - See also Bug166.fst(9,11-9,14)

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.