(317) * Error 317: - Expected LowParse.Spec.Base to be already checked but could not find it.

(317) * Error 317: - Expected CBOR.Spec.API.Format to be already checked but could not find it.

(317) * Error 317: - Expected LowParse.Math to be already checked but could not find it.

(317) * Error 317: - Expected CBOR.Spec.API.Format to be already checked but could not find it.

(317) * Error 317: - Expected LowParse.Math to be already checked but could not find it.

(317) * Error 317: - Expected CBOR.Spec.API.Format to be already checked but could not find it.

(47) * Error 47 at /__w/FStar/FStar/everparse/src/3d/Version.fst(3,4-3,21): - Duplicate top-level names [Version.everparse_version] - Previously declared at /__w/FStar/FStar/everparse/src/3d/Version.fst(2,4-2,21)

Process completed with exit code 2.

Process completed with exit code 2.

(66) * Error 66 at /__w/FStar/FStar/everparse/src/3d/tests/out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85): - Failed to resolve implicit argument ?57 of type Prims.bool introduced for Instantiating implicit argument

(12) * Error 12 at /__w/FStar/FStar/everparse/src/3d/tests/out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52): - Expected type EverParse3d.Interpreter.typ (*?u58*) _ (*?u59*) _ (*?u60*) _ (*?u61*) _ (*?u62*) _ (*?u63*) _ but EverParse3d.Interpreter.T_with_comment "should_not_be_here" (EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1) "Validating field should_not_be_here" has type EverParse3d.Interpreter.typ kind__test1 EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial false false

(19) * Error 19 at /__w/FStar/FStar/everparse/src/3d/tests/out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16): - Could not prove goal #1 - The SMT solver could not prove the query. Use --query_stats for more details. - See also /__w/FStar/FStar/FStar/ulib/Prims.fst(459,77-459,89)

(189) * Error 189 at /__w/FStar/FStar/everparse/src/3d/tests/out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67): - Expected expression of type EverParse3d.Kinds.parser_kind (*?u58*) _ EverParse3d.Kinds.WeakKindStrongPrefix got expression EverParse3d.Kinds.kind_all_bytes of type EverParse3d.Kinds.parser_kind false EverParse3d.Kinds.WeakKindConsumesAll

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

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

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fst(293,8-293,25): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction - See also /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51)

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(288) * Warning 288 at /__w/FStar/FStar/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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 /__w/FStar/FStar/FStar/src/data/FStarC.RBSet.fst(105,36-105,37): - 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 /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - 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 /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - 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 /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - 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 '@'.

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

(328) * Warning 328 at /__w/FStar/FStar/karamel/krmllib/Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body

