Skip to content

Build everparse package (windows) #3

Build everparse package (windows)

Build everparse package (windows) #3

Manually triggered January 18, 2025 06:57
Status Failure
Total duration 26m 18s
Artifacts 2

package-windows.yml

on: workflow_dispatch
Fit to window
Zoom out
Zoom in

Annotations

1 error and 20 warnings
build
Unable to locate executable file: git. Please verify either the file path exists or the file can be found within a directory specified by the PATH environment variable. Also verify the file has a valid extension for an executable file.
fstar-src: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/everparse/everparse/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
fstar-src: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/everparse/everparse/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/everparse/everparse/ulib/FStar.UInt.fsti(435,8-435,51)
fstar-src: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/everparse/everparse/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
fstar-src: ulib/FStar.Stubs.Tactics.V2.Builtins.fsti#L446
(288) * Warning 288 at /home/runner/work/everparse/everparse/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/everparse/everparse/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)
fstar-src: ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/everparse/everparse/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
fstar-src: src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
fstar-src: src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
fstar-src: src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
fstar-src: src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
fstar-src: src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
fstar-binary: fstar/ulib/FStar.TSet.fst#L28
(318) * Warning 318 at c:/gh/2/_work/everparse/everparse/fstar/ulib/FStar.TSet.fst(28,4-28,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.
fstar-binary: fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at c:/gh/2/_work/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
fstar-binary: fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at c:/gh/2/_work/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 c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.UInt.fsti(435,8-435,51)
fstar-binary: fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at c:\gh\2\_work\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
fstar-binary: dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.WellFounded.fst(86,12-86,15)
fstar-binary: dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.WellFounded.fst(126,12-126,15)
fstar-binary: ulib/FStar.GSet.fst#L23
(318) * Warning 318 at ulib/FStar.GSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.
fstar-binary: ulib/FStar.GhostSet.fst#L23
(318) * Warning 318 at ulib/FStar.GhostSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.
fstar-binary: ulib/FStar.TSet.fst#L28
(318) * Warning 318 at ulib/FStar.TSet.fst(28,4-28,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.
fstar-binary: ulib/experimental/FStar.MST.fst#L222
(330) * Warning 330 at ulib/experimental/FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

Artifacts

Produced during runtime
Name Size
fstar-package
163 MB
package-src
4.22 MB