Pulse nightly build #337
Annotations
20 warnings
|
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:
FStarC.Plugins.fst#L88
(337) * Warning 337 at /Users/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17):
- 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 '@'.
|
|
mac:
FStarC.Plugins.fst#L87
(337) * Warning 337 at /Users/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17):
- 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 '@'.
|
|
mac:
FStarC.Plugins.fst#L86
(337) * Warning 337 at /Users/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17):
- 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 '@'.
|
|
mac:
FStarC.Plugins.fst#L85
(337) * Warning 337 at /Users/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17):
- 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 '@'.
|
|
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
|
|
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:
FStarC.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17):
- 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 '@'.
|
|
linux:
FStarC.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17):
- 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 '@'.
|
|
linux:
FStarC.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17):
- 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 '@'.
|
|
linux:
FStarC.Plugins.fst#L85
(337) * Warning 337 at /home/runner/work/pulse/pulse/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17):
- 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 '@'.
|
|
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
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
package-linux
|
183 MB |
sha256:1a496578a2cd578993df737cd0653b50c0e62d0b4db546667873f4b11aa98209
|
|
|
package-mac
|
178 MB |
sha256:975146f25a47435a9b57566b6b95b57e9e2142503e63fad5792068ab6652e0e4
|
|