Skip to content

F* nightly build

F* nightly build #40

Triggered via schedule February 11, 2025 00:59
Status Failure
Total duration 20m 14s
Artifacts 3

nightly.yml

on: schedule
build-all  /  ...  /  build
14m 56s
build-all / windows / build-src / build
Matrix: build-all / linux / smoke_test
Matrix: build-all / macos / smoke_test
build-all  /  ...  /  build
5m 3s
build-all / windows / build
build-all  /  ...  /  binary-smoke
0s
build-all / windows / binary-smoke
publish
0s
publish
Fit to window
Zoom out
Zoom in

Annotations

1 error and 30 warnings
build-all / windows / build
Process completed with exit code 2.
build-all / windows / build-src / build: stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/stage0/out/bin/../lib/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
build-all / windows / build-src / build: src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / windows / build-src / build: src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / windows / build-src / build: src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / windows / build-src / build: src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / windows / build-src / build: src/parser/FStarC.Parser.AST.fst#L766
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.AST.fst(766,8-766,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body
build-all / windows / build-src / build: src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body
build-all / windows / build-src / build: src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body
build-all / windows / build-src / build: src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body
build-all / windows / build-src / build: src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body
build-all / macos / build: stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar/FStar/stage0/out/bin/../lib/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
build-all / macos / build: src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /Users/runner/work/FStar/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 '@'.
build-all / macos / build: src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /Users/runner/work/FStar/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 '@'.
build-all / macos / build: src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /Users/runner/work/FStar/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 '@'.
build-all / macos / build: src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /Users/runner/work/FStar/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 '@'.
build-all / macos / build: src/parser/FStarC.Parser.AST.fst#L766
(328) * Warning 328 at /Users/runner/work/FStar/FStar/src/parser/FStarC.Parser.AST.fst(766,8-766,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body
build-all / macos / build: src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /Users/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body
build-all / macos / build: src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /Users/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body
build-all / macos / build: src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /Users/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body
build-all / macos / build: src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /Users/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body
build-all / linux / build: stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/stage0/out/bin/../lib/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
build-all / linux / build: src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / linux / build: src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / linux / build: src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / linux / build: src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/FStar/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 '@'.
build-all / linux / build: src/parser/FStarC.Parser.AST.fst#L766
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.AST.fst(766,8-766,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body
build-all / linux / build: src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body
build-all / linux / build: src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body
build-all / linux / build: src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body
build-all / linux / build: src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /home/runner/work/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

Artifacts

Produced during runtime
Name Size
package-linux
151 MB
package-mac
142 MB
package-src
4.24 MB