← Back to PR #29099
Build Log: fstar.2025.12.15
Status: SUCCESS
Log Output
Processing: [default: loading data]
[fstar.2025.12.15: http]
[fstar.2025.12.15: extract]
-> retrieved fstar.2025.12.15 (https://github.com/FStarLang/FStar/releases/download/v2025.12.15/fstar-v2025.12.15-src.tar.gz)
[fstar: make 255]
+ /usr/bin/make "-j" "255" "ADMIT=1" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15)
- 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 symbol(s).
- File "fstar-guts/FStarC_Parser_Parse.mly", line 306, characters 0-16:
- Warning: symbol noDecorationDecl is unreachable from any of the start symbol(s).
- Warning: 20 states have shift/reduce 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.2025.12.15/src
- DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 FStar.Classical.Sugar.fsti
- LAXCHECK FStar.Mul.fst
- LAXCHECK FStar.Ghost.fsti
- LAXCHECK FStar.Sealed.fsti
- LAXCHECK FStar.Float.fsti
- LAXCHECK FStarC.Effect.fsti
- LAXCHECK FStar.ImmutableArray.Base.fsti
- LAXCHECK FStarC.Array.fsti
- LAXCHECK FStarC.VConfig.fsti
- LAXCHECK FStarC.Sealed.fsti
- LAXCHECK FStarC.NormSteps.fst
- LAXCHECK FStarC.Errors.Codes.fsti
- LAXCHECK FStar.Exn.fst
- LAXCHECK FStar.Set.fsti
- LAXCHECK FStar.Preorder.fst
- LAXCHECK FStar.Order.fst
- LAXCHECK FStar.Stubs.VConfig.fsti
- LAXCHECK FStar.Reflection.Const.fst
- LAXCHECK FStar.Classical.fsti
- LAXCHECK FStar.FunctionalExtensionality.fsti
- LAXCHECK FStar.Stubs.TypeChecker.Core.fsti
- LAXCHECK FStar.Squash.fsti
- LAXCHECK FStarC.Reflection.V2.Interpreter.fsti
- LAXCHECK FStarC.Reflection.V1.Interpreter.fsti
- LAXCHECK FStarC.Hooks.fsti
- LAXCHECK FStar.PropositionalExtensionality.fst
- LAXCHECK FStar.Math.Lemmas.fsti
- LAXCHECK FStar.Math.Lib.fst
- LAXCHECK FStar.List.Tot.Base.fst
- LAXCHECK FStar.Range.fsti
- LAXCHECK FStar.Monotonic.Pure.fst
- LAXCHECK FStar.Sealed.Inhabited.fst
- LAXCHECK FStarC.Sealed.fst
- LAXCHECK FStarC.Json.fsti
- LAXCHECK FStarC.Thunk.fsti
- LAXCHECK FStarC.Hash.fsti
- LAXCHECK FStarC.Order.fsti
- LAXCHECK FStarC.Unionfind.fsti
- LAXCHECK FStarC.Dyn.fsti
- LAXCHECK FStarC.PSMap.fsti
- LAXCHECK FStarC.SMap.fsti
- LAXCHECK FStarC.PIMap.fsti
- LAXCHECK FStarC.List.fsti
- LAXCHECK FStarC.Option.fsti
- LAXCHECK FStar.Monotonic.Witnessed.fsti
- LAXCHECK FStar.TSet.fsti
- LAXCHECK FStarC.OCaml.fsti
- LAXCHECK FStarC.Debug.fsti
- LAXCHECK FStarC.Filepath.fsti
- LAXCHECK FStarC.Profiling.fsti
- LAXCHECK FStarC.Timing.fsti
- LAXCHECK FStarC.Int.Extra.fsti
- LAXCHECK FStarC.Platform.Base.fsti
- LAXCHECK FStarC.Plugins.Base.fsti
- CHECK FStar.Prelude.fsti
- LAXCHECK FStar.Classical.Sugar.fst
- CHECK FStar.Pervasives.fst
- LAXCHECK FStarC.EditDist.fsti
- LAXCHECK FStarC.IMap.fsti
- LAXCHECK FStar.Ghost.fst
- LAXCHECK FStarC.Interactive.Ide.fsti
- LAXCHECK FStarC.Prettyprint.fsti
- LAXCHECK FStarC.Find.fsti
- LAXCHECK FStarC.Stats.fsti
- LAXCHECK FStarC.Options.Ext.fsti
- LAXCHECK FStarC.GenSym.fsti
- LAXCHECK FStar.ErasedLogic.fst
- LAXCHECK FStar.Calc.fsti
- LAXCHECK FStarC.Misc.fsti
- LAXCHECK FStarC.Hints.fsti
- LAXCHECK FStarC.Order.fst
- LAXCHECK FStar.PredicateExtensionality.fst
- LAXCHECK FStar.Monotonic.Witnessed.fst
- LAXCHECK FStarC.VConfig.fst
- LAXCHECK FStar.Classical.fst
- LAXCHECK FStarC.Thunk.fst
- LAXCHECK FStarC.Option.fst
- LAXCHECK FStar.IndefiniteDescription.fsti
- LAXCHECK FStar.Stubs.Reflection.Types.fsti
- LAXCHECK FStarC.Real.fsti
- LAXCHECK FStarC.Format.fsti
- LAXCHECK FStar.Monotonic.Heap.fsti
- LAXCHECK FStarC.Common.fsti
- LAXCHECK FStar.Set.fst
- LAXCHECK FStarC.Plugins.fsti
- LAXCHECK FStarC.GenSym.fst
- LAXCHECK FStar.Calc.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.Squash.fsti
- CHECK FStar.Tactics.Logic.Lemmas.fsti
- CHECK FStar.Stubs.VConfig.fsti
- CHECK FStar.Order.fst
- CHECK FStar.Stubs.TypeChecker.Core.fsti
- CHECK FStar.Reflection.Const.fst
- CHECK FStar.Classical.fsti
- CHECK FStar.PropositionalExtensionality.fst
- CHECK FStar.Exn.fst
- CHECK FStar.Real.fsti
- CHECK FStar.RefinementExtensionality.fsti
- CHECK FStar.FunctionalExtensionality.fsti
- CHECK FStar.Sequence.Base.fsti
- CHECK FStar.PartialMap.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
- CHECK FStar.Exception.fsti
- CHECK FStar.Parse.fst
- CHECK FStar.Date.fsti
- LAXCHECK FStar.StrongExcludedMiddle.fst
- LAXCHECK FStar.Stubs.Syntax.Syntax.fsti
- LAXCHECK FStar.Stubs.Tactics.Types.Reflection.fsti
- LAXCHECK FStar.Reflection.TermEq.Simple.fsti
- LAXCHECK FStar.Math.Lemmas.fst
- LAXCHECK FStar.IndefiniteDescription.fst
- LAXCHECK FStar.Squash.fst
- LAXCHECK FStarC.Errors.Codes.fst
- CHECK FStar.Math.Lemmas.fsti
- CHECK FStar.Math.Euclid.fsti
- CHECK FStar.Algebra.CommMonoid.fst
- LAXCHECK FStar.TSet.fst
- CHECK FStar.Tactics.Canon.Lemmas.fsti
- CHECK FStar.Math.Lib.fst
- CHECK FStar.Range.fsti
- CHECK FStar.Sealed.Inhabited.fst
- LAXCHECK FStar.Seq.Base.fsti
- LAXCHECK FStar.List.Tot.Properties.fsti
- CHECK FStar.Monotonic.Witnessed.fsti
- CHECK FStar.Witnessed.Core.fsti
- CHECK FStar.List.Tot.Base.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Monotonic.Pure.fst
- CHECK FStar.Algebra.CommMonoid.Equiv.fst
- CHECK FStar.Dyn.fst
- CHECK FStar.Classical.Sugar.fst
- CHECK FStar.Universe.fst
- CHECK FStar.Cardinality.Cantor.fsti
- CHECK FStar.TSet.fsti
- CHECK FStar.Map.fsti
- CHECK FStar.IFC.fsti
- CHECK FStar.ErasedLogic.fst
- CHECK FStar.Ghost.fst
- CHECK FStar.IndefiniteDescription.fsti
- CHECK FStar.PartialMap.fst
- CHECK FStar.PredicateExtensionality.fst
- CHECK FStar.Stubs.Reflection.Types.fsti
- LAXCHECK FStar.Heap.fst
- CHECK FStar.Calc.fsti
- LAXCHECK FStar.Monotonic.Heap.fst
- CHECK FStar.SquashProperties.fst
- CHECK FStar.DependentMap.fst
- CHECK FStar.Witnessed.Core.fst
- CHECK FStar.Algebra.Monoid.fst
- CHECK FStar.PCM.fst
- CHECK FStar.GSet.fsti
- CHECK FStar.GhostSet.fsti
- CHECK FStar.Classical.fst
- CHECK FStar.Monotonic.Witnessed.fst
- CHECK FStar.Set.fst
- CHECK FStar.Tactics.Canon.Lemmas.fst
- LAXCHECK FStar.BitVector.fsti
- CHECK FStar.Cardinality.Universes.fsti
- CHECK FStar.Cardinality.Cantor.fst
- LAXCHECK FStar.ST.fst
- CHECK FStar.Math.Fermat.fsti
- CHECK FStar.MSTTotal.fst
- CHECK FStar.Bijection.fst
- CHECK FStar.StrongExcludedMiddle.fst
- CHECK FStar.IndefiniteDescription.fst
- CHECK FStar.WellFounded.fst
- CHECK FStar.Squash.fst
- CHECK FStar.RefinementExtensionality.fst
- CHECK FStar.Tactics.Logic.Lemmas.fst
- CHECK FStar.Stubs.Syntax.Syntax.fsti
- CHECK FStar.Stubs.Tactics.Types.Reflection.fsti
- CHECK FStar.Reflection.TermEq.Simple.fsti
- CHECK FStar.ExtractAs.fst
- CHECK FStar.Calc.fst
- CHECK FStar.IFC.fst
- CHECK FStar.Monotonic.Heap.fsti
- CHECK FStar.Cardinality.Universes.fst
- LAXCHECK FStar.All.fsti
- CHECK FStar.Map.fst
- CHECK FStar.TSet.fst
- CHECK FStar.Functions.fst
- LAXCHECK FStar.UInt.fsti
- CHECK FStar.GSet.fst
- CHECK FStar.GhostSet.fst
- LAXCHECK FStar.List.Tot.fst
- LAXCHECK FStar.List.Tot.Properties.fst
- LAXCHECK FStar.Seq.Properties.fsti
- LAXCHECK FStar.List.fst
- LAXCHECK FStar.Seq.Base.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.
-
- CHECK FStar.WellFoundedRelation.fsti
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.
-
- CHECK FStar.NMSTTotal.fst
- CHECK FStar.MST.fst
- CHECK FStar.Sequence.Ambient.fst
- CHECK FStar.Sequence.Util.fst
- CHECK FStar.Universe.PCM.fst
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Sequence.fst
- CHECK FStar.Math.Lemmas.fst
- LAXCHECK FStar.UInt32.fsti
- CHECK FStar.WellFoundedRelation.fst
- * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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
-
- CHECK FStar.Sequence.Permutation.fsti
- * Warning 352 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
- LAXCHECK FStar.Char.fsti
- LAXCHECK FStar.UInt32.fst
- CHECK FStar.Heap.fst
- CHECK FStar.Monotonic.HyperHeap.fsti
- CHECK FStar.Monotonic.Heap.fst
- CHECK FStar.Sequence.Permutation.fst
- LAXCHECK FStar.Pprint.fsti
- LAXCHECK FStarC.BaseTypes.fsti
- LAXCHECK FStarC.String.fsti
- LAXCHECK FStar.String.fsti
- LAXCHECK FStar.Stubs.Reflection.V2.Data.fsti
- LAXCHECK FStar.Seq.fst
- LAXCHECK FStar.Seq.Properties.fst
- CHECK FStar.LexicographicOrdering.fst
- LAXCHECK FStarC.Util.fsti
- LAXCHECK FStarC.Getopt.fsti
- LAXCHECK FStarC.Debug.fst
- LAXCHECK FStarC.EditDist.fst
- CHECK FStar.Relational.Relational.fst
- CHECK FStar.ST.fst
- CHECK FStar.TwoLevelHeap.fst
- CHECK FStar.Axiomatic.Array.fst
- LAXCHECK FStar.BitVector.fst
- LAXCHECK FStar.UInt.fst
- LAXCHECK FStar.Issue.fsti
- LAXCHECK FStar.Stubs.Errors.Msg.fsti
- LAXCHECK FStar.Stubs.Tactics.Common.fsti
- * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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.Reflection.V2.Builtins.fsti
- LAXCHECK FStar.Reflection.V2.Compare.fsti
- * Warning 352 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.BitVector.fsti
- CHECK FStar.IntegerIntervals.fst
- * Warning 290 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Stubs.Tactics.Types.fsti
- CHECK FStar.Monotonic.HyperStack.fsti
- LAXCHECK FStarC.Pprint.fsti
- LAXCHECK FStarC.StringBuffer.fsti
- LAXCHECK FStarC.Misc.fst
- CHECK FStar.All.fsti
- CHECK FStar.Ref.fst
- CHECK FStar.MRef.fsti
- LAXCHECK FStar.Tactics.Effect.fsti
- LAXCHECK FStar.Reflection.V2.Collect.fst
- LAXCHECK FStar.Reflection.TermEq.fsti
- LAXCHECK FStarC.Common.fst
- LAXCHECK FStarC.Find.Z3.fsti
- LAXCHECK FStar.Reflection.V2.Derived.Lemmas.fst
- LAXCHECK FStar.Reflection.V2.Derived.fst
- LAXCHECK FStar.Tactics.Typeclasses.fsti
- LAXCHECK FStar.Tactics.NamedView.fsti
- LAXCHECK FStar.Tactics.Names.fsti
- LAXCHECK FStar.Tactics.Util.fst
- LAXCHECK FStar.Stubs.Tactics.Unseal.fsti
- LAXCHECK FStar.Tactics.Effect.fst
- CHECK FStar.MRef.fst
- CHECK FStar.Relational.Comp.fst
- CHECK FStar.Option.fst
- LAXCHECK FStar.Reflection.TermEq.Simple.fst
- LAXCHECK FStar.Reflection.TermEq.fst
- LAXCHECK FStar.Stubs.Tactics.V2.Builtins.fsti
- CHECK FStar.List.Tot.fst
- LAXCHECK FStarC.Class.Show.fsti
- CHECK FStar.List.Pure.Properties.fst
- LAXCHECK FStarC.Class.Deq.fsti
- CHECK FStar.List.Tot.Properties.fst
- LAXCHECK FStarC.Class.Tagged.fsti
- LAXCHECK FStarC.Errors.Msg.fsti
- LAXCHECK FStarC.Class.Monad.fsti
- LAXCHECK FStarC.Class.Listlike.fsti
- LAXCHECK FStarC.Class.Monoid.fsti
- LAXCHECK FStar.Reflection.V2.fst
- LAXCHECK FStar.Reflection.V2.Compare.fst
- LAXCHECK FStarC.Class.Tagged.fst
- LAXCHECK FStar.Tactics.Visit.fst
- LAXCHECK FStarC.Class.PP.fsti
- LAXCHECK FStarC.Options.fsti
- LAXCHECK FStarC.Path.fsti
- LAXCHECK FStarC.Time.fsti
- LAXCHECK FStarC.Platform.fsti
- LAXCHECK FStarC.Class.Monoid.fst
- LAXCHECK FStarC.Class.Deq.fst
- LAXCHECK FStarC.Class.Show.fst
- LAXCHECK FStarC.Errors.Msg.fst
- LAXCHECK FStarC.Find.fst
- CHECK FStar.UInt.fsti
- LAXCHECK FStarC.Options.Ext.fst
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- LAXCHECK FStarC.Class.Ord.fsti
- LAXCHECK FStarC.Class.Listlike.fst
- LAXCHECK FStarC.Class.Monad.fst
- LAXCHECK FStarC.Writer.fsti
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/FStar.UInt.fsti(436,8-436,51)
-
- CHECK FStar.Seq.Properties.fsti
- CHECK FStar.List.fst
- CHECK FStar.OrdSet.fsti
- CHECK FStar.Monotonic.HyperHeap.fst
- CHECK FStar.FiniteSet.Base.fsti
- CHECK FStar.ImmutableArray.fsti
- CHECK FStar.Sequence.Base.fst
- CHECK FStar.Seq.Base.fst
- LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fsti
- LAXCHECK FStar.Tactics.NamedView.fst
- LAXCHECK FStar.Reflection.V2.Formula.fst
- LAXCHECK FStar.FunctionalExtensionality.fst
- LAXCHECK FStar.Tactics.V2.SyntaxCoercions.fst
- LAXCHECK FStarC.Path.fst
- LAXCHECK FStarC.Platform.fst
- LAXCHECK FStarC.OCaml.fst
- LAXCHECK FStarC.Class.PP.fst
- LAXCHECK FStarC.Writer.fst
- LAXCHECK FStarC.Class.Setlike.fsti
- LAXCHECK FStarC.Range.Type.fsti
- LAXCHECK FStarC.Class.Hashable.fsti
- LAXCHECK FStarC.CList.fsti
- LAXCHECK FStarC.Stats.fst
- LAXCHECK FStarC.Class.Ord.fst
- LAXCHECK FStarC.Real.fst
- LAXCHECK FStar.Tactics.Names.fst
- LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fst
- LAXCHECK FStarC.Class.HasRange.fsti
- LAXCHECK FStarC.Range.Ops.fsti
- LAXCHECK FStarC.Range.Type.fst
- LAXCHECK FStarC.CList.fst
- LAXCHECK FStarC.HashMap.fsti
- LAXCHECK FStarC.Class.Hashable.fst
- LAXCHECK FStarC.Profiling.fst
- LAXCHECK FStarC.Options.fst
- LAXCHECK FStarC.Find.Z3.fst
- LAXCHECK FStarC.Ident.fsti
- LAXCHECK FStarC.FlatSet.fsti
- LAXCHECK FStarC.RBSet.fsti
- LAXCHECK FStarC.HashMap.fst
- LAXCHECK FStarC.Class.Setlike.fst
- LAXCHECK FStarC.Range.fsti
- CHECK FStar.FiniteSet.Ambient.fst
- CHECK FStar.FiniteMap.Base.fsti
- CHECK FStar.FiniteSet.Base.fst
- LAXCHECK FStarC.Range.Ops.fst
- LAXCHECK FStar.Tactics.V2.Derived.fst
- LAXCHECK FStarC.FlatSet.fst
- LAXCHECK FStarC.RBSet.fst
- LAXCHECK FStarC.Errors.fsti
- LAXCHECK FStarC.Class.HasRange.fst
- CHECK FStar.HyperStack.fst
- CHECK FStar.Monotonic.HyperStack.fst
- LAXCHECK FStarC.Const.fsti
- LAXCHECK FStarC.Parser.Const.Tuples.fsti
- LAXCHECK FStarC.Interactive.CompletionTable.fsti
- LAXCHECK FStarC.Ident.fst
- CHECK FStar.List.Pure.fst
- LAXCHECK FStarC.Parser.Const.Tuples.fst
- LAXCHECK FStarC.Interactive.CompletionTable.fst
- LAXCHECK FStarC.Syntax.Syntax.fsti
- LAXCHECK FStarC.Parser.Const.fst
- LAXCHECK FStarC.Extraction.ML.Syntax.fsti
- LAXCHECK FStarC.Const.fst
- CHECK FStar.HyperStack.ST.fsti
- LAXCHECK FStarC.Interactive.JsonHelper.fsti
- CHECK FStar.Util.fst
- LAXCHECK FStarC.Errors.fst
- LAXCHECK FStarC.Plugins.fst
- CHECK FStar.OrdSet.fst
- CHECK FStar.OrdMap.fsti
- CHECK FStar.OrdSetProps.fst
- CHECK FStar.FiniteMap.Ambient.fst
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 '@'.
-
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 '@'.
-
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 '@'.
-
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 '@'.
-
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fsti
- LAXCHECK FStarC.Extraction.ML.PrintFS.fsti
- LAXCHECK FStarC.Extraction.ML.Syntax.fst
- LAXCHECK FStarC.Extraction.ML.Code.fsti
- LAXCHECK FStarC.Extraction.ML.PrintML.fsti
- LAXCHECK FStar.Tactics.Typeclasses.fst
- LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fst
- LAXCHECK FStarC.Extraction.ML.PrintFS.fst
- CHECK FStar.OrdMapProps.fst
- CHECK FStar.OrdMap.fst
- CHECK FStar.UInt32.fsti
- CHECK FStar.BV.fsti
- 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 LowStar.Comment.fst
- CHECK FStar.HyperStack.IO.fst
- LAXCHECK FStarC.Class.Binders.fsti
- LAXCHECK FStarC.Parser.AST.fsti
- LAXCHECK FStarC.TypeChecker.Common.fsti
- LAXCHECK FStarC.Syntax.Embeddings.Base.fsti
- LAXCHECK FStarC.Tactics.Common.fsti
- LAXCHECK FStarC.Syntax.Unionfind.fsti
- LAXCHECK FStarC.Syntax.Subst.fsti
- CHECK FStar.Seq.fst
- LAXCHECK FStarC.Syntax.Hash.fsti
- CHECK FStar.Seq.Equiv.fsti
- LAXCHECK FStarC.Syntax.TermHashTable.fsti
- LAXCHECK FStarC.SMTEncoding.Term.fsti
- CHECK FStar.Seq.Properties.fst
- LAXCHECK FStarC.Reflection.V2.Constants.fst
- CHECK FStar.Char.fsti
- LAXCHECK FStarC.Syntax.VisitM.fsti
- CHECK FStar.UInt16.fsti
- LAXCHECK FStarC.Parser.Const.ExtractAs.fsti
- CHECK FStar.UInt8.fsti
- LAXCHECK FStarC.Reflection.V1.Data.fsti
- LAXCHECK FStarC.Reflection.V1.Constants.fst
- CHECK FStar.UInt64.fsti
- LAXCHECK FStarC.Reflection.V2.Data.fsti
- LAXCHECK FStarC.Syntax.Compress.fsti
- LAXCHECK FStarC.Syntax.Free.fsti
- CHECK FStar.UInt32.fst
- LAXCHECK FStarC.Syntax.MutRecTy.fsti
- LAXCHECK FStarC.Syntax.InstFV.fsti
- LAXCHECK FStarC.Syntax.Formula.fsti
- LAXCHECK FStarC.Syntax.Visit.fsti
- LAXCHECK FStarC.Syntax.Print.Ugly.fsti
- LAXCHECK FStarC.Syntax.Syntax.fst
- CHECK FStar.Tactics.BV.Lemmas.fsti
- CHECK FStar.Monotonic.DependentMap.fst
- LAXCHECK FStarC.Defensive.fsti
- LAXCHECK FStarC.Tactics.Common.fst
- CHECK FStar.Int.fsti
- CHECK FStar.Vector.Base.fsti
- CHECK FStar.BitVector.fst
- CHECK FStar.FunctionalQueue.fsti
- LAXCHECK FStarC.Syntax.Embeddings.fsti
- CHECK FStar.Buffer.fst
- CHECK FStar.BV.fst
- CHECK FStar.Array.fsti
- CHECK FStar.UInt.fst
- CHECK FStar.Sequence.Seq.fsti
- CHECK FStar.Fin.fsti
- LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fsti
- CHECK FStar.Seq.Sorted.fst
- LAXCHECK FStarC.Class.Binders.fst
- CHECK FStar.Monotonic.Seq.fst
- LAXCHECK FStarC.Syntax.Subst.fst
- CHECK FStar.Matrix2.fsti
- LAXCHECK FStarC.Syntax.Visit.fst
- LAXCHECK FStarC.Syntax.Free.fst
- LAXCHECK FStarC.Syntax.Unionfind.fst
- LAXCHECK FStarC.Syntax.Util.fsti
- LAXCHECK FStarC.Syntax.VisitM.fst
- LAXCHECK FStarC.Syntax.InstFV.fst
- 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
- LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fst
- LAXCHECK FStarC.Reflection.V1.Data.fst
- LAXCHECK FStarC.Reflection.V2.Data.fst
- CHECK FStar.Sequence.Seq.fst
- CHECK FStar.FunctionalQueue.fst
- CHECK FStar.UInt16.fst
- CHECK FStar.UInt8.fst
- CHECK FStar.UInt64.fst
- CHECK FStar.UInt128.fsti
- CHECK FStar.SizeT.fsti
- CHECK FStar.Endianness.fsti
- CHECK FStar.Tactics.BV.Lemmas.fst
- CHECK FStar.IO.fsti
- CHECK FStar.Fin.fst
- LAXCHECK FStarC.SMTEncoding.UnsatCore.fsti
- LAXCHECK FStarC.SMTEncoding.Pruning.fsti
- LAXCHECK FStarC.SMTEncoding.Term.fst
- CHECK FStar.Issue.fsti
- CHECK FStar.Stubs.Errors.Msg.fsti
- CHECK FStar.Array.fst
- LAXCHECK FStarC.Parser.Const.ExtractAs.fst
- LAXCHECK FStarC.Syntax.MutRecTy.fst
- LAXCHECK FStarC.Syntax.Hash.fst
- LAXCHECK FStarC.Syntax.Util.fst
- LAXCHECK FStarC.Syntax.Print.Ugly.fst
- CHECK FStar.Vector.Properties.fst
- CHECK FStar.Vector.Base.fst
- LAXCHECK FStarC.SMTEncoding.SolverState.fsti
- CHECK FStar.Algebra.CommMonoid.Fold.fsti
- LAXCHECK FStarC.SMTEncoding.UnsatCore.fst
- CHECK FStar.Seq.Permutation.fst
- LAXCHECK FStarC.SMTEncoding.Pruning.fst
- LAXCHECK FStarC.Parser.Dep.fsti
- LAXCHECK FStarC.Parser.AST.Util.fsti
- LAXCHECK FStarC.Parser.AST.fst
- LAXCHECK FStarC.Parser.ToDocument.fsti
- LAXCHECK FStarC.Parser.AST.Diff.fsti
- CHECK FStar.Stubs.Tactics.Common.fsti
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK FStar.Error.fst
- CHECK FStar.Stubs.Reflection.V2.Builtins.fsti
- CHECK FStar.Reflection.V2.Compare.fsti
- LAXCHECK FStarC.SMTEncoding.Z3.fsti
- LAXCHECK FStarC.Parser.AST.Diff.fst
- LAXCHECK FStarC.Parser.ToDocument.fst
- LAXCHECK FStarC.Parser.ParseIt.fsti
- LAXCHECK FStarC.Parser.AST.Util.fst
- LAXCHECK FStarC.Syntax.DsEnv.fsti
- LAXCHECK FStarC.Dependencies.fsti
- CHECK FStar.Vector.fst
- CHECK FStar.Stubs.Tactics.Types.fsti
- CHECK FStar.Matrix.fsti
- CHECK FStar.Algebra.CommMonoid.Fold.Nested.fsti
- CHECK FStar.Algebra.CommMonoid.Fold.fst
- CHECK FStar.Int16.fsti
- CHECK FStar.Int64.fsti
- CHECK FStar.Int32.fsti
- CHECK FStar.Int8.fsti
- CHECK FStar.Int.fst
- LAXCHECK FStarC.Dependencies.fst
- CHECK FStar.Reflection.V1.Compare.fsti
- LAXCHECK FStarC.SMTEncoding.Z3.fst
- LAXCHECK FStarC.Parser.Driver.fsti
- LAXCHECK FStarC.TypeChecker.Env.fsti
- LAXCHECK FStarC.Syntax.Print.fsti
- LAXCHECK FStarC.ToSyntax.Interleave.fsti
- LAXCHECK FStarC.ToSyntax.ToSyntax.fsti
- LAXCHECK FStarC.Syntax.Print.Pretty.fsti
- LAXCHECK FStarC.Syntax.Resugar.fsti
- LAXCHECK FStarC.Syntax.DsEnv.fst
- LAXCHECK FStarC.ToSyntax.TickedVars.fsti
- CHECK FStar.Tactics.Effect.fsti
- CHECK FStar.Endianness.fst
- CHECK FStar.Reflection.V2.Collect.fst
- CHECK FStar.Stubs.Reflection.V1.Data.fsti
- CHECK FStar.Reflection.TermEq.fsti
- LAXCHECK FStarC.Parser.Dep.fst
- LAXCHECK FStarC.Prettyprint.fst
- LAXCHECK FStarC.Parser.Driver.fst
- LAXCHECK FStarC.ToSyntax.Interleave.fst
- LAXCHECK FStarC.ToSyntax.TickedVars.fst
- LAXCHECK FStarC.Syntax.Print.Pretty.fst
- LAXCHECK FStarC.Syntax.Resugar.fst
- LAXCHECK FStarC.TypeChecker.Common.fst
- LAXCHECK FStarC.Syntax.Embeddings.Base.fst
- LAXCHECK FStarC.Syntax.Embeddings.fst
- LAXCHECK FStarC.Defensive.fst
- CHECK LowStar.Monotonic.Buffer.fsti
- LAXCHECK FStarC.ToSyntax.ToSyntax.fst
- LAXCHECK FStarC.Syntax.Print.fst
- LAXCHECK FStarC.Syntax.Formula.fst
- LAXCHECK FStarC.Syntax.Compress.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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.2025.12.15/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.2025.12.15/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.2025.12.15/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.Int128.fsti
- CHECK FStar.Int64.fst
- CHECK FStar.Int16.fst
- CHECK FStar.PtrdiffT.fsti
- CHECK FStar.Pointer.Base.fsti
- CHECK FStar.Int.Cast.fst
- CHECK FStar.Printf.fst
- CHECK FStar.Int32.fst
- CHECK FStar.Int8.fst
- CHECK FStar.Reflection.V2.Derived.fst
- CHECK FStar.Reflection.V2.Derived.Lemmas.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
- CHECK FStar.Stubs.Tactics.Unseal.fsti
- CHECK FStar.Tactics.Util.fst
- CHECK FStar.Tactics.Print.fsti
- CHECK FStar.Tactics.Names.fsti
- CHECK FStar.Tactics.Effect.fst
- CHECK FStar.InteractiveHelpers.Propositions.fsti
- CHECK FStar.Tactics.Canon.fsti
- CHECK FStar.Tactics.Parametricity.fsti
- CHECK FStar.Tactics.BV.fsti
- CHECK FStar.Tactics.MkProjectors.fsti
- CHECK FStar.Reflection.TermEq.Simple.fst
- CHECK FStar.Reflection.TermEq.fst
- CHECK FStar.Stubs.Tactics.V2.Builtins.fsti
- CHECK FStar.Matrix.fst
- CHECK FStar.Algebra.CommMonoid.Fold.Nested.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Class.Eq.Raw.fst
- CHECK FStar.Class.TotalOrder.Raw.fst
- CHECK FStar.Math.Euclid.fst
- CHECK FStar.Class.Printable.fst
- CHECK FStar.Class.Add.fst
- CHECK FStar.Integers.fst
- CHECK FStar.Int128.fst
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Stubs.Reflection.V1.Builtins.fsti
- LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fsti
- LAXCHECK FStarC.SMTEncoding.Solver.Cache.fsti
- LAXCHECK FStarC.Extraction.ML.UEnv.fsti
- LAXCHECK FStarC.SMTEncoding.Util.fsti
- LAXCHECK FStarC.TypeChecker.Core.fsti
- LAXCHECK FStarC.TypeChecker.Tc.fsti
- LAXCHECK FStarC.TypeChecker.Err.fsti
- LAXCHECK FStarC.Reflection.V1.Embeddings.fsti
- LAXCHECK FStarC.TypeChecker.Rel.fsti
- LAXCHECK FStarC.Reflection.V1.Builtins.fsti
- LAXCHECK FStarC.Reflection.V2.Builtins.fsti
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/FStar.UInt.fsti(436,8-436,51)
-
- LAXCHECK FStarC.TypeChecker.Util.fsti
- * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(509,13-509,47):
- - Effectful argument let _ = FStarC.Ident.string_of_id op_plus in
- _ = "+" (FStarC.Effect.ALL) to erased function assert, consider let binding it
-
- LAXCHECK FStarC.TypeChecker.Env.fst
- LAXCHECK FStarC.TypeChecker.TcEffect.fsti
- LAXCHECK FStarC.Interactive.JsonHelper.fst
- LAXCHECK FStarC.TypeChecker.DeferredImplicits.fsti
- * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(527,19-527,56):
- - Effectful argument let _ = FStarC.Ident.string_of_lid max_lid in
- _ = "max" (FStarC.Effect.ALL) to erased function assert, consider let binding it
-
- LAXCHECK FStarC.TypeChecker.PatternUtils.fsti
- LAXCHECK FStarC.Reflection.V2.Embeddings.fsti
- LAXCHECK FStarC.TypeChecker.Positivity.fsti
- LAXCHECK FStarC.TypeChecker.DMFF.fsti
- LAXCHECK FStarC.TypeChecker.Generalize.fsti
- LAXCHECK FStarC.TypeChecker.Quals.fsti
- LAXCHECK FStarC.SMTEncoding.Solver.fsti
- LAXCHECK FStarC.Tactics.Hooks.fsti
- LAXCHECK FStarC.SMTEncoding.SolverState.fst
- CHECK FStar.Tactics.Visit.fst
- CHECK FStar.Reflection.V2.fst
- CHECK FStar.Reflection.V2.Compare.fst
- CHECK FStar.Class.Ord.Raw.fsti
- CHECK FStar.Class.Eq.fst
- LAXCHECK FStarC.SMTEncoding.Solver.Cache.fst
- LAXCHECK FStarC.TypeChecker.NBETerm.fsti
- LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fst
- LAXCHECK FStarC.Tactics.Types.Reflection.fsti
- LAXCHECK FStarC.TypeChecker.DeferredImplicits.fst
- LAXCHECK FStarC.TypeChecker.PatternUtils.fst
- LAXCHECK FStarC.TypeChecker.TcTerm.fsti
- LAXCHECK FStarC.TypeChecker.TcInductive.fsti
- LAXCHECK FStarC.Extraction.ML.Modul.fsti
- LAXCHECK FStarC.SMTEncoding.Env.fst
- LAXCHECK FStarC.Extraction.ML.Util.fsti
- LAXCHECK FStarC.Extraction.ML.RegEmb.fsti
- LAXCHECK FStarC.Extraction.Krml.fsti
- LAXCHECK FStarC.Extraction.ML.Term.fsti
- LAXCHECK FStarC.SMTEncoding.ErrorReporting.fsti
- LAXCHECK FStarC.SMTEncoding.Util.fst
- LAXCHECK FStarC.Reflection.V1.Embeddings.fst
- LAXCHECK FStarC.Extraction.ML.UEnv.fst
- LAXCHECK FStarC.Reflection.V2.Embeddings.fst
- CHECK FStar.Tactics.V2.SyntaxHelpers.fsti
- CHECK FStar.Class.Embeddable.fsti
- CHECK FStar.Reflection.Typing.Builtins.fsti
- CHECK FStar.Reflection.fst
- CHECK FStar.Reflection.V1.Derived.fst
- CHECK FStar.Stubs.Tactics.V1.Builtins.fsti
- LAXCHECK FStarC.Tactics.Types.Reflection.fst
- CHECK FStar.RBMap.fsti
- CHECK FStar.RBSet.fsti
- CHECK FStar.Class.Ord.Raw.fst
- CHECK FStar.Tactics.V2.SyntaxCoercions.fst
- CHECK FStar.Reflection.V2.Formula.fst
- CHECK FStar.Tactics.SMT.fst
- CHECK FStar.Tactics.LaxTermEq.fst
- CHECK FStar.Tactics.NamedView.fst
- CHECK FStar.ModifiesGen.fst
- CHECK FStar.FunctionalExtensionality.fst
- CHECK FStar.Int.Cast.Full.fst
- CHECK FStar.Reflection.Typing.fsti
- CHECK FStar.Tactics.Names.fst
- CHECK FStar.Tactics.Builtins.fsti
- CHECK FStar.SizeT.fst
- LAXCHECK FStarC.SMTEncoding.ErrorReporting.fst
- LAXCHECK FStarC.Extraction.ML.Util.fst
- LAXCHECK FStarC.Extraction.ML.Code.fst
- LAXCHECK FStarC.Extraction.Krml.fst
- CHECK FStar.Class.Embeddable.fst
- CHECK FStar.Tactics.SyntaxHelpers.fst
- CHECK FStar.Tactics.V2.SyntaxHelpers.fst
- LAXCHECK FStarC.TypeChecker.Primops.Base.fsti
- LAXCHECK FStarC.MachineInts.fsti
- LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fsti
- LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fsti
- LAXCHECK FStarC.TypeChecker.NBETerm.fst
- CHECK FStar.RBMap.fst
- CHECK FStar.RBSet.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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
-
- CHECK FStar.Tactics.MApply.fsti
- CHECK FStar.Reflection.V1.Derived.Lemmas.fst
- CHECK FStar.Reflection.V1.Formula.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
- LAXCHECK FStarC.TypeChecker.Primops.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Array.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Sealed.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Issue.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Base.fst
- LAXCHECK FStarC.TypeChecker.Primops.Real.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Erased.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fsti
- LAXCHECK FStarC.Tactics.V1.Primops.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Eq.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Range.fsti
- LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Docs.fsti
- LAXCHECK FStarC.Tactics.V2.Primops.fsti
- CHECK FStar.Tactics.MApply.fst
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.ConstantTime.Integers.fsti
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/src/extraction/FStarC.Extraction.ML.Code.fst(785,12-785,17):
- - Local binding 'p_sig' is recursive but not used in its body
-
- CHECK FStar.PtrdiffT.fst
- CHECK FStar.Tactics.V2.Logic.fsti
- CHECK FStar.Tactics.V2.Derived.fst
- CHECK FStar.Reflection.Formula.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Tactics.Types.fsti
- LAXCHECK FStarC.TypeChecker.Cfg.fsti
- LAXCHECK FStarC.Universal.fsti
- LAXCHECK FStarC.TypeChecker.Primops.Array.fst
- LAXCHECK FStarC.SMTEncoding.Solver.fst
- LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fst
- LAXCHECK FStarC.CheckedFiles.fst
- LAXCHECK FStarC.TypeChecker.Primops.Real.fst
- LAXCHECK FStarC.TypeChecker.Primops.fst
- LAXCHECK FStarC.TypeChecker.Primops.Issue.fst
- LAXCHECK FStarC.TypeChecker.Primops.Eq.fst
- LAXCHECK FStarC.TypeChecker.Primops.Docs.fst
- LAXCHECK FStarC.TypeChecker.Primops.Range.fst
- LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fst
- LAXCHECK FStarC.TypeChecker.Primops.Sealed.fst
- LAXCHECK FStarC.TypeChecker.Primops.Erased.fst
- CHECK FStar.Reflection.V1.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/ulib/FStar.RBMap.fst(144,8-144,15):
- - Global binding 'FStar.RBMap.for_any' is recursive but not used in its body
-
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Interactive.Ide.Types.fsti
- CHECK FStar.Tactics.Logic.fst
- LAXCHECK FStarC.Tactics.Result.fsti
- LAXCHECK FStarC.Tactics.Embedding.fsti
- LAXCHECK FStarC.Tactics.Native.fsti
- LAXCHECK FStarC.Tactics.Printing.fsti
- CHECK FStar.Tactics.V1.Logic.fsti
- LAXCHECK FStarC.Tactics.Types.fst
- CHECK FStar.Tactics.V1.SyntaxHelpers.fst
- CHECK FStar.ConstantTime.Integers.fst
- LAXCHECK FStarC.TypeChecker.Normalize.fsti
- LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fsti
- LAXCHECK FStarC.Reflection.V2.Interpreter.fst
- LAXCHECK FStarC.TypeChecker.Cfg.fst
- LAXCHECK FStarC.Reflection.V1.Interpreter.fst
- LAXCHECK FStarC.Tactics.Monad.fsti
- LAXCHECK FStarC.Tactics.Result.fst
- LAXCHECK FStarC.Tactics.Printing.fst
- LAXCHECK FStarC.Tactics.Embedding.fst
- LAXCHECK FStarC.Interactive.QueryHelper.fsti
- LAXCHECK FStarC.Interactive.PushHelper.fsti
- LAXCHECK FStarC.Interactive.Incremental.fsti
- LAXCHECK FStarC.Interactive.Ide.Types.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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.2025.12.15/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.Normalize.Unfolding.fst
- LAXCHECK FStarC.TypeChecker.NBE.fsti
- LAXCHECK FStarC.TypeChecker.Err.fst
- LAXCHECK FStarC.Reflection.V1.Builtins.fst
- LAXCHECK FStarC.SMTEncoding.Encode.fst
- LAXCHECK FStarC.Extraction.ML.Term.fst
- LAXCHECK FStarC.TypeChecker.Rel.fst
- LAXCHECK FStarC.TypeChecker.Generalize.fst
- LAXCHECK FStarC.TypeChecker.Quals.fst
- LAXCHECK FStarC.Extraction.ML.Modul.fst
- LAXCHECK FStarC.TypeChecker.Tc.fst
- LAXCHECK FStarC.TypeChecker.TcTerm.fst
- CHECK FStar.Tactics.V1.Derived.fst
- LAXCHECK FStarC.TypeChecker.Normalize.fst
- LAXCHECK FStarC.TypeChecker.Util.fst
- LAXCHECK FStarC.TypeChecker.DMFF.fst
- LAXCHECK FStarC.TypeChecker.Positivity.fst
- LAXCHECK FStarC.TypeChecker.Core.fst
- LAXCHECK FStarC.TypeChecker.TcInductive.fst
- LAXCHECK FStarC.TypeChecker.TcEffect.fst
- LAXCHECK FStarC.SMTEncoding.EncodeTerm.fst
- LAXCHECK FStarC.Reflection.V2.Builtins.fst
- LAXCHECK FStarC.Tactics.InterpFuns.fsti
- LAXCHECK FStarC.Tactics.V1.Basic.fsti
- LAXCHECK FStarC.Tactics.Interpreter.fsti
- LAXCHECK FStarC.Tactics.V2.Basic.fsti
- LAXCHECK FStarC.Tactics.CtrlRewrite.fsti
- LAXCHECK FStarC.Tactics.Monad.fst
- CHECK FStar.Buffer.Quantifiers.fst
- CHECK FStar.Modifies.fsti
- LAXCHECK FStarC.Interactive.QueryHelper.fst
- LAXCHECK FStarC.Interactive.Incremental.fst
- LAXCHECK FStarC.Interactive.Ide.fst
- LAXCHECK FStarC.Interactive.PushHelper.fst
- LAXCHECK FStarC.TypeChecker.NBE.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
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/src/typechecker/FStarC.TypeChecker.Err.fst(132,30-132,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 '@'.
-
- * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/src/typechecker/FStarC.TypeChecker.Err.fst(140,29-140,30):
- - 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 '@'.
-
- LAXCHECK FStarC.Tactics.CtrlRewrite.fst
- LAXCHECK FStarC.Main.fst
- LAXCHECK FStarC.Tactics.Interpreter.fst
- LAXCHECK FStarC.Hooks.fst
- CHECK FStar.Pointer.Derived1.fsti
- LAXCHECK FStarC.Universal.fst
- CHECK FStar.Pointer.Base.fst
- LAXCHECK FStarC.Extraction.ML.RegEmb.fst
- LAXCHECK FStarC.Tactics.InterpFuns.fst
- LAXCHECK FStarC.Tactics.V1.Primops.fst
- LAXCHECK FStarC.Tactics.V1.Basic.fst
- LAXCHECK FStarC.Tactics.V2.Basic.fst
- LAXCHECK FStarC.Tactics.V2.Primops.fst
- LAXCHECK FStarC.Tactics.Hooks.fst
- * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 FStar.Tactics.V2.Bare.fsti
- CHECK FStar.Tactics.CanonCommSemiring.fst
- CHECK FStar.Tactics.MkProjectors.fst
- CHECK FStar.Tactics.Print.fst
- CHECK FStar.Tactics.Typeclasses.fst
- CHECK FStar.Tactics.V2.Logic.fst
- CHECK FStar.Tactics.Derived.fst
- CHECK FStar.UInt128.fst
- CHECK FStar.Tactics.MApply0.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/ulib/LowStar.Printf.fst(253,8-253,13):
- - Global binding 'LowStar.Printf.arg_t' is recursive but not used in its body
-
- CHECK LowStar.Modifies.fst
- CHECK LowStar.BufferOps.fst
- CHECK LowStar.ImmutableBuffer.fst
- CHECK LowStar.BufferCompat.fst
- * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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 FStar.Tactics.V2.fsti
- CHECK FStar.Reflection.V2.Arith.fst
- CHECK FStar.Tactics.CanonCommMonoidSimple.Equiv.fst
- CHECK FStar.Tactics.PrettifyType.fsti
- CHECK FStar.Tactics.Easy.fst
- CHECK FStar.Tactics.Parametricity.fst
- CHECK FStar.Tactics.TypeRepr.fsti
- CHECK FStar.Tactics.CheckLN.fsti
- CHECK FStar.Tactics.CanonCommMonoidSimple.fst
- CHECK LowStar.BufferView.fst
- CHECK LowStar.BufferView.Up.fsti
- CHECK LowStar.BufferView.Down.fst
- CHECK FStar.Bytes.fsti
- CHECK LowStar.ModifiesPat.fst
- CHECK LowStar.Vector.fst
- CHECK LowStar.Regional.fst
- CHECK LowStar.ToFStarBuffer.fst
- CHECK FStar.Modifies.fst
- CHECK LowStar.Endianness.fst
- CHECK FStar.Pointer.Derived2.fsti
- CHECK FStar.Pointer.Derived3.fsti
- CHECK FStar.Pointer.Derived1.fst
- CHECK FStar.Tactics.CheckLN.fst
- CHECK FStar.ReflexiveTransitiveClosure.fst
- CHECK FStar.Tactics.fsti
- CHECK FStar.Tactics.Simplifier.fst
- CHECK FStar.Tactics.CanonCommMonoid.fst
- CHECK FStar.Tactics.TypeRepr.fst
- CHECK FStar.FiniteMap.Base.fst
- CHECK FStar.Tactics.CanonMonoid.fst
- CHECK FStar.BigOps.fst
- CHECK FStar.Reflection.Typing.fst
- CHECK FStar.Tactics.PrettifyType.fst
- CHECK FStar.Tactics.V1.fsti
- CHECK FStar.Tactics.V1.Logic.fst
- * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/Prims.fst(289,5-289,13)
-
- * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/Prims.fst(289,5-289,13)
-
- * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/Prims.fst(289,5-289,13)
-
- * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/ulib/Prims.fst(289,5-289,13)
-
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.Pointer.Derived3.fst
- CHECK FStar.Pointer.Derived2.fst
- CHECK FStar.Pointer.fst
- CHECK FStar.Tactics.BreakVC.fsti
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.WellFounded.Util.fst
- CHECK FStar.Tactics.PatternMatching.fst
- CHECK FStar.Pure.BreakVC.fsti
- CHECK LowStar.BufferView.Up.fst
- CHECK LowStar.ConstBuffer.fsti
- CHECK LowStar.UninitializedBuffer.fst
- CHECK LowStar.Literal.fsti
- CHECK FStar.InteractiveHelpers.Base.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK FStar.Crypto.fst
- CHECK FStar.Udp.fsti
- CHECK FStar.Tcp.fsti
- CHECK FStar.Tactics.Arith.fst
- CHECK FStar.Tactics.Canon.fst
- CHECK FStar.Tactics.BV.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK FStar.TaggedUnion.fsti
- CHECK FStar.BufferNG.fst
- CHECK FStar.Tactics.BreakVC.fst
- CHECK FStar.Pure.BreakVC.fst
- CHECK LowStar.ConstBuffer.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.TaggedUnion.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK LowStar.PrefixFreezableBuffer.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK FStar.InteractiveHelpers.ExploreTerm.fst
- CHECK LowStar.RVector.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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 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.2025.12.15/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
-
- DONE CHECK FSTARC
- CHECK FStar.InteractiveHelpers.PostProcess.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.2025.12.15/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.Math.Fermat.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- CHECK LowStar.Regional.Instances.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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.InteractiveHelpers.fst
- * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15/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
-
- INSTALL LIB
- INSTALL FSTARC
-> compiled fstar.2025.12.15
[fstar: make install]
+ /usr/bin/make "PREFIX=/home/opam/.opam/default" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2025.12.15)
- DUNE BUILD
- DUNE INSTALL
- CHECK LIB
- INSTALL LIB SRC
- INSTALL LIB
- CHECK FSTARC
- DONE CHECK FSTARC
- INSTALL FSTARC
-> installed fstar.2025.12.15
[WARNING] Opam package conf-gmp.5 depends on the following system package that can no longer be found: libgmp-dev
Dependency Graph
Loading graph...
View raw DOT format
digraph opam {
"base-bytes.base" -> {"ocaml.5.3.0" "ocamlfind.1.9.8"}
"batteries.3.10.0" -> {"camlp-streams.5.0.1" "dune.3.20.2" "num.1.6" "ocaml.5.3.0" "ocamlfind.1.9.8"}
"camlp-streams.5.0.1" -> {"dune.3.20.2" "ocaml.5.3.0"}
"cppo.1.8.0" -> {"base-unix.base" "dune.3.20.2" "ocaml.5.3.0"}
"dune.3.20.2" -> {"base-threads.base" "base-unix.base" "ocaml.5.3.0"}
"fstar.2025.12.15" -> {"batteries.3.10.0" "dune.3.20.2" "memtrace.0.2.3" "menhir.20250912" "menhirLib.20250912" "mtime.2.1.0" "ocaml.5.3.0" "pprint.20230830" "ppx_deriving.6.1.1" "ppx_deriving_yojson.3.10.0" "ppxlib.0.37.0" "process.0.2.1" "sedlex.3.7" "stdint.0.7.2" "yojson.3.0.0" "zarith.1.14"}
"gen.1.1" -> {"dune.3.20.2" "ocaml.5.3.0" "seq.base"}
"memtrace.0.2.3" -> {"dune.3.20.2" "ocaml.5.3.0"}
"menhir.20250912" -> {"dune.3.20.2" "menhirCST.20250912" "menhirLib.20250912" "menhirSdk.20250912" "ocaml.5.3.0"}
"menhirCST.20250912" -> {"dune.3.20.2" "ocaml.5.3.0"}
"menhirLib.20250912" -> {"dune.3.20.2" "ocaml.5.3.0"}
"menhirSdk.20250912" -> {"dune.3.20.2" "ocaml.5.3.0"}
"mtime.2.1.0" -> {"ocaml.5.3.0" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"num.1.6" -> "ocaml.5.3.0";
"ocaml.5.3.0" -> {"ocaml-base-compiler.5.3.0" "ocaml-config.3"}
"ocaml-base-compiler.5.3.0" -> "ocaml-compiler.5.3.0";
"ocaml-compiler-libs.v0.17.0" -> {"dune.3.20.2" "ocaml.5.3.0"}
"ocaml-config.3" -> "ocaml-base-compiler.5.3.0";
"ocamlbuild.0.16.1" -> "ocaml.5.3.0";
"ocamlfind.1.9.8" -> "ocaml.5.3.0";
"pprint.20230830" -> {"dune.3.20.2" "ocaml.5.3.0"}
"ppx_derivers.1.2.1" -> {"dune.3.20.2" "ocaml.5.3.0"}
"ppx_deriving.6.1.1" -> {"cppo.1.8.0" "dune.3.20.2" "ocaml.5.3.0" "ocamlfind.1.9.8" "ppx_derivers.1.2.1" "ppxlib.0.37.0"}
"ppx_deriving_yojson.3.10.0" -> {"dune.3.20.2" "ocaml.5.3.0" "ppx_deriving.6.1.1" "ppxlib.0.37.0" "yojson.3.0.0"}
"ppxlib.0.37.0" -> {"dune.3.20.2" "ocaml.5.3.0" "ocaml-compiler-libs.v0.17.0" "ppx_derivers.1.2.1" "sexplib0.v0.17.0" "stdlib-shims.0.3.0"}
"process.0.2.1" -> {"base-bytes.base" "base-unix.base" "ocaml.5.3.0" "ocamlbuild.0.16.1" "ocamlfind.1.9.8"}
"sedlex.3.7" -> {"dune.3.20.2" "gen.1.1" "ocaml.5.3.0" "ppxlib.0.37.0"}
"seq.base" -> "ocaml.5.3.0";
"sexplib0.v0.17.0" -> {"dune.3.20.2" "ocaml.5.3.0"}
"stdint.0.7.2" -> {"dune.3.20.2" "ocaml.5.3.0"}
"stdlib-shims.0.3.0" -> {"dune.3.20.2" "ocaml.5.3.0"}
"topkg.1.1.1" -> {"ocaml.5.3.0" "ocamlbuild.0.16.1" "ocamlfind.1.9.8"}
"yojson.3.0.0" -> {"dune.3.20.2" "ocaml.5.3.0"}
"zarith.1.14" -> {"conf-gmp.5" "conf-pkg-config.4" "ocaml.5.3.0" "ocamlfind.1.9.8"}
}