Skip to content

F* nightly build

F* nightly build #12

Manually triggered January 15, 2025 02:31
Status Failure
Total duration 20m 1s
Artifacts 3

nightly.yml

on: workflow_dispatch
build-all  /  ...  /  build-linux
1m 58s
build-all / build-windows / build-src / build-linux
build-all  /  ...  /  build-linux
19m 18s
build-all / build-linux / build-linux
build-all  /  ...  /  build-macos
19m 53s
build-all / build-macos / build-macos
build-all  /  ...  /  build-windows
28s
build-all / build-windows / build-windows
publish
0s
publish
Fit to window
Zoom out
Zoom in

Annotations

1 error and 21 warnings
build-all / build-windows / build-windows
Process completed with exit code 1.
build-all / build-windows / build-windows
No files were found with the provided path: fstar/fstar-*.zip. No artifacts will be uploaded.
build-all / build-linux / build-linux: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/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 / build-linux / build-linux: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/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 /home/runner/work/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51)
build-all / build-linux / build-linux: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/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 / build-linux / build-linux: ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L446
(288) * Warning 288 at /home/runner/work/FStar/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 /home/runner/work/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)
build-all / build-linux / build-linux: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/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 / build-linux / build-linux: src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/FStar/FStar/src/data/FStarC.Compiler.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 / build-linux / build-linux: src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/FStar/FStar/src/data/FStarC.Compiler.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 / build-linux / build-linux: src/basic/FStarC.Compiler.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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 / build-linux / build-linux: src/basic/FStarC.Compiler.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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 / build-linux / build-linux: src/basic/FStarC.Compiler.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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 / build-macos / build-macos: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar/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 / build-macos / build-macos: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar/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 /Users/runner/work/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51)
build-all / build-macos / build-macos: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar/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 / build-macos / build-macos: ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L446
(288) * Warning 288 at /Users/runner/work/FStar/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 /Users/runner/work/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)
build-all / build-macos / build-macos: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /Users/runner/work/FStar/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 / build-macos / build-macos: src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /Users/runner/work/FStar/FStar/src/data/FStarC.Compiler.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 / build-macos / build-macos: src/data/FStarC.Compiler.RBSet.fst#L105
(337) * Warning 337 at /Users/runner/work/FStar/FStar/src/data/FStarC.Compiler.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 / build-macos / build-macos: src/basic/FStarC.Compiler.Plugins.fst#L86
(337) * Warning 337 at /Users/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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 / build-macos / build-macos: src/basic/FStarC.Compiler.Plugins.fst#L87
(337) * Warning 337 at /Users/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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 / build-macos / build-macos: src/basic/FStarC.Compiler.Plugins.fst#L88
(337) * Warning 337 at /Users/runner/work/FStar/FStar/src/basic/FStarC.Compiler.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
152 MB
package-mac
143 MB
package-src
4.99 MB