Build:
- 0
2026-06-26 10:26.38: New job: build fstar.2026.03.24 (c98ad36ecd1a) 2026-06-26 10:26.38: Waiting for resource in pool day11-builds 2026-06-26 11:10.41: Got resource from pool day11-builds 2026-06-26 11:10.41: [profile full] build fstar.2026.03.24 2026-06-26 11:10.41: build fstar.2026.03.24 (c98ad36ecd1a) === DEPENDENCIES (39 transitive) === base-bytes.base 4691f51dd9fd base-threads.base c9e7bdbf5823 base-unix.base 7d1428be9ddb batteries.3.10.0 4588a8f55d48 camlp-streams.5.0.1 d48629cb1d21 conf-gmp.5 be11edf77089 conf-pkg-config.5 d5de2c6a88f9 cppo.1.8.0 5c4880c36377 dune.3.23.1 dc7ac21ea3be gen.1.1 c2ec000cc973 memtrace.0.2.3 71d19a0e8496 menhir.20260209 33fcc346f20f menhirCST.20260209 b78f18598292 menhirGLR.20260209 14503fb187dd menhirLib.20260209 b8ed5f168c3f menhirSdk.20260209 997f6d4de9b4 mtime.2.1.0 287d85022f99 num.1.6 3d665f14515a ocaml.5.4.1 71fed6f83b21 ocaml-base-compiler.5.4.1 4b8cbe74bda9 ocaml-compiler.5.4.1 df07189447bd ocaml-compiler-libs.v0.17.0 16db8c1cf256 ocaml-config.3 e4a06a221f09 ocamlbuild.0.16.1 17067329c57b ocamlfind.1.9.8 567e34ecf540 pprint.20230830 f1fa32f51e9c ppx_derivers.1.2.1 9db920257470 ppx_deriving.6.1.1 61fa95bb193b ppx_deriving_yojson.3.10.0 b2b69e6de53c ppxlib.0.38.0 778175ab9125 process.0.2.1 9838e41fb4f7 sedlex.3.7 5a4f234350b3 seq.base cf386be98197 sexplib0.v0.17.0 bc4140a6824d stdint.0.7.2 aab3bc1ad4d1 stdlib-shims.0.3.0 d3f2d28ed00d topkg.1.1.1 6f52f98db34d yojson.3.0.0 08149c2c002d zarith.1.14 442c15edac63 === STDOUT === Processing: [default: loading data] [fstar.2026.03.24: dl] [fstar.2026.03.24: extract] -> retrieved fstar.2026.03.24 (https://opam.ocaml.org/cache) [fstar: make 39] + /usr/bin/make "-j" "39" "ADMIT=1" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24) - DUNE BUILD - INSTALL LIB SRC - File "fstar-guts/FStarC_Parser_Parse.mly", line 129, characters 60-70: - Warning: the token LBRACK_BAR is unused. - File "fstar-guts/FStarC_Parser_Parse.mly", line 323, characters 0-15: - Warning: symbol decoratableDecl is unreachable from any of the start symbols. - File "fstar-guts/FStarC_Parser_Parse.mly", line 306, characters 0-16: - Warning: symbol noDecorationDecl is unreachable from any of the start symbols. - Warning: 20 states have shift/reduce conflicts. - Warning: 226 states have end-of-stream conflicts. - Warning: 302 shift/reduce conflicts were arbitrarily resolved. - Warning: 226 end-of-stream conflicts were arbitrarily resolved. - DUNE INSTALL - CHECK LIB - CHECK FSTARC - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib - CHECK Prims.fst - CHECK FStar.Attributes.fsti - CHECK FStar.NormSteps.fsti - CHECK FStar.Pervasives.Native.fst - CHECK FStar.NormSteps.fst - LAXCHECK Prims.fst - LAXCHECK FStar.Attributes.fsti - LAXCHECK FStar.NormSteps.fsti - LAXCHECK FStar.Pervasives.Native.fst - LAXCHECK FStar.NormSteps.fst - CHECK FStar.Pervasives.fsti - LAXCHECK FStar.Pervasives.fsti - LAXCHECK FStar.Prelude.fsti - LAXCHECK FStar.Pervasives.fst - LAXCHECK FStarC.Effect.fsti - LAXCHECK FStar.Preorder.fst - LAXCHECK FStar.Sealed.fsti - LAXCHECK FStar.Set.fsti - LAXCHECK FStar.Ghost.fsti - LAXCHECK FStar.Squash.fsti - LAXCHECK FStar.FunctionalExtensionality.fsti - LAXCHECK FStar.Mul.fst - LAXCHECK FStar.Classical.fsti - LAXCHECK FStar.Float.fsti - LAXCHECK FStar.Classical.Sugar.fsti - LAXCHECK FStar.ImmutableArray.Base.fsti - LAXCHECK FStarC.Array.fsti - LAXCHECK FStarC.VConfig.fsti - LAXCHECK FStarC.Errors.Codes.fsti - LAXCHECK FStarC.Reflection.V2.Interpreter.fsti - LAXCHECK FStar.Stubs.VConfig.fsti - LAXCHECK FStar.Order.fst - LAXCHECK FStarC.Sealed.fsti - LAXCHECK FStarC.NormSteps.fst - LAXCHECK FStar.Exn.fst - LAXCHECK FStarC.Hooks.fsti - LAXCHECK FStar.PropositionalExtensionality.fst - LAXCHECK FStar.Stubs.TypeChecker.Core.fsti - LAXCHECK FStarC.Reflection.V1.Interpreter.fsti - LAXCHECK FStar.Reflection.Const.fst - LAXCHECK FStar.Math.Lib.fst - LAXCHECK FStar.Math.Lemmas.fsti - LAXCHECK FStar.Monotonic.Witnessed.fsti - LAXCHECK FStar.Range.fsti - LAXCHECK FStar.Sealed.Inhabited.fst - LAXCHECK FStarC.Sealed.fst - LAXCHECK FStar.List.Tot.Base.fst - LAXCHECK FStar.Monotonic.Pure.fst - LAXCHECK FStar.Classical.Sugar.fst - LAXCHECK FStarC.Int.Extra.fsti - LAXCHECK FStarC.PSMap.fsti - LAXCHECK FStarC.PIMap.fsti - LAXCHECK FStarC.Order.fsti - LAXCHECK FStarC.Json.fsti - LAXCHECK FStarC.Thunk.fsti - LAXCHECK FStarC.Hash.fsti - LAXCHECK FStarC.Unionfind.fsti - LAXCHECK FStarC.Dyn.fsti - LAXCHECK FStarC.SMap.fsti - LAXCHECK FStarC.Option.fsti - LAXCHECK FStarC.Debug.fsti - LAXCHECK FStarC.List.fsti - LAXCHECK FStarC.Misc.fsti - LAXCHECK FStarC.Stats.fsti - LAXCHECK FStarC.Profiling.fsti - LAXCHECK FStarC.GenSym.fsti - LAXCHECK FStarC.Filepath.fsti - LAXCHECK FStarC.Find.fsti - LAXCHECK FStarC.Platform.Base.fsti - LAXCHECK FStarC.Options.Ext.fsti - LAXCHECK FStar.PredicateExtensionality.fst - LAXCHECK FStarC.IMap.fsti - LAXCHECK FStarC.Interactive.Ide.fsti - LAXCHECK FStarC.Timing.fsti - LAXCHECK FStarC.OCaml.fsti - LAXCHECK FStarC.Prettyprint.fsti - LAXCHECK FStarC.Plugins.Base.fsti - LAXCHECK FStar.Calc.fsti - LAXCHECK FStar.Set.fst - LAXCHECK FStarC.Hints.fsti - LAXCHECK FStar.Ghost.fst - CHECK FStar.Prelude.fsti - LAXCHECK FStarC.EditDist.fsti - LAXCHECK FStarC.Thunk.fst - LAXCHECK FStar.Classical.fst - CHECK FStar.Pervasives.fst - LAXCHECK FStar.Monotonic.Witnessed.fst - LAXCHECK FStar.Stubs.Reflection.Types.fsti - LAXCHECK FStar.TSet.fsti - LAXCHECK FStar.ErasedLogic.fst - LAXCHECK FStarC.VConfig.fst - LAXCHECK FStarC.Format.fsti - LAXCHECK FStar.IndefiniteDescription.fsti - LAXCHECK FStarC.Option.fst - LAXCHECK FStarC.GenSym.fst - LAXCHECK FStarC.Real.fsti - LAXCHECK FStarC.Order.fst - LAXCHECK FStarC.Common.fsti - LAXCHECK FStarC.Plugins.fsti - LAXCHECK FStar.Calc.fst - LAXCHECK FStar.Reflection.TermEq.Simple.fsti - LAXCHECK FStar.Stubs.Syntax.Syntax.fsti - LAXCHECK FStar.Stubs.Tactics.Types.Reflection.fsti - LAXCHECK FStar.StrongExcludedMiddle.fst - LAXCHECK FStar.IndefiniteDescription.fst - LAXCHECK FStar.Squash.fst - LAXCHECK FStar.Monotonic.Heap.fsti - LAXCHECK FStar.TSet.fst - CHECK FStar.Classical.Sugar.fsti - CHECK FStar.Mul.fst - CHECK FStar.Ghost.fsti - CHECK FStar.Sealed.fsti - CHECK FStar.Float.fsti - CHECK FStar.Preorder.fst - CHECK FStar.Set.fsti - CHECK FStar.ReflexiveTransitiveClosure.fsti - CHECK FStar.Stubs.VConfig.fsti - CHECK FStar.Tactics.Logic.Lemmas.fsti - CHECK FStar.Squash.fsti - CHECK FStar.Order.fst - CHECK FStar.Stubs.TypeChecker.Core.fsti - CHECK FStar.Reflection.Const.fst - CHECK FStar.Classical.fsti - CHECK FStar.Exn.fst - CHECK FStar.PropositionalExtensionality.fst - CHECK FStar.Real.fsti - CHECK FStar.RefinementExtensionality.fsti - CHECK FStar.FunctionalExtensionality.fsti - CHECK FStar.PartialMap.fsti - CHECK FStar.Sequence.Base.fsti - CHECK FStar.DependentMap.fsti - CHECK FStar.Bijection.fsti - CHECK FStar.Functions.fsti - CHECK FStar.Dyn.fsti - CHECK FStar.MarkovsPrinciple.fst - CHECK FStar.Constructive.fst - CHECK FStar.ImmutableArray.Base.fsti - CHECK FStar.Universe.fsti - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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. - - LAXCHECK FStar.Math.Lemmas.fst - CHECK FStar.Exception.fsti - CHECK FStar.Parse.fst - LAXCHECK FStarC.Errors.Codes.fst - CHECK FStar.Date.fsti - CHECK FStar.List.Tot.Base.fst - CHECK FStar.Math.Lemmas.fsti - CHECK FStar.Range.fsti - CHECK FStar.Monotonic.Pure.fst - CHECK FStar.Sealed.Inhabited.fst - CHECK FStar.Algebra.CommMonoid.Equiv.fst - CHECK FStar.Math.Euclid.fsti - CHECK FStar.Algebra.CommMonoid.fst - CHECK FStar.Tactics.Canon.Lemmas.fsti - CHECK FStar.Math.Lib.fst - CHECK FStar.Classical.fst - CHECK FStar.Classical.Sugar.fst - CHECK FStar.Universe.fst - CHECK FStar.Monotonic.Witnessed.fsti - CHECK FStar.Dyn.fst - CHECK FStar.Algebra.Monoid.fst - CHECK FStar.Witnessed.Core.fsti - CHECK FStar.IndefiniteDescription.fsti - CHECK FStar.IFC.fsti - CHECK FStar.ErasedLogic.fst - CHECK FStar.PCM.fst - CHECK FStar.Ghost.fst - LAXCHECK FStar.Seq.Base.fsti - LAXCHECK FStar.List.Tot.Properties.fsti - CHECK FStar.Cardinality.Cantor.fsti - CHECK FStar.TSet.fsti - CHECK FStar.GSet.fsti - CHECK FStar.Map.fsti - CHECK FStar.GhostSet.fsti - CHECK FStar.Monotonic.Witnessed.fst - CHECK FStar.Stubs.Reflection.Types.fsti - CHECK FStar.Calc.fsti - CHECK FStar.PartialMap.fst - CHECK FStar.PredicateExtensionality.fst - CHECK FStar.Set.fst - CHECK FStar.StrongExcludedMiddle.fst - CHECK FStar.DependentMap.fst - CHECK FStar.SquashProperties.fst - CHECK FStar.IndefiniteDescription.fst - CHECK FStar.Witnessed.Core.fst - CHECK FStar.WellFounded.fst - CHECK FStar.Squash.fst - CHECK FStar.Tactics.Logic.Lemmas.fst - CHECK FStar.Bijection.fst - CHECK FStar.MSTTotal.fst - CHECK FStar.Tactics.Canon.Lemmas.fst - CHECK FStar.Cardinality.Universes.fsti - CHECK FStar.Cardinality.Cantor.fst - LAXCHECK FStar.Monotonic.Heap.fst - CHECK FStar.Stubs.Syntax.Syntax.fsti - LAXCHECK FStar.Heap.fst - CHECK FStar.Stubs.Tactics.Types.Reflection.fsti - CHECK FStar.Reflection.TermEq.Simple.fsti - CHECK FStar.Math.Fermat.fsti - CHECK FStar.ExtractAs.fst - CHECK FStar.Functions.fst - LAXCHECK FStar.BitVector.fsti - CHECK FStar.RefinementExtensionality.fst - CHECK FStar.IFC.fst - CHECK FStar.Calc.fst - CHECK FStar.Monotonic.Heap.fsti - LAXCHECK FStar.ST.fst - CHECK FStar.GhostSet.fst - CHECK FStar.TSet.fst - CHECK FStar.GSet.fst - CHECK FStar.Map.fst - CHECK FStar.Cardinality.Universes.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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. - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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. - - CHECK FStar.WellFounded.Util.fsti - CHECK FStar.LexicographicOrdering.fsti - CHECK FStar.WellFoundedRelation.fsti - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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. - - LAXCHECK FStar.All.fsti - CHECK FStar.Sequence.Util.fst - CHECK FStar.Sequence.Ambient.fst - LAXCHECK FStar.List.Tot.fst - LAXCHECK FStar.List.Tot.Properties.fst - LAXCHECK FStar.UInt.fsti - CHECK FStar.NMSTTotal.fst - CHECK FStar.MST.fst - LAXCHECK FStar.Seq.Base.fst - LAXCHECK FStar.Seq.Properties.fsti - LAXCHECK FStar.List.fst - CHECK FStar.Universe.PCM.fst - CHECK FStar.Sequence.fst - CHECK FStar.Math.Lemmas.fst - CHECK FStar.WellFoundedRelation.fst - CHECK FStar.Sequence.Permutation.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 352 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.Seq.Base.fsti - CHECK FStar.List.Tot.Properties.fsti - CHECK FStar.BigOps.fsti - CHECK FStar.Tactics.CanonCommSwaps.fst - CHECK FStar.List.Pure.Base.fst - CHECK FStar.NMST.fst - CHECK FStar.Sequence.Permutation.fst - LAXCHECK FStar.UInt32.fsti - CHECK FStar.Monotonic.HyperHeap.fsti - CHECK FStar.Heap.fst - CHECK FStar.Monotonic.Heap.fst - CHECK FStar.LexicographicOrdering.fst - LAXCHECK FStar.Char.fsti - LAXCHECK FStar.UInt32.fst - CHECK FStar.Relational.Relational.fst - CHECK FStar.ST.fst - CHECK FStar.TwoLevelHeap.fst - CHECK FStar.Axiomatic.Array.fst - LAXCHECK FStar.Pprint.fsti - LAXCHECK FStarC.BaseTypes.fsti - LAXCHECK FStar.Stubs.Reflection.V2.Data.fsti - LAXCHECK FStarC.String.fsti - LAXCHECK FStar.String.fsti - LAXCHECK FStar.Seq.fst - LAXCHECK FStar.Seq.Properties.fst - CHECK FStar.BitVector.fsti - CHECK FStar.IntegerIntervals.fst - LAXCHECK FStarC.Util.fsti - LAXCHECK FStarC.Getopt.fsti - LAXCHECK FStar.BitVector.fst - * Warning 290 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.WellFoundedRelation.fst(152,21-152,46): - - In the decreases clause for this function, the SMT solver may not be able to - prove that the types of - wfr_a.decreaser (FStar.Pervasives.dfst xy) - (bound in - FStar.WellFoundedRelation.fst(152,21-152,46)) - and - wfr_a.decreaser (FStar.Pervasives.dfst xy) - (bound in - FStar.WellFoundedRelation.fst(152,21-152,46)) - are equal. - - The type of the first term is: - FStar.WellFoundedRelation.acc_classical wfr_a.relation - (FStar.Pervasives.dfst xy) - - The type of the second term is: - FStar.WellFoundedRelation.acc_classical wfr_a.relation - (FStar.Pervasives.dfst xy) - - If the proof fails, try annotating these with the same type. - - LAXCHECK FStar.UInt.fst - LAXCHECK FStarC.EditDist.fst - LAXCHECK FStarC.Debug.fst - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/experimental/FStar.NMST.fst(200,45-200,58): - - Polymonadic binds ((DIV, NMSTATE) |> NMSTATE) 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 - - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/experimental/FStar.NMST.fst(200,45-200,58): - - Polymonadic binds ((DIV, NMSTATE) |> NMSTATE) 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 - - LAXCHECK FStar.Stubs.Errors.Msg.fsti - LAXCHECK FStar.Issue.fsti - * Warning 352 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/experimental/FStar.NMST.fst(224,45-224,65): - - Combinator FStar.NMSTTotal.NMSTATETOT ~> FStar.NMST.NMSTATE is not a - substitutive indexed effect combinator, it is better to make it one if - possible for better performance and ease of use - - CHECK FStar.Monotonic.HyperStack.fsti - LAXCHECK FStar.Stubs.Tactics.Common.fsti - CHECK FStar.All.fsti - CHECK FStar.Ref.fst - CHECK FStar.MRef.fsti - LAXCHECK FStar.Stubs.Reflection.V2.Builtins.fsti - LAXCHECK FStar.Reflection.V2.Compare.fsti - LAXCHECK FStar.Stubs.Tactics.Types.fsti - CHECK FStar.Relational.Comp.fst - CHECK FStar.Option.fst - LAXCHECK FStarC.Pprint.fsti - LAXCHECK FStarC.StringBuffer.fsti - CHECK FStar.MRef.fst - LAXCHECK FStarC.Misc.fst - LAXCHECK FStar.Reflection.V2.Collect.fst - LAXCHECK FStar.Reflection.TermEq.fsti - LAXCHECK FStar.Tactics.Effect.fsti - CHECK FStar.List.Tot.fst - CHECK FStar.List.Pure.Properties.fst - CHECK FStar.List.Tot.Properties.fst - LAXCHECK FStarC.Common.fst - LAXCHECK FStarC.Find.Z3.fsti - LAXCHECK FStar.Reflection.V2.Derived.Lemmas.fst - LAXCHECK FStar.Reflection.V2.Derived.fst - CHECK FStar.Seq.Properties.fsti - CHECK FStar.List.fst - CHECK FStar.OrdSet.fsti - CHECK FStar.Monotonic.HyperHeap.fst - CHECK FStar.FiniteSet.Base.fsti - LAXCHECK FStar.Reflection.TermEq.fst - CHECK FStar.Seq.Base.fst - CHECK FStar.ImmutableArray.fsti - CHECK FStar.Sequence.Base.fst - LAXCHECK FStar.Reflection.TermEq.Simple.fst - LAXCHECK FStar.Tactics.Effect.fst - LAXCHECK FStar.Tactics.Util.fst - LAXCHECK FStar.Tactics.Typeclasses.fsti - LAXCHECK FStar.Tactics.NamedView.fsti - LAXCHECK FStar.Tactics.Names.fsti - LAXCHECK FStar.Stubs.Tactics.Unseal.fsti - CHECK FStar.UInt.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.UInt.fst(296,8-296,25): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.UInt.fsti(436,8-436,51) - - LAXCHECK FStar.Stubs.Tactics.V2.Builtins.fsti - LAXCHECK FStarC.Class.Listlike.fsti - LAXCHECK FStarC.Class.Deq.fsti - LAXCHECK FStarC.Class.Monoid.fsti - LAXCHECK FStarC.Class.Show.fsti - LAXCHECK FStarC.Class.Tagged.fsti - LAXCHECK FStarC.Errors.Msg.fsti - LAXCHECK FStarC.Class.Monad.fsti - LAXCHECK FStar.Tactics.Visit.fst - LAXCHECK FStar.Reflection.V2.Compare.fst - LAXCHECK FStar.Reflection.V2.fst - LAXCHECK FStarC.Path.fsti - LAXCHECK FStarC.Class.Deq.fst - LAXCHECK FStarC.Class.Ord.fsti - LAXCHECK FStarC.Class.PP.fsti - LAXCHECK FStarC.Options.fsti - LAXCHECK FStarC.Find.fst - LAXCHECK FStarC.Time.fsti - LAXCHECK FStarC.Platform.fsti - LAXCHECK FStarC.Options.Ext.fst - LAXCHECK FStarC.Class.Show.fst - LAXCHECK FStarC.Class.Monoid.fst - LAXCHECK FStarC.Class.Tagged.fst - LAXCHECK FStarC.Class.Listlike.fst - LAXCHECK FStarC.Errors.Msg.fst - LAXCHECK FStarC.Writer.fsti - LAXCHECK FStarC.Class.Monad.fst - LAXCHECK FStarC.Path.fst - LAXCHECK FStar.Tactics.V2.SyntaxCoercions.fst - LAXCHECK FStar.Reflection.V2.Formula.fst - LAXCHECK FStar.FunctionalExtensionality.fst - LAXCHECK FStar.Tactics.NamedView.fst - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fsti - LAXCHECK FStarC.Range.Type.fsti - LAXCHECK FStarC.CList.fsti - LAXCHECK FStarC.Class.Setlike.fsti - LAXCHECK FStarC.Class.Ord.fst - LAXCHECK FStarC.Class.Hashable.fsti - LAXCHECK FStarC.Stats.fst - LAXCHECK FStarC.OCaml.fst - LAXCHECK FStarC.Real.fst - LAXCHECK FStarC.Platform.fst - LAXCHECK FStarC.Class.PP.fst - LAXCHECK FStar.Tactics.Names.fst - LAXCHECK FStarC.Class.HasRange.fsti - LAXCHECK FStarC.Range.Ops.fsti - LAXCHECK FStarC.Range.Type.fst - LAXCHECK FStarC.Writer.fst - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fst - CHECK FStar.FiniteSet.Ambient.fst - CHECK FStar.FiniteMap.Base.fsti - LAXCHECK FStarC.Range.fsti - CHECK FStar.FiniteSet.Base.fst - LAXCHECK FStarC.CList.fst - LAXCHECK FStarC.HashMap.fsti - LAXCHECK FStarC.Class.Hashable.fst - LAXCHECK FStarC.Options.fst - LAXCHECK FStarC.Find.Z3.fst - CHECK FStar.HyperStack.fst - LAXCHECK FStarC.Profiling.fst - CHECK FStar.Monotonic.HyperStack.fst - LAXCHECK FStarC.FlatSet.fsti - LAXCHECK FStarC.RBSet.fsti - LAXCHECK FStarC.Class.Setlike.fst - LAXCHECK FStarC.Ident.fsti - LAXCHECK FStarC.Range.Ops.fst - LAXCHECK FStarC.Errors.fsti - LAXCHECK FStarC.Class.HasRange.fst - LAXCHECK FStarC.FlatSet.fst - LAXCHECK FStarC.HashMap.fst - LAXCHECK FStarC.RBSet.fst - CHECK FStar.List.Pure.fst - LAXCHECK FStarC.Const.fsti - LAXCHECK FStarC.Interactive.CompletionTable.fsti - LAXCHECK FStarC.Parser.Const.Tuples.fsti - LAXCHECK FStarC.Ident.fst - LAXCHECK FStar.Tactics.V2.Derived.fst - CHECK FStar.Util.fst - CHECK FStar.HyperStack.ST.fsti - LAXCHECK FStarC.Parser.Const.Tuples.fst - CHECK FStar.OrdMap.fsti - CHECK FStar.OrdSet.fst - CHECK FStar.OrdSetProps.fst - LAXCHECK FStarC.Syntax.Syntax.fsti - LAXCHECK FStarC.Extraction.ML.Syntax.fsti - LAXCHECK FStarC.Parser.Const.fst - LAXCHECK FStarC.Const.fst - LAXCHECK FStarC.Interactive.JsonHelper.fsti - LAXCHECK FStarC.Plugins.fst - LAXCHECK FStarC.Errors.fst - LAXCHECK FStarC.Interactive.CompletionTable.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.FiniteMap.Ambient.fst - CHECK FStar.OrdMap.fst - CHECK FStar.OrdMapProps.fst - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fsti - LAXCHECK FStarC.Extraction.ML.Syntax.fst - LAXCHECK FStarC.Extraction.ML.Code.fsti - LAXCHECK FStarC.Extraction.ML.PrintML.fsti - LAXCHECK FStarC.Extraction.ML.PrintFS.fsti - LAXCHECK FStar.Tactics.Typeclasses.fst - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fst - CHECK FStar.UInt32.fsti - CHECK FStar.BV.fsti - LAXCHECK FStarC.Extraction.ML.PrintFS.fst - CHECK FStar.ModifiesGen.fsti - CHECK LowStar.Failure.fsti - CHECK FStar.HyperStack.All.fst - CHECK LowStar.Comment.fsti - CHECK FStar.Monotonic.Map.fst - CHECK LowStar.Ignore.fsti - CHECK FStar.Monotonic.DependentMap.fsti - CHECK FStar.HyperStack.ST.fst - CHECK FStar.Seq.Equiv.fsti - CHECK FStar.Seq.fst - CHECK FStar.Seq.Properties.fst - CHECK FStar.HyperStack.IO.fst - CHECK LowStar.Comment.fst - CHECK FStar.Char.fsti - CHECK FStar.UInt16.fsti - CHECK FStar.UInt8.fsti - CHECK FStar.UInt64.fsti - CHECK FStar.UInt32.fst - CHECK FStar.Vector.Base.fsti - CHECK FStar.Int.fsti - CHECK FStar.BitVector.fst - CHECK FStar.FunctionalQueue.fsti - CHECK FStar.Buffer.fst - CHECK FStar.Array.fsti - CHECK FStar.UInt.fst - CHECK FStar.Seq.Sorted.fst - CHECK FStar.Sequence.Seq.fsti - CHECK FStar.Fin.fsti - CHECK FStar.Monotonic.Seq.fst - CHECK FStar.Matrix2.fsti - CHECK FStar.Monotonic.DependentMap.fst - CHECK FStar.BV.fst - CHECK FStar.Tactics.BV.Lemmas.fsti - CHECK FStar.Pprint.fsti - CHECK FStar.Stubs.Reflection.V2.Data.fsti - CHECK FStar.String.fsti - CHECK FStar.Seq.Permutation.fsti - CHECK FStar.Seq.Equiv.fst - CHECK FStar.Sequence.Seq.fst - CHECK FStar.UInt16.fst - CHECK FStar.FunctionalQueue.fst - CHECK FStar.UInt64.fst - CHECK FStar.UInt128.fsti - CHECK FStar.SizeT.fsti - CHECK FStar.Fin.fst - CHECK FStar.UInt8.fst - CHECK FStar.Endianness.fsti - CHECK FStar.IO.fsti - LAXCHECK FStarC.TypeChecker.Common.fsti - LAXCHECK FStarC.Parser.AST.fsti - LAXCHECK FStarC.Class.Binders.fsti - LAXCHECK FStarC.Syntax.Subst.fsti - LAXCHECK FStarC.SMTEncoding.Term.fsti - LAXCHECK FStarC.Syntax.Embeddings.Base.fsti - LAXCHECK FStarC.Reflection.V2.Data.fsti - LAXCHECK FStarC.Syntax.Unionfind.fsti - CHECK FStar.Issue.fsti - CHECK FStar.Stubs.Errors.Msg.fsti - LAXCHECK FStarC.Tactics.Common.fsti - CHECK FStar.Array.fst - CHECK FStar.Stubs.Tactics.Common.fsti - CHECK FStar.Tactics.BV.Lemmas.fst - LAXCHECK FStarC.Syntax.InstFV.fsti - LAXCHECK FStarC.Syntax.Free.fsti - LAXCHECK FStarC.Reflection.V1.Data.fsti - LAXCHECK FStarC.Reflection.V1.Constants.fst - CHECK FStar.Algebra.CommMonoid.Fold.fsti - CHECK FStar.Vector.Properties.fst - CHECK FStar.Vector.Base.fst - LAXCHECK FStarC.Reflection.V2.Constants.fst - CHECK FStar.Seq.Permutation.fst - LAXCHECK FStarC.Defensive.fsti - CHECK FStar.Stubs.Tactics.Types.fsti - LAXCHECK FStarC.Syntax.Visit.fsti - CHECK FStar.Error.fst - LAXCHECK FStarC.Syntax.Formula.fsti - LAXCHECK FStarC.Syntax.Compress.fsti - LAXCHECK FStarC.Syntax.Hash.fsti - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.HyperStack.ST.fst(317,4-317,8): - - Values of type `drgn` will be erased during extraction, but its interface - hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val drgn` declaration - for this symbol in the interface - - LAXCHECK FStarC.Syntax.Subst.fst - LAXCHECK FStarC.Syntax.MutRecTy.fsti - LAXCHECK FStarC.Syntax.TermHashTable.fsti - LAXCHECK FStarC.Syntax.Print.Ugly.fsti - LAXCHECK FStarC.Syntax.InstFV.fst - LAXCHECK FStarC.Parser.Const.ExtractAs.fsti - LAXCHECK FStarC.Syntax.VisitM.fsti - LAXCHECK FStarC.Class.Binders.fst - CHECK FStar.Stubs.Reflection.V2.Builtins.fsti - CHECK FStar.Reflection.V2.Compare.fsti - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fsti - LAXCHECK FStarC.Syntax.Unionfind.fst - LAXCHECK FStarC.Tactics.Common.fst - LAXCHECK FStarC.Syntax.Syntax.fst - CHECK FStar.Int64.fsti - CHECK FStar.Int32.fsti - CHECK FStar.Int8.fsti - CHECK FStar.Matrix.fsti - CHECK FStar.Algebra.CommMonoid.Fold.Nested.fsti - LAXCHECK FStarC.Syntax.Embeddings.fsti - LAXCHECK FStarC.Syntax.Util.fsti - LAXCHECK FStarC.Syntax.Free.fst - CHECK FStar.Algebra.CommMonoid.Fold.fst - LAXCHECK FStarC.Reflection.V2.Data.fst - LAXCHECK FStarC.Reflection.V1.Data.fst - LAXCHECK FStarC.Syntax.VisitM.fst - LAXCHECK FStarC.Syntax.Visit.fst - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fst - CHECK FStar.Int16.fsti - CHECK FStar.Int.fst - CHECK FStar.Tactics.Effect.fsti - CHECK FStar.Vector.fst - CHECK FStar.Endianness.fst - CHECK FStar.Reflection.V1.Compare.fsti - CHECK FStar.Int128.fsti - LAXCHECK FStarC.SMTEncoding.UnsatCore.fsti - CHECK FStar.Int64.fst - LAXCHECK FStarC.SMTEncoding.Pruning.fsti - LAXCHECK FStarC.SMTEncoding.Term.fst - CHECK FStar.Reflection.V2.Collect.fst - CHECK FStar.Stubs.Reflection.V1.Data.fsti - CHECK FStar.Reflection.TermEq.fsti - CHECK FStar.Int32.fst - LAXCHECK FStarC.SMTEncoding.SolverState.fsti - LAXCHECK FStarC.SMTEncoding.UnsatCore.fst - CHECK FStar.Tactics.SMT.fsti - CHECK FStar.Tactics.LaxTermEq.fsti - CHECK FStar.Tactics.Easy.fsti - CHECK FStar.Tactics.Typeclasses.fsti - CHECK FStar.Tactics.MApply0.fsti - CHECK FStar.Tactics.NamedView.fsti - LAXCHECK FStarC.SMTEncoding.Pruning.fst - CHECK FStar.Stubs.Tactics.Unseal.fsti - CHECK FStar.Tactics.Util.fst - CHECK FStar.Tactics.Print.fsti - CHECK FStar.Tactics.Names.fsti - LAXCHECK FStarC.Parser.Dep.fsti - CHECK FStar.Tactics.Effect.fst - CHECK FStar.InteractiveHelpers.Propositions.fsti - LAXCHECK FStarC.Parser.AST.Util.fsti - CHECK LowStar.Monotonic.Buffer.fsti - LAXCHECK FStarC.Parser.ToDocument.fsti - LAXCHECK FStarC.Parser.AST.Diff.fsti - CHECK FStar.Tactics.Canon.fsti - CHECK FStar.Tactics.Parametricity.fsti - CHECK FStar.Tactics.BV.fsti - LAXCHECK FStarC.Syntax.Hash.fst - CHECK FStar.Tactics.MkProjectors.fsti - CHECK FStar.Int8.fst - CHECK FStar.Int16.fst - CHECK FStar.Pointer.Base.fsti - CHECK FStar.Int.Cast.fst - CHECK FStar.Class.TotalOrder.Raw.fst - CHECK FStar.Printf.fst - CHECK FStar.Int128.fst - LAXCHECK FStarC.Syntax.Print.Ugly.fst - CHECK FStar.PtrdiffT.fsti - CHECK FStar.Class.Printable.fst - LAXCHECK FStarC.Parser.Const.ExtractAs.fst - LAXCHECK FStarC.Syntax.Util.fst - CHECK FStar.Class.Add.fst - LAXCHECK FStarC.Parser.AST.fst - CHECK FStar.Stubs.Tactics.V2.Builtins.fsti - CHECK FStar.Reflection.V2.Derived.fst - CHECK FStar.Reflection.V2.Derived.Lemmas.fst - LAXCHECK FStarC.Syntax.MutRecTy.fst - LAXCHECK FStarC.Parser.ToDocument.fst - CHECK FStar.Class.Eq.Raw.fst - CHECK FStar.Integers.fst - CHECK FStar.Reflection.TermEq.Simple.fst - CHECK FStar.Reflection.TermEq.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.Math.Euclid.fst - CHECK FStar.Tactics.Visit.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.UInt.fst(296,8-296,25): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.UInt.fsti(436,8-436,51) - - CHECK FStar.Stubs.Reflection.V1.Builtins.fsti - CHECK FStar.Matrix.fst - CHECK FStar.Algebra.CommMonoid.Fold.Nested.fst - LAXCHECK FStarC.Syntax.DsEnv.fsti - LAXCHECK FStarC.Parser.ParseIt.fsti - LAXCHECK FStarC.Dependencies.fsti - LAXCHECK FStarC.SMTEncoding.Z3.fsti - LAXCHECK FStarC.Parser.AST.Util.fst - CHECK FStar.Class.Ord.Raw.fsti - CHECK FStar.Class.Eq.fst - LAXCHECK FStarC.Parser.AST.Diff.fst - CHECK FStar.Tactics.V2.SyntaxCoercions.fst - CHECK FStar.Reflection.V2.Formula.fst - LAXCHECK FStarC.Dependencies.fst - CHECK FStar.Reflection.V1.Derived.fst - CHECK FStar.Stubs.Tactics.V1.Builtins.fsti - CHECK FStar.Tactics.SMT.fst - CHECK FStar.Reflection.V2.Compare.fst - CHECK FStar.Tactics.LaxTermEq.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.ModifiesGen.fst - LAXCHECK FStarC.Parser.Driver.fsti - LAXCHECK FStarC.SMTEncoding.Z3.fst - CHECK FStar.FunctionalExtensionality.fst - CHECK FStar.Int.Cast.Full.fst - LAXCHECK FStarC.ToSyntax.TickedVars.fsti - CHECK FStar.Tactics.Names.fst - CHECK FStar.Tactics.Builtins.fsti - CHECK FStar.Reflection.V2.fst - LAXCHECK FStarC.ToSyntax.Interleave.fsti - CHECK FStar.SizeT.fst - CHECK FStar.RBMap.fsti - LAXCHECK FStarC.Syntax.DsEnv.fst - CHECK FStar.RBSet.fsti - CHECK FStar.Class.Ord.Raw.fst - LAXCHECK FStarC.TypeChecker.Env.fsti - LAXCHECK FStarC.Syntax.Print.fsti - LAXCHECK FStarC.Syntax.Print.Pretty.fsti - LAXCHECK FStarC.Syntax.Resugar.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Buffer.fst(1004,2-1004,69): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Addition - - CHECK FStar.Tactics.MApply.fsti - CHECK FStar.Reflection.V1.Derived.Lemmas.fst - LAXCHECK FStarC.ToSyntax.ToSyntax.fsti - CHECK FStar.Reflection.V1.Formula.fst - LAXCHECK FStarC.Prettyprint.fst - LAXCHECK FStarC.ToSyntax.TickedVars.fst - LAXCHECK FStarC.ToSyntax.Interleave.fst - LAXCHECK FStarC.Parser.Dep.fst - CHECK FStar.RBMap.fst - LAXCHECK FStarC.TypeChecker.Common.fst - CHECK FStar.Tactics.V2.SyntaxHelpers.fsti - CHECK FStar.Class.Embeddable.fsti - CHECK FStar.Reflection.Typing.Builtins.fsti - LAXCHECK FStarC.Syntax.Print.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.SizeT.fst(36,4-36,12): - - Values of type `fits_u32` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val fits_u32` - declaration for this symbol in the interface - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.SizeT.fst(37,4-37,12): - - Values of type `fits_u64` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val fits_u64` - declaration for this symbol in the interface - - LAXCHECK FStarC.Syntax.Embeddings.fst - LAXCHECK FStarC.Syntax.Formula.fst - CHECK FStar.Tactics.NamedView.fst - CHECK FStar.RBSet.fst - CHECK FStar.Reflection.Typing.fsti - CHECK FStar.Reflection.fst - LAXCHECK FStarC.Parser.Driver.fst - LAXCHECK FStarC.Syntax.Embeddings.Base.fst - CHECK FStar.Tactics.V2.Logic.fsti - CHECK FStar.ConstantTime.Integers.fsti - CHECK FStar.Reflection.Formula.fst - CHECK FStar.PtrdiffT.fst - CHECK FStar.Tactics.MApply.fst - CHECK FStar.Class.Embeddable.fst - LAXCHECK FStarC.Syntax.Print.Pretty.fst - CHECK FStar.Tactics.SyntaxHelpers.fst - LAXCHECK FStarC.Defensive.fst - CHECK FStar.Tactics.V2.SyntaxHelpers.fst - CHECK FStar.Tactics.V2.Derived.fst - CHECK FStar.Reflection.V1.fst - LAXCHECK FStarC.Syntax.Resugar.fst - LAXCHECK FStarC.Syntax.Compress.fst - LAXCHECK FStarC.ToSyntax.ToSyntax.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.RBMap.fst(144,8-144,15): - - Global binding 'FStar.RBMap.for_any' is recursive but not used in its body - - CHECK FStar.Tactics.Logic.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.ModifiesGen.fst(75,4-75,7): - - Values of type `loc` will be erased during extraction, but its interface - hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc` declaration - for this symbol in the interface - - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fsti - LAXCHECK FStarC.Extraction.ML.UEnv.fsti - LAXCHECK FStarC.SMTEncoding.Util.fsti - LAXCHECK FStarC.Reflection.V2.Builtins.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fsti - CHECK FStar.Tactics.V1.Logic.fsti - CHECK FStar.Tactics.V1.SyntaxHelpers.fst - LAXCHECK FStarC.TypeChecker.Generalize.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fsti - LAXCHECK FStarC.Reflection.V1.Builtins.fsti - LAXCHECK FStarC.SMTEncoding.Solver.fsti - LAXCHECK FStarC.Reflection.V2.Embeddings.fsti - LAXCHECK FStarC.TypeChecker.Core.fsti - LAXCHECK FStarC.TypeChecker.Tc.fsti - LAXCHECK FStarC.TypeChecker.Err.fsti - LAXCHECK FStarC.TypeChecker.Rel.fsti - LAXCHECK FStarC.TypeChecker.Env.fst - LAXCHECK FStarC.TypeChecker.PatternUtils.fsti - LAXCHECK FStarC.TypeChecker.Positivity.fsti - CHECK FStar.ConstantTime.Integers.fst - LAXCHECK FStarC.TypeChecker.Quals.fsti - LAXCHECK FStarC.TypeChecker.TcEffect.fsti - LAXCHECK FStarC.TypeChecker.Util.fsti - LAXCHECK FStarC.TypeChecker.DMFF.fsti - LAXCHECK FStarC.SMTEncoding.SolverState.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.Buffer.Quantifiers.fst - LAXCHECK FStarC.Interactive.JsonHelper.fst - LAXCHECK FStarC.Tactics.Hooks.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fst - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fsti - CHECK FStar.Modifies.fsti - LAXCHECK FStarC.TypeChecker.NBETerm.fsti - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fst - LAXCHECK FStarC.TypeChecker.PatternUtils.fst - LAXCHECK FStarC.TypeChecker.TcInductive.fsti - LAXCHECK FStarC.Reflection.V2.Embeddings.fst - LAXCHECK FStarC.TypeChecker.TcTerm.fsti - LAXCHECK FStarC.Tactics.Types.Reflection.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fst - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fsti - LAXCHECK FStarC.SMTEncoding.Util.fst - LAXCHECK FStarC.SMTEncoding.Env.fst - LAXCHECK FStarC.Extraction.ML.RegEmb.fsti - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - CHECK FStar.Tactics.V1.Derived.fst - LAXCHECK FStarC.Extraction.Krml.fsti - LAXCHECK FStarC.Extraction.ML.Util.fsti - LAXCHECK FStarC.Extraction.ML.UEnv.fst - LAXCHECK FStarC.Extraction.ML.Term.fsti - LAXCHECK FStarC.Extraction.ML.Modul.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Buffer.Quantifiers.fst(32,2-32,77): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Addition - - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fst - LAXCHECK FStarC.Tactics.Types.Reflection.fst - CHECK FStar.Pointer.Derived1.fsti - CHECK FStar.Pointer.Base.fst - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fst - LAXCHECK FStarC.Extraction.ML.Util.fst - LAXCHECK FStarC.Extraction.ML.Code.fst - LAXCHECK FStarC.Extraction.Krml.fst - LAXCHECK FStarC.TypeChecker.Primops.Base.fsti - LAXCHECK FStarC.TypeChecker.NBETerm.fst - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fsti - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fsti - LAXCHECK FStarC.MachineInts.fsti - CHECK FStar.Tactics.V2.Bare.fsti - CHECK FStar.Tactics.CanonCommSemiring.fst - CHECK FStar.Tactics.MkProjectors.fst - CHECK FStar.Tactics.V2.Logic.fst - CHECK FStar.Tactics.Typeclasses.fst - CHECK FStar.Tactics.Print.fst - CHECK FStar.Tactics.Derived.fst - CHECK FStar.UInt128.fst - CHECK FStar.Tactics.MApply0.fst - CHECK LowStar.Buffer.fst - CHECK LowStar.BufferView.Down.fsti - CHECK LowStar.BufferView.fsti - CHECK LowStar.Printf.fst - CHECK LowStar.PrefixFreezableBuffer.fsti - CHECK LowStar.Monotonic.Buffer.fst - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fst - LAXCHECK FStarC.MachineInts.fst - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fst - LAXCHECK FStarC.CheckedFiles.fsti - LAXCHECK FStarC.SMTEncoding.Encode.fsti - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fsti - CHECK FStar.Modifies.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/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 - - LAXCHECK FStarC.TypeChecker.Primops.fsti - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fsti - LAXCHECK FStarC.TypeChecker.Primops.Issue.fsti - LAXCHECK FStarC.TypeChecker.Primops.Base.fst - LAXCHECK FStarC.TypeChecker.Primops.Docs.fsti - LAXCHECK FStarC.Tactics.V1.Primops.fsti - LAXCHECK FStarC.Tactics.V2.Primops.fsti - CHECK FStar.Tactics.V2.fsti - LAXCHECK FStarC.TypeChecker.Primops.Real.fsti - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fsti - LAXCHECK FStarC.TypeChecker.Primops.Erased.fsti - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fsti - LAXCHECK FStarC.TypeChecker.Primops.Eq.fsti - LAXCHECK FStarC.TypeChecker.Primops.Range.fsti - CHECK FStar.Reflection.V2.Arith.fst - CHECK FStar.Tactics.CanonCommMonoidSimple.Equiv.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Printf.fst(253,8-253,13): - - Global binding 'LowStar.Printf.arg_t' is recursive but not used in its body - - CHECK FStar.Pointer.Derived2.fsti - LAXCHECK FStarC.TypeChecker.Primops.Array.fsti - LAXCHECK FStarC.SMTEncoding.Solver.fst - LAXCHECK FStarC.CheckedFiles.fst - LAXCHECK FStarC.Universal.fsti - CHECK FStar.Tactics.PrettifyType.fsti - LAXCHECK FStarC.TypeChecker.Cfg.fsti - CHECK FStar.Tactics.V1.Logic.fst - LAXCHECK FStarC.Tactics.Types.fsti - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(181,4-181,7): - - Values of type `loc` will be erased during extraction, but its interface - hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc` declaration - for this symbol in the interface - - CHECK FStar.Tactics.Easy.fst - LAXCHECK FStarC.TypeChecker.Primops.Docs.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(204,4-204,16): - - Values of type `loc_includes` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_includes` - declaration for this symbol in the interface - - CHECK FStar.Tactics.Parametricity.fst - LAXCHECK FStarC.TypeChecker.Primops.Real.fst - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fst - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fst - LAXCHECK FStarC.TypeChecker.Primops.Issue.fst - CHECK LowStar.ImmutableBuffer.fst - CHECK FStar.Tactics.TypeRepr.fsti - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fst - CHECK FStar.FiniteMap.Base.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(238,4-238,16): - - Values of type `loc_disjoint` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_disjoint` - declaration for this symbol in the interface - - LAXCHECK FStarC.TypeChecker.Primops.fst - CHECK FStar.Tactics.CheckLN.fsti - CHECK FStar.Pointer.Derived3.fsti - CHECK LowStar.BufferView.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(260,4-260,12): - - Values of type `modifies` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val modifies` - declaration for this symbol in the interface - - LAXCHECK FStarC.TypeChecker.Primops.Array.fst - CHECK FStar.Tactics.CanonMonoid.fst - LAXCHECK FStarC.TypeChecker.Primops.Erased.fst - LAXCHECK FStarC.TypeChecker.Primops.Eq.fst - LAXCHECK FStarC.Tactics.Types.fst - CHECK FStar.Pointer.Derived1.fst - LAXCHECK FStarC.TypeChecker.Primops.Range.fst - LAXCHECK FStarC.Interactive.Ide.Types.fsti - LAXCHECK FStarC.TypeChecker.Normalize.fsti - CHECK FStar.Tactics.CanonCommMonoidSimple.fst - LAXCHECK FStarC.Tactics.Result.fsti - LAXCHECK FStarC.Tactics.Printing.fsti - LAXCHECK FStarC.Tactics.Embedding.fsti - CHECK LowStar.BufferCompat.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(237,21-237,29): - - Prims.has_type is deprecated - - 'has_type' is intended for internal use and debugging purposes only; do not - rely on it for your proofs - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/Prims.fst(289,5-289,13) - - CHECK FStar.BigOps.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(236,21-236,29): - - Prims.has_type is deprecated - - 'has_type' is intended for internal use and debugging purposes only; do not - rely on it for your proofs - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/Prims.fst(289,5-289,13) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(237,21-237,29): - - Prims.has_type is deprecated - - 'has_type' is intended for internal use and debugging purposes only; do not - rely on it for your proofs - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/Prims.fst(289,5-289,13) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(236,21-236,29): - - Prims.has_type is deprecated - - 'has_type' is intended for internal use and debugging purposes only; do not - rely on it for your proofs - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/Prims.fst(289,5-289,13) - - LAXCHECK FStarC.Tactics.Native.fsti - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fsti - CHECK FStar.Reflection.Typing.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.Krml.fst(653,8-653,37): - - Global binding - 'FStarC.Extraction.Krml.translate_type_without_decay'' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.Krml.fst(756,4-756,19): - - Global binding - 'FStarC.Extraction.Krml.translate_type'' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.Krml.fst(773,4-773,19): - - Global binding - 'FStarC.Extraction.Krml.translate_expr'' - is recursive but not used in its body - - LAXCHECK FStarC.TypeChecker.Cfg.fst - LAXCHECK FStarC.Extraction.ML.Term.fst - CHECK FStar.ReflexiveTransitiveClosure.fst - LAXCHECK FStarC.Reflection.V2.Interpreter.fst - LAXCHECK FStarC.TypeChecker.Util.fst - LAXCHECK FStarC.TypeChecker.NBE.fsti - LAXCHECK FStarC.TypeChecker.Positivity.fst - LAXCHECK FStarC.TypeChecker.Quals.fst - LAXCHECK FStarC.TypeChecker.Rel.fst - CHECK FStar.Tactics.fsti - LAXCHECK FStarC.SMTEncoding.Encode.fst - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fst - LAXCHECK FStarC.TypeChecker.DMFF.fst - LAXCHECK FStarC.Reflection.V1.Builtins.fst - LAXCHECK FStarC.Reflection.V1.Interpreter.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(416,4-416,25): - - Values of type `does_not_contain_addr` will be erased during extraction, but - its interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val - does_not_contain_addr` declaration for this symbol in the interface - - CHECK FStar.Tactics.V1.fsti - CHECK LowStar.Modifies.fst - CHECK FStar.Pointer.Derived2.fst - LAXCHECK FStarC.Interactive.Incremental.fsti - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/FStar.Modifies.fst(435,4-435,12): - - Values of type `cloc_cls` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val cloc_cls` - declaration for this symbol in the interface - - LAXCHECK FStarC.Reflection.V2.Builtins.fst - LAXCHECK FStarC.TypeChecker.Generalize.fst - CHECK FStar.Tactics.PrettifyType.fst - CHECK FStar.Tactics.Simplifier.fst - CHECK FStar.Tactics.Canon.fst - LAXCHECK FStarC.Tactics.Monad.fsti - CHECK LowStar.ModifiesPat.fst - CHECK LowStar.BufferOps.fst - LAXCHECK FStarC.Interactive.PushHelper.fsti - CHECK LowStar.BufferView.Up.fsti - CHECK FStar.Tactics.BreakVC.fsti - CHECK FStar.Tactics.CanonCommMonoid.fst - LAXCHECK FStarC.Interactive.QueryHelper.fsti - LAXCHECK FStarC.Interactive.Ide.Types.fst - CHECK LowStar.BufferView.Down.fst - CHECK LowStar.Vector.fst - CHECK FStar.Tactics.BV.fst - LAXCHECK FStarC.Tactics.Embedding.fst - LAXCHECK FStarC.Tactics.Printing.fst - CHECK FStar.WellFounded.Util.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(804,4-804,7): - - Values of type `loc` will be erased during extraction, but its interface - hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc` declaration - for this symbol in the interface - - CHECK FStar.Tactics.PatternMatching.fst - LAXCHECK FStarC.Tactics.Result.fst - LAXCHECK FStarC.TypeChecker.Tc.fst - CHECK FStar.Tactics.TypeRepr.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.ML.Term.fst(710,8-710,31): - - Global binding - 'FStarC.Extraction.ML.Term.translate_term_to_mlty'' - is recursive but not used in its body - - CHECK FStar.Pointer.Derived3.fst - CHECK LowStar.Regional.fst - LAXCHECK FStarC.Tactics.CtrlRewrite.fsti - CHECK FStar.Pointer.fst - LAXCHECK FStarC.Tactics.V1.Basic.fsti - LAXCHECK FStarC.TypeChecker.Err.fst - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/typechecker/FStarC.TypeChecker.Generalize.fst(264,9-264,54): - - Effectful argument FStarC.List.for_all (fun _ -> - (let l, _, _ = _ in - Inr? l) - <: - Prims.bool) - lecs (FStarC.Effect.ALL) to erased function assert, consider let binding it - - CHECK LowStar.ToFStarBuffer.fst - CHECK LowStar.Endianness.fst - LAXCHECK FStarC.TypeChecker.Core.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(867,4-867,16): - - Values of type `loc_includes` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_includes` - declaration for this symbol in the interface - - LAXCHECK FStarC.Interactive.QueryHelper.fst - CHECK FStar.Pure.BreakVC.fsti - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.ML.Term.fst(1343,4-1343,20): - - Global binding - 'FStarC.Extraction.ML.Term.extract_lb_iface' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/extraction/FStarC.Extraction.ML.Term.fst(1389,4-1389,19): - - Global binding - 'FStarC.Extraction.ML.Term.term_as_mlexpr'' - is recursive but not used in its body - - CHECK LowStar.ConstBuffer.fsti - LAXCHECK FStarC.TypeChecker.TcEffect.fst - LAXCHECK FStarC.TypeChecker.TcInductive.fst - LAXCHECK FStarC.TypeChecker.TcTerm.fst - CHECK LowStar.UninitializedBuffer.fst - CHECK LowStar.Literal.fsti - CHECK FStar.Tactics.CheckLN.fst - CHECK FStar.BufferNG.fst - LAXCHECK FStarC.Extraction.ML.Modul.fst - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fst - LAXCHECK FStarC.Tactics.V1.Basic.fst - LAXCHECK FStarC.TypeChecker.Normalize.fst - CHECK FStar.Tactics.Arith.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(1048,4-1048,16): - - Values of type `loc_disjoint` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_disjoint` - declaration for this symbol in the interface - - CHECK FStar.InteractiveHelpers.Base.fst - CHECK FStar.Bytes.fsti - LAXCHECK FStarC.Interactive.PushHelper.fst - CHECK FStar.Tactics.BreakVC.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(1103,4-1103,12): - - Values of type `modifies` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val modifies` - declaration for this symbol in the interface - - CHECK LowStar.BufferView.Up.fst - CHECK FStar.TaggedUnion.fsti - CHECK LowStar.ConstBuffer.fst - LAXCHECK FStarC.Tactics.Monad.fst - LAXCHECK FStarC.Tactics.CtrlRewrite.fst - CHECK FStar.Pure.BreakVC.fst - LAXCHECK FStarC.TypeChecker.NBE.fst - LAXCHECK FStarC.Tactics.InterpFuns.fsti - LAXCHECK FStarC.Interactive.Ide.fst - LAXCHECK FStarC.Tactics.Interpreter.fsti - LAXCHECK FStarC.Tactics.V2.Basic.fsti - LAXCHECK FStarC.Interactive.Incremental.fst - CHECK FStar.Crypto.fst - CHECK FStar.Udp.fsti - CHECK FStar.Tcp.fsti - LAXCHECK FStarC.Main.fst - LAXCHECK FStarC.Hooks.fst - LAXCHECK FStarC.Universal.fst - LAXCHECK FStarC.Tactics.Interpreter.fst - CHECK FStar.InteractiveHelpers.ExploreTerm.fst - LAXCHECK FStarC.Extraction.ML.RegEmb.fst - LAXCHECK FStarC.Tactics.V1.Primops.fst - LAXCHECK FStarC.Tactics.InterpFuns.fst - CHECK FStar.TaggedUnion.fst - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/src/interactive/FStarC.Interactive.Ide.fst(156,13-156,53): - - Effectful argument let _ = - let _ = - let _ = - let _ = !FStarC.Interactive.PushHelper.repl_stack in - FStarC.List.hd _ - in - FStar.Pervasives.Native.snd _ - in - FStar.Pervasives.Native.fst _ - in - task = _ (FStarC.Effect.ALL) to erased function assert, consider let binding it - - LAXCHECK FStarC.Tactics.V2.Basic.fst - LAXCHECK FStarC.Tactics.V2.Primops.fst - LAXCHECK FStarC.Tactics.Hooks.fst - CHECK LowStar.PrefixFreezableBuffer.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/LowStar.Monotonic.Buffer.fst(1422,4-1422,25): - - Values of type `does_not_contain_addr` will be erased during extraction, but - its interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val - does_not_contain_addr` declaration for this symbol in the interface - - CHECK LowStar.RVector.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Pointer.Base.fst(3649,4-3649,7): - - Values of type `loc` will be erased during extraction, but its interface - hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc` declaration - for this symbol in the interface - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Pointer.Base.fst(3667,4-3667,16): - - Values of type `loc_includes` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_includes` - declaration for this symbol in the interface - - CHECK FStar.InteractiveHelpers.Propositions.fst - CHECK FStar.InteractiveHelpers.Output.fst - CHECK FStar.InteractiveHelpers.Effectful.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Pointer.Base.fst(3721,4-3721,16): - - Values of type `loc_disjoint` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val loc_disjoint` - declaration for this symbol in the interface - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Pointer.Base.fst(3778,4-3778,12): - - Values of type `modifies` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val modifies` - declaration for this symbol in the interface - - CHECK FStar.Math.Fermat.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24/ulib/legacy/FStar.Pointer.Base.fst(4246,4-4246,12): - - Values of type `cloc_cls` will be erased during extraction, but its - interface hides this fact. - - Add the `must_erase_for_extraction` attribute to the `val cloc_cls` - declaration for this symbol in the interface - - CHECK FStar.InteractiveHelpers.PostProcess.fst - CHECK FStar.InteractiveHelpers.fst - CHECK LowStar.Regional.Instances.fst - DONE CHECK FSTARC - INSTALL LIB - INSTALL FSTARC -> compiled fstar.2026.03.24 [fstar: make install] + /usr/bin/make "PREFIX=/home/opam/.opam/default" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2026.03.24) - DUNE BUILD - DUNE INSTALL - CHECK LIB - INSTALL LIB SRC - INSTALL LIB - CHECK FSTARC - DONE CHECK FSTARC - INSTALL FSTARC -> installed fstar.2026.03.24 [WARNING] Opam package conf-pkg-config.5 depends on the following system package that can no longer be found: pkg-config === STDERR === 2026-06-26 11:23.52: OK: build fstar.2026.03.24 (runc: 771.0s, disk: 73KB) 2026-06-26 11:23.52: Job succeeded