Check world (test F* + all subprojects) #76
Annotations
11 warnings
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Sugar.fst#L366
(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
|
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Sugar.fst#L512
(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
|
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Sugar.fst#L621
(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 '@'.
|
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Sugar.fst#L622
(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 '@'.
|
|
Build (after setting up cargo env):
src/checker/Pulse.Common.fst#L84
(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 '@'.
|
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Desugar.fst#L791
(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
|
|
Build (after setting up cargo env):
pulse/src/checker/Pulse.Syntax.Base.fsti#L372
(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.
|
|
Build (after setting up cargo env):
src/checker/Pulse.Syntax.Base.fst#L121
(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.
|
|
Build (after setting up cargo env):
src/checker/Pulse.Syntax.Base.fst#L137
(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.
|
|
Build (after setting up cargo env):
src/checker/Pulse.Syntax.Base.fst#L291
(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(291,15-291,17):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
b1 (bound in src/checker/Pulse.Syntax.Base.fst(291,15-291,17))
and t1 (bound in src/checker/Pulse.Syntax.Base.fst(169,20-169,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.
|
Loading