Pulse nightly build #394
Annotations
20 warnings
|
linux:
FStarC.Extraction.Krml.fst#L330
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/extraction/FStarC.Extraction.Krml.fst(330,8-330,19):
- Global binding
'FStarC.Extraction.Krml.decl_to_doc'
is recursive but not used in its body
|
|
linux:
FStarC.ToSyntax.ToSyntax.fst#L527
(319) * Warning 319 at /home/runner/work/pulse/pulse/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(527,19-527,57):
- Effectful argument let _ = FStarC.Ident.string_of_lid _max_lid in
_ = "max" (FStarC.Effect.ALL) to erased function assert, consider let binding it
|
|
linux:
FStarC.ToSyntax.ToSyntax.fst#L509
(319) * Warning 319 at /home/runner/work/pulse/pulse/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(509,13-509,48):
- Effectful argument let _ = FStarC.Ident.string_of_id _op_plus in
_ = "+" (FStarC.Effect.ALL) to erased function assert, consider let binding it
|
|
linux:
FStarC.Syntax.Resugar.fst#L327
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/syntax/FStarC.Syntax.Resugar.fst(327,8-327,26):
- Global binding
'FStarC.Syntax.Resugar.resugar_term_base''
is recursive but not used in its body
|
|
linux:
FStarC.Parser.ToDocument.fst#L1994
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1994,4-1994,12):
- Global binding
'FStarC.Parser.ToDocument.p_tmNoEq'
is recursive but not used in its body
|
|
linux:
FStarC.Parser.ToDocument.fst#L1730
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1730,4-1730,21):
- Global binding
'FStarC.Parser.ToDocument.p_maybeFocusArrow'
is recursive but not used in its body
|
|
linux:
FStarC.Parser.ToDocument.fst#L1095
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24):
- Global binding
'FStarC.Parser.ToDocument.p_disjunctivePattern'
is recursive but not used in its body
|
|
linux:
FStarC.Parser.ToDocument.fst#L756
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13):
- Global binding
'FStarC.Parser.ToDocument.p_justSig'
is recursive but not used in its body
|
|
linux:
FStarC.Parser.ToDocument.fst#L735
(328) * Warning 328 at /home/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14):
- Global binding
'FStarC.Parser.ToDocument.p_decl'
is recursive but not used in its body
|
|
linux:
FStar.UInt.fsti#L436
(271) * Warning 271 at /home/runner/work/pulse/pulse/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
mac:
FStarC.Extraction.Krml.fst#L330
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/extraction/FStarC.Extraction.Krml.fst(330,8-330,19):
- Global binding
'FStarC.Extraction.Krml.decl_to_doc'
is recursive but not used in its body
|
|
mac:
FStarC.ToSyntax.ToSyntax.fst#L527
(319) * Warning 319 at /Users/runner/work/pulse/pulse/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(527,19-527,57):
- Effectful argument let _ = FStarC.Ident.string_of_lid _max_lid in
_ = "max" (FStarC.Effect.ALL) to erased function assert, consider let binding it
|
|
mac:
FStarC.ToSyntax.ToSyntax.fst#L509
(319) * Warning 319 at /Users/runner/work/pulse/pulse/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(509,13-509,48):
- Effectful argument let _ = FStarC.Ident.string_of_id _op_plus in
_ = "+" (FStarC.Effect.ALL) to erased function assert, consider let binding it
|
|
mac:
FStarC.Syntax.Resugar.fst#L327
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/syntax/FStarC.Syntax.Resugar.fst(327,8-327,26):
- Global binding
'FStarC.Syntax.Resugar.resugar_term_base''
is recursive but not used in its body
|
|
mac:
FStarC.Parser.ToDocument.fst#L1994
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1994,4-1994,12):
- Global binding
'FStarC.Parser.ToDocument.p_tmNoEq'
is recursive but not used in its body
|
|
mac:
FStarC.Parser.ToDocument.fst#L1730
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1730,4-1730,21):
- Global binding
'FStarC.Parser.ToDocument.p_maybeFocusArrow'
is recursive but not used in its body
|
|
mac:
FStarC.Parser.ToDocument.fst#L1095
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24):
- Global binding
'FStarC.Parser.ToDocument.p_disjunctivePattern'
is recursive but not used in its body
|
|
mac:
FStarC.Parser.ToDocument.fst#L756
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13):
- Global binding
'FStarC.Parser.ToDocument.p_justSig'
is recursive but not used in its body
|
|
mac:
FStarC.Parser.ToDocument.fst#L735
(328) * Warning 328 at /Users/runner/work/pulse/pulse/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14):
- Global binding
'FStarC.Parser.ToDocument.p_decl'
is recursive but not used in its body
|
|
mac:
FStar.UInt.fsti#L436
(271) * Warning 271 at /Users/runner/work/pulse/pulse/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
package-linux
|
176 MB |
sha256:0cade0feb4bb9792b93bfaa4ffadf0f4f4c77bb4bfa1ca923d8831c9e4058b11
|
|
|
package-mac
|
171 MB |
sha256:b5bff09133b745340defe02a2acbc3366c1326fb85bfe904bc5de00814cc75f0
|
|