Skip to content
Pulse CI

Profiling and revising slprop_equiv checking for fold and unfold #297

Sign in to view logs

Profiling and revising slprop_equiv checking for fold and unfold

Profiling and revising slprop_equiv checking for fold and unfold #297

Triggered via pull request April 2, 2025 18:50
@nikswamynikswamy
synchronize #395
_nik_slprop_equiv_profiling
Status Success
Total duration 23m 14s
Artifacts –
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

ci.yml

on: pull_request
ci
23m 9s
ci
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
ci: Pulse.Syntax.Base.fst#L293
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17)) and q1 (bound in Pulse.Syntax.Base.fst(298,14-298,16)) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: Pulse.Syntax.Base.qualifier - If the proof fails, try annotating these with the same type.
ci: Pulse.Syntax.Base.fst#L293
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17)) and t1 (bound in Pulse.Syntax.Base.fst(171,20-171,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.
ci: Pulse.Syntax.Base.fst#L139
(290) * Warning 290 at /__w/pulse/pulse/pulse/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 Pulse.Syntax.Base.fst(139,16-139,19)) and p1 (bound in 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.
ci: Pulse.Syntax.Base.fst#L123
(290) * Warning 290 at /__w/pulse/pulse/pulse/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 Pulse.Syntax.Base.fst(123,20-123,22)) and pb1 (bound in 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.
ci: PulseSyntaxExtension.Desugar.fst#L872
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(872,4-872,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body
ci: Pulse.Common.fst#L84
(337) * Warning 337 at /__w/pulse/pulse/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 '@'.
ci: PulseSyntaxExtension.Sugar.fst#L624
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(624,47-624,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 '@'.
ci: PulseSyntaxExtension.Sugar.fst#L623
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(623,47-623,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 '@'.
ci: PulseSyntaxExtension.Sugar.fst#L516
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(516,8-516,17): - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body
ci: PulseSyntaxExtension.Sugar.fst#L369
(328) * Warning 328 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(369,8-369,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body