Skip to content

Updating Pulse code to new matcher (for taramana_cbor branch) #32

Updating Pulse code to new matcher (for taramana_cbor branch)

Updating Pulse code to new matcher (for taramana_cbor branch) #32

Triggered via pull request February 24, 2025 17:47
Status Success
Total duration 36m 47s
Artifacts 4

package-windows.yml

on: pull_request
Fit to window
Zoom out
Zoom in

Annotations

30 warnings
fstar-src: stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/everparse/everparse/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
fstar-src: src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /home/runner/work/everparse/everparse/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 '@'.
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-src: src/parser/FStarC.Parser.AST.fst#L772
(328) * Warning 328 at /home/runner/work/everparse/everparse/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body
fstar-src: src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /home/runner/work/everparse/everparse/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
fstar-src: src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /home/runner/work/everparse/everparse/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
fstar-src: src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /home/runner/work/everparse/everparse/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
fstar-src: src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /home/runner/work/everparse/everparse/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
fstar-binary: FStar.TSet.fst#L27
(318) * Warning 318 at C:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.TSet.fst(27,4-27,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.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.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.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 c:\gh\2\_work\everparse\everparse\fstar\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: c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.WellFounded.fst(86,12-86,15)
fstar-binary: dummy#L1
(242) * Warning 242 at c:\gh\2\_work\everparse\everparse\fstar\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: c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.WellFounded.fst(126,12-126,15)
fstar-binary: FStar.GSet.fst#L23
(318) * Warning 318 at c:\gh\2\_work\everparse\everparse\fstar\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: FStar.GhostSet.fst#L23
(318) * Warning 318 at c:\gh\2\_work\everparse\everparse\fstar\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: FStar.MST.fst#L222
(330) * Warning 330 at c:\gh\2\_work\everparse\everparse\fstar\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
fstar-binary: FStar.MST.fst#L247
(352) * Warning 352 at c:\gh\2\_work\everparse\everparse\fstar\ulib\experimental\FStar.MST.fst(247,42-247,60): - Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use
build: Spec.Loops.fst#L47
(328) * Warning 328 at Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body
build: dummy#L1
(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")
build: dummy#L1
(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")
build: dummy#L1
(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")
build: LowStar.Printf.fst#L253
(328) * Warning 328 at C:\gh\2\_work\everparse\everparse\__fstar-install\fstar\lib\fstar\ulib\LowStar.Printf.fst(253,8-253,13): - Global binding 'LowStar.Printf.arg_t' is recursive but not used in its body
build: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
build: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
build: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
build: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
build: FStar.Krml.Endianness.fst#L36
(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also FStar.Krml.Endianness.fst(36,4-36,28)

Artifacts

Produced during runtime
Name Size
everparse
128 MB
everparse-nupkg
126 MB
fstar-package
159 MB
package-src
4.24 MB