(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(36,4-36,28)

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(21,8-21,15)

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

(285) * Warning 285 at /__w/FStar/FStar/karamel/test/MemCpyModel.fst(10,5-10,7): - No modules in namespace ST and no file with that name either

(285) * Warning 285 at /__w/FStar/FStar/karamel/test/TopLevelArray.fst(7,5-7,7): - No modules in namespace ST and no file with that name either

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(250) * Warning 250: - Error while extracting FStar.Tactics.NamedView.close_term_n to KaRaMeL. - Failure("Internal error: name not found aux\n")

(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")

(242) * Warning 242: - Not extracting uu___is_S to KaRaMeL

(272) * Warning 272 at /__w/FStar/FStar/karamel/test/Wasm10.fst(16,0-17,77): - Top-level let-bindings must be total; this term may have effects

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

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

(340) * Warning 340 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(463,24-463,37): - Unfolding name which is marked as a plugin: frame_vc_norm

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(802,9-802,20): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1612,18-1612,29): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1632,7-1632,18): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1638,7-1638,18): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(337) * Warning 337 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2068,65-2068,66): - 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 '@'.

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2204,11-2204,22): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2782,10-2782,21): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(170,16-170,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(171,19-171,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

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

(271) * Warning 271 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Spec.Base.fsti(544,13-546,17): - Pattern misses at least one bound variable: t

(271) * Warning 271 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Spec.Base.fsti(546,14-546,16): - SMT pattern misses at least one bound variable: t

(361) * Warning 361 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Spec.BoundedInt.fsti(232,0-235,62): - Some #push-options have not been popped. Current depth is 1.

(328) * Warning 328 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Spec.Enum.fst(107,8-107,24): - Global binding 'LowParse.Spec.Enum.assoc_flip_intro' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Low.Base.Spec.fst(487,8-487,18): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(328) * Warning 328 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Low.Base.Spec.fst(511,8-511,24): - Global binding 'LowParse.Low.Base.Spec.valid_list_equiv' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Low.Base.Spec.fst(548,8-548,21): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(337) * Warning 337 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Low.Base.Spec.fst(612,8-612,41): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(361) * Warning 361 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.BitFields.fst(1276,0-1276,29): - Some #push-options have not been popped. Current depth is 1.

(331) * Warning 331 at /__w/FStar/FStar/everparse/src/lowparse/LowParse.Spec.BitSum.fst(1421,7-1421,8): - This name is being ignored

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

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(366,8-366,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(512,8-512,17): - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(621,47-621,48): - 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 /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(622,47-622,48): - 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 /__w/FStar/FStar/pulse/src/checker/Pulse.Common.fst(84,11-84,12): - 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 '@'.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(781,4-781,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(125,20-125,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(125,20-125,22)) and pb1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(141,16-141,19)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(141,16-141,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(141,16-141,19)) and p1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(125,20-125,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool - The type of the second term is: Pulse.Syntax.Base.pattern - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17)) and t1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(173,20-173,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17)) and q1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(301,14-301,16)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.qualifier - If the proof fails, try annotating these with the same type.

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

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

(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/FStar/FStar/karamel/krmllib/C.fst". - Rename "/__w/FStar/FStar/karamel/krmllib/C.fst" to avoid conflicts.

(361) * Warning 361 at /__w/FStar/FStar/everparse/src/3d/Options.fst(594,0-597,15): - Some #push-options have not been popped. Current depth is 1.

(242) * Warning 242 at /__w/FStar/FStar/everparse/src/3d/Ast.fst(395,0-429,18): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /__w/FStar/FStar/everparse/src/3d/Ast.fst(397,12-397,15)

(242) * Warning 242 at /__w/FStar/FStar/everparse/src/3d/Ast.fst(1251,0-1256,14): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /__w/FStar/FStar/everparse/src/3d/Ast.fst(397,12-397,15)

(242) * Warning 242 at /__w/FStar/FStar/everparse/src/3d/InterpreterTarget.fst(394,0-527,16): - Definitions of inner let-rec typ_of_parser and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /__w/FStar/FStar/everparse/src/3d/InterpreterTarget.fst(395,10-395,23)

(242) * Warning 242 at /__w/FStar/FStar/everparse/src/3d/InterpreterTarget.fst(1168,0-1177,13): - Definitions of inner let-rec typ_of_parser and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /__w/FStar/FStar/everparse/src/3d/InterpreterTarget.fst(395,10-395,23)

(337) * Warning 337 at /__w/FStar/FStar/everparse/src/3d/Target.fst(958,28-958,29): - 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 /__w/FStar/FStar/everparse/src/3d/Target.fst(1051,69-1051,70): - 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 /__w/FStar/FStar/everparse/src/3d/Target.fst(1395,54-1395,55): - 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 '@'.

(361) * Warning 361 at /__w/FStar/FStar/everparse/src/3d/Target.fst(1477,0-1501,9): - Some #push-options have not been popped. Current depth is 1.

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

(350) * Warning 350 at /__w/FStar/FStar/steel/share/steel/examples/steel/Duplex.PingPong.fst(14,2-16,6): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/steel/share/steel/examples/steel/Duplex.PingPong.fst(15,2-16,6): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/steel/share/steel/examples/steel/PingPong.fst(33,2-35,15): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/steel/share/steel/examples/steel/PingPong.fst(34,2-35,15): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(274) * Warning 274: - Implicitly opening namespace 'cqueue.' shadows module 'llist' in file "/__w/FStar/FStar/steel/share/steel/examples/steel/LList.fst". - Rename "/__w/FStar/FStar/steel/share/steel/examples/steel/LList.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'duplex.' shadows module 'pingpong' in file "/__w/FStar/FStar/steel/share/steel/examples/steel/PingPong.fst". - Rename "/__w/FStar/FStar/steel/share/steel/examples/steel/PingPong.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'selectors.' shadows module 'llist' in file "/__w/FStar/FStar/steel/share/steel/examples/steel/LList.fst". - Rename "/__w/FStar/FStar/steel/share/steel/examples/steel/LList.fst" to avoid conflicts.

(272) * Warning 272 at /__w/FStar/FStar/steel/share/steel/tests/TopLevelIndexedEffects.fst(18,0-21,49): - Top-level let-bindings must be total; this term may have effects

(272) * Warning 272 at /__w/FStar/FStar/steel/share/steel/tests/TopLevelIndexedEffects.fst(32,0-35,91): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at /__w/FStar/FStar/steel/share/steel/tutorial/References.fst(59,0-72,6): - Some #push-options have not been popped. Current depth is 1.

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 /__w/FStar/FStar/pulse/pulse2rust/src/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 /__w/FStar/FStar/pulse/pulse2rust/src/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 /__w/FStar/FStar/pulse/share/pulse/examples/by-example/PulseTutorial.ImplicationAndForall.fst(24,5-24,7): - No modules in namespace GR and no file with that name either

(285) * Warning 285 at /__w/FStar/FStar/pulse/share/pulse/examples/by-example/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 "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst". - Rename "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst" to avoid conflicts.

(285) * Warning 285 at /__w/FStar/FStar/pulse/share/pulse/examples/by-example/PulseTutorial.ImplicationAndForall.fst(24,5-24,7): - No modules in namespace GR and no file with that name either

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst". - Rename "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst". - Rename "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst". - Rename "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst". - Rename "/__w/FStar/FStar/pulse/share/pulse/examples/by-example/ParallelIncrement.fst" to avoid conflicts.

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

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

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 186, characters 16-118 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, characters 6-39

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 186, characters 16-118 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, characters 6-39

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v1.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 186, characters 16-118 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, characters 6-39

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, chara

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v1.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, chara

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v1.' shadows module 'data' in file "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst". - Rename "/__w/FStar/FStar/everparse/tests/sample/Data.fsti, /__w/FStar/FStar/everparse/tests/sample/Data.fst" to avoid conflicts. - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace.(fun) in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1068, characters 23-271 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Called from Fstarcompiler__FStarC_Util.smap_iter in file "fstar-guts/bare/FStarC_Util.ml" (inlined), line 439, characters 34-56 Called from Fstarcompiler__FStarC_Parser_Dep.enter_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 999, characters 10-1023 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data.record_open_namespace in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1158, characters 14-73 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one.from_parsing_data in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1251, characters 15-711 Called from Fstarcompiler__FStarC_Parser_Dep.collect_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 1272, characters 12-58 Called from Fstarcompiler__FStarC_Parser_Dep.collect.discover_one in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2167, characters 18-104 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Fstarcompiler__FStarC_Parser_Dep.profile in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml" (inlined), line 16, characters 20-77 Called from Fstarcompiler__FStarC_Parser_Dep.collect in file "fstar-guts/fstarc.ml/FStarC_Parser_Dep.ml", line 2198, characters 6-124 Called from Fstarcompiler__FStarC_Dependencies.find_deps_if_needed in file "fstar-guts/fstarc.ml/FStarC_Dependencies.ml", line 10, characters 18-77 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 424, characters 25-150 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL - Stack trace: Raised by primitive operation at Fstarcompiler__FStarC_Util.stack_dump in file "fstar-guts/bare/FStarC_Util.ml", line 139, characters 53-82 Called from Fstarcompiler__FStarC_Errors_Msg.backtrace_doc in file "fstar-guts/fstarc.ml/FStarC_Errors_Msg.ml", line 59, characters 12-37 Called from Fstarcompiler__FStarC_Errors.maybe_add_backtrace in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 787, characters 21-55 Called from Fstarcompiler__FStarC_Errors.log_issue_ctx in file "fstar-guts/fstarc.ml/FStarC_Errors.ml", line 914, characters 23-46 Called from Fstarcompiler__FStarC_Errors.log_issue0 in file "fstar-guts/fstarc.ml/FStarC_Errors.ml" (inlined), line 1038, characters 10-113 Called from Fstarcompiler__FStarC_Extraction_Krml.translate_let' in file "fstar-guts/fstarc.ml/FStarC_Extraction_Krml.ml", line 3857, characters 14-214 Called from BatList.filter_map.loop in file "src/batList.ml", line 550, characters 12-15 Called from BatList.filter_map in file "src/batList.ml", line 556, characters 2-14 Called from BatList.map.loop in file "src/batList.ml", line 244, characters 28-33 Called from BatList.map in file "src/batList.ml", line 247, characters 4-12 Called from Fstarcompiler__FStar_List.collect in file "fstar-guts/app/FStar_List.ml" (inlined), line 43, characters 34-51 Called from Fstarcompiler__FStarC_Extraction_Krml.translate_module in file "fstar-guts/fstarc.ml/FStarC_Extraction_Krml.ml", line 3930, characters 16-102 Called from Fstarcompiler__FStarC_Extraction_Krml.translate.(fun) in file "fstar-guts/fstarc.ml/FStarC_Extraction_Krml.ml", line 3962, characters 39-60 Called from BatList.filter_map.loop in file "src/batList.ml", line 550, characters 12-15 Called from BatList.filter_map in file "src/batList.ml", line 556, characters 2-14 Called from BatList.map in file "src/batList.ml", line 246, characters 23-28 Called from Fstarcompiler__FStar_List.collect in file "fstar-guts/app/FStar_List.ml" (inlined), line 43, characters 34-51 Called from Fstarcompiler__FStarC_Universal.emit in file "fstar-guts/fstarc.ml/FStarC_Universal.ml", line 1096, characters 14-212 Called from Fstarcompiler__FStarC_Universal.batch_mode_tc in file "fstar-guts/fstarc.ml/FStarC_Universal.ml", line 1552, characters 28-49 Called from Fstarcompiler__FStarC_Main.go_normal in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 429, characters 29-111 Called from Fstarcompiler__FStarC_Util.record_time_ns in file "fstar-guts/bare/FStarC_Util.ml", line 24, characters 14-18 Called from Fstarcompiler__FStarC_Util.record_time_ms in file "fstar-guts/bare/FStarC_Util.ml", line 28, characters 18-34 Called from Fstarcompiler__FStarC_Main.main.(fun) in file "fstar-guts/fstarc.ml/FStarC_Main.ml", line 488, characters 28-57 Called from Dune__exe__Fstarc2_full.x in file "fstarc-full/fstarc2_full.ml", line 19, characters 6-39

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

(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fsti(599,0-613,142): - Some #push-options have not been popped. Current depth is 1.

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15): - Module not found: Core

(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.ialloca_of_list to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

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

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

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

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15): - Module not found: Core

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

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15): - Module not found: Core

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(250) * Warning 250: - Error while extracting FStar.Tactics.NamedView.close_term_n to KaRaMeL. - Failure("Internal error: name not found aux\n")

(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.ialloca_of_list to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")

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