Check world (test F* + all subprojects) #73
Annotations
10 errors and 11 warnings
|
Build:
hacl-star/code/meta/Meta.Interface.fst#L193
(189) * Error 189 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,12-193,16):
- Expected expression of type
_: FStar.Pervasives.Native.option (*?u23*) _ -> Type
got expression fun _ -> (*?u23*) _
of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Prims.GTot Type
- See also /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,4-193,8)
|
|
Build:
hacl-star/code/meta/Meta.Interface.fst#L193
(189) * Error 189 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,12-193,16):
- Expected expression of type
_: FStar.Pervasives.Native.option (*?u23*) _ -> Type
got expression fun _ -> (*?u23*) _
of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Prims.GTot Type
- See also /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,4-193,8)
|
|
Build:
hacl-star/lib/Lib.Buffer.fst#L452
(66) * Error 66 at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17):
- Failed to resolve implicit argument ?33
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17)
|
|
Build:
hacl-star/lib/Lib.Buffer.fst#L452
(66) * Error 66 at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17):
- Failed to resolve implicit argument ?33
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17)
|
|
Build:
hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst#L44
(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17):
- Failed to resolve implicit argument ?48
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17)
|
|
Build:
hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst#L44
(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17):
- Failed to resolve implicit argument ?48
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17)
|
|
Build:
hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst#L501
(19) * Error 19 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,6-501,12):
- Assertion failed
- See also /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,13-501,26)
|
|
Build:
hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst#L501
(19) * Error 19 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,6-501,12):
- Assertion failed
- See also /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,13-501,26)
|
|
Build:
hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst#L178
(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17):
- Failed to resolve implicit argument ?29
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17)
|
|
Build:
hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst#L178
(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17):
- Failed to resolve implicit argument ?29
of type Type
introduced for
user-provided implicit term at
/__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17)
|
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
Build:
dummy#L1
(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21):
- Some #push-options have not been popped. Current depth is 1.
|
|
Build:
dummy#L1
(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fsti(599,0-613,142):
- Some #push-options have not been popped. Current depth is 1.
|
|
Build:
hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst#L51
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15):
- Module not found: Core
|
|
Build:
hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst#L51
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(51,11-51,15):
- Module not found: Core
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting FStar.List.filter_map to KaRaMeL.
- Failure("Internal error: name not found filter_map_acc\n")
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting FStar.List.index to KaRaMeL.
- Failure("Internal error: name not found index\n")
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to
KaRaMeL.
- Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting LowStar.ImmutableBuffer.ialloca_of_list to KaRaMeL.
- Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list to KaRaMeL.
- Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
Build:
dummy#L1
(250) * Warning 250:
- Error while extracting LowStar.ImmutableBuffer.igcmalloc_of_list_partial to
KaRaMeL.
- Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
Loading