Errors: Introducing '--message_format github', for github actions #104
Annotations
11 warnings
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) - Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) - Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.GhostSet.fst#L23
(318) - Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.TSet.fst#L28
(318) - Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.GSet.fst#L23
(318) - Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level
letbinding are not encoded to the solver, you will only be able to reason with
their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst(75,14-75,28)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) - Definitions of inner let-rec get_acc and its enclosing top-level letbinding
are not encoded to the solver, you will only be able to reason with their
types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst(124,10-124,17)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/experimental/FStar.MST.fst#L222
(330) - Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us informed
(on github etc.) about how you are using it
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/experimental/FStar.MST.fst#L247
(352) - Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a substitutive
indexed effect combinator, it is better to make it one if possible for better
performance and ease of use
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.WellFoundedRelation.fst#L152
(290) - In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
wfr_a.decreaser (FStar.Pervasives.dfst xy)
(bound in
/home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFoundedRelation.fst(152,21-152,46))
and
wfr_a.decreaser (FStar.Pervasives.dfst xy)
(bound in
/home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFoundedRelation.fst(152,21-152,46))
are equal.
- The type of the first term is:
FStar.WellFoundedRelation.acc_classical wfr_a.relation
(FStar.Pervasives.dfst xy)
- The type of the second term is:
FStar.WellFoundedRelation.acc_classical wfr_a.relation
(FStar.Pervasives.dfst xy)
- If the proof fails, try annotating these with the same type.
|
Loading