(189) * Error 189 at src/checker/Pulse.Common.fst(63,0-68,16): - Expected expression of type f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _) -> Type got expression fun _ -> (*?u95*) _ of type f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _) -> Prims.GTot Type

(54) * Error 54 at lib/core/Pulse.Lib.NonInformative.fst(32,21-33,62): - (*?u42*) _ is not equal to the expected type y: a{y == FStar.Ghost.elift1 (fun _ -> _._1) p} & (*?u12*) _

(54) * Error 54 at lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,52-20,53): - _: Prims.unit -> Prims.nat is not a subtype of the expected type _: Prims.unit -> FStar.Pervasives.Dv (k: Prims.nat{k == n}) - See also lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,14-20,15)

(66) * Error 66 at lib/core/PulseCore.HeapExtension.fsti(291,25-291,32): - Failed to resolve implicit argument ?24 of type Type introduced for Instantiating implicit argument

(66) * Error 66 at lib/core/PulseCore.BaseHeapSig.fsti(300,25-300,32): - Failed to resolve implicit argument ?21 of type Type introduced for Instantiating implicit argument

Process completed with exit code 2.

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 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 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 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 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 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 src/syntax_extension/PulseSyntaxExtension.Desugar.fst(791,4-791,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.fsti(372,16-372,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/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(372,16-372,18)) and b1 (bound in src/checker/Pulse.Syntax.Base.fst(291,15-291,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.pattern & Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(121,20-121,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(121,20-121,22)) and pb1 (bound in src/checker/Pulse.Syntax.Base.fst(137,16-137,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 src/checker/Pulse.Syntax.Base.fst(137,16-137,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(137,16-137,19)) and p1 (bound in src/checker/Pulse.Syntax.Base.fst(121,20-121,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.