F* nightly build #28
Triggered via schedule
February 27, 2025 00:23
Status
Failure
Total duration
1d 1h 53m 59s
Artifacts
3
nightly.yml
on: schedule
build-all
/
...
/
build
2m 4s
build-all
/
...
/
build
19m 41s
build-all
/
...
/
build
20m 59s
publish
0s
Annotations
1 error and 20 warnings
build-all / windows / build
This request was automatically failed because there were no enabled runners online to process the request for more than 1 days.
|
build-all / linux / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar-1/FStar-1/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
|
build-all / linux / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar-1/FStar-1/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 /home/runner/work/FStar-1/FStar-1/ulib/FStar.UInt.fsti(435,8-435,51)
|
build-all / linux / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar-1/FStar-1/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
|
build-all / linux / build:
ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L448
(288) * Warning 288 at /home/runner/work/FStar-1/FStar-1/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 /home/runner/work/FStar-1/FStar-1/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)
|
build-all / linux / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar-1/FStar-1/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
|
build-all / linux / build:
src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / linux / build:
src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / linux / build:
src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / linux / build:
src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / linux / build:
src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / macos / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar-1/FStar-1/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
|
build-all / macos / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar-1/FStar-1/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 /Users/runner/work/FStar-1/FStar-1/ulib/FStar.UInt.fsti(435,8-435,51)
|
build-all / macos / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar-1/FStar-1/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
|
build-all / macos / build:
ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L448
(288) * Warning 288 at /Users/runner/work/FStar-1/FStar-1/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 /Users/runner/work/FStar-1/FStar-1/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)
|
build-all / macos / build:
ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar-1/FStar-1/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
|
build-all / macos / build:
src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /Users/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / macos / build:
src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /Users/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / macos / build:
src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /Users/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / macos / build:
src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /Users/runner/work/FStar-1/FStar-1/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 '@'.
|
build-all / macos / build:
src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /Users/runner/work/FStar-1/FStar-1/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 '@'.
|
Artifacts
Produced during runtime
Name | Size | |
---|---|---|
package-linux
|
151 MB |
|
package-mac
|
143 MB |
|
package-src
|
4.22 MB |
|