Check world (test F* + all subprojects) #72
Annotations
3 errors and 4 warnings
|
Build:
steel/lib/steel/Steel.Effect.Common.fsti#L597
(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(597,2-597,37):
- Expected type Type but vdep_payload v p _ has type Type0
|
|
Build:
steel/lib/steel/Steel.Effect.Common.fsti#L597
(34) * Error 34 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(597,2-597,37):
- Computed type Type0
and effect Prims.PURE
is not compatible with the annotated type Type
and effect GTot
|
|
Build
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
|
|
Build:
steel/lib/steel/Steel.Effect.Common.fsti#L463
(340) * Warning 340 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(463,24-463,37):
- Unfolding name which is marked as a plugin: frame_vc_norm
|
|
Build:
steel/lib/steel/Steel.Effect.Common.fsti#L2068
(337) * Warning 337 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2068,65-2068,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 '@'.
|
|
Build:
dummy#L1
(361) * Warning 361 at /__w/FStar/FStar/steel/lib/steel/Steel.Semantics.Hoare.MST.fst(1351,0-1372,15):
- Some #push-options have not been popped. Current depth is 1.
|
Loading