lib.mk: include most FStar.Class modules #220
Annotations
10 warnings
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.TSet.fst#L28
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(28,4-28,7):
- 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:
ulib/FStar.GhostSet.fst#L23
(318) * Warning 318 at ulib/FStar.GhostSet.fst(23,4-23,7):
- 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) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33):
- 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: ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33):
- 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: ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- 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: ulib/FStar.LexicographicOrdering.fst(75,14-75,28)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- 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: ulib/FStar.LexicographicOrdering.fst(124,10-124,17)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/experimental/FStar.MST.fst#L222
(330) * Warning 330 at ulib/experimental/FStar.MST.fst(222,43-222,55):
- 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:
ulib/experimental/FStar.MST.fst#L247
(352) * Warning 352 at ulib/experimental/FStar.MST.fst(247,42-247,60):
- 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:
ulib/FStar.GSet.fst#L23
(318) * Warning 318 at ulib/FStar.GSet.fst(23,4-23,7):
- 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:
ulib/FStar.TSet.fst#L28
(318) * Warning 318 at ulib/FStar.TSet.fst(28,4-28,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
Set up job
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run cda-tum/setup-z3@main
2s
2s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Get fstar package
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run tar xzf fstar-src.tar.gz
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Set-up OCaml
32s
32s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run opam install . --deps-only --with-test
1m 17s
1m 17s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run eval $(opam env) && make -kj$(nproc) ADMIT=1
5m 46s
5m 46s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Smoke test
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post Set-up OCaml
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Complete job
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Loading