Build:
- 0
2026-06-26 10:07.10: New job: build fstar.2025.02.17 (2db3a674a5f3) 2026-06-26 10:07.10: Waiting for resource in pool day11-builds 2026-06-26 10:28.22: Got resource from pool day11-builds 2026-06-26 10:28.22: [profile full] build fstar.2025.02.17 2026-06-26 10:28.22: build fstar.2025.02.17 (2db3a674a5f3) === DEPENDENCIES (39 transitive) === base-bytes.base b1e4ea0d0665 base-threads.base c9e7bdbf5823 base-unix.base 7d1428be9ddb batteries.3.10.0 17c83a7580ee camlp-streams.5.0.1 c03309bddd0c conf-gmp.5 be11edf77089 conf-pkg-config.5 d5de2c6a88f9 cppo.1.8.0 e33aa9aae66d dune.3.23.1 9d721df3a13a gen.1.1 2291834c6da2 memtrace.0.2.3 8a880fb056d1 menhir.20260209 05da01205928 menhirCST.20260209 10afe0461689 menhirGLR.20260209 7b22500e7305 menhirLib.20260209 0f58e6c70ac8 menhirSdk.20260209 caf07569aba6 mtime.2.1.0 f8086d5bd93e num.1.6 bf28d08d4620 ocaml.5.3.0 ec34d524d97d ocaml-base-compiler.5.3.0 1841888fe75b ocaml-compiler.5.3.0 f295fe609c87 ocaml-compiler-libs.v0.17.0 ae1038bc23cf ocaml-config.3 a52eea84eedb ocamlbuild.0.16.1 bdeca1c5518a ocamlfind.1.9.8 558092066ff0 pprint.20230830 6132a6b605b1 ppx_derivers.1.2.1 fe71b19cf412 ppx_deriving.6.0.3 1fd3759ed4f6 ppx_deriving_yojson.3.9.1 1d4431eaeea6 ppxlib.0.35.0 c1fcf64e4dff process.0.2.1 42eeaba9574c sedlex.3.4 75801697c62a seq.base cd738ac20daf sexplib0.v0.17.0 a15b0f614c90 stdint.0.7.2 e045bac3d3f8 stdlib-shims.0.3.0 c94355dec213 topkg.1.1.1 e3d6961e1f2d yojson.3.0.0 2870f90eedda zarith.1.14 88f19ac83a9a === STDOUT === Processing: [default: loading data] [fstar.2025.02.17: dl] [fstar.2025.02.17: extract] -> retrieved fstar.2025.02.17 (https://opam.ocaml.org/cache) [fstar: make 39] + /usr/bin/make "-j" "39" "ADMIT=1" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17) - STAGE 0 - DUNE BUILD - INSTALL LIB SRC - File "fstar-guts/FStarC_Parser_Parse.mly", line 126, characters 60-70: - Warning: the token LBRACK_BAR is unused. - File "fstar-guts/FStarC_Parser_Parse.mly", line 324, characters 0-15: - Warning: symbol decoratableDecl is unreachable from any of the start symbols. - File "fstar-guts/FStarC_Parser_Parse.mly", line 307, characters 0-16: - Warning: symbol noDecorationDecl is unreachable from any of the start symbols. - Warning: 20 states have shift/reduce conflicts. - Warning: 232 states have end-of-stream conflicts. - Warning: 305 shift/reduce conflicts were arbitrarily resolved. - Warning: 232 end-of-stream conflicts were arbitrarily resolved. - DUNE INSTALL - DUNE CLEAN - EXTRACT STAGE 1 FSTARC-BARE - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src - LAXCHECK Prims.fst - LAXCHECK FStar.Pervasives.Native.fst - LAXCHECK FStar.Pervasives.fsti - LAXCHECK FStar.Pervasives.fst - LAXCHECK FStar.Ghost.fsti - LAXCHECK FStar.Classical.Sugar.fsti - LAXCHECK FStar.Classical.fsti - LAXCHECK FStar.Squash.fsti - LAXCHECK FStar.Sealed.fsti - LAXCHECK FStar.Float.fsti - LAXCHECK FStar.Mul.fst - LAXCHECK FStar.Stubs.TypeChecker.Core.fsti - LAXCHECK FStar.Monotonic.Pure.fst - LAXCHECK FStarC.Effect.fsti - LAXCHECK FStar.ImmutableArray.Base.fsti - LAXCHECK FStarC.Array.fsti - LAXCHECK FStarC.VConfig.fsti - LAXCHECK FStar.Exn.fst - LAXCHECK FStar.Set.fsti - LAXCHECK FStarC.Errors.Codes.fsti - LAXCHECK FStar.Preorder.fst - LAXCHECK FStarC.Sealed.fsti - LAXCHECK FStarC.NormSteps.fst - LAXCHECK FStarC.Real.fsti - LAXCHECK FStar.Order.fst - LAXCHECK FStarC.Reflection.V2.Interpreter.fsti - LAXCHECK FStarC.Reflection.V1.Interpreter.fsti - LAXCHECK FStar.Range.fsti - LAXCHECK FStar.List.Tot.Base.fst - LAXCHECK FStar.Math.Lemmas.fsti - LAXCHECK FStarC.Real.fst - LAXCHECK FStarC.PIMap.fsti - LAXCHECK FStarC.Misc.fsti - LAXCHECK FStarC.OCaml.fsti - LAXCHECK FStarC.Hints.fsti - LAXCHECK FStarC.Interactive.Ide.fsti - LAXCHECK FStarC.Hooks.fsti - LAXCHECK FStarC.Interactive.Legacy.fsti - LAXCHECK FStarC.Interactive.Lsp.fsti - LAXCHECK FStarC.Prettyprint.fsti - LAXCHECK FStarC.BigInt.fsti - LAXCHECK FStarC.Json.fsti - LAXCHECK FStarC.List.fsti - LAXCHECK FStarC.PSMap.fsti - LAXCHECK FStarC.Find.fsti - LAXCHECK FStarC.SMap.fsti - LAXCHECK FStarC.Filepath.fsti - LAXCHECK FStarC.Debug.fsti - LAXCHECK FStarC.Options.Ext.fsti - LAXCHECK FStarC.VConfig.fst - LAXCHECK FStarC.Order.fsti - LAXCHECK FStar.Monotonic.Witnessed.fsti - LAXCHECK FStarC.GenSym.fsti - LAXCHECK FStarC.Thunk.fsti - LAXCHECK FStarC.Unionfind.fsti - LAXCHECK FStarC.Dyn.fsti - LAXCHECK FStarC.Option.fsti - LAXCHECK FStarC.Platform.Base.fsti - LAXCHECK FStarC.Plugins.Base.fsti - LAXCHECK FStarC.Hash.fsti - LAXCHECK FStarC.Profiling.fsti - LAXCHECK FStarC.Timing.fsti - LAXCHECK FStarC.Sealed.fst - EXTRACT FStarC_NormSteps.ml - EXTRACT FStarC_Real.ml - LAXCHECK FStar.IndefiniteDescription.fsti - LAXCHECK FStar.Stubs.Reflection.Types.fsti - LAXCHECK FStarC.Option.fst - LAXCHECK FStarC.Thunk.fst - LAXCHECK FStarC.GenSym.fst - LAXCHECK FStarC.Plugins.fsti - LAXCHECK FStarC.Common.fsti - LAXCHECK FStarC.Order.fst - LAXCHECK FStar.TSet.fsti - EXTRACT FStarC_Sealed.ml - EXTRACT FStarC_GenSym.ml - EXTRACT FStarC_Thunk.ml - EXTRACT FStarC_VConfig.ml - LAXCHECK FStar.StrongExcludedMiddle.fst - EXTRACT FStarC_Option.ml - EXTRACT FStarC_Order.ml - LAXCHECK FStar.Monotonic.Heap.fsti - LAXCHECK FStarC.Errors.Codes.fst - EXTRACT FStar_Pervasives.ml - LAXCHECK FStar.List.Tot.Properties.fsti - LAXCHECK FStar.Heap.fst - LAXCHECK FStar.List.Tot.fst - LAXCHECK FStar.ST.fst - LAXCHECK FStar.Seq.Base.fsti - EXTRACT FStarC_Errors_Codes.ml - LAXCHECK FStar.Seq.Base.fst - LAXCHECK FStar.Seq.Properties.fsti - LAXCHECK FStar.BitVector.fsti - LAXCHECK FStar.All.fsti - LAXCHECK FStar.List.fst - LAXCHECK FStar.UInt.fsti - EXTRACT FStar_Seq_Base.ml - LAXCHECK FStar.Seq.Properties.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - LAXCHECK FStar.UInt32.fsti - LAXCHECK FStar.Char.fsti - LAXCHECK FStar.Pprint.fsti - LAXCHECK FStarC.BaseTypes.fsti - LAXCHECK FStarC.String.fsti - LAXCHECK FStar.String.fsti - LAXCHECK FStarC.Getopt.fsti - LAXCHECK FStarC.Util.fsti - LAXCHECK FStarC.Bytes.fsti - LAXCHECK FStar.Issue.fsti - LAXCHECK FStar.Stubs.Errors.Msg.fsti - LAXCHECK FStar.Stubs.Tactics.Common.fsti - LAXCHECK FStarC.Common.fst - LAXCHECK FStarC.Debug.fst - LAXCHECK FStarC.Pprint.fsti - LAXCHECK FStarC.StringBuffer.fsti - LAXCHECK FStarC.Misc.fst - LAXCHECK FStar.Stubs.Tactics.Types.fsti - LAXCHECK FStar.Stubs.Tactics.Result.fsti - LAXCHECK FStarC.Find.Z3.fsti - EXTRACT FStarC_Common.ml - EXTRACT FStarC_Debug.ml - EXTRACT FStarC_Misc.ml - LAXCHECK FStar.Tactics.Effect.fsti - EXTRACT FStar_Seq_Properties.ml - LAXCHECK FStar.Tactics.Typeclasses.fsti - LAXCHECK FStarC.Class.Monad.fsti - LAXCHECK FStarC.Class.Show.fsti - LAXCHECK FStarC.Errors.Msg.fsti - LAXCHECK FStarC.Class.Deq.fsti - LAXCHECK FStarC.Class.Tagged.fsti - LAXCHECK FStarC.Class.Listlike.fsti - LAXCHECK FStarC.Class.Monoid.fsti - LAXCHECK FStarC.Class.Monoid.fst - LAXCHECK FStarC.Errors.Msg.fst - LAXCHECK FStarC.Class.Monad.fst - LAXCHECK FStarC.Writer.fsti - LAXCHECK FStarC.Class.Listlike.fst - LAXCHECK FStarC.Class.Show.fst - LAXCHECK FStarC.Find.fst - LAXCHECK FStarC.Options.Ext.fst - LAXCHECK FStarC.Options.fsti - LAXCHECK FStarC.Class.PP.fsti - LAXCHECK FStarC.Platform.fsti - LAXCHECK FStarC.Class.Tagged.fst - LAXCHECK FStarC.Class.Deq.fst - LAXCHECK FStarC.Class.Ord.fsti - LAXCHECK FStarC.Path.fsti - LAXCHECK FStarC.Writer.fst - EXTRACT FStarC_Class_Monoid.ml - EXTRACT FStarC_Errors_Msg.ml - LAXCHECK FStarC.Platform.fst - LAXCHECK FStarC.OCaml.fst - EXTRACT FStarC_Class_Tagged.ml - LAXCHECK FStarC.Path.fst - LAXCHECK FStarC.Class.PP.fst - LAXCHECK FStarC.Range.Type.fsti - LAXCHECK FStarC.Class.Ord.fst - LAXCHECK FStarC.Class.Setlike.fsti - LAXCHECK FStarC.CList.fsti - LAXCHECK FStarC.Class.Hashable.fsti - EXTRACT FStarC_Options_Ext.ml - EXTRACT FStarC_Class_Show.ml - EXTRACT FStarC_Find.ml - EXTRACT FStarC_Class_Listlike.ml - EXTRACT FStarC_Writer.ml - EXTRACT FStarC_Class_Monad.ml - EXTRACT FStarC_Class_Deq.ml - LAXCHECK FStarC.Options.fst - LAXCHECK FStarC.Profiling.fst - LAXCHECK FStarC.Find.Z3.fst - LAXCHECK FStarC.Class.Hashable.fst - EXTRACT FStarC_Platform.ml - EXTRACT FStarC_OCaml.ml - LAXCHECK FStarC.CList.fst - EXTRACT FStarC_Path.ml - LAXCHECK FStarC.Range.Type.fst - LAXCHECK FStarC.Range.Ops.fsti - LAXCHECK FStarC.Class.HasRange.fsti - EXTRACT FStarC_Class_PP.ml - EXTRACT FStarC_Class_Hashable.ml - LAXCHECK FStarC.Range.fsti - EXTRACT FStarC_Range_Type.ml - LAXCHECK FStarC.Range.Ops.fst - EXTRACT FStarC_CList.ml - LAXCHECK FStarC.Class.Setlike.fst - LAXCHECK FStarC.FlatSet.fsti - LAXCHECK FStarC.RBSet.fsti - LAXCHECK FStarC.Class.HasRange.fst - LAXCHECK FStarC.Ident.fsti - LAXCHECK FStarC.Errors.fsti - EXTRACT FStarC_Class_Ord.ml - EXTRACT FStarC_Range_Ops.ml - EXTRACT FStarC_Find_Z3.ml - EXTRACT FStarC_Class_HasRange.ml - EXTRACT FStarC_Profiling.ml - LAXCHECK FStarC.Ident.fst - LAXCHECK FStarC.Parser.Const.Tuples.fsti - LAXCHECK FStarC.Parser.Dep.fsti - LAXCHECK FStarC.Const.fsti - LAXCHECK FStarC.Interactive.CompletionTable.fsti - LAXCHECK FStarC.Errors.fst - LAXCHECK FStarC.Plugins.fst - LAXCHECK FStarC.Interactive.JsonHelper.fsti - LAXCHECK FStarC.RBSet.fst - LAXCHECK FStarC.FlatSet.fst - EXTRACT FStarC_Class_Setlike.ml - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.02.17/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.02.17/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.02.17/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 '@'. - - EXTRACT FStarC_Plugins.ml - LAXCHECK FStarC.Parser.Const.Tuples.fst - LAXCHECK FStarC.Interactive.CompletionTable.fst - EXTRACT FStarC_FlatSet.ml - LAXCHECK FStarC.Const.fst - LAXCHECK FStarC.Parser.Const.fst - LAXCHECK FStarC.Syntax.Syntax.fsti - LAXCHECK FStarC.Extraction.ML.Syntax.fsti - EXTRACT FStarC_Ident.ml - LAXCHECK FStarC.Dependencies.fsti - EXTRACT FStarC_RBSet.ml - EXTRACT FStarC_Parser_Const_Tuples.ml - EXTRACT FStarC_Const.ml - LAXCHECK FStarC.Dependencies.fst - EXTRACT FStarC_Errors.ml - EXTRACT FStarC_Parser_Const.ml - EXTRACT FStarC_Interactive_CompletionTable.ml - LAXCHECK FStarC.Extraction.ML.Syntax.fst - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fsti - LAXCHECK FStarC.Extraction.ML.Code.fsti - LAXCHECK FStarC.Extraction.ML.PrintFS.fsti - LAXCHECK FStarC.Extraction.ML.PrintML.fsti - EXTRACT FStarC_Dependencies.ml - EXTRACT FStarC_Options.ml - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fst - EXTRACT FStarC_Extraction_ML_Syntax.ml - LAXCHECK FStarC.Extraction.ML.PrintFS.fst - LAXCHECK FStarC.Syntax.Syntax.fst - LAXCHECK FStarC.Syntax.Unionfind.fsti - LAXCHECK FStarC.Syntax.Subst.fsti - LAXCHECK FStarC.Syntax.InstFV.fsti - LAXCHECK FStarC.Syntax.Free.fsti - LAXCHECK FStarC.Syntax.VisitM.fsti - LAXCHECK FStarC.Parser.AST.fsti - LAXCHECK FStarC.Syntax.Formula.fsti - LAXCHECK FStarC.Syntax.MutRecTy.fsti - LAXCHECK FStarC.Syntax.Print.Ugly.fsti - LAXCHECK FStarC.Syntax.Embeddings.Base.fsti - LAXCHECK FStarC.Syntax.Visit.fsti - LAXCHECK FStarC.Class.Binders.fsti - LAXCHECK FStarC.TypeChecker.Common.fsti - LAXCHECK FStarC.SMTEncoding.Term.fsti - LAXCHECK FStarC.Reflection.V2.Constants.fst - LAXCHECK FStarC.Reflection.V2.Data.fsti - LAXCHECK FStarC.Reflection.V1.Constants.fst - LAXCHECK FStarC.Tactics.Common.fsti - LAXCHECK FStarC.Syntax.Hash.fsti - LAXCHECK FStarC.Syntax.Compress.fsti - LAXCHECK FStarC.Syntax.TermHashTable.fsti - EXTRACT FStarC_Extraction_ML_RemoveUnusedParameters.ml - LAXCHECK FStarC.Reflection.V1.Data.fsti - EXTRACT FStarC_Reflection_V1_Constants.ml - LAXCHECK FStarC.Tactics.Common.fst - LAXCHECK FStarC.Class.Binders.fst - LAXCHECK FStarC.Defensive.fsti - LAXCHECK FStarC.Syntax.Unionfind.fst - LAXCHECK FStarC.Syntax.Embeddings.fsti - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fsti - LAXCHECK FStarC.Syntax.InstFV.fst - LAXCHECK FStarC.Syntax.Subst.fst - LAXCHECK FStarC.Syntax.Visit.fst - LAXCHECK FStarC.Syntax.Free.fst - LAXCHECK FStarC.Syntax.Util.fsti - LAXCHECK FStarC.Syntax.VisitM.fst - LAXCHECK FStarC.Syntax.Hash.fst - EXTRACT FStarC_Reflection_V2_Constants.ml - EXTRACT FStarC_Extraction_ML_PrintFS.ml - LAXCHECK FStarC.Reflection.V1.Data.fst - LAXCHECK FStarC.Reflection.V2.Data.fst - LAXCHECK FStarC.SMTEncoding.Term.fst - LAXCHECK FStarC.SMTEncoding.UnsatCore.fsti - EXTRACT FStarC_Tactics_Common.ml - LAXCHECK FStarC.SMTEncoding.Pruning.fsti - EXTRACT FStarC_Class_Binders.ml - EXTRACT FStarC_Syntax_InstFV.ml - EXTRACT FStarC_Syntax_Visit.ml - LAXCHECK FStarC.Syntax.Util.fst - LAXCHECK FStarC.Syntax.Print.Ugly.fst - LAXCHECK FStarC.Syntax.MutRecTy.fst - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fst - EXTRACT FStarC_Syntax_Unionfind.ml - LAXCHECK FStarC.SMTEncoding.UnsatCore.fst - LAXCHECK FStarC.SMTEncoding.SolverState.fsti - EXTRACT FStarC_Syntax_Free.ml - EXTRACT FStarC_Syntax_Embeddings_AppEmb.ml - EXTRACT FStarC_Syntax_Hash.ml - LAXCHECK FStarC.SMTEncoding.Pruning.fst - LAXCHECK FStarC.Parser.AST.fst - LAXCHECK FStarC.Parser.ToDocument.fsti - LAXCHECK FStarC.Parser.AST.Util.fsti - LAXCHECK FStarC.Syntax.DsEnv.fsti - EXTRACT FStarC_Reflection_V2_Data.ml - EXTRACT FStarC_Reflection_V1_Data.ml - EXTRACT FStarC_Syntax_Subst.ml - EXTRACT FStarC_SMTEncoding_UnsatCore.ml - EXTRACT FStarC_Syntax_MutRecTy.ml - LAXCHECK FStarC.Syntax.DsEnv.fst - LAXCHECK FStarC.Syntax.Resugar.fsti - LAXCHECK FStarC.Syntax.Print.Pretty.fsti - LAXCHECK FStarC.Syntax.Print.fsti - LAXCHECK FStarC.ToSyntax.ToSyntax.fsti - LAXCHECK FStarC.TypeChecker.Env.fsti - LAXCHECK FStarC.ToSyntax.Interleave.fsti - LAXCHECK FStarC.Parser.ParseIt.fsti - LAXCHECK FStarC.Parser.AST.Util.fst - LAXCHECK FStarC.Parser.ToDocument.fst - EXTRACT FStarC_Syntax_Print_Ugly.ml - EXTRACT FStarC_Syntax_VisitM.ml - LAXCHECK FStarC.SMTEncoding.Z3.fsti - LAXCHECK FStarC.ToSyntax.Interleave.fst - EXTRACT FStarC_SMTEncoding_Pruning.ml - LAXCHECK FStarC.Parser.Driver.fsti - LAXCHECK FStarC.Syntax.Print.fst - LAXCHECK FStarC.Syntax.Formula.fst - LAXCHECK FStarC.Syntax.Embeddings.Base.fst - LAXCHECK FStarC.Syntax.Embeddings.fst - LAXCHECK FStarC.TypeChecker.Common.fst - LAXCHECK FStarC.Defensive.fst - LAXCHECK FStarC.Syntax.Compress.fst - LAXCHECK FStarC.SMTEncoding.Z3.fst - LAXCHECK FStarC.Syntax.Resugar.fst - LAXCHECK FStarC.Syntax.Print.Pretty.fst - EXTRACT FStarC_SMTEncoding_Term.ml - EXTRACT FStarC_Syntax_Util.ml - LAXCHECK FStarC.ToSyntax.ToSyntax.fst - EXTRACT FStarC_Syntax_Syntax.ml - LAXCHECK FStarC.Parser.Driver.fst - LAXCHECK FStarC.Parser.Dep.fst - LAXCHECK FStarC.Prettyprint.fst - EXTRACT FStarC_Parser_AST_Util.ml - EXTRACT FStarC_ToSyntax_Interleave.ml - EXTRACT FStarC_Syntax_Compress.ml - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - - Global binding - 'FStarC.Parser.AST.decl_to_string' - is recursive but not used in its body - - EXTRACT FStarC_Parser_AST.ml - EXTRACT FStarC_Defensive.ml - LAXCHECK FStarC.TypeChecker.Env.fst - LAXCHECK FStarC.SMTEncoding.SolverState.fst - LAXCHECK FStarC.SMTEncoding.Util.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fsti - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fsti - LAXCHECK FStarC.TypeChecker.Err.fsti - LAXCHECK FStarC.TypeChecker.PatternUtils.fsti - LAXCHECK FStarC.TypeChecker.Rel.fsti - LAXCHECK FStarC.TypeChecker.Positivity.fsti - LAXCHECK FStarC.TypeChecker.Util.fsti - LAXCHECK FStarC.Reflection.V2.Builtins.fsti - LAXCHECK FStarC.Reflection.V2.Embeddings.fsti - LAXCHECK FStarC.TypeChecker.Generalize.fsti - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fsti - LAXCHECK FStarC.SMTEncoding.Solver.fsti - LAXCHECK FStarC.TypeChecker.Quals.fsti - LAXCHECK FStarC.TypeChecker.Core.fsti - LAXCHECK FStarC.TypeChecker.DMFF.fsti - LAXCHECK FStarC.TypeChecker.TcEffect.fsti - LAXCHECK FStarC.TypeChecker.Tc.fsti - LAXCHECK FStarC.Extraction.ML.UEnv.fsti - LAXCHECK FStarC.Tactics.Hooks.fsti - LAXCHECK FStarC.Reflection.V1.Builtins.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fsti - LAXCHECK FStarC.Interactive.JsonHelper.fst - EXTRACT FStarC_Prettyprint.ml - EXTRACT FStarC_Parser_Driver.ml - EXTRACT FStarC_Syntax_DsEnv.ml - EXTRACT FStarC_Syntax_Print_Pretty.ml - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - - Global binding - 'FStarC.Parser.ToDocument.p_decl' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - - Global binding - 'FStarC.Parser.ToDocument.p_justSig' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - - Global binding - 'FStarC.Parser.ToDocument.p_disjunctivePattern' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - - Global binding - 'FStarC.Parser.ToDocument.p_maybeFocusArrow' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1995,4-1995,12): - - Global binding - 'FStarC.Parser.ToDocument.p_tmNoEq' - is recursive but not used in its body - - EXTRACT FStarC_Syntax_Print.ml - EXTRACT FStarC_Syntax_Formula.ml - EXTRACT FStarC_Syntax_Embeddings_Base.ml - EXTRACT FStarC_TypeChecker_Common.ml - EXTRACT FStarC_SMTEncoding_Z3.ml - LAXCHECK FStarC.SMTEncoding.Util.fst - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fst - LAXCHECK FStarC.TypeChecker.NBETerm.fsti - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fst - LAXCHECK FStarC.Reflection.V2.Embeddings.fst - LAXCHECK FStarC.SMTEncoding.Env.fst - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fst - LAXCHECK FStarC.Extraction.ML.UEnv.fst - LAXCHECK FStarC.Extraction.ML.Util.fsti - LAXCHECK FStarC.Extraction.ML.Term.fsti - LAXCHECK FStarC.Extraction.ML.RegEmb.fsti - LAXCHECK FStarC.Extraction.ML.Modul.fsti - LAXCHECK FStarC.Extraction.Krml.fsti - EXTRACT FStarC_Parser_ToDocument.ml - EXTRACT FStarC_Syntax_Resugar.ml - LAXCHECK FStarC.TypeChecker.PatternUtils.fst - LAXCHECK FStarC.TypeChecker.TcTerm.fsti - LAXCHECK FStarC.TypeChecker.TcInductive.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fst - LAXCHECK FStarC.Tactics.Types.Reflection.fsti - EXTRACT FStarC_Parser_Dep.ml - EXTRACT FStarC_SMTEncoding_SolverState.ml - EXTRACT FStarC_SMTEncoding_Util.ml - EXTRACT FStarC_Interactive_JsonHelper.ml - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fst - EXTRACT FStarC_Syntax_Embeddings.ml - EXTRACT FStarC_TypeChecker_DeferredImplicits.ml - LAXCHECK FStarC.Extraction.ML.Util.fst - LAXCHECK FStarC.Extraction.ML.Code.fst - LAXCHECK FStarC.Extraction.Krml.fst - EXTRACT FStarC_SMTEncoding_Env.ml - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fsti - LAXCHECK FStarC.SMTEncoding.Encode.fsti - LAXCHECK FStarC.CheckedFiles.fsti - LAXCHECK FStarC.TypeChecker.NBETerm.fst - LAXCHECK FStarC.TypeChecker.Primops.Base.fsti - LAXCHECK FStarC.MachineInts.fsti - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fsti - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fsti - EXTRACT FStarC_TypeChecker_PatternUtils.ml - EXTRACT FStarC_SMTEncoding_Solver_Cache.ml - EXTRACT FStarC_Extraction_ML_UEnv.ml - LAXCHECK FStarC.Tactics.Types.Reflection.fst - EXTRACT FStarC_SMTEncoding_ErrorReporting.ml - EXTRACT FStarC_TypeChecker_TermEqAndSimplify.ml - EXTRACT FStarC_Extraction_ML_Util.ml - LAXCHECK FStarC.CheckedFiles.fst - LAXCHECK FStarC.Universal.fsti - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fst - EXTRACT FStarC_Tactics_Types_Reflection.ml - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fsti - LAXCHECK FStarC.TypeChecker.Primops.Base.fst - LAXCHECK FStarC.TypeChecker.Primops.Eq.fsti - LAXCHECK FStarC.TypeChecker.Primops.Real.fsti - LAXCHECK FStarC.TypeChecker.Primops.Range.fsti - LAXCHECK FStarC.TypeChecker.Primops.Docs.fsti - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fsti - LAXCHECK FStarC.TypeChecker.Primops.Issue.fsti - LAXCHECK FStarC.TypeChecker.Primops.Erased.fsti - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fsti - LAXCHECK FStarC.TypeChecker.Primops.Array.fsti - LAXCHECK FStarC.TypeChecker.Primops.fsti - LAXCHECK FStarC.Tactics.V2.Primops.fsti - LAXCHECK FStarC.Tactics.V1.Primops.fsti - LAXCHECK FStarC.MachineInts.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.ML.Code.fst(789,12-789,17): - - Local binding 'p_sig' is recursive but not used in its body - - EXTRACT FStarC_Extraction_ML_Code.ml - LAXCHECK FStarC.TypeChecker.Primops.Docs.fst - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fst - LAXCHECK FStarC.SMTEncoding.Solver.fst - EXTRACT FStarC_Reflection_V2_Embeddings.ml - LAXCHECK FStarC.TypeChecker.Primops.Issue.fst - EXTRACT FStarC_TypeChecker_Env.ml - EXTRACT FStarC_TypeChecker_Primops_Docs.ml - LAXCHECK FStarC.TypeChecker.Cfg.fsti - LAXCHECK FStarC.Tactics.Types.fsti - EXTRACT FStarC_MachineInts.ml - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fst - LAXCHECK FStarC.TypeChecker.Primops.Erased.fst - EXTRACT FStarC_CheckedFiles.ml - LAXCHECK FStarC.TypeChecker.Primops.Range.fst - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fst - LAXCHECK FStarC.TypeChecker.Primops.Eq.fst - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fst - LAXCHECK FStarC.TypeChecker.Primops.Array.fst - LAXCHECK FStarC.TypeChecker.Primops.Real.fst - LAXCHECK FStarC.TypeChecker.Primops.fst - EXTRACT FStarC_TypeChecker_Primops_Issue.ml - LAXCHECK FStarC.Tactics.Printing.fsti - LAXCHECK FStarC.Tactics.Types.fst - LAXCHECK FStarC.Tactics.Native.fsti - LAXCHECK FStarC.Tactics.Result.fsti - LAXCHECK FStarC.Interactive.Ide.Types.fsti - EXTRACT FStarC_Reflection_V1_Embeddings.ml - LAXCHECK FStarC.TypeChecker.Cfg.fst - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fsti - LAXCHECK FStarC.TypeChecker.Normalize.fsti - LAXCHECK FStarC.Reflection.V1.Interpreter.fst - LAXCHECK FStarC.Reflection.V2.Interpreter.fst - EXTRACT FStarC_TypeChecker_Primops_Range.ml - EXTRACT FStarC_Reflection_V1_NBEEmbeddings.ml - EXTRACT FStarC_TypeChecker_Primops_MachineInts.ml - EXTRACT FStarC_TypeChecker_Primops_Eq.ml - EXTRACT FStarC_TypeChecker_Primops_Errors_Msg.ml - EXTRACT FStarC_Reflection_V2_NBEEmbeddings.ml - EXTRACT FStarC_TypeChecker_Primops_Sealed.ml - EXTRACT FStarC_TypeChecker_Primops_Erased.ml - EXTRACT FStarC_TypeChecker_Primops_Base.ml - EXTRACT FStarC_TypeChecker_NBETerm.ml - LAXCHECK FStarC.Tactics.Monad.fsti - LAXCHECK FStarC.Tactics.Result.fst - LAXCHECK FStarC.Tactics.Embedding.fsti - EXTRACT FStarC_TypeChecker_Primops.ml - EXTRACT FStarC_SMTEncoding_Solver.ml - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fst - EXTRACT FStarC_TypeChecker_Primops_Real.ml - LAXCHECK FStarC.TypeChecker.Normalize.fst - LAXCHECK FStarC.TypeChecker.Err.fst - LAXCHECK FStarC.TypeChecker.Rel.fst - LAXCHECK FStarC.TypeChecker.Util.fst - LAXCHECK FStarC.Reflection.V2.Builtins.fst - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fst - LAXCHECK FStarC.SMTEncoding.Encode.fst - LAXCHECK FStarC.TypeChecker.Generalize.fst - LAXCHECK FStarC.TypeChecker.Positivity.fst - LAXCHECK FStarC.TypeChecker.TcTerm.fst - LAXCHECK FStarC.TypeChecker.TcInductive.fst - LAXCHECK FStarC.Tactics.Printing.fst - LAXCHECK FStarC.TypeChecker.NBE.fsti - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.Krml.fst(335,8-335,19): - - Global binding - 'FStarC.Extraction.Krml.decl_to_doc' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.Krml.fst(679,8-679,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.02.17/src/extraction/FStarC.Extraction.Krml.fst(782,4-782,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.02.17/src/extraction/FStarC.Extraction.Krml.fst(799,4-799,19): - - Global binding - 'FStarC.Extraction.Krml.translate_expr'' - is recursive but not used in its body - - LAXCHECK FStarC.TypeChecker.Quals.fst - LAXCHECK FStarC.TypeChecker.Core.fst - LAXCHECK FStarC.TypeChecker.DMFF.fst - LAXCHECK FStarC.TypeChecker.TcEffect.fst - LAXCHECK FStarC.TypeChecker.Tc.fst - LAXCHECK FStarC.Extraction.ML.Term.fst - EXTRACT FStarC_Tactics_Result.ml - LAXCHECK FStarC.Tactics.Monad.fst - LAXCHECK FStarC.Tactics.InterpFuns.fsti - LAXCHECK FStarC.Extraction.ML.Modul.fst - EXTRACT FStarC_Extraction_Krml.ml - LAXCHECK FStarC.Tactics.CtrlRewrite.fsti - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(718,13-718,47): - - 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.2025.02.17/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(736,19-736,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.Tactics.Interpreter.fsti - LAXCHECK FStarC.Tactics.V2.Basic.fsti - LAXCHECK FStarC.Reflection.V1.Builtins.fst - LAXCHECK FStarC.Tactics.V1.Basic.fsti - LAXCHECK FStarC.Interactive.Ide.Types.fst - LAXCHECK FStarC.Interactive.PushHelper.fsti - LAXCHECK FStarC.Interactive.QueryHelper.fsti - LAXCHECK FStarC.Interactive.Incremental.fsti - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Err.fst(133,30-133,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.02.17/src/typechecker/FStarC.TypeChecker.Err.fst(142,29-142,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.Interactive.Legacy.fst - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Generalize.fst(265,9-265,58): - - Effectful argument FStarC.List.for_all (fun _ -> - (let l, _, _ = _ in - FStarC.Util.is_right l) - <: - Prims.bool) - lecs (FStarC.Effect.ALL) to erased function assert, consider let binding it - - EXTRACT FStarC_Reflection_V2_Interpreter.ml - EXTRACT FStarC_Reflection_V1_Interpreter.ml - EXTRACT FStarC_ToSyntax_ToSyntax.ml - EXTRACT FStarC_TypeChecker_Primops_Array.ml - EXTRACT FStarC_TypeChecker_Normalize_Unfolding.ml - EXTRACT FStarC_TypeChecker_Err.ml - EXTRACT FStarC_Reflection_V2_Builtins.ml - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Quals.fst(142,12-142,13): - - 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 '@'. - - EXTRACT FStarC_TypeChecker_Generalize.ml - EXTRACT FStarC_Tactics_Types.ml - EXTRACT FStarC_Tactics_Printing.ml - LAXCHECK FStarC.TypeChecker.NBE.fst - EXTRACT FStarC_TypeChecker_Quals.ml - LAXCHECK FStarC.Tactics.Embedding.fst - LAXCHECK FStarC.Tactics.InterpFuns.fst - LAXCHECK FStarC.Extraction.ML.RegEmb.fst - LAXCHECK FStarC.Tactics.CtrlRewrite.fst - LAXCHECK FStarC.Tactics.Interpreter.fst - LAXCHECK FStarC.Tactics.V2.Basic.fst - LAXCHECK FStarC.Tactics.Hooks.fst - LAXCHECK FStarC.Universal.fst - LAXCHECK FStarC.Tactics.V2.Primops.fst - EXTRACT FStarC_Reflection_V1_Builtins.ml - LAXCHECK FStarC.Tactics.V1.Basic.fst - LAXCHECK FStarC.Tactics.V1.Primops.fst - LAXCHECK FStarC.Hooks.fst - EXTRACT FStarC_Interactive_Ide_Types.ml - LAXCHECK FStarC.Interactive.PushHelper.fst - LAXCHECK FStarC.Main.fst - EXTRACT FStarC_TypeChecker_Cfg.ml - EXTRACT FStarC_TypeChecker_Positivity.ml - EXTRACT FStarC_TypeChecker_TcInductive.ml - EXTRACT FStarC_TypeChecker_Tc.ml - EXTRACT FStarC_Tactics_Monad.ml - EXTRACT FStarC_Tactics_CtrlRewrite.ml - LAXCHECK FStarC.Interactive.QueryHelper.fst - LAXCHECK FStarC.Interactive.Incremental.fst - LAXCHECK FStarC.Interactive.Ide.fst - LAXCHECK FStarC.Interactive.Lsp.fst - EXTRACT FStarC_SMTEncoding_EncodeTerm.ml - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(709,8-709,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.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(1335,4-1335,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.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(1381,4-1381,19): - - Global binding - 'FStarC.Extraction.ML.Term.term_as_mlexpr'' - is recursive but not used in its body - - EXTRACT FStarC_Tactics_Embedding.ml - EXTRACT FStarC_Extraction_ML_RegEmb.ml - EXTRACT FStarC_Extraction_ML_Modul.ml - EXTRACT FStarC_Interactive_Legacy.ml - EXTRACT FStarC_TypeChecker_DMFF.ml - EXTRACT FStarC_Extraction_ML_Term.ml - EXTRACT FStarC_SMTEncoding_Encode.ml - EXTRACT FStarC_Hooks.ml - EXTRACT FStarC_TypeChecker_Core.ml - EXTRACT FStarC_Tactics_Interpreter.ml - EXTRACT FStarC_Interactive_PushHelper.ml - EXTRACT FStarC_TypeChecker_NBE.ml - EXTRACT FStarC_Interactive_QueryHelper.ml - EXTRACT FStarC_Universal.ml - EXTRACT FStarC_Interactive_Lsp.ml - EXTRACT FStarC_Interactive_Incremental.ml - EXTRACT FStarC_Main.ml - EXTRACT FStarC_Tactics_V1_Primops.ml - EXTRACT FStarC_TypeChecker_Util.ml - EXTRACT FStarC_TypeChecker_Normalize.ml - EXTRACT FStarC_Tactics_Hooks.ml - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/interactive/FStarC.Interactive.Ide.fst(152,13-152,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 - - EXTRACT FStarC_TypeChecker_TcEffect.ml - EXTRACT FStarC_Interactive_Ide.ml - EXTRACT FStarC_Tactics_V1_Basic.ml - EXTRACT FStarC_Tactics_InterpFuns.ml - EXTRACT FStarC_Tactics_V2_Primops.ml - EXTRACT FStarC_Tactics_V2_Basic.ml - EXTRACT FStarC_TypeChecker_TcTerm.ml - EXTRACT FStarC_TypeChecker_Rel.ml - BUILD STAGE 1 FSTARC-BARE - File "fstar-guts/FStarC_Parser_Parse.mly", line 126, characters 60-70: - Warning: the token LBRACK_BAR is unused. - File "fstar-guts/FStarC_Parser_Parse.mly", line 324, characters 0-15: - Warning: symbol decoratableDecl is unreachable from any of the start symbols. - File "fstar-guts/FStarC_Parser_Parse.mly", line 307, characters 0-16: - Warning: symbol noDecorationDecl is unreachable from any of the start symbols. - Warning: 20 states have shift/reduce conflicts. - Warning: 233 states have end-of-stream conflicts. - Warning: 305 shift/reduce conflicts were arbitrarily resolved. - Warning: 233 end-of-stream conflicts were arbitrarily resolved. - EXTRACT STAGE 1 PLUGINS - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib - LAXCHECK Prims.fst - LAXCHECK FStar.NormSteps.fsti - LAXCHECK FStar.Pervasives.Native.fst - LAXCHECK FStar.Attributes.fsti - LAXCHECK FStar.NormSteps.fst - EXTRACT FStar.NormSteps.fst.checked.lax - LAXCHECK FStar.Pervasives.fsti - LAXCHECK FStar.Pervasives.fst - LAXCHECK FStar.Prelude.fsti - LAXCHECK FStar.Ghost.fsti - LAXCHECK FStar.Squash.fsti - LAXCHECK FStar.Classical.Sugar.fsti - LAXCHECK FStar.Mul.fst - LAXCHECK FStar.Classical.fsti - LAXCHECK FStar.Monotonic.Pure.fst - LAXCHECK FStar.Preorder.fst - LAXCHECK FStar.Sealed.fsti - LAXCHECK FStar.Order.fst - LAXCHECK FStar.Float.fsti - LAXCHECK FStar.Stubs.VConfig.fsti - LAXCHECK FStar.Reflection.Const.fst - LAXCHECK FStar.Stubs.TypeChecker.Core.fsti - LAXCHECK FStar.FunctionalExtensionality.fsti - LAXCHECK FStar.Set.fsti - LAXCHECK FStar.PropositionalExtensionality.fst - LAXCHECK FStar.Tactics.V1.Logic.Lemmas.fsti - LAXCHECK FStar.Exn.fst - EXTRACT FStar.Mul.fst.checked.lax - LAXCHECK FStar.Math.Lib.fst - LAXCHECK FStar.Math.Lemmas.fsti - LAXCHECK FStar.Tactics.Canon.Lemmas.fsti - EXTRACT FStar.PropositionalExtensionality.fst.checked.lax - EXTRACT FStar.Monotonic.Pure.fst.checked.lax - LAXCHECK FStar.Classical.Sugar.fst - LAXCHECK FStar.Algebra.CommMonoid.Equiv.fst - LAXCHECK FStar.List.Tot.Base.fst - LAXCHECK FStar.Sealed.Inhabited.fst - LAXCHECK FStar.Range.fsti - EXTRACT FStar.Preorder.fst.checked.lax - LAXCHECK FStar.Monotonic.Witnessed.fsti - EXTRACT FStar.Reflection.Const.fst.checked.lax - LAXCHECK FStar.IndefiniteDescription.fsti - LAXCHECK FStar.ErasedLogic.fst - EXTRACT FStar.Order.fst.checked.lax - LAXCHECK FStar.Calc.fsti - LAXCHECK FStar.Stubs.Reflection.Types.fsti - EXTRACT FStar.Sealed.Inhabited.fst.checked.lax - LAXCHECK FStar.Tactics.Canon.Lemmas.fst - EXTRACT FStar.ErasedLogic.fst.checked.lax - LAXCHECK FStar.IndefiniteDescription.fst - LAXCHECK FStar.Squash.fst - LAXCHECK FStar.StrongExcludedMiddle.fst - LAXCHECK FStar.Classical.fst - LAXCHECK FStar.Monotonic.Witnessed.fst - LAXCHECK FStar.Tactics.V1.Logic.Lemmas.fst - LAXCHECK FStar.Stubs.Syntax.Syntax.fsti - LAXCHECK FStar.Stubs.Tactics.Types.Reflection.fsti - LAXCHECK FStar.Reflection.TermEq.Simple.fsti - LAXCHECK FStar.TSet.fsti - EXTRACT FStar.StrongExcludedMiddle.fst.checked.lax - EXTRACT FStar.Math.Lib.fst.checked.lax - EXTRACT FStar.Classical.Sugar.fst.checked.lax - LAXCHECK FStar.Calc.fst - LAXCHECK FStar.PredicateExtensionality.fst - LAXCHECK FStar.Set.fst - EXTRACT FStar.Squash.fst.checked.lax - EXTRACT FStar.Tactics.Canon.Lemmas.fst.checked.lax - EXTRACT FStar.IndefiniteDescription.fst.checked.lax - LAXCHECK FStar.Stubs.Reflection.V2.Data.fsti - EXTRACT FStar.Algebra.CommMonoid.Equiv.fst.checked.lax - EXTRACT FStar.Tactics.V1.Logic.Lemmas.fst.checked.lax - EXTRACT FStar.Monotonic.Witnessed.fst.checked.lax - LAXCHECK FStar.Monotonic.Heap.fsti - LAXCHECK FStar.Math.Lemmas.fst - EXTRACT FStar.PredicateExtensionality.fst.checked.lax - EXTRACT FStar.Pervasives.fst.checked.lax - EXTRACT FStar.Classical.fst.checked.lax - EXTRACT FStar.Set.fst.checked.lax - EXTRACT FStar.Calc.fst.checked.lax - LAXCHECK FStar.List.Tot.Properties.fsti - LAXCHECK FStar.Seq.Base.fsti - LAXCHECK FStar.Tactics.CanonCommSwaps.fst - LAXCHECK FStar.Stubs.Reflection.V2.Builtins.fsti - LAXCHECK FStar.Reflection.V2.Compare.fsti - LAXCHECK FStar.Reflection.TermEq.fsti - LAXCHECK FStar.Reflection.V2.Collect.fst - LAXCHECK FStar.Stubs.Reflection.V1.Data.fsti - EXTRACT FStar.Tactics.CanonCommSwaps.fst.checked.lax - LAXCHECK FStar.Reflection.V1.Compare.fsti - LAXCHECK FStar.BitVector.fsti - EXTRACT FStar.Reflection.V2.Collect.fst.checked.lax - LAXCHECK FStar.Heap.fst - LAXCHECK FStar.Reflection.TermEq.Simple.fst - EXTRACT FStar.Reflection.TermEq.Simple.fst.checked.lax - LAXCHECK FStar.UInt.fsti - LAXCHECK FStar.ST.fst - LAXCHECK FStar.All.fsti - LAXCHECK FStar.List.Tot.Properties.fst - LAXCHECK FStar.List.Tot.fst - LAXCHECK FStar.Seq.Base.fst - LAXCHECK FStar.Seq.Properties.fsti - LAXCHECK FStar.Reflection.V2.Derived.Lemmas.fst - LAXCHECK FStar.Reflection.V2.Derived.fst - LAXCHECK FStar.Reflection.TermEq.fst - LAXCHECK FStar.List.fst - LAXCHECK FStar.Stubs.Reflection.V1.Builtins.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - LAXCHECK FStar.Reflection.V1.Derived.fst - LAXCHECK FStar.UInt32.fsti - EXTRACT FStar.Reflection.V2.Derived.fst.checked.lax - EXTRACT FStar.Reflection.V2.Derived.Lemmas.fst.checked.lax - LAXCHECK FStar.Reflection.V2.Compare.fst - LAXCHECK FStar.Reflection.V2.fst - LAXCHECK FStar.Reflection.V1.Derived.Lemmas.fst - EXTRACT FStar.Reflection.V1.Derived.fst.checked.lax - LAXCHECK FStar.BV.fsti - LAXCHECK FStar.Char.fsti - EXTRACT FStar.Reflection.V2.fst.checked.lax - LAXCHECK FStar.Pprint.fsti - EXTRACT FStar.Reflection.V1.Derived.Lemmas.fst.checked.lax - LAXCHECK FStar.Reflection.V1.fst - EXTRACT FStar.Reflection.V2.Compare.fst.checked.lax - LAXCHECK FStar.Issue.fsti - LAXCHECK FStar.Stubs.Errors.Msg.fsti - EXTRACT FStar.Reflection.V1.fst.checked.lax - LAXCHECK FStar.Stubs.Tactics.Common.fsti - LAXCHECK FStar.Tactics.BV.Lemmas.fsti - LAXCHECK FStar.Stubs.Tactics.Types.fsti - LAXCHECK FStar.Seq.Properties.fst - LAXCHECK FStar.Seq.fst - LAXCHECK FStar.Stubs.Tactics.Result.fsti - EXTRACT FStar.Seq.fst.checked.lax - LAXCHECK FStar.BitVector.fst - LAXCHECK FStar.UInt.fst - LAXCHECK FStar.BV.fst - LAXCHECK FStar.Tactics.BV.Lemmas.fst - LAXCHECK FStar.Tactics.Effect.fsti - EXTRACT FStar.Reflection.TermEq.fst.checked.lax - LAXCHECK FStar.Tactics.Effect.fst - LAXCHECK FStar.Tactics.Util.fst - LAXCHECK FStar.Tactics.NamedView.fsti - LAXCHECK FStar.Stubs.Tactics.Unseal.fsti - LAXCHECK FStar.Tactics.Names.fsti - LAXCHECK FStar.Tactics.SMT.fsti - LAXCHECK FStar.Tactics.Print.fsti - LAXCHECK FStar.Tactics.BV.fsti - LAXCHECK FStar.Tactics.MApply0.fsti - LAXCHECK FStar.Tactics.Canon.fsti - LAXCHECK FStar.Tactics.Typeclasses.fsti - LAXCHECK FStar.Tactics.MkProjectors.fsti - LAXCHECK FStar.Tactics.Parametricity.fsti - EXTRACT FStar.Seq.Base.fst.checked.lax - EXTRACT FStar.Tactics.BV.Lemmas.fst.checked.lax - LAXCHECK FStar.Stubs.Tactics.V2.Builtins.fsti - LAXCHECK FStar.Stubs.Tactics.V1.Builtins.fsti - LAXCHECK FStar.Tactics.V1.SyntaxHelpers.fst - LAXCHECK FStar.Reflection.V1.Formula.fst - EXTRACT FStar.Tactics.Effect.fst.checked.lax - EXTRACT FStar.Tactics.Util.fst.checked.lax - LAXCHECK FStar.Tactics.Visit.fst - EXTRACT FStar.Tactics.V1.SyntaxHelpers.fst.checked.lax - LAXCHECK FStar.FunctionalExtensionality.fst - LAXCHECK FStar.Tactics.SMT.fst - EXTRACT FStar.Reflection.V1.Formula.fst.checked.lax - LAXCHECK FStar.Tactics.V1.Derived.fst - LAXCHECK FStar.Tactics.V1.Logic.fsti - EXTRACT FStar.BitVector.fst.checked.lax - EXTRACT FStar.Math.Lemmas.fst.checked.lax - EXTRACT FStar.BV.fst.checked.lax - LAXCHECK FStar.Tactics.NamedView.fst - LAXCHECK FStar.Tactics.V2.SyntaxCoercions.fst - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fsti - LAXCHECK FStar.Reflection.V2.Formula.fst - EXTRACT FStar.Tactics.Visit.fst.checked.lax - LAXCHECK FStar.Tactics.Names.fst - EXTRACT FStar.FunctionalExtensionality.fst.checked.lax - EXTRACT FStar.Tactics.SMT.fst.checked.lax - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fst - EXTRACT FStar.List.Tot.Properties.fst.checked.lax - EXTRACT FStar.Tactics.Names.fst.checked.lax - EXTRACT FStar.Tactics.V2.SyntaxCoercions.fst.checked.lax - EXTRACT FStar.Tactics.V2.SyntaxHelpers.fst.checked.lax - EXTRACT FStar.Reflection.V2.Formula.fst.checked.lax - LAXCHECK FStar.Tactics.V2.Derived.fst - LAXCHECK FStar.Tactics.V2.Logic.fsti - EXTRACT FStar.Seq.Properties.fst.checked.lax - EXTRACT FStar.Tactics.NamedView.fst.checked.lax - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fst(293,8-293,25): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51) - - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - EXTRACT FStar.UInt.fst.checked.lax - EXTRACT FStar.Tactics.V1.Derived.fst.checked.lax - LAXCHECK FStar.Tactics.V1.Logic.fst - EXTRACT FStar.Tactics.V2.Derived.fst.checked.lax - LAXCHECK FStar.Tactics.Print.fst - LAXCHECK FStar.Tactics.V2.Logic.fst - LAXCHECK FStar.Tactics.V2.Bare.fsti - LAXCHECK FStar.Tactics.Typeclasses.fst - LAXCHECK FStar.Tactics.MApply0.fst - LAXCHECK FStar.Tactics.MkProjectors.fst - EXTRACT FStar.Tactics.V1.Logic.fst.checked.lax - LAXCHECK FStar.Reflection.V2.Arith.fst - LAXCHECK FStar.Tactics.TypeRepr.fsti - LAXCHECK FStar.Tactics.CheckLN.fsti - LAXCHECK FStar.Tactics.Parametricity.fst - LAXCHECK FStar.Tactics.CanonCommMonoidSimple.Equiv.fst - EXTRACT FStar.Tactics.Print.fst.checked.lax - EXTRACT FStar.Tactics.MApply0.fst.checked.lax - EXTRACT FStar.Tactics.V2.Logic.fst.checked.lax - LAXCHECK FStar.Tactics.TypeRepr.fst - LAXCHECK FStar.Tactics.CheckLN.fst - EXTRACT FStar.Tactics.MkProjectors.fst.checked.lax - EXTRACT FStar.Tactics.CheckLN.fst.checked.lax - EXTRACT FStar.Tactics.Typeclasses.fst.checked.lax - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - EXTRACT FStar.Reflection.V2.Arith.fst.checked.lax - LAXCHECK FStar.Tactics.BV.fst - LAXCHECK FStar.Tactics.Canon.fst - EXTRACT FStar.Tactics.Parametricity.fst.checked.lax - EXTRACT FStar.Tactics.TypeRepr.fst.checked.lax - EXTRACT FStar.Tactics.Canon.fst.checked.lax - EXTRACT FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.checked.lax - EXTRACT FStar.Tactics.BV.fst.checked.lax - BUILD STAGE 1 FSTARC - EXTRACT STAGE 2 FSTARC - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src - LAXCHECK Prims.fst - LAXCHECK FStar.NormSteps.fsti - LAXCHECK FStar.Pervasives.Native.fst - LAXCHECK FStar.Attributes.fsti - LAXCHECK FStar.Pervasives.fsti - LAXCHECK FStar.Prelude.fsti - LAXCHECK FStar.Pervasives.fst - LAXCHECK FStar.Classical.Sugar.fsti - LAXCHECK FStar.Ghost.fsti - LAXCHECK FStar.Classical.fsti - LAXCHECK FStar.Squash.fsti - LAXCHECK FStar.Monotonic.Pure.fst - LAXCHECK FStar.Sealed.fsti - LAXCHECK FStar.Mul.fst - LAXCHECK FStar.Float.fsti - LAXCHECK FStarC.Effect.fsti - LAXCHECK FStar.ImmutableArray.Base.fsti - LAXCHECK FStarC.VConfig.fsti - LAXCHECK FStarC.Array.fsti - LAXCHECK FStar.Exn.fst - LAXCHECK FStar.Set.fsti - LAXCHECK FStar.Preorder.fst - LAXCHECK FStarC.Errors.Codes.fsti - LAXCHECK FStarC.Sealed.fsti - LAXCHECK FStarC.Real.fsti - LAXCHECK FStarC.NormSteps.fst - LAXCHECK FStar.Order.fst - LAXCHECK FStarC.Reflection.V2.Interpreter.fsti - LAXCHECK FStarC.Reflection.V1.Interpreter.fsti - LAXCHECK FStarC.Real.fst - EXTRACT FStarC.NormSteps.fst.checked.lax - LAXCHECK FStarC.Sealed.fst - LAXCHECK FStar.Monotonic.Witnessed.fsti - LAXCHECK FStar.Range.fsti - EXTRACT FStarC.Real.fst.checked.lax - EXTRACT FStarC.Sealed.fst.checked.lax - LAXCHECK FStar.List.Tot.Base.fst - LAXCHECK FStarC.VConfig.fst - LAXCHECK FStar.Stubs.Reflection.Types.fsti - LAXCHECK FStar.Math.Lemmas.fsti - LAXCHECK FStar.IndefiniteDescription.fsti - LAXCHECK FStarC.BigInt.fsti - LAXCHECK FStarC.List.fsti - LAXCHECK FStarC.PSMap.fsti - LAXCHECK FStarC.Json.fsti - LAXCHECK FStarC.Find.fsti - LAXCHECK FStarC.SMap.fsti - LAXCHECK FStarC.Filepath.fsti - LAXCHECK FStarC.Debug.fsti - LAXCHECK FStarC.Options.Ext.fsti - LAXCHECK FStarC.GenSym.fsti - LAXCHECK FStarC.Thunk.fsti - LAXCHECK FStarC.Order.fsti - LAXCHECK FStarC.Dyn.fsti - LAXCHECK FStarC.Unionfind.fsti - LAXCHECK FStarC.Hash.fsti - LAXCHECK FStarC.Option.fsti - LAXCHECK FStarC.Plugins.Base.fsti - LAXCHECK FStarC.Platform.Base.fsti - LAXCHECK FStarC.Profiling.fsti - LAXCHECK FStarC.Timing.fsti - LAXCHECK FStarC.PIMap.fsti - LAXCHECK FStarC.Misc.fsti - LAXCHECK FStarC.Hints.fsti - LAXCHECK FStarC.OCaml.fsti - LAXCHECK FStarC.Hooks.fsti - LAXCHECK FStarC.Interactive.Legacy.fsti - LAXCHECK FStarC.Interactive.Ide.fsti - LAXCHECK FStarC.Interactive.Lsp.fsti - LAXCHECK FStarC.Prettyprint.fsti - LAXCHECK FStar.TSet.fsti - LAXCHECK FStar.StrongExcludedMiddle.fst - EXTRACT FStarC.VConfig.fst.checked.lax - LAXCHECK FStarC.Option.fst - LAXCHECK FStarC.Common.fsti - LAXCHECK FStarC.GenSym.fst - LAXCHECK FStarC.Thunk.fst - LAXCHECK FStarC.Plugins.fsti - LAXCHECK FStarC.Order.fst - EXTRACT FStarC.Option.fst.checked.lax - EXTRACT FStarC.GenSym.fst.checked.lax - EXTRACT FStarC.Thunk.fst.checked.lax - EXTRACT FStarC.Order.fst.checked.lax - LAXCHECK FStar.Monotonic.Heap.fsti - EXTRACT FStar.Pervasives.fst.checked.lax - LAXCHECK FStar.Seq.Base.fsti - LAXCHECK FStar.List.Tot.Properties.fsti - LAXCHECK FStar.BitVector.fsti - LAXCHECK FStarC.Errors.Codes.fst - LAXCHECK FStar.UInt.fsti - EXTRACT FStarC.Errors.Codes.fst.checked.lax - LAXCHECK FStar.Heap.fst - LAXCHECK FStar.ST.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - LAXCHECK FStar.UInt32.fsti - LAXCHECK FStar.List.Tot.fst - LAXCHECK FStar.Seq.Base.fst - LAXCHECK FStar.Seq.Properties.fsti - LAXCHECK FStar.Char.fsti - LAXCHECK FStar.All.fsti - LAXCHECK FStar.Pprint.fsti - LAXCHECK FStarC.BaseTypes.fsti - LAXCHECK FStarC.String.fsti - LAXCHECK FStar.List.fst - LAXCHECK FStarC.Util.fsti - LAXCHECK FStarC.Getopt.fsti - LAXCHECK FStarC.Bytes.fsti - LAXCHECK FStar.Issue.fsti - LAXCHECK FStar.Stubs.Errors.Msg.fsti - LAXCHECK FStar.String.fsti - LAXCHECK FStar.Stubs.Tactics.Common.fsti - LAXCHECK FStar.Seq.Properties.fst - LAXCHECK FStar.Stubs.Tactics.Types.fsti - LAXCHECK FStarC.Pprint.fsti - LAXCHECK FStarC.Common.fst - LAXCHECK FStarC.Debug.fst - LAXCHECK FStarC.StringBuffer.fsti - LAXCHECK FStarC.Misc.fst - LAXCHECK FStarC.Find.Z3.fsti - EXTRACT FStar.Seq.Base.fst.checked.lax - EXTRACT FStarC.Debug.fst.checked.lax - EXTRACT FStarC.Common.fst.checked.lax - LAXCHECK FStar.Stubs.Tactics.Result.fsti - EXTRACT FStarC.Misc.fst.checked.lax - LAXCHECK FStar.Tactics.Effect.fsti - LAXCHECK FStar.Tactics.Typeclasses.fsti - LAXCHECK FStarC.Class.Show.fsti - LAXCHECK FStarC.Class.Monad.fsti - LAXCHECK FStarC.Errors.Msg.fsti - LAXCHECK FStarC.Class.Deq.fsti - LAXCHECK FStarC.Class.Tagged.fsti - LAXCHECK FStarC.Class.Listlike.fsti - LAXCHECK FStarC.Class.Monoid.fsti - LAXCHECK FStarC.Path.fsti - LAXCHECK FStarC.Class.Deq.fst - LAXCHECK FStarC.Class.Ord.fsti - LAXCHECK FStarC.Class.Monoid.fst - LAXCHECK FStarC.Path.fst - EXTRACT FStarC.Class.Monoid.fst.checked.lax - LAXCHECK FStarC.Range.Type.fsti - LAXCHECK FStarC.Class.Ord.fst - LAXCHECK FStarC.Class.Setlike.fsti - EXTRACT FStarC.Class.Deq.fst.checked.lax - LAXCHECK FStarC.Class.Tagged.fst - LAXCHECK FStarC.Class.Show.fst - LAXCHECK FStarC.Options.Ext.fst - LAXCHECK FStarC.Options.fsti - LAXCHECK FStarC.Find.fst - LAXCHECK FStarC.Class.PP.fsti - LAXCHECK FStarC.Platform.fsti - LAXCHECK FStarC.Class.Hashable.fsti - LAXCHECK FStarC.Errors.Msg.fst - LAXCHECK FStarC.Class.Monad.fst - LAXCHECK FStarC.Writer.fsti - LAXCHECK FStarC.CList.fsti - LAXCHECK FStarC.Class.Listlike.fst - EXTRACT FStarC.Path.fst.checked.lax - LAXCHECK FStarC.Range.Type.fst - LAXCHECK FStarC.Class.HasRange.fsti - EXTRACT FStarC.Class.Tagged.fst.checked.lax - LAXCHECK FStarC.Platform.fst - LAXCHECK FStarC.OCaml.fst - LAXCHECK FStarC.Class.Hashable.fst - LAXCHECK FStarC.Range.Ops.fsti - LAXCHECK FStarC.Class.PP.fst - LAXCHECK FStarC.Writer.fst - EXTRACT FStarC.Errors.Msg.fst.checked.lax - EXTRACT FStarC.Options.Ext.fst.checked.lax - LAXCHECK FStarC.CList.fst - EXTRACT FStarC.Class.Show.fst.checked.lax - LAXCHECK FStarC.Options.fst - LAXCHECK FStarC.Find.Z3.fst - LAXCHECK FStarC.Profiling.fst - EXTRACT FStarC.Class.Listlike.fst.checked.lax - EXTRACT FStarC.Find.fst.checked.lax - EXTRACT FStarC.Class.Monad.fst.checked.lax - EXTRACT FStarC.Range.Type.fst.checked.lax - LAXCHECK FStarC.Ident.fsti - EXTRACT FStarC.Platform.fst.checked.lax - EXTRACT FStarC.Writer.fst.checked.lax - EXTRACT FStarC.Class.PP.fst.checked.lax - EXTRACT FStarC.OCaml.fst.checked.lax - LAXCHECK FStarC.Range.Ops.fst - LAXCHECK FStarC.Range.fsti - EXTRACT FStarC.Class.Ord.fst.checked.lax - LAXCHECK FStarC.Const.fsti - LAXCHECK FStarC.Parser.Dep.fsti - LAXCHECK FStarC.Interactive.CompletionTable.fsti - EXTRACT FStarC.Class.Hashable.fst.checked.lax - EXTRACT FStarC.CList.fst.checked.lax - EXTRACT FStarC.Profiling.fst.checked.lax - EXTRACT FStarC.Find.Z3.fst.checked.lax - LAXCHECK FStarC.Interactive.CompletionTable.fst - LAXCHECK FStarC.Class.Setlike.fst - LAXCHECK FStarC.FlatSet.fsti - LAXCHECK FStarC.RBSet.fsti - LAXCHECK FStarC.Class.HasRange.fst - LAXCHECK FStarC.Ident.fst - LAXCHECK FStarC.Parser.Const.Tuples.fsti - LAXCHECK FStarC.Errors.fsti - LAXCHECK FStarC.Dependencies.fsti - EXTRACT FStarC.Range.Ops.fst.checked.lax - LAXCHECK FStarC.FlatSet.fst - LAXCHECK FStarC.Const.fst - LAXCHECK FStarC.Syntax.Syntax.fsti - LAXCHECK FStarC.Extraction.ML.Syntax.fsti - EXTRACT FStar.Seq.Properties.fst.checked.lax - LAXCHECK FStarC.RBSet.fst - EXTRACT FStarC.FlatSet.fst.checked.lax - LAXCHECK FStarC.Parser.Const.fst - LAXCHECK FStarC.Parser.Const.Tuples.fst - EXTRACT FStarC.Class.HasRange.fst.checked.lax - EXTRACT FStarC.RBSet.fst.checked.lax - EXTRACT FStarC.Const.fst.checked.lax - EXTRACT FStarC.Parser.Const.Tuples.fst.checked.lax - EXTRACT FStarC.Class.Setlike.fst.checked.lax - EXTRACT FStarC.Ident.fst.checked.lax - LAXCHECK FStarC.Errors.fst - LAXCHECK FStarC.Plugins.fst - LAXCHECK FStarC.Dependencies.fst - LAXCHECK FStarC.Interactive.JsonHelper.fsti - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.02.17/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.02.17/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.02.17/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 '@'. - - EXTRACT FStarC.Plugins.fst.checked.lax - EXTRACT FStarC.Interactive.CompletionTable.fst.checked.lax - LAXCHECK FStarC.Extraction.ML.Syntax.fst - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fsti - LAXCHECK FStarC.Extraction.ML.Code.fsti - LAXCHECK FStarC.Extraction.ML.PrintFS.fsti - LAXCHECK FStarC.Extraction.ML.PrintML.fsti - EXTRACT FStarC.Parser.Const.fst.checked.lax - EXTRACT FStarC.Dependencies.fst.checked.lax - LAXCHECK FStarC.Extraction.ML.RemoveUnusedParameters.fst - EXTRACT FStarC.Extraction.ML.Syntax.fst.checked.lax - EXTRACT FStarC.Options.fst.checked.lax - EXTRACT FStarC.Errors.fst.checked.lax - EXTRACT FStarC.Extraction.ML.RemoveUnusedParameters.fst.checked.lax - LAXCHECK FStarC.Extraction.ML.PrintFS.fst - LAXCHECK FStarC.Syntax.Syntax.fst - LAXCHECK FStarC.Syntax.Unionfind.fsti - LAXCHECK FStarC.Syntax.Subst.fsti - LAXCHECK FStarC.Syntax.InstFV.fsti - LAXCHECK FStarC.Syntax.Free.fsti - LAXCHECK FStarC.Syntax.Print.Ugly.fsti - LAXCHECK FStarC.Parser.AST.fsti - LAXCHECK FStarC.Syntax.Formula.fsti - LAXCHECK FStarC.Syntax.MutRecTy.fsti - LAXCHECK FStarC.Syntax.VisitM.fsti - LAXCHECK FStarC.Syntax.Visit.fsti - LAXCHECK FStarC.SMTEncoding.Term.fsti - LAXCHECK FStarC.Syntax.Embeddings.Base.fsti - LAXCHECK FStarC.TypeChecker.Common.fsti - LAXCHECK FStarC.Class.Binders.fsti - LAXCHECK FStarC.Reflection.V2.Data.fsti - LAXCHECK FStarC.Reflection.V2.Constants.fst - LAXCHECK FStarC.Reflection.V1.Constants.fst - LAXCHECK FStarC.Tactics.Common.fsti - LAXCHECK FStarC.Syntax.Hash.fsti - LAXCHECK FStarC.Syntax.Compress.fsti - LAXCHECK FStarC.Syntax.TermHashTable.fsti - LAXCHECK FStarC.Reflection.V1.Data.fsti - LAXCHECK FStarC.Reflection.V1.Data.fst - EXTRACT FStarC.Reflection.V2.Constants.fst.checked.lax - LAXCHECK FStarC.Syntax.Unionfind.fst - LAXCHECK FStarC.Defensive.fsti - EXTRACT FStarC.Reflection.V1.Data.fst.checked.lax - LAXCHECK FStarC.Tactics.Common.fst - LAXCHECK FStarC.Class.Binders.fst - LAXCHECK FStarC.Syntax.Visit.fst - EXTRACT FStarC.Reflection.V1.Constants.fst.checked.lax - LAXCHECK FStarC.Syntax.Subst.fst - LAXCHECK FStarC.Syntax.InstFV.fst - LAXCHECK FStarC.Syntax.Free.fst - LAXCHECK FStarC.Syntax.Util.fsti - LAXCHECK FStarC.Syntax.Hash.fst - LAXCHECK FStarC.Syntax.VisitM.fst - EXTRACT FStarC.Extraction.ML.PrintFS.fst.checked.lax - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fsti - LAXCHECK FStarC.Syntax.Embeddings.fsti - LAXCHECK FStarC.Reflection.V2.Data.fst - EXTRACT FStarC.Tactics.Common.fst.checked.lax - LAXCHECK FStarC.SMTEncoding.Term.fst - LAXCHECK FStarC.SMTEncoding.Pruning.fsti - LAXCHECK FStarC.SMTEncoding.UnsatCore.fsti - LAXCHECK FStarC.Syntax.Embeddings.AppEmb.fst - EXTRACT FStarC.Syntax.Unionfind.fst.checked.lax - EXTRACT FStarC.Syntax.InstFV.fst.checked.lax - EXTRACT FStarC.Syntax.Visit.fst.checked.lax - EXTRACT FStarC.Class.Binders.fst.checked.lax - LAXCHECK FStarC.Syntax.Print.Ugly.fst - LAXCHECK FStarC.Syntax.Util.fst - LAXCHECK FStarC.Syntax.MutRecTy.fst - EXTRACT FStarC.Syntax.MutRecTy.fst.checked.lax - EXTRACT FStarC.Syntax.Free.fst.checked.lax - LAXCHECK FStarC.Parser.AST.fst - LAXCHECK FStarC.Parser.ToDocument.fsti - LAXCHECK FStarC.Parser.AST.Util.fsti - LAXCHECK FStarC.Syntax.DsEnv.fsti - LAXCHECK FStarC.SMTEncoding.Pruning.fst - EXTRACT FStarC.Syntax.Subst.fst.checked.lax - EXTRACT FStarC.Syntax.Hash.fst.checked.lax - LAXCHECK FStarC.SMTEncoding.UnsatCore.fst - LAXCHECK FStarC.SMTEncoding.SolverState.fsti - LAXCHECK FStarC.Parser.ToDocument.fst - LAXCHECK FStarC.Parser.AST.Util.fst - LAXCHECK FStarC.Parser.ParseIt.fsti - EXTRACT FStarC.Reflection.V2.Data.fst.checked.lax - EXTRACT FStarC.Syntax.Print.Ugly.fst.checked.lax - LAXCHECK FStarC.SMTEncoding.Z3.fsti - EXTRACT FStarC.Syntax.Embeddings.AppEmb.fst.checked.lax - EXTRACT FStarC.SMTEncoding.UnsatCore.fst.checked.lax - LAXCHECK FStarC.Syntax.DsEnv.fst - LAXCHECK FStarC.Syntax.Resugar.fsti - LAXCHECK FStarC.Syntax.Print.Pretty.fsti - LAXCHECK FStarC.Syntax.Print.fsti - LAXCHECK FStarC.ToSyntax.ToSyntax.fsti - LAXCHECK FStarC.TypeChecker.Env.fsti - LAXCHECK FStarC.ToSyntax.Interleave.fsti - EXTRACT FStarC.Syntax.VisitM.fst.checked.lax - EXTRACT FStarC.Parser.AST.Util.fst.checked.lax - LAXCHECK FStarC.Parser.Driver.fsti - LAXCHECK FStarC.SMTEncoding.Z3.fst - LAXCHECK FStarC.ToSyntax.Interleave.fst - EXTRACT FStarC.Syntax.Util.fst.checked.lax - LAXCHECK FStarC.Syntax.Print.Pretty.fst - LAXCHECK FStarC.Syntax.Resugar.fst - LAXCHECK FStarC.Parser.Driver.fst - LAXCHECK FStarC.Parser.Dep.fst - LAXCHECK FStarC.Prettyprint.fst - LAXCHECK FStarC.Syntax.Print.fst - LAXCHECK FStarC.Syntax.Formula.fst - LAXCHECK FStarC.Syntax.Embeddings.Base.fst - LAXCHECK FStarC.Syntax.Embeddings.fst - LAXCHECK FStarC.Defensive.fst - LAXCHECK FStarC.TypeChecker.Common.fst - LAXCHECK FStarC.Syntax.Compress.fst - EXTRACT FStarC.SMTEncoding.Pruning.fst.checked.lax - LAXCHECK FStarC.ToSyntax.ToSyntax.fst - EXTRACT FStarC.Syntax.Syntax.fst.checked.lax - EXTRACT FStarC.SMTEncoding.Term.fst.checked.lax - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - - Global binding - 'FStarC.Parser.AST.decl_to_string' - is recursive but not used in its body - - EXTRACT FStarC.Parser.AST.fst.checked.lax - EXTRACT FStarC.Parser.Driver.fst.checked.lax - EXTRACT FStarC.Prettyprint.fst.checked.lax - EXTRACT FStarC.Syntax.Print.Pretty.fst.checked.lax - EXTRACT FStarC.Defensive.fst.checked.lax - EXTRACT FStarC.Syntax.Compress.fst.checked.lax - EXTRACT FStarC.ToSyntax.Interleave.fst.checked.lax - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - - Global binding - 'FStarC.Parser.ToDocument.p_decl' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - - Global binding - 'FStarC.Parser.ToDocument.p_justSig' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - - Global binding - 'FStarC.Parser.ToDocument.p_disjunctivePattern' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - - Global binding - 'FStarC.Parser.ToDocument.p_maybeFocusArrow' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/parser/FStarC.Parser.ToDocument.fst(1995,4-1995,12): - - Global binding - 'FStarC.Parser.ToDocument.p_tmNoEq' - is recursive but not used in its body - - EXTRACT FStarC.Parser.ToDocument.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Env.fst - LAXCHECK FStarC.SMTEncoding.SolverState.fst - LAXCHECK FStarC.SMTEncoding.Util.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fsti - LAXCHECK FStarC.TypeChecker.Err.fsti - LAXCHECK FStarC.TypeChecker.Rel.fsti - LAXCHECK FStarC.TypeChecker.PatternUtils.fsti - LAXCHECK FStarC.TypeChecker.Util.fsti - LAXCHECK FStarC.Reflection.V2.Builtins.fsti - LAXCHECK FStarC.Reflection.V2.Embeddings.fsti - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fsti - LAXCHECK FStarC.TypeChecker.Generalize.fsti - LAXCHECK FStarC.TypeChecker.Positivity.fsti - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fsti - LAXCHECK FStarC.TypeChecker.Quals.fsti - LAXCHECK FStarC.SMTEncoding.Solver.fsti - LAXCHECK FStarC.TypeChecker.Core.fsti - LAXCHECK FStarC.TypeChecker.DMFF.fsti - LAXCHECK FStarC.TypeChecker.TcEffect.fsti - LAXCHECK FStarC.TypeChecker.Tc.fsti - LAXCHECK FStarC.Extraction.ML.UEnv.fsti - LAXCHECK FStarC.Tactics.Hooks.fsti - LAXCHECK FStarC.Reflection.V1.Builtins.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fsti - LAXCHECK FStarC.Interactive.JsonHelper.fst - EXTRACT FStarC.Syntax.DsEnv.fst.checked.lax - EXTRACT FStarC.Syntax.Resugar.fst.checked.lax - EXTRACT FStarC.Syntax.Print.fst.checked.lax - EXTRACT FStarC.Syntax.Formula.fst.checked.lax - EXTRACT FStarC.Syntax.Embeddings.Base.fst.checked.lax - EXTRACT FStarC.TypeChecker.Common.fst.checked.lax - EXTRACT FStarC.SMTEncoding.Z3.fst.checked.lax - LAXCHECK FStarC.SMTEncoding.Util.fst - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fsti - LAXCHECK FStarC.TypeChecker.TermEqAndSimplify.fst - LAXCHECK FStarC.TypeChecker.NBETerm.fsti - LAXCHECK FStarC.TypeChecker.DeferredImplicits.fst - LAXCHECK FStarC.SMTEncoding.Env.fst - LAXCHECK FStarC.SMTEncoding.Solver.Cache.fst - EXTRACT FStarC.Parser.Dep.fst.checked.lax - LAXCHECK FStarC.TypeChecker.PatternUtils.fst - LAXCHECK FStarC.Reflection.V2.Embeddings.fst - LAXCHECK FStarC.Extraction.ML.UEnv.fst - LAXCHECK FStarC.Extraction.ML.Util.fsti - LAXCHECK FStarC.Extraction.ML.Term.fsti - LAXCHECK FStarC.Extraction.ML.RegEmb.fsti - LAXCHECK FStarC.Extraction.ML.Modul.fsti - LAXCHECK FStarC.Extraction.Krml.fsti - LAXCHECK FStarC.TypeChecker.TcTerm.fsti - LAXCHECK FStarC.TypeChecker.TcInductive.fsti - LAXCHECK FStarC.Reflection.V1.Embeddings.fst - EXTRACT FStarC.SMTEncoding.SolverState.fst.checked.lax - LAXCHECK FStarC.Tactics.Types.Reflection.fsti - EXTRACT FStarC.Syntax.Embeddings.fst.checked.lax - LAXCHECK FStarC.SMTEncoding.ErrorReporting.fst - EXTRACT FStarC.Interactive.JsonHelper.fst.checked.lax - EXTRACT FStarC.SMTEncoding.Util.fst.checked.lax - LAXCHECK FStarC.Extraction.ML.Code.fst - LAXCHECK FStarC.Extraction.ML.Util.fst - LAXCHECK FStarC.Extraction.Krml.fst - EXTRACT FStarC.Extraction.ML.UEnv.fst.checked.lax - EXTRACT FStarC.TypeChecker.DeferredImplicits.fst.checked.lax - EXTRACT FStarC.TypeChecker.PatternUtils.fst.checked.lax - EXTRACT FStarC.SMTEncoding.Env.fst.checked.lax - LAXCHECK FStarC.CheckedFiles.fsti - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fsti - LAXCHECK FStarC.SMTEncoding.Encode.fsti - LAXCHECK FStarC.TypeChecker.NBETerm.fst - LAXCHECK FStarC.TypeChecker.Primops.Base.fsti - LAXCHECK FStarC.MachineInts.fsti - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fsti - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fsti - LAXCHECK FStarC.Tactics.Types.Reflection.fst - EXTRACT FStarC.SMTEncoding.Solver.Cache.fst.checked.lax - EXTRACT FStarC.TypeChecker.TermEqAndSimplify.fst.checked.lax - EXTRACT FStarC.SMTEncoding.ErrorReporting.fst.checked.lax - LAXCHECK FStarC.CheckedFiles.fst - LAXCHECK FStarC.Universal.fsti - EXTRACT FStarC.Extraction.ML.Util.fst.checked.lax - LAXCHECK FStarC.MachineInts.fst - LAXCHECK FStarC.Reflection.V2.NBEEmbeddings.fst - LAXCHECK FStarC.Reflection.V1.NBEEmbeddings.fst - LAXCHECK FStarC.TypeChecker.Primops.Base.fst - LAXCHECK FStarC.TypeChecker.Primops.Eq.fsti - LAXCHECK FStarC.TypeChecker.Primops.Real.fsti - LAXCHECK FStarC.TypeChecker.Primops.Range.fsti - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fsti - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fsti - LAXCHECK FStarC.TypeChecker.Primops.Docs.fsti - LAXCHECK FStarC.TypeChecker.Primops.Erased.fsti - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fsti - LAXCHECK FStarC.TypeChecker.Primops.Array.fsti - LAXCHECK FStarC.TypeChecker.Primops.Issue.fsti - LAXCHECK FStarC.Tactics.V2.Primops.fsti - LAXCHECK FStarC.TypeChecker.Primops.fsti - LAXCHECK FStarC.Tactics.V1.Primops.fsti - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.ML.Code.fst(789,12-789,17): - - Local binding 'p_sig' is recursive but not used in its body - - EXTRACT FStarC.Extraction.ML.Code.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Primops.Sealed.fst - LAXCHECK FStarC.SMTEncoding.Solver.fst - EXTRACT FStarC.Tactics.Types.Reflection.fst.checked.lax - EXTRACT FStarC.Reflection.V2.Embeddings.fst.checked.lax - EXTRACT FStarC.TypeChecker.Env.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Primops.Range.fst - LAXCHECK FStarC.TypeChecker.Primops.Real.fst - EXTRACT FStarC.MachineInts.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Primops.Array.fst - LAXCHECK FStarC.TypeChecker.Primops.Eq.fst - LAXCHECK FStarC.TypeChecker.Primops.Errors.Msg.fst - EXTRACT FStarC.CheckedFiles.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Primops.Docs.fst - LAXCHECK FStarC.TypeChecker.Primops.Erased.fst - LAXCHECK FStarC.TypeChecker.Primops.MachineInts.fst - LAXCHECK FStarC.TypeChecker.Primops.Issue.fst - LAXCHECK FStarC.TypeChecker.Primops.fst - LAXCHECK FStarC.TypeChecker.Cfg.fsti - LAXCHECK FStarC.Tactics.Types.fsti - EXTRACT FStarC.TypeChecker.Primops.Sealed.fst.checked.lax - EXTRACT FStarC.Reflection.V1.Embeddings.fst.checked.lax - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.Krml.fst(335,8-335,19): - - Global binding - 'FStarC.Extraction.Krml.decl_to_doc' - is recursive but not used in its body - - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.Krml.fst(679,8-679,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.02.17/src/extraction/FStarC.Extraction.Krml.fst(782,4-782,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.02.17/src/extraction/FStarC.Extraction.Krml.fst(799,4-799,19): - - Global binding - 'FStarC.Extraction.Krml.translate_expr'' - is recursive but not used in its body - - EXTRACT FStarC.Extraction.Krml.fst.checked.lax - LAXCHECK FStarC.Interactive.Ide.Types.fsti - EXTRACT FStarC.TypeChecker.Primops.Range.fst.checked.lax - EXTRACT FStarC.TypeChecker.NBETerm.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Base.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Real.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Docs.fst.checked.lax - LAXCHECK FStarC.Tactics.Types.fst - LAXCHECK FStarC.Tactics.Printing.fsti - LAXCHECK FStarC.Tactics.Result.fsti - LAXCHECK FStarC.Tactics.Native.fsti - EXTRACT FStarC.TypeChecker.Primops.Array.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Eq.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Errors.Msg.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Issue.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.Erased.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.MachineInts.fst.checked.lax - EXTRACT FStarC.Reflection.V1.NBEEmbeddings.fst.checked.lax - EXTRACT FStarC.Reflection.V2.NBEEmbeddings.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Cfg.fst - LAXCHECK FStarC.TypeChecker.Normalize.fsti - LAXCHECK FStarC.Reflection.V2.Interpreter.fst - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fsti - LAXCHECK FStarC.Reflection.V1.Interpreter.fst - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(718,13-718,47): - - 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.2025.02.17/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst(736,19-736,56): - - Effectful argument let _ = FStarC.Ident.string_of_lid max_lid in - _ = "max" (FStarC.Effect.ALL) to erased function assert, consider let binding it - - EXTRACT FStarC.ToSyntax.ToSyntax.fst.checked.lax - EXTRACT FStarC.TypeChecker.Primops.fst.checked.lax - LAXCHECK FStarC.Tactics.Result.fst - LAXCHECK FStarC.Tactics.Embedding.fsti - LAXCHECK FStarC.Tactics.Monad.fsti - LAXCHECK FStarC.Tactics.Printing.fst - EXTRACT FStarC.SMTEncoding.Solver.fst.checked.lax - LAXCHECK FStarC.TypeChecker.Err.fst - LAXCHECK FStarC.TypeChecker.Rel.fst - LAXCHECK FStarC.TypeChecker.Util.fst - LAXCHECK FStarC.Reflection.V2.Builtins.fst - LAXCHECK FStarC.SMTEncoding.EncodeTerm.fst - LAXCHECK FStarC.SMTEncoding.Encode.fst - LAXCHECK FStarC.TypeChecker.Generalize.fst - LAXCHECK FStarC.TypeChecker.Positivity.fst - LAXCHECK FStarC.TypeChecker.TcTerm.fst - LAXCHECK FStarC.TypeChecker.TcInductive.fst - EXTRACT FStarC.Tactics.Types.fst.checked.lax - LAXCHECK FStarC.TypeChecker.NBE.fsti - LAXCHECK FStarC.TypeChecker.Quals.fst - LAXCHECK FStarC.TypeChecker.Core.fst - LAXCHECK FStarC.TypeChecker.DMFF.fst - LAXCHECK FStarC.TypeChecker.TcEffect.fst - LAXCHECK FStarC.TypeChecker.Tc.fst - LAXCHECK FStarC.Extraction.ML.Term.fst - EXTRACT FStarC.Tactics.Result.fst.checked.lax - LAXCHECK FStarC.Extraction.ML.Modul.fst - LAXCHECK FStarC.Reflection.V1.Builtins.fst - LAXCHECK FStarC.Interactive.Ide.Types.fst - LAXCHECK FStarC.Interactive.PushHelper.fsti - LAXCHECK FStarC.Interactive.QueryHelper.fsti - LAXCHECK FStarC.Interactive.Incremental.fsti - LAXCHECK FStarC.Interactive.Legacy.fst - LAXCHECK FStarC.TypeChecker.Normalize.Unfolding.fst - LAXCHECK FStarC.TypeChecker.Normalize.fst - EXTRACT FStarC.Tactics.Printing.fst.checked.lax - LAXCHECK FStarC.Tactics.Embedding.fst - LAXCHECK FStarC.Tactics.Monad.fst - LAXCHECK FStarC.Tactics.InterpFuns.fsti - LAXCHECK FStarC.Tactics.CtrlRewrite.fsti - LAXCHECK FStarC.Tactics.Interpreter.fsti - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Generalize.fst(265,9-265,58): - - Effectful argument FStarC.List.for_all (fun _ -> - (let l, _, _ = _ in - FStarC.Util.is_right l) - <: - Prims.bool) - lecs (FStarC.Effect.ALL) to erased function assert, consider let binding it - - LAXCHECK FStarC.Tactics.V2.Basic.fsti - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Err.fst(133,30-133,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.02.17/src/typechecker/FStarC.TypeChecker.Err.fst(142,29-142,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.V1.Basic.fsti - EXTRACT FStarC.Reflection.V2.Interpreter.fst.checked.lax - EXTRACT FStarC.Reflection.V1.Interpreter.fst.checked.lax - EXTRACT FStarC.TypeChecker.Cfg.fst.checked.lax - EXTRACT FStarC.TypeChecker.Err.fst.checked.lax - EXTRACT FStarC.Reflection.V2.Builtins.fst.checked.lax - * Warning 337 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/typechecker/FStarC.TypeChecker.Quals.fst(142,12-142,13): - - 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 '@'. - - EXTRACT FStarC.TypeChecker.Generalize.fst.checked.lax - EXTRACT FStarC.TypeChecker.Positivity.fst.checked.lax - LAXCHECK FStarC.TypeChecker.NBE.fst - EXTRACT FStarC.TypeChecker.Quals.fst.checked.lax - LAXCHECK FStarC.Tactics.CtrlRewrite.fst - LAXCHECK FStarC.Tactics.Interpreter.fst - LAXCHECK FStarC.Universal.fst - LAXCHECK FStarC.Hooks.fst - LAXCHECK FStarC.Interactive.PushHelper.fst - LAXCHECK FStarC.Interactive.QueryHelper.fst - LAXCHECK FStarC.Interactive.Lsp.fst - LAXCHECK FStarC.Main.fst - EXTRACT FStarC.TypeChecker.Normalize.Unfolding.fst.checked.lax - EXTRACT FStarC.TypeChecker.TcInductive.fst.checked.lax - EXTRACT FStarC.Tactics.Embedding.fst.checked.lax - LAXCHECK FStarC.Tactics.InterpFuns.fst - LAXCHECK FStarC.Extraction.ML.RegEmb.fst - EXTRACT FStarC.Reflection.V1.Builtins.fst.checked.lax - LAXCHECK FStarC.Tactics.V1.Basic.fst - LAXCHECK FStarC.Tactics.V1.Primops.fst - EXTRACT FStarC.Interactive.Ide.Types.fst.checked.lax - LAXCHECK FStarC.Interactive.Incremental.fst - LAXCHECK FStarC.Interactive.Ide.fst - EXTRACT FStarC.Interactive.Legacy.fst.checked.lax - EXTRACT FStarC.SMTEncoding.EncodeTerm.fst.checked.lax - EXTRACT FStarC.Tactics.Monad.fst.checked.lax - EXTRACT FStarC.Extraction.ML.Modul.fst.checked.lax - EXTRACT FStarC.Tactics.CtrlRewrite.fst.checked.lax - LAXCHECK FStarC.Tactics.V2.Basic.fst - LAXCHECK FStarC.Tactics.Hooks.fst - LAXCHECK FStarC.Tactics.V2.Primops.fst - EXTRACT FStarC.Hooks.fst.checked.lax - EXTRACT FStarC.SMTEncoding.Encode.fst.checked.lax - EXTRACT FStarC.TypeChecker.Core.fst.checked.lax - EXTRACT FStarC.Interactive.QueryHelper.fst.checked.lax - EXTRACT FStarC.Tactics.Interpreter.fst.checked.lax - EXTRACT FStarC.Interactive.PushHelper.fst.checked.lax - EXTRACT FStarC.TypeChecker.DMFF.fst.checked.lax - EXTRACT FStarC.TypeChecker.Tc.fst.checked.lax - EXTRACT FStarC.Interactive.Lsp.fst.checked.lax - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(709,8-709,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.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(1335,4-1335,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.02.17/src/extraction/FStarC.Extraction.ML.Term.fst(1381,4-1381,19): - - Global binding - 'FStarC.Extraction.ML.Term.term_as_mlexpr'' - is recursive but not used in its body - - EXTRACT FStarC.Extraction.ML.Term.fst.checked.lax - EXTRACT FStarC.Universal.fst.checked.lax - EXTRACT FStarC.TypeChecker.NBE.fst.checked.lax - EXTRACT FStarC.TypeChecker.Util.fst.checked.lax - EXTRACT FStarC.Interactive.Incremental.fst.checked.lax - EXTRACT FStarC.Tactics.V1.Primops.fst.checked.lax - EXTRACT FStarC.Extraction.ML.RegEmb.fst.checked.lax - EXTRACT FStarC.Main.fst.checked.lax - EXTRACT FStarC.TypeChecker.TcEffect.fst.checked.lax - * Warning 319 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/src/interactive/FStarC.Interactive.Ide.fst(152,13-152,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 - - EXTRACT FStarC.Interactive.Ide.fst.checked.lax - EXTRACT FStarC.TypeChecker.Normalize.fst.checked.lax - EXTRACT FStarC.Tactics.V1.Basic.fst.checked.lax - EXTRACT FStarC.Tactics.Hooks.fst.checked.lax - EXTRACT FStarC.Tactics.InterpFuns.fst.checked.lax - EXTRACT FStarC.Tactics.V2.Primops.fst.checked.lax - EXTRACT FStarC.TypeChecker.TcTerm.fst.checked.lax - EXTRACT FStarC.TypeChecker.Rel.fst.checked.lax - EXTRACT FStarC.Tactics.V2.Basic.fst.checked.lax - BUILD STAGE 2 FSTARC-BARE - (cd _build/.sandbox/38f23419084190bebd90a5772dd0f733/default && /home/opam/.opam/default/bin/menhir fstar-guts/FStarC_Parser_Parse.mly --base fstar-guts/FStarC_Parser_Parse --infer-write-query fstar-guts/FStarC_Parser_Parse__mock.ml.mock) - File "fstar-guts/FStarC_Parser_Parse.mly", line 126, characters 60-70: - Warning: the token LBRACK_BAR is unused. - File "fstar-guts/FStarC_Parser_Parse.mly", line 324, characters 0-15: - Warning: symbol decoratableDecl is unreachable from any of the start symbols. - File "fstar-guts/FStarC_Parser_Parse.mly", line 307, characters 0-16: - Warning: symbol noDecorationDecl is unreachable from any of the start symbols. - (cd _build/.sandbox/cb71630efa4a54d0348163ae0b1c3e01/default && /home/opam/.opam/default/bin/menhir fstar-guts/FStarC_Parser_Parse.mly --base fstar-guts/FStarC_Parser_Parse --infer-read-reply fstar-guts/FStarC_Parser_Parse__mock.mli.inferred) - Warning: 20 states have shift/reduce conflicts. - Warning: 233 states have end-of-stream conflicts. - Warning: 305 shift/reduce conflicts were arbitrarily resolved. - Warning: 233 end-of-stream conflicts were arbitrarily resolved. - EXTRACT STAGE 2 PLUGINS - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib - LAXCHECK Prims.fst - LAXCHECK FStar.NormSteps.fsti - LAXCHECK FStar.Pervasives.Native.fst - LAXCHECK FStar.Attributes.fsti - LAXCHECK FStar.NormSteps.fst - EXTRACT FStar.NormSteps.fst.checked.lax - LAXCHECK FStar.Pervasives.fsti - LAXCHECK FStar.Prelude.fsti - LAXCHECK FStar.Pervasives.fst - LAXCHECK FStar.Squash.fsti - LAXCHECK FStar.Ghost.fsti - LAXCHECK FStar.Classical.Sugar.fsti - LAXCHECK FStar.Mul.fst - LAXCHECK FStar.Classical.fsti - LAXCHECK FStar.Preorder.fst - LAXCHECK FStar.Sealed.fsti - LAXCHECK FStar.Monotonic.Pure.fst - LAXCHECK FStar.Float.fsti - LAXCHECK FStar.Order.fst - LAXCHECK FStar.Stubs.VConfig.fsti - LAXCHECK FStar.Reflection.Const.fst - LAXCHECK FStar.Stubs.TypeChecker.Core.fsti - LAXCHECK FStar.FunctionalExtensionality.fsti - LAXCHECK FStar.Set.fsti - LAXCHECK FStar.PropositionalExtensionality.fst - LAXCHECK FStar.Exn.fst - LAXCHECK FStar.Tactics.V1.Logic.Lemmas.fsti - EXTRACT FStar.PropositionalExtensionality.fst.checked.lax - LAXCHECK FStar.Monotonic.Witnessed.fsti - EXTRACT FStar.Preorder.fst.checked.lax - LAXCHECK FStar.Range.fsti - LAXCHECK FStar.Sealed.Inhabited.fst - EXTRACT FStar.Order.fst.checked.lax - LAXCHECK FStar.Math.Lib.fst - EXTRACT FStar.Mul.fst.checked.lax - LAXCHECK FStar.Math.Lemmas.fsti - LAXCHECK FStar.Tactics.Canon.Lemmas.fsti - LAXCHECK FStar.Classical.Sugar.fst - LAXCHECK FStar.List.Tot.Base.fst - LAXCHECK FStar.Algebra.CommMonoid.Equiv.fst - EXTRACT FStar.Monotonic.Pure.fst.checked.lax - EXTRACT FStar.Reflection.Const.fst.checked.lax - EXTRACT FStar.Sealed.Inhabited.fst.checked.lax - LAXCHECK FStar.Stubs.Reflection.Types.fsti - LAXCHECK FStar.Calc.fsti - LAXCHECK FStar.Classical.fst - LAXCHECK FStar.Monotonic.Witnessed.fst - LAXCHECK FStar.IndefiniteDescription.fsti - LAXCHECK FStar.ErasedLogic.fst - LAXCHECK FStar.Tactics.Canon.Lemmas.fst - EXTRACT FStar.Classical.Sugar.fst.checked.lax - LAXCHECK FStar.Reflection.TermEq.Simple.fsti - LAXCHECK FStar.Stubs.Tactics.Types.Reflection.fsti - LAXCHECK FStar.Stubs.Syntax.Syntax.fsti - LAXCHECK FStar.PredicateExtensionality.fst - LAXCHECK FStar.Squash.fst - LAXCHECK FStar.IndefiniteDescription.fst - LAXCHECK FStar.StrongExcludedMiddle.fst - LAXCHECK FStar.Tactics.V1.Logic.Lemmas.fst - LAXCHECK FStar.Calc.fst - EXTRACT FStar.ErasedLogic.fst.checked.lax - EXTRACT FStar.Math.Lib.fst.checked.lax - LAXCHECK FStar.Math.Lemmas.fst - EXTRACT FStar.Squash.fst.checked.lax - EXTRACT FStar.StrongExcludedMiddle.fst.checked.lax - LAXCHECK FStar.Set.fst - LAXCHECK FStar.TSet.fsti - EXTRACT FStar.Tactics.Canon.Lemmas.fst.checked.lax - LAXCHECK FStar.Stubs.Reflection.V2.Data.fsti - EXTRACT FStar.Tactics.V1.Logic.Lemmas.fst.checked.lax - EXTRACT FStar.PredicateExtensionality.fst.checked.lax - EXTRACT FStar.IndefiniteDescription.fst.checked.lax - EXTRACT FStar.Monotonic.Witnessed.fst.checked.lax - EXTRACT FStar.Calc.fst.checked.lax - EXTRACT FStar.Algebra.CommMonoid.Equiv.fst.checked.lax - EXTRACT FStar.Classical.fst.checked.lax - LAXCHECK FStar.Seq.Base.fsti - LAXCHECK FStar.List.Tot.Properties.fsti - LAXCHECK FStar.Tactics.CanonCommSwaps.fst - EXTRACT FStar.Pervasives.fst.checked.lax - LAXCHECK FStar.Monotonic.Heap.fsti - EXTRACT FStar.Set.fst.checked.lax - EXTRACT FStar.Tactics.CanonCommSwaps.fst.checked.lax - LAXCHECK FStar.Stubs.Reflection.V2.Builtins.fsti - LAXCHECK FStar.Reflection.V2.Compare.fsti - LAXCHECK FStar.BitVector.fsti - LAXCHECK FStar.Reflection.V1.Compare.fsti - LAXCHECK FStar.Reflection.V2.Collect.fst - LAXCHECK FStar.Reflection.TermEq.fsti - LAXCHECK FStar.Stubs.Reflection.V1.Data.fsti - LAXCHECK FStar.List.Tot.Properties.fst - LAXCHECK FStar.List.Tot.fst - LAXCHECK FStar.Reflection.TermEq.Simple.fst - EXTRACT FStar.Reflection.V2.Collect.fst.checked.lax - LAXCHECK FStar.Seq.Base.fst - LAXCHECK FStar.Seq.Properties.fsti - LAXCHECK FStar.Reflection.V2.Derived.Lemmas.fst - LAXCHECK FStar.Reflection.V2.Derived.fst - LAXCHECK FStar.Reflection.TermEq.fst - EXTRACT FStar.Reflection.TermEq.Simple.fst.checked.lax - LAXCHECK FStar.UInt.fsti - LAXCHECK FStar.Heap.fst - LAXCHECK FStar.Stubs.Reflection.V1.Builtins.fsti - EXTRACT FStar.Reflection.V2.Derived.fst.checked.lax - EXTRACT FStar.Reflection.V2.Derived.Lemmas.fst.checked.lax - LAXCHECK FStar.Reflection.V2.Compare.fst - LAXCHECK FStar.Reflection.V2.fst - LAXCHECK FStar.ST.fst - LAXCHECK FStar.Reflection.V1.Derived.fst - EXTRACT FStar.Reflection.V2.fst.checked.lax - LAXCHECK FStar.All.fsti - LAXCHECK FStar.List.fst - EXTRACT FStar.Reflection.V1.Derived.fst.checked.lax - LAXCHECK FStar.Reflection.V1.Derived.Lemmas.fst - EXTRACT FStar.Reflection.V2.Compare.fst.checked.lax - EXTRACT FStar.Seq.Base.fst.checked.lax - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - LAXCHECK FStar.UInt32.fsti - LAXCHECK FStar.BV.fsti - LAXCHECK FStar.Char.fsti - LAXCHECK FStar.Pprint.fsti - EXTRACT FStar.Reflection.V1.Derived.Lemmas.fst.checked.lax - LAXCHECK FStar.Reflection.V1.fst - LAXCHECK FStar.Seq.Properties.fst - LAXCHECK FStar.Seq.fst - EXTRACT FStar.Reflection.V1.fst.checked.lax - LAXCHECK FStar.Issue.fsti - LAXCHECK FStar.Stubs.Errors.Msg.fsti - EXTRACT FStar.Math.Lemmas.fst.checked.lax - EXTRACT FStar.Seq.fst.checked.lax - LAXCHECK FStar.BitVector.fst - LAXCHECK FStar.UInt.fst - LAXCHECK FStar.BV.fst - LAXCHECK FStar.Tactics.BV.Lemmas.fsti - LAXCHECK FStar.Stubs.Tactics.Common.fsti - LAXCHECK FStar.Stubs.Tactics.Types.fsti - LAXCHECK FStar.Tactics.BV.Lemmas.fst - LAXCHECK FStar.Stubs.Tactics.Result.fsti - EXTRACT FStar.BitVector.fst.checked.lax - EXTRACT FStar.Tactics.BV.Lemmas.fst.checked.lax - EXTRACT FStar.BV.fst.checked.lax - LAXCHECK FStar.Tactics.Effect.fsti - EXTRACT FStar.List.Tot.Properties.fst.checked.lax - EXTRACT FStar.Reflection.TermEq.fst.checked.lax - LAXCHECK FStar.Tactics.Effect.fst - LAXCHECK FStar.Tactics.Util.fst - LAXCHECK FStar.Tactics.NamedView.fsti - LAXCHECK FStar.Tactics.Print.fsti - LAXCHECK FStar.Stubs.Tactics.Unseal.fsti - LAXCHECK FStar.Tactics.SMT.fsti - LAXCHECK FStar.Tactics.Names.fsti - LAXCHECK FStar.Tactics.MApply0.fsti - LAXCHECK FStar.Tactics.Typeclasses.fsti - LAXCHECK FStar.Tactics.BV.fsti - LAXCHECK FStar.Tactics.Canon.fsti - LAXCHECK FStar.Tactics.MkProjectors.fsti - LAXCHECK FStar.Tactics.Parametricity.fsti - LAXCHECK FStar.Stubs.Tactics.V2.Builtins.fsti - LAXCHECK FStar.Stubs.Tactics.V1.Builtins.fsti - LAXCHECK FStar.Reflection.V1.Formula.fst - LAXCHECK FStar.Tactics.V1.SyntaxHelpers.fst - EXTRACT FStar.Tactics.Effect.fst.checked.lax - EXTRACT FStar.Tactics.Util.fst.checked.lax - LAXCHECK FStar.Tactics.Visit.fst - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fsti - LAXCHECK FStar.Tactics.NamedView.fst - LAXCHECK FStar.FunctionalExtensionality.fst - LAXCHECK FStar.Tactics.SMT.fst - LAXCHECK FStar.Tactics.V2.SyntaxCoercions.fst - LAXCHECK FStar.Reflection.V2.Formula.fst - EXTRACT FStar.Tactics.V1.SyntaxHelpers.fst.checked.lax - LAXCHECK FStar.Tactics.V2.SyntaxHelpers.fst - EXTRACT FStar.Tactics.Visit.fst.checked.lax - LAXCHECK FStar.Tactics.Names.fst - EXTRACT FStar.Tactics.V2.SyntaxCoercions.fst.checked.lax - EXTRACT FStar.Reflection.V1.Formula.fst.checked.lax - LAXCHECK FStar.Tactics.V1.Derived.fst - LAXCHECK FStar.Tactics.V1.Logic.fsti - EXTRACT FStar.Tactics.SMT.fst.checked.lax - EXTRACT FStar.Tactics.Names.fst.checked.lax - EXTRACT FStar.FunctionalExtensionality.fst.checked.lax - LAXCHECK FStar.Tactics.V2.Derived.fst - EXTRACT FStar.Reflection.V2.Formula.fst.checked.lax - LAXCHECK FStar.Tactics.V2.Logic.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fst(293,8-293,25): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51) - - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - EXTRACT FStar.UInt.fst.checked.lax - EXTRACT FStar.Tactics.V2.SyntaxHelpers.fst.checked.lax - EXTRACT FStar.Tactics.NamedView.fst.checked.lax - EXTRACT FStar.Seq.Properties.fst.checked.lax - EXTRACT FStar.Tactics.V1.Derived.fst.checked.lax - LAXCHECK FStar.Tactics.V1.Logic.fst - EXTRACT FStar.Tactics.V2.Derived.fst.checked.lax - LAXCHECK FStar.Tactics.Print.fst - LAXCHECK FStar.Tactics.V2.Logic.fst - LAXCHECK FStar.Tactics.V2.Bare.fsti - LAXCHECK FStar.Tactics.MApply0.fst - LAXCHECK FStar.Tactics.Typeclasses.fst - LAXCHECK FStar.Tactics.MkProjectors.fst - LAXCHECK FStar.Reflection.V2.Arith.fst - LAXCHECK FStar.Tactics.TypeRepr.fsti - LAXCHECK FStar.Tactics.CheckLN.fsti - LAXCHECK FStar.Tactics.CanonCommMonoidSimple.Equiv.fst - LAXCHECK FStar.Tactics.Parametricity.fst - EXTRACT FStar.Tactics.V2.Logic.fst.checked.lax - EXTRACT FStar.Tactics.V1.Logic.fst.checked.lax - LAXCHECK FStar.Tactics.TypeRepr.fst - EXTRACT FStar.Tactics.MApply0.fst.checked.lax - EXTRACT FStar.Tactics.Print.fst.checked.lax - EXTRACT FStar.Tactics.MkProjectors.fst.checked.lax - LAXCHECK FStar.Tactics.CheckLN.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - EXTRACT FStar.Reflection.V2.Arith.fst.checked.lax - LAXCHECK FStar.Tactics.BV.fst - LAXCHECK FStar.Tactics.Canon.fst - EXTRACT FStar.Tactics.CheckLN.fst.checked.lax - EXTRACT FStar.Tactics.Typeclasses.fst.checked.lax - EXTRACT FStar.Tactics.TypeRepr.fst.checked.lax - EXTRACT FStar.Tactics.Canon.fst.checked.lax - EXTRACT FStar.Tactics.Parametricity.fst.checked.lax - EXTRACT FStar.Tactics.BV.fst.checked.lax - EXTRACT FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.checked.lax - BUILD STAGE 2 FSTARC - EXTRACT STAGE 2 LIB - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib - CHECK Prims.fst - CHECK FStar.Pervasives.Native.fst - CHECK FStar.NormSteps.fsti - CHECK FStar.Attributes.fsti - CHECK FStar.NormSteps.fst - EXTRACT FStar.NormSteps.fst.checked - CHECK FStar.Pervasives.fsti - CHECK FStar.Pervasives.fst - CHECK FStar.Prelude.fsti - CHECK FStar.Ghost.fsti - CHECK FStar.Mul.fst - CHECK FStar.Squash.fsti - CHECK FStar.Classical.fsti - CHECK FStar.Classical.Sugar.fsti - CHECK FStar.Sealed.fsti - CHECK FStar.Preorder.fst - CHECK FStar.Monotonic.Pure.fst - CHECK FStar.PropositionalExtensionality.fst - CHECK FStar.Order.fst - CHECK FStar.FunctionalExtensionality.fsti - CHECK FStar.Float.fsti - CHECK FStar.Stubs.TypeChecker.Core.fsti - CHECK FStar.Set.fsti - CHECK FStar.Reflection.Const.fst - CHECK FStar.Tactics.V1.Logic.Lemmas.fsti - CHECK FStar.Stubs.VConfig.fsti - CHECK FStar.Exn.fst - CHECK FStar.Universe.fsti - CHECK FStar.DependentMap.fsti - CHECK FStar.Functions.fsti - CHECK FStar.PartialMap.fsti - CHECK FStar.MarkovsPrinciple.fst - CHECK FStar.Sequence.Base.fsti - CHECK FStar.ReflexiveTransitiveClosure.fsti - CHECK FStar.Constructive.fst - CHECK FStar.RefinementExtensionality.fsti - CHECK FStar.Parse.fst - CHECK FStar.Real.fsti - CHECK FStar.Dyn.fsti - CHECK FStar.ImmutableArray.Base.fsti - CHECK FStar.Date.fsti - EXTRACT FStar.Monotonic.Pure.fst.checked - CHECK FStar.Real.Old.fsti - EXTRACT FStar.Parse.fst.checked - EXTRACT FStar.Preorder.fst.checked - CHECK FStar.Monotonic.Witnessed.fsti - CHECK FStar.Witnessed.Core.fsti - CHECK FStar.Range.fsti - CHECK FStar.Sealed.Inhabited.fst - CHECK FStar.Dyn.fst - EXTRACT FStar.Mul.fst.checked - CHECK FStar.Math.Lib.fst - CHECK FStar.Math.Lemmas.fsti - CHECK FStar.Algebra.CommMonoid.fst - CHECK FStar.Math.Euclid.fsti - CHECK FStar.Tactics.Canon.Lemmas.fsti - EXTRACT FStar.PropositionalExtensionality.fst.checked - CHECK FStar.Universe.fst - EXTRACT FStar.MarkovsPrinciple.fst.checked - CHECK FStar.List.Tot.Base.fst - CHECK FStar.Algebra.CommMonoid.Equiv.fst - CHECK FStar.Classical.Sugar.fst - EXTRACT FStar.Order.fst.checked - CHECK FStar.Cardinality.Cantor.fsti - CHECK FStar.Stubs.Reflection.Types.fsti - CHECK FStar.Calc.fsti - CHECK FStar.SquashProperties.fst - CHECK FStar.MSTTotal.fst - CHECK FStar.Witnessed.Core.fst - EXTRACT FStar.Universe.fst.checked - CHECK FStar.IndefiniteDescription.fsti - CHECK FStar.ErasedLogic.fst - CHECK FStar.IFC.fsti - CHECK FStar.Ghost.fst - CHECK FStar.Cardinality.Universes.fsti - CHECK FStar.Map.fsti - CHECK FStar.TSet.fsti - CHECK FStar.Tactics.Canon.Lemmas.fst - CHECK FStar.Classical.fst - CHECK FStar.Monotonic.Witnessed.fst - CHECK FStar.GSet.fsti - CHECK FStar.GhostSet.fsti - CHECK FStar.PCM.fst - CHECK FStar.Cardinality.Cantor.fst - CHECK FStar.Algebra.Monoid.fst - CHECK FStar.Set.fst - CHECK FStar.PredicateExtensionality.fst - CHECK FStar.PartialMap.fst - CHECK FStar.Stubs.Tactics.Types.Reflection.fsti - CHECK FStar.Stubs.Syntax.Syntax.fsti - CHECK FStar.Reflection.TermEq.Simple.fsti - CHECK FStar.ExtractAs.fst - CHECK FStar.Calc.fst - CHECK FStar.IndefiniteDescription.fst - CHECK FStar.Squash.fst - CHECK FStar.StrongExcludedMiddle.fst - CHECK FStar.WellFounded.fst - CHECK FStar.Tactics.V1.Logic.Lemmas.fst - EXTRACT FStar.ErasedLogic.fst.checked - EXTRACT FStar.ExtractAs.fst.checked - CHECK FStar.Cardinality.Universes.fst - EXTRACT FStar.Algebra.CommMonoid.fst.checked - EXTRACT FStar.Witnessed.Core.fst.checked - CHECK FStar.DependentMap.fst - EXTRACT FStar.Math.Lib.fst.checked - CHECK FStar.Math.Lemmas.fst - EXTRACT FStar.StrongExcludedMiddle.fst.checked - CHECK FStar.Functions.fst - CHECK FStar.Real.Old.fst - CHECK FStar.Stubs.Reflection.V2.Data.fsti - EXTRACT FStar.Classical.Sugar.fst.checked - EXTRACT FStar.Cardinality.Cantor.fst.checked - CHECK FStar.IFC.fst - EXTRACT FStar.SquashProperties.fst.checked - EXTRACT FStar.Squash.fst.checked - EXTRACT FStar.PredicateExtensionality.fst.checked - CHECK FStar.RefinementExtensionality.fst - EXTRACT FStar.IndefiniteDescription.fst.checked - CHECK FStar.Math.Fermat.fsti - EXTRACT FStar.Cardinality.Universes.fst.checked - CHECK FStar.Monotonic.Heap.fsti - CHECK FStar.TSet.fst - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.fst(122,0-131,33): - - Definitions of inner let-rec aux and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.fst(86,12-86,15) - - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.fst(122,0-131,33): - - Definitions of inner let-rec aux and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.fst(126,12-126,15) - - EXTRACT FStar.WellFounded.fst.checked - CHECK FStar.WellFounded.Util.fsti - CHECK FStar.LexicographicOrdering.fsti - CHECK FStar.WellFoundedRelation.fsti - EXTRACT FStar.Monotonic.Witnessed.fst.checked - CHECK FStar.MST.fst - CHECK FStar.NMSTTotal.fst - CHECK FStar.GSet.fst - EXTRACT FStar.PartialMap.fst.checked - EXTRACT FStar.Set.fst.checked - CHECK FStar.GhostSet.fst - EXTRACT FStar.Real.Old.fst.checked - EXTRACT FStar.IFC.fst.checked - EXTRACT FStar.RefinementExtensionality.fst.checked - CHECK FStar.Map.fst - EXTRACT FStar.Functions.fst.checked - CHECK FStar.Sequence.Util.fst - CHECK FStar.Sequence.Ambient.fst - EXTRACT FStar.Algebra.CommMonoid.Equiv.fst.checked - EXTRACT FStar.Pervasives.fst.checked - EXTRACT FStar.Calc.fst.checked - EXTRACT FStar.Algebra.Monoid.fst.checked - EXTRACT FStar.Sequence.Ambient.fst.checked - CHECK FStar.Sequence.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.TSet.fst(27,4-27,7): - - Values of type `set` cannot be erased during extraction, but the - `must_erase_for_extraction` attribute claims that it can. - - Please remove the attribute. - - EXTRACT FStar.Classical.fst.checked - EXTRACT FStar.DependentMap.fst.checked - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.2025.02.17/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 - - EXTRACT FStar.PCM.fst.checked - CHECK FStar.Universe.PCM.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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. - - EXTRACT FStar.GhostSet.fst.checked - EXTRACT FStar.Sequence.Util.fst.checked - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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. - - EXTRACT FStar.GSet.fst.checked - EXTRACT FStar.Sequence.fst.checked - CHECK FStar.Sequence.Permutation.fsti - CHECK FStar.NMST.fst - CHECK FStar.WellFoundedRelation.fst - * Warning 330 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 352 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.List.Tot.Properties.fsti - CHECK FStar.Seq.Base.fsti - CHECK FStar.BigOps.fsti - CHECK FStar.List.Pure.Base.fst - CHECK FStar.Tactics.CanonCommSwaps.fst - CHECK FStar.Stubs.Reflection.V2.Builtins.fsti - CHECK FStar.Reflection.V2.Compare.fsti - EXTRACT FStar.Map.fst.checked - CHECK FStar.Sequence.Permutation.fst - EXTRACT FStar.Universe.PCM.fst.checked - CHECK FStar.Reflection.V1.Compare.fsti - EXTRACT FStar.List.Pure.Base.fst.checked - CHECK FStar.Reflection.V2.Collect.fst - CHECK FStar.Stubs.Reflection.V1.Data.fsti - CHECK FStar.Reflection.TermEq.fsti - CHECK FStar.LexicographicOrdering.fst - CHECK FStar.Monotonic.HyperHeap.fsti - CHECK FStar.Heap.fst - CHECK FStar.Monotonic.Heap.fst - CHECK FStar.BitVector.fsti - CHECK FStar.IntegerIntervals.fst - CHECK FStar.ST.fst - CHECK FStar.Axiomatic.Array.fst - CHECK FStar.Relational.Relational.fst - CHECK FStar.TwoLevelHeap.fst - CHECK FStar.Reflection.TermEq.Simple.fst - * Warning 290 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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. - - EXTRACT FStar.WellFoundedRelation.fst.checked - EXTRACT FStar.TwoLevelHeap.fst.checked - EXTRACT FStar.IntegerIntervals.fst.checked - CHECK FStar.List.Tot.Properties.fst - CHECK FStar.List.Tot.fst - CHECK FStar.List.Pure.Properties.fst - EXTRACT FStar.Axiomatic.Array.fst.checked - CHECK FStar.Monotonic.HyperStack.fsti - CHECK FStar.All.fsti - CHECK FStar.Ref.fst - CHECK FStar.MRef.fsti - EXTRACT FStar.Relational.Relational.fst.checked - CHECK FStar.Stubs.Reflection.V1.Builtins.fsti - CHECK FStar.Seq.Base.fst - CHECK FStar.Seq.Properties.fsti - CHECK FStar.FiniteSet.Base.fsti - CHECK FStar.Reflection.V2.Derived.Lemmas.fst - CHECK FStar.Reflection.V2.Derived.fst - CHECK FStar.Monotonic.HyperHeap.fst - CHECK FStar.OrdSet.fsti - CHECK FStar.Sequence.Base.fst - CHECK FStar.Reflection.TermEq.fst - CHECK FStar.ImmutableArray.fsti - CHECK FStar.MRef.fst - CHECK FStar.List.fst - CHECK FStar.Relational.Comp.fst - CHECK FStar.Option.fst - CHECK FStar.Reflection.V1.Derived.fst - CHECK FStar.UInt.fsti - EXTRACT FStar.Ref.fst.checked - EXTRACT FStar.MRef.fst.checked - CHECK FStar.Reflection.V2.fst - CHECK FStar.Reflection.V2.Compare.fst - CHECK FStar.FiniteSet.Ambient.fst - CHECK FStar.FiniteMap.Base.fsti - CHECK FStar.FiniteSet.Base.fst - CHECK FStar.List.Pure.fst - EXTRACT FStar.Relational.Comp.fst.checked - EXTRACT FStar.Monotonic.HyperHeap.fst.checked - CHECK FStar.Reflection.V1.Derived.Lemmas.fst - EXTRACT FStar.FiniteSet.Ambient.fst.checked - CHECK FStar.Reflection.Typing.Builtins.fsti - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59): - - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level - letbinding are not encoded to the solver, you will only be able to reason - with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.LexicographicOrdering.fst(75,14-75,28) - - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59): - - Definitions of inner let-rec get_acc and its enclosing top-level letbinding - are not encoded to the solver, you will only be able to reason with their - types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.LexicographicOrdering.fst(124,10-124,17) - - EXTRACT FStar.LexicographicOrdering.fst.checked - CHECK FStar.OrdSet.fst - CHECK FStar.OrdMap.fsti - CHECK FStar.OrdSetProps.fst - CHECK FStar.Monotonic.HyperStack.fst - CHECK FStar.HyperStack.fst - CHECK FStar.FiniteMap.Ambient.fst - EXTRACT FStar.HyperStack.fst.checked - CHECK FStar.HyperStack.ST.fsti - CHECK FStar.Util.fst - EXTRACT FStar.OrdSetProps.fst.checked - CHECK FStar.Reflection.V1.fst - CHECK FStar.OrdMap.fst - CHECK FStar.OrdMapProps.fst - EXTRACT FStar.FiniteMap.Ambient.fst.checked - CHECK FStar.Reflection.fst - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - CHECK FStar.UInt32.fsti - CHECK FStar.BV.fsti - EXTRACT FStar.OrdMapProps.fst.checked - EXTRACT FStar.Sequence.Permutation.fst.checked - EXTRACT FStar.Seq.Base.fst.checked - CHECK FStar.ModifiesGen.fsti - CHECK FStar.Monotonic.DependentMap.fsti - CHECK LowStar.Comment.fsti - CHECK FStar.Monotonic.Map.fst - CHECK LowStar.Failure.fsti - CHECK FStar.HyperStack.All.fst - CHECK FStar.HyperStack.ST.fst - CHECK LowStar.Ignore.fsti - CHECK FStar.UInt64.fsti - CHECK FStar.Char.fsti - CHECK FStar.UInt16.fsti - CHECK FStar.UInt8.fsti - CHECK FStar.UInt32.fst - CHECK LowStar.Comment.fst - CHECK FStar.Tactics.BV.Lemmas.fsti - EXTRACT FStar.OrdMap.fst.checked - CHECK FStar.String.fsti - CHECK FStar.Pprint.fsti - CHECK FStar.HyperStack.IO.fst - CHECK FStar.Seq.Properties.fst - CHECK FStar.Seq.fst - CHECK FStar.Seq.Equiv.fsti - CHECK FStar.Issue.fsti - CHECK FStar.Stubs.Errors.Msg.fsti - CHECK FStar.BitVector.fst - EXTRACT FStar.Seq.fst.checked - CHECK FStar.UInt.fst - CHECK FStar.Int.fsti - CHECK FStar.BV.fst - CHECK FStar.Sequence.Seq.fsti - CHECK FStar.Fin.fsti - CHECK FStar.Monotonic.Seq.fst - CHECK FStar.Buffer.fst - CHECK FStar.FunctionalQueue.fsti - CHECK FStar.Seq.Sorted.fst - CHECK FStar.Array.fsti - CHECK FStar.Vector.Base.fsti - CHECK FStar.Matrix2.fsti - CHECK FStar.UInt16.fst - EXTRACT LowStar.Comment.fst.checked - EXTRACT FStar.FiniteSet.Base.fst.checked - EXTRACT FStar.Monotonic.HyperStack.fst.checked - CHECK FStar.UInt8.fst - CHECK FStar.UInt128.fsti - CHECK FStar.Endianness.fsti - CHECK FStar.SizeT.fsti - CHECK FStar.IO.fsti - CHECK FStar.UInt64.fst - CHECK FStar.Seq.Equiv.fst - CHECK FStar.Seq.Permutation.fsti - CHECK FStar.Monotonic.DependentMap.fst - EXTRACT FStar.Monotonic.Map.fst.checked - CHECK FStar.Stubs.Tactics.Common.fsti - CHECK FStar.Sequence.Seq.fst - CHECK FStar.Error.fst - CHECK FStar.FunctionalQueue.fst - CHECK FStar.Tactics.BV.Lemmas.fst - CHECK FStar.Array.fst - CHECK FStar.Fin.fst - CHECK FStar.Stubs.Tactics.Types.fsti - CHECK FStar.Vector.Properties.fst - CHECK FStar.Vector.Base.fst - EXTRACT FStar.Sequence.Seq.fst.checked - EXTRACT FStar.Error.fst.checked - EXTRACT FStar.Seq.Sorted.fst.checked - CHECK FStar.Algebra.CommMonoid.Fold.fsti - CHECK FStar.Seq.Permutation.fst - CHECK FStar.Stubs.Tactics.Result.fsti - CHECK FStar.Int.fst - CHECK FStar.Int64.fsti - CHECK FStar.Int32.fsti - CHECK FStar.Int16.fsti - CHECK FStar.Int8.fsti - EXTRACT FStar.Math.Lemmas.fst.checked - EXTRACT FStar.Monotonic.DependentMap.fst.checked - EXTRACT FStar.Seq.Equiv.fst.checked - CHECK FStar.Vector.fst - EXTRACT FStar.FunctionalQueue.fst.checked - CHECK FStar.Tactics.Effect.fsti - CHECK FStar.Tactics.Result.fsti - EXTRACT FStar.BV.fst.checked - CHECK FStar.Matrix.fsti - CHECK FStar.Algebra.CommMonoid.Fold.Nested.fsti - CHECK FStar.Algebra.CommMonoid.Fold.fst - CHECK FStar.Int32.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.Endianness.fst - EXTRACT FStar.List.Tot.Properties.fst.checked - CHECK FStar.Int64.fst - CHECK FStar.Int128.fsti - CHECK FStar.Int8.fst - EXTRACT FStar.BitVector.fst.checked - EXTRACT FStar.Monotonic.Seq.fst.checked - CHECK FStar.Int.Cast.fst - CHECK FStar.PtrdiffT.fsti - CHECK FStar.Int16.fst - CHECK FStar.Printf.fst - EXTRACT FStar.Array.fst.checked - CHECK FStar.Tactics.Typeclasses.fsti - CHECK FStar.Stubs.Tactics.Unseal.fsti - CHECK FStar.Tactics.MApply0.fsti - CHECK FStar.Tactics.NamedView.fsti - CHECK FStar.Tactics.SMT.fsti - CHECK FStar.Tactics.Util.fst - CHECK FStar.Tactics.Print.fsti - CHECK FStar.Tactics.Names.fsti - CHECK FStar.Tactics.BV.fsti - CHECK FStar.Tactics.Canon.fsti - CHECK FStar.Tactics.Effect.fst - CHECK FStar.InteractiveHelpers.Propositions.fsti - CHECK FStar.Tactics.Parametricity.fsti - CHECK FStar.Tactics.MkProjectors.fsti - CHECK FStar.Stubs.Tactics.V2.Builtins.fsti - CHECK FStar.Stubs.Tactics.V1.Builtins.fsti - CHECK FStar.Class.Add.fst - CHECK FStar.Class.Printable.fst - CHECK FStar.Class.Eq.Raw.fst - CHECK FStar.Class.TotalOrder.Raw.fst - CHECK FStar.Class.Embeddable.fsti - CHECK FStar.Math.Euclid.fst - EXTRACT FStar.Fin.fst.checked - CHECK FStar.Int128.fst - CHECK FStar.Integers.fst - CHECK FStar.Pointer.Base.fsti - CHECK LowStar.Monotonic.Buffer.fsti - EXTRACT FStar.Class.Eq.Raw.fst.checked - CHECK FStar.Class.Eq.fst - EXTRACT FStar.Algebra.CommMonoid.Fold.fst.checked - CHECK FStar.Tactics.Visit.fst - EXTRACT FStar.Class.Add.fst.checked - CHECK FStar.Matrix.fst - CHECK FStar.Algebra.CommMonoid.Fold.Nested.fst - EXTRACT FStar.Int.fst.checked - CHECK FStar.Tactics.SMT.fst - CHECK FStar.ModifiesGen.fst - CHECK FStar.FunctionalExtensionality.fst - CHECK FStar.Reflection.Typing.fsti - CHECK FStar.Reflection.V1.Formula.fst - CHECK FStar.Tactics.V1.SyntaxHelpers.fst - CHECK FStar.Tactics.Builtins.fsti - CHECK FStar.Tactics.V2.SyntaxCoercions.fst - CHECK FStar.Tactics.V2.SyntaxHelpers.fsti - CHECK FStar.Reflection.V2.Formula.fst - CHECK FStar.Tactics.NamedView.fst - CHECK FStar.Class.Embeddable.fst - EXTRACT FStar.Class.TotalOrder.Raw.fst.checked - EXTRACT FStar.Int.Cast.fst.checked - CHECK FStar.SizeT.fst - CHECK FStar.Int.Cast.Full.fst - EXTRACT FStar.Class.Eq.fst.checked - EXTRACT FStar.Class.Printable.fst.checked - EXTRACT FStar.Int128.fst.checked - CHECK FStar.Tactics.V2.SyntaxHelpers.fst - CHECK FStar.Tactics.Names.fst - CHECK FStar.Tactics.MApply.fsti - EXTRACT FStar.Int.Cast.Full.fst.checked - CHECK FStar.Tactics.SyntaxHelpers.fst - EXTRACT FStar.FunctionalExtensionality.fst.checked - EXTRACT FStar.Algebra.CommMonoid.Fold.Nested.fst.checked - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.SizeT.fst(34,4-34,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.02.17/ulib/FStar.SizeT.fst(35,4-35,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 - - EXTRACT FStar.SizeT.fst.checked - CHECK FStar.PtrdiffT.fst - CHECK FStar.Tactics.MApply.fst - CHECK FStar.Tactics.V1.Derived.fst - CHECK FStar.Tactics.V1.Logic.fsti - CHECK FStar.Reflection.Formula.fst - CHECK FStar.Tactics.V2.Logic.fsti - CHECK FStar.Tactics.V2.Derived.fst - EXTRACT FStar.Endianness.fst.checked - EXTRACT FStar.PtrdiffT.fst.checked - EXTRACT FStar.OrdSet.fst.checked - EXTRACT FStar.Integers.fst.checked - CHECK FStar.ConstantTime.Integers.fsti - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.NamedView.fst(665,0-683,28): - - Definitions of inner let-rec aux and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.NamedView.fst(262,10-262,13) - - CHECK FStar.Tactics.Logic.fst - EXTRACT FStar.Math.Euclid.fst.checked - EXTRACT FStar.Seq.Properties.fst.checked - EXTRACT FStar.Sequence.Base.fst.checked - CHECK FStar.ConstantTime.Integers.fst - CHECK LowStar.Buffer.fst - CHECK LowStar.Monotonic.Buffer.fst - CHECK LowStar.BufferView.fsti - CHECK LowStar.BufferView.Down.fsti - CHECK LowStar.PrefixFreezableBuffer.fsti - CHECK LowStar.Printf.fst - CHECK FStar.Pointer.Base.fst - CHECK FStar.Pointer.Derived1.fsti - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fst(293,8-293,25): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51) - - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.UInt.fsti(435,8-435,51): - - Pattern uses these theory symbols or terms that should not be in an SMT - pattern: - Prims.op_Subtraction - - EXTRACT FStar.UInt.fst.checked - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.Buffer.Quantifiers.fst - CHECK FStar.Modifies.fsti - EXTRACT FStar.Seq.Permutation.fst.checked - * Warning 271 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - EXTRACT FStar.ConstantTime.Integers.fst.checked - CHECK FStar.Tactics.V2.Bare.fsti - CHECK FStar.UInt128.fst - 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.MApply0.fst - CHECK FStar.Pointer.Derived3.fsti - CHECK FStar.Pointer.Derived1.fst - CHECK FStar.Pointer.Derived2.fsti - CHECK FStar.Reflection.Typing.fst - CHECK FStar.Tactics.V1.fsti - CHECK FStar.Tactics.V1.Logic.fst - CHECK FStar.Tactics.Derived.fst - CHECK FStar.Reflection.V2.Arith.fst - CHECK FStar.Tactics.V2.fsti - CHECK FStar.Tactics.TypeRepr.fsti - CHECK FStar.Tactics.CanonCommMonoidSimple.Equiv.fst - CHECK FStar.Tactics.Parametricity.fst - CHECK FStar.Tactics.CheckLN.fsti - CHECK FStar.Tactics.CanonCommMonoidSimple.fst - CHECK LowStar.BufferView.Down.fst - CHECK LowStar.BufferView.Up.fsti - CHECK FStar.Tactics.TypeRepr.fst - CHECK LowStar.BufferView.fst - EXTRACT LowStar.Buffer.fst.checked - CHECK LowStar.BufferOps.fst - CHECK LowStar.Modifies.fst - CHECK LowStar.ImmutableBuffer.fst - CHECK LowStar.BufferCompat.fst - CHECK FStar.Tactics.CheckLN.fst - CHECK FStar.Pointer.Derived2.fst - CHECK FStar.Tactics.fsti - EXTRACT LowStar.Modifies.fst.checked - CHECK LowStar.ModifiesPat.fst - CHECK FStar.Bytes.fsti - CHECK LowStar.Vector.fst - CHECK LowStar.Regional.fst - CHECK FStar.ReflexiveTransitiveClosure.fst - CHECK FStar.Tactics.Simplifier.fst - CHECK FStar.Tactics.CanonCommMonoid.fst - CHECK FStar.Tactics.CanonMonoid.fst - * Warning 328 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Printf.fst(253,8-253,13): - - Global binding 'LowStar.Printf.arg_t' is recursive but not used in its body - - CHECK FStar.BigOps.fst - CHECK FStar.FiniteMap.Base.fst - CHECK LowStar.BufferView.Up.fst - CHECK FStar.Modifies.fst - CHECK LowStar.ToFStarBuffer.fst - CHECK FStar.Pointer.fst - CHECK FStar.Pointer.Derived3.fst - EXTRACT LowStar.BufferOps.fst.checked - CHECK LowStar.Endianness.fst - EXTRACT LowStar.BufferCompat.fst.checked - CHECK FStar.InteractiveHelpers.Base.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoidSimple.fst(25,46-25,57): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - CHECK FStar.Tactics.BreakVC.fsti - CHECK FStar.Tactics.PatternMatching.fst - EXTRACT LowStar.ModifiesPat.fst.checked - CHECK FStar.WellFounded.Util.fst - CHECK FStar.Pure.BreakVC.fsti - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonMonoid.fst(91,7-91,18): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonMonoid.fst(95,7-95,18): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - CHECK FStar.Tactics.Canon.fst - CHECK FStar.Tactics.Arith.fst - CHECK FStar.Tactics.BV.fst - CHECK FStar.Tactics.BreakVC.fst - EXTRACT FStar.BigOps.fst.checked - EXTRACT FStar.Pointer.fst.checked - CHECK FStar.TaggedUnion.fsti - CHECK FStar.BufferNG.fst - EXTRACT LowStar.ImmutableBuffer.fst.checked - CHECK LowStar.UninitializedBuffer.fst - CHECK LowStar.ConstBuffer.fsti - CHECK LowStar.Literal.fsti - CHECK FStar.Pure.BreakVC.fst - CHECK FStar.Crypto.fst - CHECK FStar.Udp.fsti - CHECK FStar.Tcp.fsti - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(111,0-121,5): - - Definitions of inner let-rec aux and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(50,12-50,15) - - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(111,0-121,5): - - Definitions of inner let-rec aux and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(80,12-80,15) - - * Warning 242 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(111,0-121,5): - - Definitions of inner let-rec f and its enclosing top-level letbinding are - not encoded to the solver, you will only be able to reason with their types - - Also see: /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.WellFounded.Util.fst(113,12-113,13) - - EXTRACT FStar.WellFounded.Util.fst.checked - EXTRACT FStar.ReflexiveTransitiveClosure.fst.checked - EXTRACT LowStar.Regional.fst.checked - EXTRACT FStar.FiniteMap.Base.fst.checked - CHECK LowStar.ConstBuffer.fst - EXTRACT LowStar.ToFStarBuffer.fst.checked - EXTRACT FStar.Crypto.fst.checked - EXTRACT LowStar.BufferView.Up.fst.checked - EXTRACT LowStar.Endianness.fst.checked - CHECK LowStar.PrefixFreezableBuffer.fst - CHECK FStar.TaggedUnion.fst - EXTRACT FStar.Pure.BreakVC.fst.checked - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.02.17/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 - - EXTRACT FStar.Modifies.fst.checked - CHECK FStar.InteractiveHelpers.ExploreTerm.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoid.fst(239,18-239,29): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoid.fst(255,7-255,18): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoid.fst(261,7-261,18): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoid.fst(287,17-287,28): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Tactics.CanonCommMonoid.fst(343,9-343,20): - - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - - Use Reflection.term_eq instead - - See also /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(449,0-449,42) - - EXTRACT LowStar.BufferView.Down.fst.checked - EXTRACT LowStar.UninitializedBuffer.fst.checked - EXTRACT LowStar.ConstBuffer.fst.checked - EXTRACT LowStar.Vector.fst.checked - CHECK LowStar.RVector.fst - EXTRACT LowStar.PrefixFreezableBuffer.fst.checked - EXTRACT FStar.Matrix.fst.checked - CHECK FStar.InteractiveHelpers.Propositions.fst - CHECK FStar.InteractiveHelpers.Output.fst - CHECK FStar.InteractiveHelpers.Effectful.fst - EXTRACT FStar.UInt128.fst.checked - EXTRACT LowStar.BufferView.fst.checked - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - CHECK FStar.InteractiveHelpers.PostProcess.fst - CHECK FStar.Math.Fermat.fst - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Monotonic.Buffer.fst(238,21-238,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.02.17/ulib/Prims.fst(289,5-289,13) - - * Warning 288 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Monotonic.Buffer.fst(239,21-239,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.02.17/ulib/Prims.fst(289,5-289,13) - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Monotonic.Buffer.fst(806,4-806,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.02.17/ulib/LowStar.Monotonic.Buffer.fst(869,4-869,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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Monotonic.Buffer.fst(1050,4-1050,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.02.17/ulib/LowStar.Monotonic.Buffer.fst(1105,4-1105,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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib/LowStar.Monotonic.Buffer.fst(1424,4-1424,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 - - EXTRACT LowStar.Monotonic.Buffer.fst.checked - CHECK LowStar.Regional.Instances.fst - EXTRACT LowStar.RVector.fst.checked - EXTRACT LowStar.Regional.Instances.fst.checked - CHECK FStar.InteractiveHelpers.fst - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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.2025.02.17/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 - - * Warning 318 at /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/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 - - EXTRACT FStar.Pointer.Base.fst.checked - EXTRACT FStar.Math.Fermat.fst.checked - EXTRACT STAGE 2 PLUGLIB - DEPEND /home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17/ulib - EXTRACT FStar.NormSteps.fst.checked - EXTRACT FStar.Pervasives.fst.checked - EXTRACT FStar.Mul.fst.checked - EXTRACT FStar.IndefiniteDescription.fst.checked - EXTRACT FStar.Squash.fst.checked - EXTRACT FStar.Classical.fst.checked - EXTRACT FStar.Classical.Sugar.fst.checked - EXTRACT FStar.StrongExcludedMiddle.fst.checked - EXTRACT FStar.List.Tot.Properties.fst.checked - EXTRACT FStar.Seq.Base.fst.checked - EXTRACT FStar.Preorder.fst.checked - EXTRACT FStar.Calc.fst.checked - EXTRACT FStar.Seq.Properties.fst.checked - EXTRACT FStar.Seq.fst.checked - EXTRACT FStar.Math.Lemmas.fst.checked - EXTRACT FStar.Math.Lib.fst.checked - EXTRACT FStar.BitVector.fst.checked - EXTRACT FStar.UInt.fst.checked - EXTRACT FStar.Monotonic.Pure.fst.checked - EXTRACT FStar.Tactics.Effect.fst.checked - EXTRACT FStar.Tactics.Util.fst.checked - EXTRACT FStar.Sealed.Inhabited.fst.checked - EXTRACT FStar.Reflection.TermEq.Simple.fst.checked - EXTRACT FStar.Order.fst.checked - EXTRACT FStar.Reflection.TermEq.fst.checked - EXTRACT FStar.Reflection.V2.Derived.Lemmas.fst.checked - EXTRACT FStar.Reflection.V2.Collect.fst.checked - EXTRACT FStar.Tactics.NamedView.fst.checked - EXTRACT FStar.Reflection.Const.fst.checked - EXTRACT FStar.Reflection.V2.Derived.fst.checked - EXTRACT FStar.Reflection.V2.fst.checked - EXTRACT FStar.Reflection.V2.Compare.fst.checked - EXTRACT FStar.Tactics.V2.SyntaxCoercions.fst.checked - EXTRACT FStar.PropositionalExtensionality.fst.checked - EXTRACT FStar.Tactics.Visit.fst.checked - EXTRACT FStar.Tactics.Names.fst.checked - EXTRACT FStar.Tactics.V2.Derived.fst.checked - EXTRACT FStar.Tactics.V2.SyntaxHelpers.fst.checked - EXTRACT FStar.Reflection.V2.Formula.fst.checked - EXTRACT FStar.Tactics.Typeclasses.fst.checked - EXTRACT FStar.Tactics.MApply0.fst.checked - EXTRACT FStar.Tactics.MApply.fst.checked - EXTRACT FStar.Tactics.SMT.fst.checked - EXTRACT FStar.Tactics.Print.fst.checked - EXTRACT FStar.Tactics.V1.Logic.Lemmas.fst.checked - EXTRACT FStar.Tactics.V2.Logic.fst.checked - EXTRACT FStar.FunctionalExtensionality.fst.checked - EXTRACT FStar.FiniteSet.Base.fst.checked - EXTRACT FStar.FiniteSet.Ambient.fst.checked - EXTRACT FStar.FiniteMap.Base.fst.checked - EXTRACT FStar.ErasedLogic.fst.checked - EXTRACT FStar.Set.fst.checked - EXTRACT FStar.PredicateExtensionality.fst.checked - EXTRACT FStar.Monotonic.HyperHeap.fst.checked - EXTRACT FStar.Map.fst.checked - EXTRACT FStar.Monotonic.HyperStack.fst.checked - EXTRACT FStar.HyperStack.fst.checked - EXTRACT FStar.Int.fst.checked - EXTRACT FStar.Int.Cast.fst.checked - EXTRACT FStar.Monotonic.Witnessed.fst.checked - EXTRACT FStar.BV.fst.checked - EXTRACT FStar.Tactics.BV.Lemmas.fst.checked - EXTRACT FStar.Reflection.V2.Arith.fst.checked - EXTRACT FStar.Tactics.BV.fst.checked - EXTRACT FStar.UInt128.fst.checked - EXTRACT FStar.Universe.fst.checked - EXTRACT FStar.GSet.fst.checked - EXTRACT FStar.BigOps.fst.checked - EXTRACT LowStar.Monotonic.Buffer.fst.checked - EXTRACT LowStar.Buffer.fst.checked - EXTRACT LowStar.BufferOps.fst.checked - EXTRACT FStar.Endianness.fst.checked - EXTRACT LowStar.Endianness.fst.checked - EXTRACT LowStar.PrefixFreezableBuffer.fst.checked - EXTRACT FStar.OrdSet.fst.checked - EXTRACT FStar.OrdMap.fst.checked - EXTRACT FStar.OrdMapProps.fst.checked - EXTRACT FStar.Functions.fst.checked - EXTRACT FStar.SizeT.fst.checked - EXTRACT FStar.PtrdiffT.fst.checked - EXTRACT LowStar.Modifies.fst.checked - EXTRACT FStar.Crypto.fst.checked - EXTRACT LowStar.ModifiesPat.fst.checked - EXTRACT FStar.Int128.fst.checked - EXTRACT FStar.Integers.fst.checked - EXTRACT LowStar.Vector.fst.checked - EXTRACT LowStar.Regional.fst.checked - EXTRACT LowStar.RVector.fst.checked - EXTRACT FStar.Tactics.TypeRepr.fst.checked - EXTRACT FStar.Class.Add.fst.checked - EXTRACT LowStar.BufferView.fst.checked - EXTRACT FStar.ExtractAs.fst.checked - EXTRACT FStar.Reflection.V1.Derived.fst.checked - EXTRACT FStar.Reflection.V1.Derived.Lemmas.fst.checked - EXTRACT FStar.Reflection.V1.fst.checked - EXTRACT FStar.Tactics.V1.SyntaxHelpers.fst.checked - EXTRACT FStar.Reflection.V1.Formula.fst.checked - EXTRACT FStar.Tactics.V1.Derived.fst.checked - EXTRACT FStar.Tactics.V1.Logic.fst.checked - EXTRACT FStar.WellFounded.fst.checked - EXTRACT FStar.WellFounded.Util.fst.checked - EXTRACT FStar.DependentMap.fst.checked - EXTRACT FStar.Monotonic.DependentMap.fst.checked - EXTRACT LowStar.Comment.fst.checked - EXTRACT FStar.Tactics.Canon.Lemmas.fst.checked - EXTRACT FStar.Algebra.CommMonoid.Equiv.fst.checked - EXTRACT FStar.GhostSet.fst.checked - EXTRACT FStar.PartialMap.fst.checked - EXTRACT FStar.PCM.fst.checked - EXTRACT FStar.Universe.PCM.fst.checked - EXTRACT FStar.Cardinality.Cantor.fst.checked - EXTRACT FStar.Cardinality.Universes.fst.checked - EXTRACT FStar.Pure.BreakVC.fst.checked - EXTRACT FStar.MarkovsPrinciple.fst.checked - EXTRACT FStar.Algebra.CommMonoid.fst.checked - EXTRACT FStar.Sequence.Base.fst.checked - EXTRACT FStar.Sequence.Util.fst.checked - EXTRACT FStar.Sequence.Ambient.fst.checked - EXTRACT FStar.Sequence.fst.checked - EXTRACT FStar.Sequence.Permutation.fst.checked - EXTRACT FStar.Tactics.Canon.fst.checked - EXTRACT FStar.Math.Euclid.fst.checked - EXTRACT FStar.Tactics.CanonCommSwaps.fst.checked - EXTRACT FStar.Tactics.CanonCommMonoid.fst.checked - EXTRACT LowStar.BufferView.Down.fst.checked - EXTRACT LowStar.BufferView.Up.fst.checked - EXTRACT FStar.Ref.fst.checked - EXTRACT FStar.Tactics.Arith.fst.checked - EXTRACT LowStar.Regional.Instances.fst.checked - EXTRACT FStar.ReflexiveTransitiveClosure.fst.checked - EXTRACT FStar.LexicographicOrdering.fst.checked - EXTRACT FStar.Sequence.Seq.fst.checked - EXTRACT FStar.Reflection.Formula.fst.checked - EXTRACT FStar.Tactics.CanonCommSemiring.fst.checked - EXTRACT FStar.Tactics.CheckLN.fst.checked - EXTRACT FStar.Algebra.Monoid.fst.checked - EXTRACT FStar.Tactics.CanonMonoid.fst.checked - EXTRACT FStar.Axiomatic.Array.fst.checked - EXTRACT FStar.Relational.Relational.fst.checked - EXTRACT FStar.Tactics.MkProjectors.fst.checked - EXTRACT FStar.Fin.fst.checked - EXTRACT FStar.SquashProperties.fst.checked - EXTRACT FStar.MRef.fst.checked - EXTRACT LowStar.ImmutableBuffer.fst.checked - EXTRACT FStar.IntegerIntervals.fst.checked - EXTRACT FStar.Seq.Equiv.fst.checked - EXTRACT FStar.Seq.Permutation.fst.checked - EXTRACT FStar.Algebra.CommMonoid.Fold.fst.checked - EXTRACT FStar.RefinementExtensionality.fst.checked - EXTRACT FStar.Int.Cast.Full.fst.checked - EXTRACT FStar.Tactics.Simplifier.fst.checked - EXTRACT FStar.Monotonic.Map.fst.checked - EXTRACT LowStar.BufferCompat.fst.checked - EXTRACT FStar.Matrix.fst.checked - EXTRACT FStar.Modifies.fst.checked - EXTRACT LowStar.ToFStarBuffer.fst.checked - EXTRACT FStar.Monotonic.Seq.fst.checked - EXTRACT FStar.Class.Printable.fst.checked - EXTRACT FStar.Seq.Sorted.fst.checked - EXTRACT FStar.List.Pure.Base.fst.checked - EXTRACT FStar.OrdSetProps.fst.checked - EXTRACT FStar.Tactics.CanonCommMonoidSimple.fst.checked - EXTRACT FStar.Class.Eq.Raw.fst.checked - EXTRACT FStar.Class.Eq.fst.checked - EXTRACT LowStar.UninitializedBuffer.fst.checked - EXTRACT FStar.Pointer.Base.fst.checked - EXTRACT FStar.FunctionalQueue.fst.checked - EXTRACT FStar.Reflection.Typing.fst.checked - EXTRACT FStar.IFC.fst.checked - EXTRACT FStar.Reflection.fst.checked - EXTRACT FStar.Relational.Comp.fst.checked - EXTRACT FStar.Witnessed.Core.fst.checked - EXTRACT FStar.Tactics.BreakVC.fst.checked - EXTRACT FStar.Tactics.Logic.fst.checked - EXTRACT FStar.Tactics.PatternMatching.fst.checked - EXTRACT FStar.Pointer.fst.checked - EXTRACT FStar.Error.fst.checked - EXTRACT FStar.Algebra.CommMonoid.Fold.Nested.fst.checked - EXTRACT FStar.Tactics.Derived.fst.checked - EXTRACT FStar.Real.Old.fst.checked - EXTRACT FStar.Parse.fst.checked - EXTRACT FStar.TwoLevelHeap.fst.checked - EXTRACT FStar.Math.Fermat.fst.checked - EXTRACT FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.checked - EXTRACT LowStar.ConstBuffer.fst.checked - EXTRACT FStar.Class.TotalOrder.Raw.fst.checked - EXTRACT FStar.WellFoundedRelation.fst.checked - EXTRACT FStar.Tactics.Parametricity.fst.checked - EXTRACT FStar.ConstantTime.Integers.fst.checked - EXTRACT FStar.Tactics.SyntaxHelpers.fst.checked - EXTRACT FStar.Array.fst.checked - EXTRACT FStar.FiniteMap.Ambient.fst.checked - INSTALL STAGE 2 -> compiled fstar.2025.02.17 [fstar: make install] + /usr/bin/make "PREFIX=/home/opam/.opam/default" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/fstar.2025.02.17) - INSTALL STAGE 2 -> installed fstar.2025.02.17 [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:32.19: OK: build fstar.2025.02.17 (runc: 3823.6s, disk: 165KB) 2026-06-26 11:32.19: Job succeeded