Process completed with exit code 2.

Process completed with exit code 2.

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/steel/lib/steel/Steel.ST.GenElim1.Base.fst.checked'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/steel/lib/steel/Steel.ST.GenElim.Base.fst.checked'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/steel/lib/steel/Steel.Effect.Common.fst.checked'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/steel/build/extraction.checked/ExtractSteelC.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/steel/build/extraction.checked/ExtractSteel.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/syntax_extension.checked/PulseSyntaxExtension.TransformRValues.fst.checked.lax'

(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.ASTBuilder.fst(125,19-125,27): - Identifier not found: [Filepath.basename] - Could not resolve module name Filepath

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/checker.checked/Pulse.Common.fst.checked'

(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.Desugar.fst(740,47-740,64): - Identifier not found: [Parser.Const.Tuples.mk_tuple_data_lid] - Could not resolve module name Parser.Const.Tuples

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/syntax_extension.checked/PulseSyntaxExtension.Env.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/extraction.checked/ExtractPulse.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/extraction.checked/ExtractPulseC.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/extraction.checked/ExtractPulseOCaml.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/syntax_extension.checked/PulseSyntaxExtension.Err.fst.checked.lax'

(151) * Error 151: - Not a valid FStar file: '/__w/FStar-1/FStar-1/pulse/build/syntax_extension.checked/PulseSyntaxExtension.Sugar.fst.checked.lax'

Magic Nix Cache has been deprecated due to a change in the underlying GitHub APIs and will stop working on 1 February 2025. To continue caching Nix builds in GitHub Actions, use FlakeHub Cache instead. Replace... - uses: DeterminateSystems/magic-nix-cache-action@main ...with... - uses: DeterminateSystems/flakehub-cache-action@main For more details: https://dtr.mn/magic-nix-cache-eol

Magic Nix Cache has been deprecated due to a change in the underlying GitHub APIs and will stop working on 1 February 2025. To continue caching Nix builds in GitHub Actions, use FlakeHub Cache instead. Replace... - uses: DeterminateSystems/magic-nix-cache-action@main ...with... - uses: DeterminateSystems/flakehub-cache-action@main For more details: https://dtr.mn/magic-nix-cache-eol

Magic Nix Cache has been deprecated due to a change in the underlying GitHub APIs and will stop working on 1 February 2025. To continue caching Nix builds in GitHub Actions, use FlakeHub Cache instead. Replace... - uses: DeterminateSystems/magic-nix-cache-action@main ...with... - uses: DeterminateSystems/flakehub-cache-action@main For more details: https://dtr.mn/magic-nix-cache-eol

Magic Nix Cache has been deprecated due to a change in the underlying GitHub APIs and will stop working on 1 February 2025. To continue caching Nix builds in GitHub Actions, use FlakeHub Cache instead. Replace... - uses: DeterminateSystems/magic-nix-cache-action@main ...with... - uses: DeterminateSystems/flakehub-cache-action@main For more details: https://dtr.mn/magic-nix-cache-eol

(337) * Warning 337 at /__w/FStar-1/FStar-1/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 '@'.

(337) * Warning 337 at /__w/FStar-1/FStar-1/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-1/FStar-1/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-1/FStar-1/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-1/FStar-1/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 '@'.

(271) * Warning 271 at /__w/FStar-1/FStar-1/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-1/FStar-1/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-1/FStar-1/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(271) * Warning 271 at /__w/FStar-1/FStar-1/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-1/FStar-1/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-1/FStar-1/FStar/ulib/FStar.UInt.fsti(435,8-435,51)

(271) * Warning 271 at /__w/FStar-1/FStar-1/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

(352) * Warning 352 at /__w/FStar-1/FStar-1/steel/lib/steel/Steel.ST.Effect.fsti(169,19-169,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

(352) * Warning 352 at /__w/FStar-1/FStar-1/steel/lib/steel/Steel.ST.Effect.fsti(168,16-168,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

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

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

(337) * Warning 337 at /__w/FStar-1/FStar-1/steel/lib/steel/Steel.Effect.Common.fsti(2067,65-2067,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-1/FStar-1/steel/lib/steel/Steel.Effect.Common.fsti(1637,7-1637,18): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

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

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

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

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

(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(139,16-139,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in src/checker/Pulse.Syntax.Base.fst(139,16-139,19)) and p1 (bound in src/checker/Pulse.Syntax.Base.fst(123,20-123,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 src/checker/Pulse.Syntax.Base.fst(123,20-123,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in src/checker/Pulse.Syntax.Base.fst(123,20-123,22)) and pb1 (bound in src/checker/Pulse.Syntax.Base.fst(139,16-139,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-1/FStar-1/pulse/src/checker/Pulse.Syntax.Base.fsti(385,16-385,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in /__w/FStar-1/FStar-1/pulse/src/checker/Pulse.Syntax.Base.fsti(385,16-385,18)) and q1 (bound in src/checker/Pulse.Syntax.Base.fst(298,14-298,16)) are equal. - The type of the first term is: 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.

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

(337) * Warning 337 at 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 '@'.

(285) * Warning 285 at src/checker/Pulse.VC.fsti(7,38-7,48): - module not found in search path: fstar.stubs.tactics.types.reflection

(337) * Warning 337 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(641,47-641,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 src/syntax_extension/PulseSyntaxExtension.Sugar.fst(640,47-640,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 '@'.

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