Check world (test F* + all subprojects) #78
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:
dummy#L1
(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.
|
|
Build:
dummy#L1
(361) * Warning 361 at Options.fst(594,0-597,15):
- Some #push-options have not been popped. Current depth is 1.
|
|
Build:
dummy#L1
(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.
|
|
Build:
dummy#L1
(242) * Warning 242 at 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: Ast.fst(397,12-397,15)
|
|
Build:
dummy#L1
(242) * Warning 242 at 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: Ast.fst(397,12-397,15)
|
|
Build:
everparse/src/lowparse/LowParse.Spec.Base.fsti#L544
(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
|
|
Build:
everparse/src/lowparse/LowParse.Spec.Base.fsti#L546
(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
|
|
Build:
src/lowparse/LowParse.Spec.Enum.fst#L107
(328) * Warning 328 at 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
|
|
Build:
dummy#L1
(361) * Warning 361 at src/lowparse/LowParse.BitFields.fst(1276,0-1276,29):
- Some #push-options have not been popped. Current depth is 1.
|
|
Build:
Target.fst#L958
(337) * Warning 337 at 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 '@'.
|
Loading