Replace Windows CI workflow with #165 #41
Triggered via pull request
January 21, 2025 23:37
Status
Success
Total duration
1h 17m 50s
Artifacts
–
Annotations
4 errors and 22 warnings
ci:
out.fail.batch/FAILAllBytesCompose.fst#L81
(66) * Error 66 at out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85):
- Failed to resolve implicit argument ?57
of type Prims.bool
introduced for Instantiating implicit argument
|
ci:
out.fail.batch/FAILAllBytesCompose.fst#L83
(12) * Error 12 at out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52):
- Expected type
EverParse3d.Interpreter.typ (*?u58*)
_
(*?u59*)
_
(*?u60*)
_
(*?u61*)
_
(*?u62*)
_
(*?u63*)
_
but
EverParse3d.Interpreter.T_with_comment "should_not_be_here"
(EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1)
"Validating field should_not_be_here"
has type
EverParse3d.Interpreter.typ kind__test1
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
false
false
|
ci:
ulib/Prims.fst#L459
(19) * Error 19 at out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16):
- Could not prove goal #1
- The SMT solver could not prove the query. Use --query_stats for more
details.
- See also ulib/Prims.fst(459,77-459,89)
|
ci:
out.fail.batch/FAILAllBytesNotLast.fst#L43
(189) * Error 189 at out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67):
- Expected expression of type
EverParse3d.Kinds.parser_kind (*?u58*)
_
EverParse3d.Kinds.WeakKindStrongPrefix
got expression EverParse3d.Kinds.kind_all_bytes
of type
EverParse3d.Kinds.parser_kind false
EverParse3d.Kinds.WeakKindConsumesAll
|
ci
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
ci:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/everparse/everparse/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
ci:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/everparse/everparse/FStar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /__w/everparse/everparse/FStar/ulib/FStar.UInt.fsti(435,8-435,51)
|
ci:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/everparse/everparse/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
ci:
FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L448
(288) * Warning 288 at /__w/everparse/everparse/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31):
- FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated
- Use Reflection.term_eq instead
- See also /__w/everparse/everparse/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)
|
ci:
FStar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/everparse/everparse/FStar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
ci:
FStar/src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/data/FStarC.RBSet.fst(105,30-105,31):
- 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 '@'.
|
ci:
FStar/src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/data/FStarC.RBSet.fst(105,36-105,37):
- 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 '@'.
|
ci:
FStar/src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/everparse/everparse/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 '@'.
|
ci:
FStar/src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/everparse/everparse/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 '@'.
|
ci:
FStar/src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/everparse/everparse/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 '@'.
|
ci:
dummy#L1
(361) * Warning 361 at LowParse.Spec.BoundedInt.fsti(232,0-235,62):
- Some #push-options have not been popped. Current depth is 1.
|
ci:
LowParse.Spec.Base.fsti#L544
(271) * Warning 271 at LowParse.Spec.Base.fsti(544,13-546,17):
- Pattern misses at least one bound variable: t
|
ci:
LowParse.Spec.Base.fsti#L546
(271) * Warning 271 at LowParse.Spec.Base.fsti(546,14-546,16):
- SMT pattern misses at least one bound variable: t
|
ci:
LowParse.Spec.Enum.fst#L107
(328) * Warning 328 at LowParse.Spec.Enum.fst(107,8-107,24):
- Global binding
'LowParse.Spec.Enum.assoc_flip_intro'
is recursive but not used in its body
|
ci:
dummy#L1
(361) * Warning 361 at LowParse.BitFields.fst(1276,0-1276,29):
- Some #push-options have not been popped. Current depth is 1.
|
ci:
LowParse.Spec.BitSum.fst#L1421
(331) * Warning 331 at LowParse.Spec.BitSum.fst(1421,7-1421,8):
- This name is being ignored
|
ci:
dummy#L1
(361) * Warning 361 at LowParse.Spec.BitSum.fst(2116,0-2141,57):
- Some #push-options have not been popped. Current depth is 2.
|
ci:
LowParse.Low.Base.Spec.fst#L487
(337) * Warning 337 at LowParse.Low.Base.Spec.fst(487,8-487,18):
- This definitions has multiple decreases clauses.
- The decreases clause on the declaration is ignored, please remove it.
|
ci:
LowParse.Low.Base.Spec.fst#L511
(328) * Warning 328 at LowParse.Low.Base.Spec.fst(511,8-511,24):
- Global binding
'LowParse.Low.Base.Spec.valid_list_equiv'
is recursive but not used in its body
|
ci:
LowParse.Low.Base.Spec.fst#L548
(337) * Warning 337 at LowParse.Low.Base.Spec.fst(548,8-548,21):
- This definitions has multiple decreases clauses.
- The decreases clause on the declaration is ignored, please remove it.
|
ciok
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|