(318) * Warning 318 at /Users/runner/work/everparse/everparse/everparse/opt/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.

(242) * Warning 242 at /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59): - Definitions of inner let-rec get_acc and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.LexicographicOrdering.fst(124,10-124,17)

(242) * Warning 242 at /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59): - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.LexicographicOrdering.fst(75,14-75,28)

(242) * Warning 242 at /Users/runner/work/everparse/everparse/everparse/opt/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: /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.WellFounded.fst(126,12-126,15)

(242) * Warning 242 at /Users/runner/work/everparse/everparse/everparse/opt/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: /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.WellFounded.fst(86,12-86,15)

(318) * Warning 318 at /Users/runner/work/everparse/everparse/everparse/opt/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.

(271) * Warning 271 at /Users/runner/work/everparse/everparse/everparse/opt/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/everparse/everparse/everparse/opt/FStar/ulib/FStar.UInt.fsti(436,8-436,51)

(271) * Warning 271 at /Users/runner/work/everparse/everparse/everparse/opt/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

(271) * Warning 271 at /Users/runner/work/everparse/everparse/everparse/opt/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

(318) * Warning 318 at /Users/runner/work/everparse/everparse/everparse/opt/FStar/ulib/FStar.TSet.fst(26,4-26,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.

InvalidDefaultArgInFrom: Default value for ARG ghcr.io/$CI_REPO:$CI_BRANCH results in empty or invalid base image name More info: https://docs.docker.com/go/dockerfile/rule/invalid-default-arg-in-from/