Skip to content

Upgrade to F* Universes #345

Upgrade to F* Universes

Upgrade to F* Universes #345

Triggered via pull request February 28, 2026 16:19
Status Success
Total duration 41m 51s
Artifacts 1

package-linux.yml

on: pull_request
Fit to window
Zoom out
Zoom in

Annotations

12 warnings
build: FStarC.Extraction.Krml.fst#L330
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/extraction/FStarC.Extraction.Krml.fst(330,8-330,19): - Global binding 'FStarC.Extraction.Krml.decl_to_doc' is recursive but not used in its body
build: FStarC.ToSyntax.ToSyntax.fst#L527
(319) * Warning 319 at /home/runner/work/everparse/everparse/opt/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(527,19-527,57): - Effectful argument let _ = FStarC.Ident.string_of_lid _max_lid in _ = "max" (FStarC.Effect.ALL) to erased function assert, consider let binding it
build: FStarC.ToSyntax.ToSyntax.fst#L509
(319) * Warning 319 at /home/runner/work/everparse/everparse/opt/FStar/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(509,13-509,48): - Effectful argument let _ = FStarC.Ident.string_of_id _op_plus in _ = "+" (FStarC.Effect.ALL) to erased function assert, consider let binding it
build: FStarC.Syntax.Resugar.fst#L327
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/syntax/FStarC.Syntax.Resugar.fst(327,8-327,26): - Global binding 'FStarC.Syntax.Resugar.resugar_term_base'' is recursive but not used in its body
build: FStarC.Parser.ToDocument.fst#L1994
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/parser/FStarC.Parser.ToDocument.fst(1994,4-1994,12): - Global binding 'FStarC.Parser.ToDocument.p_tmNoEq' is recursive but not used in its body
build: FStarC.Parser.ToDocument.fst#L1730
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/parser/FStarC.Parser.ToDocument.fst(1730,4-1730,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body
build: FStarC.Parser.ToDocument.fst#L1095
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body
build: FStarC.Parser.ToDocument.fst#L756
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body
build: FStarC.Parser.ToDocument.fst#L735
(328) * Warning 328 at /home/runner/work/everparse/everparse/opt/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body
build: FStar.UInt.fsti#L436
(271) * Warning 271 at /home/runner/work/everparse/everparse/opt/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction
test: dummy#L0
(274) * Warning 274: - Implicitly opening namespace 'cddl.pulse.ast.det.' shadows module 'c' in file "/home/runner/work/everparse/everparse/test/krmllib/C.fst". - Rename "/home/runner/work/everparse/everparse/test/krmllib/C.fst" to avoid conflicts.
test: dummy#L0
(274) * Warning 274: - Implicitly opening namespace 'cddl.pulse.ast.det.' shadows module 'c' in file "/home/runner/work/everparse/everparse/test/krmllib/C.fst". - Rename "/home/runner/work/everparse/everparse/test/krmllib/C.fst" to avoid conflicts.

Artifacts

Produced during runtime
Name Size Digest
everparse
281 MB
sha256:96ba8bbdb5d91770aeb99cade4b4e362f3470198d5e10e60f2ca600c294fc053